Search code examples
setisabelleproof

how to do a proof for subset in Isabelle

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

Solution

  • 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