14152
|
1 |
header{*Examples of Reasoning in ZF Set Theory*}
|
|
2 |
|
|
3 |
theory ZF_examples = Main_ZFC:
|
|
4 |
|
|
5 |
subsection {* Binary Trees *}
|
|
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 |
|
|
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]} *}
|
|
18 |
apply (induct_tac l)
|
|
19 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
20 |
apply auto
|
|
21 |
done
|
|
22 |
|
|
23 |
(*
|
|
24 |
apply (Inductive.case_tac l)
|
|
25 |
apply (tactic {*exhaust_tac "l" 1*})
|
|
26 |
*)
|
|
27 |
|
|
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]} *}
|
|
33 |
apply auto
|
|
34 |
done
|
|
35 |
|
|
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)
|
|
39 |
|
|
40 |
inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
|
|
41 |
-- "An elimination rule, for type-checking."
|
|
42 |
|
|
43 |
text {*
|
|
44 |
@{thm[display] BrE[no_vars]}
|
|
45 |
\rulename{BrE}
|
|
46 |
*};
|
|
47 |
|
|
48 |
subsection{*Powerset example*}
|
|
49 |
|
|
50 |
lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
|
|
51 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
52 |
apply (rule subsetI)
|
|
53 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
54 |
apply (rule PowI)
|
|
55 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
56 |
apply (drule PowD)
|
|
57 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
58 |
apply (erule subset_trans, assumption)
|
|
59 |
done
|
|
60 |
|
|
61 |
lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
|
|
62 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
63 |
apply (rule equalityI)
|
|
64 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
65 |
apply (rule Int_greatest)
|
|
66 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
67 |
apply (rule Int_lower1 [THEN Pow_mono])
|
|
68 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
69 |
apply (rule Int_lower2 [THEN Pow_mono])
|
|
70 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
71 |
apply (rule subsetI)
|
|
72 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
73 |
apply (erule IntE)
|
|
74 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
75 |
apply (rule PowI)
|
|
76 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
77 |
apply (drule PowD)+
|
|
78 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
79 |
apply (rule Int_greatest, assumption+)
|
|
80 |
done
|
|
81 |
|
|
82 |
text{*Trying again from the beginning in order to use @{text blast}*}
|
|
83 |
lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
|
|
84 |
by blast
|
|
85 |
|
|
86 |
|
|
87 |
lemma "C<=D ==> Union(C) <= Union(D)"
|
|
88 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
89 |
apply (rule subsetI)
|
|
90 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
91 |
apply (erule UnionE)
|
|
92 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
93 |
apply (rule UnionI)
|
|
94 |
apply (erule subsetD, assumption, assumption)
|
|
95 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
96 |
done
|
|
97 |
|
|
98 |
text{*Trying again from the beginning in order to prove from the definitions*}
|
|
99 |
|
|
100 |
lemma "C<=D ==> Union(C) <= Union(D)"
|
|
101 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
102 |
apply (rule Union_least)
|
|
103 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
104 |
apply (rule Union_upper)
|
|
105 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
106 |
apply (erule subsetD, assumption)
|
|
107 |
done
|
|
108 |
|
|
109 |
|
|
110 |
lemma "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> (f Un g)`a = f`a"
|
|
111 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
112 |
apply (rule apply_equality)
|
|
113 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
114 |
apply (rule UnI1)
|
|
115 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
116 |
apply (rule apply_Pair, assumption+)
|
|
117 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
118 |
apply (rule fun_disjoint_Un, assumption+)
|
|
119 |
done
|
|
120 |
|
|
121 |
end
|