1 header{*Examples of Reasoning in ZF Set Theory*}
3 theory ZF_examples imports Main_ZFC begin
5 subsection {* Binary Trees *}
11 Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
13 declare bt.intros [simp]
15 text{*Induction via tactic emulation*}
16 lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l"
17 --{* @{subgoals[display,indent=0,margin=65]} *}
19 --{* @{subgoals[display,indent=0,margin=65]} *}
24 apply (Inductive.case_tac l)
25 apply (tactic {*exhaust_tac "l" 1*})
28 text{*The new induction method, which I don't understand*}
29 lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
30 --{* @{subgoals[display,indent=0,margin=65]} *}
31 apply (induct set: bt)
32 --{* @{subgoals[display,indent=0,margin=65]} *}
36 lemma Br_iff: "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'"
37 -- "Proving a freeness theorem."
38 by (blast elim!: bt.free_elims)
40 inductive_cases Br_in_bt: "Br(a,l,r) \<in> bt(A)"
41 -- "An elimination rule, for type-checking."
44 @{thm[display] Br_in_bt[no_vars]}
47 subsection{*Primitive recursion*}
49 consts n_nodes :: "i => i"
52 "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
54 lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
55 by (induct_tac t, auto)
57 consts n_nodes_aux :: "i => i"
59 "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
60 "n_nodes_aux(Br(a,l,r)) =
61 (\<lambda>k \<in> nat. n_nodes_aux(r) ` (n_nodes_aux(l) ` succ(k)))"
63 lemma n_nodes_aux_eq [rule_format]:
64 "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
65 by (induct_tac t, simp_all)
67 definition n_nodes_tail :: "i => i" where
68 "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
70 lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
71 by (simp add: n_nodes_tail_def n_nodes_aux_eq)
74 subsection {*Inductive definitions*}
78 domains "Fin(A)" \<subseteq> "Pow(A)"
80 emptyI: "0 \<in> Fin(A)"
81 consI: "[| a \<in> A; b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
82 type_intros empty_subsetI cons_subsetI PowI
83 type_elims PowD [THEN revcut_rl]
86 consts acc :: "i => i"
88 domains "acc(r)" \<subseteq> "field(r)"
90 vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
98 "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
101 (*Coinductive definition of equality*)
105 (*Previously used <*> in the domain and variant pairs as elements. But
106 standard pairs work just as well. To use variant pairs, must change prefix
107 a q/Q to the Sigma, Pair and converse rules.*)
109 domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
111 LNil: "<LNil, LNil> \<in> lleq(A)"
112 LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |]
113 ==> <LCons(a,l), LCons(a,l')> \<in> lleq(A)"
114 type_intros llist.intros
117 subsection{*Powerset example*}
119 lemma Pow_mono: "A\<subseteq>B ==> Pow(A) \<subseteq> Pow(B)"
123 apply (erule subset_trans, assumption)
126 lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
127 --{* @{subgoals[display,indent=0,margin=65]} *}
128 apply (rule equalityI)
129 --{* @{subgoals[display,indent=0,margin=65]} *}
130 apply (rule Int_greatest)
131 --{* @{subgoals[display,indent=0,margin=65]} *}
132 apply (rule Int_lower1 [THEN Pow_mono])
133 --{* @{subgoals[display,indent=0,margin=65]} *}
134 apply (rule Int_lower2 [THEN Pow_mono])
135 --{* @{subgoals[display,indent=0,margin=65]} *}
137 --{* @{subgoals[display,indent=0,margin=65]} *}
139 --{* @{subgoals[display,indent=0,margin=65]} *}
141 --{* @{subgoals[display,indent=0,margin=65]} *}
143 --{* @{subgoals[display,indent=0,margin=65]} *}
144 apply (rule Int_greatest)
145 --{* @{subgoals[display,indent=0,margin=65]} *}
149 text{*Trying again from the beginning in order to use @{text blast}*}
150 lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
154 lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
155 --{* @{subgoals[display,indent=0,margin=65]} *}
157 --{* @{subgoals[display,indent=0,margin=65]} *}
159 --{* @{subgoals[display,indent=0,margin=65]} *}
161 --{* @{subgoals[display,indent=0,margin=65]} *}
162 apply (erule subsetD)
163 --{* @{subgoals[display,indent=0,margin=65]} *}
165 --{* @{subgoals[display,indent=0,margin=65]} *}
169 text{*A more abstract version of the same proof*}
171 lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
172 --{* @{subgoals[display,indent=0,margin=65]} *}
173 apply (rule Union_least)
174 --{* @{subgoals[display,indent=0,margin=65]} *}
175 apply (rule Union_upper)
176 --{* @{subgoals[display,indent=0,margin=65]} *}
177 apply (erule subsetD, assumption)
181 lemma "[| a \<in> A; f \<in> A->B; g \<in> C->D; A \<inter> C = 0 |] ==> (f \<union> g)`a = f`a"
182 --{* @{subgoals[display,indent=0,margin=65]} *}
183 apply (rule apply_equality)
184 --{* @{subgoals[display,indent=0,margin=65]} *}
186 --{* @{subgoals[display,indent=0,margin=65]} *}
187 apply (rule apply_Pair)
188 --{* @{subgoals[display,indent=0,margin=65]} *}
190 --{* @{subgoals[display,indent=0,margin=65]} *}
192 --{* @{subgoals[display,indent=0,margin=65]} *}
193 apply (rule fun_disjoint_Un)
194 --{* @{subgoals[display,indent=0,margin=65]} *}
196 --{* @{subgoals[display,indent=0,margin=65]} *}
198 --{* @{subgoals[display,indent=0,margin=65]} *}