author | wenzelm |
Fri, 12 Jan 2018 14:08:53 +0100 | |
changeset 67406 | 23307fd33906 |
parent 65449 | c82e63b11b8b |
child 67443 | 3abf6a722518 |
permissions | -rw-r--r-- |
67406 | 1 |
section\<open>Examples of Reasoning in ZF Set Theory\<close> |
14152 | 2 |
|
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
58889
diff
changeset
|
3 |
theory ZF_examples imports ZFC begin |
14152 | 4 |
|
67406 | 5 |
subsection \<open>Binary Trees\<close> |
14152 | 6 |
|
7 |
consts |
|
8 |
bt :: "i => i" |
|
9 |
||
10 |
datatype "bt(A)" = |
|
11 |
Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)") |
|
12 |
||
13 |
declare bt.intros [simp] |
|
14 |
||
67406 | 15 |
text\<open>Induction via tactic emulation\<close> |
14152 | 16 |
lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l" |
67406 | 17 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 18 |
apply (induct_tac l) |
67406 | 19 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 20 |
apply auto |
21 |
done |
|
22 |
||
23 |
(* |
|
24 |
apply (Inductive.case_tac l) |
|
25 |
apply (tactic {*exhaust_tac "l" 1*}) |
|
26 |
*) |
|
27 |
||
67406 | 28 |
text\<open>The new induction method, which I don't understand\<close> |
14152 | 29 |
lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)" |
67406 | 30 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 31 |
apply (induct set: bt) |
67406 | 32 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 33 |
apply auto |
34 |
done |
|
35 |
||
14159 | 36 |
lemma Br_iff: "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'" |
67406 | 37 |
\<comment> "Proving a freeness theorem." |
14152 | 38 |
by (blast elim!: bt.free_elims) |
39 |
||
14159 | 40 |
inductive_cases Br_in_bt: "Br(a,l,r) \<in> bt(A)" |
67406 | 41 |
\<comment> "An elimination rule, for type-checking." |
14152 | 42 |
|
67406 | 43 |
text \<open> |
14159 | 44 |
@{thm[display] Br_in_bt[no_vars]} |
67406 | 45 |
\<close> |
14152 | 46 |
|
67406 | 47 |
subsection\<open>Primitive recursion\<close> |
14159 | 48 |
|
49 |
consts n_nodes :: "i => i" |
|
50 |
primrec |
|
51 |
"n_nodes(Lf) = 0" |
|
52 |
"n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))" |
|
53 |
||
54 |
lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat" |
|
55 |
by (induct_tac t, auto) |
|
56 |
||
57 |
consts n_nodes_aux :: "i => i" |
|
58 |
primrec |
|
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)))" |
|
62 |
||
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) |
|
66 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
67 |
definition n_nodes_tail :: "i => i" where |
14159 | 68 |
"n_nodes_tail(t) == n_nodes_aux(t) ` 0" |
69 |
||
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) |
|
72 |
||
73 |
||
67406 | 74 |
subsection \<open>Inductive definitions\<close> |
14159 | 75 |
|
76 |
consts Fin :: "i=>i" |
|
77 |
inductive |
|
78 |
domains "Fin(A)" \<subseteq> "Pow(A)" |
|
79 |
intros |
|
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 |
|
46471 | 83 |
type_elims PowD [elim_format] |
14159 | 84 |
|
85 |
||
86 |
consts acc :: "i => i" |
|
87 |
inductive |
|
88 |
domains "acc(r)" \<subseteq> "field(r)" |
|
89 |
intros |
|
90 |
vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)" |
|
91 |
monos Pow_mono |
|
92 |
||
93 |
||
94 |
consts |
|
58860 | 95 |
llist :: "i=>i" |
14159 | 96 |
|
97 |
codatatype |
|
98 |
"llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)") |
|
99 |
||
100 |
||
101 |
(*Coinductive definition of equality*) |
|
102 |
consts |
|
103 |
lleq :: "i=>i" |
|
104 |
||
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.*) |
|
108 |
coinductive |
|
109 |
domains "lleq(A)" \<subseteq> "llist(A) * llist(A)" |
|
110 |
intros |
|
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 |
|
115 |
||
116 |
||
67406 | 117 |
subsection\<open>Powerset example\<close> |
14152 | 118 |
|
14159 | 119 |
lemma Pow_mono: "A\<subseteq>B ==> Pow(A) \<subseteq> Pow(B)" |
14152 | 120 |
apply (rule subsetI) |
121 |
apply (rule PowI) |
|
122 |
apply (drule PowD) |
|
123 |
apply (erule subset_trans, assumption) |
|
124 |
done |
|
125 |
||
126 |
lemma "Pow(A Int B) = Pow(A) Int Pow(B)" |
|
67406 | 127 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 128 |
apply (rule equalityI) |
67406 | 129 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 130 |
apply (rule Int_greatest) |
67406 | 131 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 132 |
apply (rule Int_lower1 [THEN Pow_mono]) |
67406 | 133 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 134 |
apply (rule Int_lower2 [THEN Pow_mono]) |
67406 | 135 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 136 |
apply (rule subsetI) |
67406 | 137 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 138 |
apply (erule IntE) |
67406 | 139 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 140 |
apply (rule PowI) |
67406 | 141 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 142 |
apply (drule PowD)+ |
67406 | 143 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 144 |
apply (rule Int_greatest) |
67406 | 145 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 146 |
apply (assumption+) |
14152 | 147 |
done |
148 |
||
67406 | 149 |
text\<open>Trying again from the beginning in order to use @{text blast}\<close> |
14152 | 150 |
lemma "Pow(A Int B) = Pow(A) Int Pow(B)" |
151 |
by blast |
|
152 |
||
153 |
||
14159 | 154 |
lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)" |
67406 | 155 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 156 |
apply (rule subsetI) |
67406 | 157 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 158 |
apply (erule UnionE) |
67406 | 159 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 160 |
apply (rule UnionI) |
67406 | 161 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 162 |
apply (erule subsetD) |
67406 | 163 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 164 |
apply assumption |
67406 | 165 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 166 |
apply assumption |
14152 | 167 |
done |
168 |
||
67406 | 169 |
text\<open>A more abstract version of the same proof\<close> |
14152 | 170 |
|
14159 | 171 |
lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)" |
67406 | 172 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 173 |
apply (rule Union_least) |
67406 | 174 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 175 |
apply (rule Union_upper) |
67406 | 176 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 177 |
apply (erule subsetD, assumption) |
178 |
done |
|
179 |
||
180 |
||
14159 | 181 |
lemma "[| a \<in> A; f \<in> A->B; g \<in> C->D; A \<inter> C = 0 |] ==> (f \<union> g)`a = f`a" |
67406 | 182 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 183 |
apply (rule apply_equality) |
67406 | 184 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14152 | 185 |
apply (rule UnI1) |
67406 | 186 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 187 |
apply (rule apply_Pair) |
67406 | 188 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 189 |
apply assumption |
67406 | 190 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 191 |
apply assumption |
67406 | 192 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 193 |
apply (rule fun_disjoint_Un) |
67406 | 194 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 195 |
apply assumption |
67406 | 196 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 197 |
apply assumption |
67406 | 198 |
\<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
14159 | 199 |
apply assumption |
14152 | 200 |
done |
201 |
||
202 |
end |