how to do a proof for subset in Isabelle

Question

I'm trying to do some proofs manually in Isabelle but I'm struggling with the following proof: lemma "(A ∩ B) ∪ C ⊆ A ∪ C "

I'm trying to transform it Propositional Logic then prove it.

So here's what I tried:

 lemma "(A ∩ B) ∪ C ⊆ A  ∪ C "
  apply (subst subset_iff)+
  apply(rule allI)
  apply (rule impI)
 (*here normally we should try to get rid of Union and Inter*)
  apply(subst Un_iff)+ 
  apply(subst  (asm)  Un_iff)+
  apply(subst Inter_iff) (*not working*)

I'm stuck at the last step, could someone please help me finish this proof and explain how should one find the right theorems till the end?

I use find_theorems, but it takes a lot of time + the only useful (and understandable) ressource I found so far is this link: https://www.inf.ed.ac.uk/teaching/courses/ar/isabelle/FormalCheatSheet.pdf and some very few random lecture notes containing almost the same content as the link above...

Other resources I found are 100+ pages and do not look like a place to start for a beginner...

Thanks in advance

why on earth do you even want to do that apply style? Every Isabelle lecture teaches you to do by blast (one step). Anyway, isabelle.in.tum.de/dist/Isabelle2020/doc/tutorial.pdf, Section 5 documents this kind of proofs. — Mathias Fleury
@MathiasFleury, what a coincidence, I happened to be reading a few documents that mentioned your name a few days ago I'm aware that blast can do it, but the online course I'm following suggested that we do it manually. it's the Int_iff tip that I needed, thanks a lot! — user206904
There are a lot of different approaches to teaching Isabelle. Some think it is best to teach such very low-level reasoning first. I don't think I agree, but it's not unreasonable. In any case, I have been using Isabelle for a long time and I usually only use low-level tactics like subst, rule, etc. as a first step and then hit all the arising subgoals with automation like auto. That is more typical of the style we use these days. And of course structured Isar proofs. But I'm sure your course will get there. — Manuel Eberl

Mathias Fleury Mathias Fleury · Accepted Answer · 2021-01-15T11:08:56

First writing such kind of proofs manually is not useful as it can be solved by blast. It is mostly reserved for advanced users. The only documentation I know is the old tutorial, Section 5.

Anyway, you have the wrong intersection theorems: you want to use Int_iff. Here is the full proof:


lemma "(A ∩ B) ∪ C ⊆ A  ∪ C "
  apply (subst subset_iff)+
  apply(rule allI)
  apply (rule impI)
    (*here normally we should try to get rid of Union and Inter*)
  apply(subst Un_iff)+ 
  apply(subst  (asm)  Un_iff)
  apply(subst (asm) Int_iff)
  apply (elim disjE)
   apply (elim conjE)
   apply (rule disjI1)
   apply assumption
  apply (rule disjI2)
  apply assumption
  done

How did would I find such proof? I know by heart the low-level theorems on implication, conjunction, and disjunction (allI, impI, conjI, conjE, disjE, disjI1,...). There is a consistent naming convention (I: intro rule, E: elimination rule, D: destruction rule), so it is not so hard to remember.

For the rest, searching with find_theorems (or the query panel) is the way to go.

Here is the proof I would write (but the other one is nicer for teaching: conjE is way more important than IntE):

lemma "(A ∩ B) ∪ C ⊆ A  ∪ C "
  apply (rule subset_iff[THEN iffD2])
  apply(intro allI impI)
  apply (elim UnE)
   apply (elim IntE)
   apply (rule UnI1)
   apply assumption
  apply (rule UnI2)
  apply assumption
  done

how to do a proof for subset in Isabelle

1 Answers