paulson@14152: header{*Examples of Reasoning in ZF Set Theory*}
paulson@14152: 
haftmann@16417: theory ZF_examples imports Main_ZFC begin
paulson@14152: 
paulson@14152: subsection {* Binary Trees *}
paulson@14152: 
paulson@14152: consts
paulson@14152:   bt :: "i => i"
paulson@14152: 
paulson@14152: datatype "bt(A)" =
paulson@14152:   Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
paulson@14152: 
paulson@14152: declare bt.intros [simp]
paulson@14152: 
paulson@14152: text{*Induction via tactic emulation*}
paulson@14152: lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152:   apply (induct_tac l)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152:   apply auto
paulson@14152:   done
paulson@14152: 
paulson@14152: (*
paulson@14152:   apply (Inductive.case_tac l)
paulson@14152:   apply (tactic {*exhaust_tac "l" 1*})
paulson@14152: *)
paulson@14152: 
paulson@14152: text{*The new induction method, which I don't understand*}
paulson@14152: lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152:   apply (induct set: bt)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152:   apply auto
paulson@14152:   done
paulson@14152: 
paulson@14159: lemma Br_iff: "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'"
paulson@14152:   -- "Proving a freeness theorem."
paulson@14152:   by (blast elim!: bt.free_elims)
paulson@14152: 
paulson@14159: inductive_cases Br_in_bt: "Br(a,l,r) \<in> bt(A)"
paulson@14152:   -- "An elimination rule, for type-checking."
paulson@14152: 
paulson@14152: text {*
paulson@14159: @{thm[display] Br_in_bt[no_vars]}
paulson@14152: *};
paulson@14152: 
paulson@14159: subsection{*Primitive recursion*}
paulson@14159: 
paulson@14159: consts  n_nodes :: "i => i"
paulson@14159: primrec
paulson@14159:   "n_nodes(Lf) = 0"
paulson@14159:   "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
paulson@14159: 
paulson@14159: lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
paulson@14159:   by (induct_tac t, auto) 
paulson@14159: 
paulson@14159: consts  n_nodes_aux :: "i => i"
paulson@14159: primrec
paulson@14159:   "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
paulson@14159:   "n_nodes_aux(Br(a,l,r)) = 
paulson@14159:       (\<lambda>k \<in> nat. n_nodes_aux(r) `  (n_nodes_aux(l) ` succ(k)))"
paulson@14159: 
paulson@14159: lemma n_nodes_aux_eq [rule_format]:
paulson@14159:      "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
paulson@14159:   by (induct_tac t, simp_all) 
paulson@14159: 
haftmann@35413: definition n_nodes_tail :: "i => i" where
paulson@14159:    "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
paulson@14159: 
paulson@14159: lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
paulson@14159:  by (simp add: n_nodes_tail_def n_nodes_aux_eq) 
paulson@14159: 
paulson@14159: 
paulson@14159: subsection {*Inductive definitions*}
paulson@14159: 
paulson@14159: consts  Fin       :: "i=>i"
paulson@14159: inductive
paulson@14159:   domains   "Fin(A)" \<subseteq> "Pow(A)"
paulson@14159:   intros
paulson@14159:     emptyI:  "0 \<in> Fin(A)"
paulson@14159:     consI:   "[| a \<in> A;  b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
paulson@14159:   type_intros  empty_subsetI cons_subsetI PowI
paulson@14159:   type_elims   PowD [THEN revcut_rl]
paulson@14159: 
paulson@14159: 
paulson@14159: consts  acc :: "i => i"
paulson@14159: inductive
paulson@14159:   domains "acc(r)" \<subseteq> "field(r)"
paulson@14159:   intros
paulson@14159:     vimage:  "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
paulson@14159:   monos      Pow_mono
paulson@14159: 
paulson@14159: 
paulson@14159: consts
paulson@14159:   llist  :: "i=>i";
paulson@14159: 
paulson@14159: codatatype
paulson@14159:   "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
paulson@14159: 
paulson@14159: 
paulson@14159: (*Coinductive definition of equality*)
paulson@14159: consts
paulson@14159:   lleq :: "i=>i"
paulson@14159: 
paulson@14159: (*Previously used <*> in the domain and variant pairs as elements.  But
paulson@14159:   standard pairs work just as well.  To use variant pairs, must change prefix
paulson@14159:   a q/Q to the Sigma, Pair and converse rules.*)
paulson@14159: coinductive
paulson@14159:   domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
paulson@14159:   intros
paulson@14159:     LNil:  "<LNil, LNil> \<in> lleq(A)"
paulson@14159:     LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |] 
paulson@14159:             ==> <LCons(a,l), LCons(a,l')> \<in> lleq(A)"
paulson@14159:   type_intros  llist.intros
paulson@14159: 
paulson@14159: 
paulson@14152: subsection{*Powerset example*}
paulson@14152: 
paulson@14159: lemma Pow_mono: "A\<subseteq>B  ==>  Pow(A) \<subseteq> Pow(B)"
paulson@14152: apply (rule subsetI)
paulson@14152: apply (rule PowI)
paulson@14152: apply (drule PowD)
paulson@14152: apply (erule subset_trans, assumption)
paulson@14152: done
paulson@14152: 
paulson@14152: lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule equalityI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule Int_greatest)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule Int_lower1 [THEN Pow_mono])
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule Int_lower2 [THEN Pow_mono])
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule subsetI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule IntE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule PowI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (drule PowD)+
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply (rule Int_greatest)
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply (assumption+)
paulson@14152: done
paulson@14152: 
paulson@14152: text{*Trying again from the beginning in order to use @{text blast}*}
paulson@14152: lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
paulson@14152: by blast
paulson@14152: 
paulson@14152: 
paulson@14159: lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule subsetI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule UnionE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule UnionI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply (erule subsetD)
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply assumption 
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply assumption 
paulson@14152: done
paulson@14152: 
paulson@14159: text{*A more abstract version of the same proof*}
paulson@14152: 
paulson@14159: lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule Union_least)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule Union_upper)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule subsetD, assumption)
paulson@14152: done
paulson@14152: 
paulson@14152: 
paulson@14159: lemma "[| a \<in> A;  f \<in> A->B;  g \<in> C->D;  A \<inter> C = 0 |] ==> (f \<union> g)`a = f`a"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule apply_equality)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule UnI1)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply (rule apply_Pair)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply assumption 
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply assumption 
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply (rule fun_disjoint_Un)
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply assumption 
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply assumption 
paulson@14159:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14159: apply assumption 
paulson@14152: done
paulson@14152: 
paulson@14152: end