12229
|
1 |
(* Title: ZF/Induct/Ntree.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
|
7 |
header {* Datatype definition n-ary branching trees *}
|
|
8 |
|
|
9 |
theory Ntree = Main:
|
|
10 |
|
|
11 |
text {*
|
|
12 |
Demonstrates a simple use of function space in a datatype
|
|
13 |
definition. Based upon theory @{text Term}.
|
|
14 |
*}
|
|
15 |
|
|
16 |
consts
|
|
17 |
ntree :: "i => i"
|
|
18 |
maptree :: "i => i"
|
|
19 |
maptree2 :: "[i, i] => i"
|
|
20 |
|
|
21 |
datatype "ntree(A)" = Branch ("a \<in> A", "h \<in> (\<Union>n \<in> nat. n -> ntree(A))")
|
|
22 |
monos UN_mono [OF subset_refl Pi_mono] -- {* MUST have this form *}
|
|
23 |
type_intros nat_fun_univ [THEN subsetD]
|
|
24 |
type_elims UN_E
|
|
25 |
|
|
26 |
datatype "maptree(A)" = Sons ("a \<in> A", "h \<in> maptree(A) -||> maptree(A)")
|
|
27 |
monos FiniteFun_mono1 -- {* Use monotonicity in BOTH args *}
|
|
28 |
type_intros FiniteFun_univ1 [THEN subsetD]
|
|
29 |
|
|
30 |
datatype "maptree2(A, B)" = Sons2 ("a \<in> A", "h \<in> B -||> maptree2(A, B)")
|
|
31 |
monos FiniteFun_mono [OF subset_refl]
|
|
32 |
type_intros FiniteFun_in_univ'
|
|
33 |
|
|
34 |
constdefs
|
|
35 |
ntree_rec :: "[[i, i, i] => i, i] => i"
|
|
36 |
"ntree_rec(b) ==
|
|
37 |
Vrecursor(%pr. ntree_case(%x h. b(x, h, \<lambda>i \<in> domain(h). pr`(h`i))))"
|
|
38 |
|
|
39 |
constdefs
|
|
40 |
ntree_copy :: "i => i"
|
|
41 |
"ntree_copy(z) == ntree_rec(%x h r. Branch(x,r), z)"
|
|
42 |
|
|
43 |
|
|
44 |
text {*
|
|
45 |
\medskip @{text ntree}
|
|
46 |
*}
|
|
47 |
|
|
48 |
lemma ntree_unfold: "ntree(A) = A \<times> (\<Union>n \<in> nat. n -> ntree(A))"
|
|
49 |
by (fast intro!: ntree.intros [unfolded ntree.con_defs]
|
|
50 |
elim: ntree.cases [unfolded ntree.con_defs])
|
|
51 |
|
|
52 |
lemma ntree_induct [induct set: ntree]:
|
|
53 |
"[| t \<in> ntree(A);
|
|
54 |
!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); \<forall>i \<in> n. P(h`i)
|
|
55 |
|] ==> P(Branch(x,h))
|
|
56 |
|] ==> P(t)"
|
|
57 |
-- {* A nicer induction rule than the standard one. *}
|
|
58 |
proof -
|
|
59 |
case rule_context
|
|
60 |
assume "t \<in> ntree(A)"
|
|
61 |
thus ?thesis
|
|
62 |
apply induct
|
|
63 |
apply (erule UN_E)
|
|
64 |
apply (assumption | rule rule_context)+
|
|
65 |
apply (fast elim: fun_weaken_type)
|
|
66 |
apply (fast dest: apply_type)
|
|
67 |
done
|
|
68 |
qed
|
|
69 |
|
|
70 |
lemma ntree_induct_eqn:
|
|
71 |
"[| t \<in> ntree(A); f \<in> ntree(A)->B; g \<in> ntree(A)->B;
|
|
72 |
!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); f O h = g O h |] ==>
|
|
73 |
f ` Branch(x,h) = g ` Branch(x,h)
|
|
74 |
|] ==> f`t=g`t"
|
|
75 |
-- {* Induction on @{term "ntree(A)"} to prove an equation *}
|
|
76 |
proof -
|
|
77 |
case rule_context
|
|
78 |
assume "t \<in> ntree(A)"
|
|
79 |
thus ?thesis
|
|
80 |
apply induct
|
|
81 |
apply (assumption | rule rule_context)+
|
|
82 |
apply (insert rule_context)
|
|
83 |
apply (rule fun_extension)
|
|
84 |
apply (assumption | rule comp_fun)+
|
|
85 |
apply (simp add: comp_fun_apply)
|
|
86 |
done
|
|
87 |
qed
|
|
88 |
|
|
89 |
text {*
|
|
90 |
\medskip Lemmas to justify using @{text Ntree} in other recursive
|
|
91 |
type definitions.
|
|
92 |
*}
|
|
93 |
|
|
94 |
lemma ntree_mono: "A \<subseteq> B ==> ntree(A) \<subseteq> ntree(B)"
|
|
95 |
apply (unfold ntree.defs)
|
|
96 |
apply (rule lfp_mono)
|
|
97 |
apply (rule ntree.bnd_mono)+
|
|
98 |
apply (assumption | rule univ_mono basic_monos)+
|
|
99 |
done
|
|
100 |
|
|
101 |
lemma ntree_univ: "ntree(univ(A)) \<subseteq> univ(A)"
|
|
102 |
-- {* Easily provable by induction also *}
|
|
103 |
apply (unfold ntree.defs ntree.con_defs)
|
|
104 |
apply (rule lfp_lowerbound)
|
|
105 |
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
|
|
106 |
apply (blast intro: Pair_in_univ nat_fun_univ [THEN subsetD])
|
|
107 |
done
|
|
108 |
|
|
109 |
lemma ntree_subset_univ: "A \<subseteq> univ(B) ==> ntree(A) \<subseteq> univ(B)"
|
|
110 |
by (rule subset_trans [OF ntree_mono ntree_univ])
|
|
111 |
|
|
112 |
|
|
113 |
text {*
|
|
114 |
\medskip @{text ntree} recursion.
|
|
115 |
*}
|
|
116 |
|
|
117 |
lemma ntree_rec_Branch: "ntree_rec(b, Branch(x,h))
|
|
118 |
= b(x, h, \<lambda>i \<in> domain(h). ntree_rec(b, h`i))"
|
|
119 |
apply (rule ntree_rec_def [THEN def_Vrecursor, THEN trans])
|
|
120 |
apply (simp add: ntree.con_defs rank_pair2 [THEN [2] lt_trans] rank_apply)
|
|
121 |
done
|
|
122 |
|
|
123 |
lemma ntree_copy_Branch [simp]:
|
|
124 |
"ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))"
|
|
125 |
apply (unfold ntree_copy_def)
|
|
126 |
apply (rule ntree_rec_Branch)
|
|
127 |
done
|
|
128 |
|
|
129 |
lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z"
|
|
130 |
apply (induct_tac z)
|
|
131 |
apply (auto simp add: domain_of_fun Pi_Collect_iff)
|
|
132 |
done
|
|
133 |
|
|
134 |
|
|
135 |
text {*
|
|
136 |
\medskip @{text maptree}
|
|
137 |
*}
|
|
138 |
|
|
139 |
lemma maptree_unfold: "maptree(A) = A \<times> (maptree(A) -||> maptree(A))"
|
|
140 |
by (fast intro!: maptree.intros [unfolded maptree.con_defs]
|
|
141 |
elim: maptree.cases [unfolded maptree.con_defs])
|
|
142 |
|
|
143 |
lemma maptree_induct [induct set: maptree]:
|
|
144 |
"[| t \<in> maptree(A);
|
|
145 |
!!x n h. [| x \<in> A; h \<in> maptree(A) -||> maptree(A);
|
|
146 |
\<forall>y \<in> field(h). P(y)
|
|
147 |
|] ==> P(Sons(x,h))
|
|
148 |
|] ==> P(t)"
|
|
149 |
-- {* A nicer induction rule than the standard one. *}
|
|
150 |
proof -
|
|
151 |
case rule_context
|
|
152 |
assume "t \<in> maptree(A)"
|
|
153 |
thus ?thesis
|
|
154 |
apply induct
|
|
155 |
apply (assumption | rule rule_context)+
|
|
156 |
apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
|
|
157 |
apply (drule FiniteFun.dom_subset [THEN subsetD])
|
|
158 |
apply (drule Fin.dom_subset [THEN subsetD])
|
|
159 |
apply fast
|
|
160 |
done
|
|
161 |
qed
|
|
162 |
|
|
163 |
|
|
164 |
text {*
|
|
165 |
\medskip @{text maptree2}
|
|
166 |
*}
|
|
167 |
|
|
168 |
lemma maptree2_unfold: "maptree2(A, B) = A \<times> (B -||> maptree2(A, B))"
|
|
169 |
by (fast intro!: maptree2.intros [unfolded maptree2.con_defs]
|
|
170 |
elim: maptree2.cases [unfolded maptree2.con_defs])
|
|
171 |
|
|
172 |
lemma maptree2_induct [induct set: maptree2]:
|
|
173 |
"[| t \<in> maptree2(A, B);
|
|
174 |
!!x n h. [| x \<in> A; h \<in> B -||> maptree2(A,B); \<forall>y \<in> range(h). P(y)
|
|
175 |
|] ==> P(Sons2(x,h))
|
|
176 |
|] ==> P(t)"
|
|
177 |
proof -
|
|
178 |
case rule_context
|
|
179 |
assume "t \<in> maptree2(A, B)"
|
|
180 |
thus ?thesis
|
|
181 |
apply induct
|
|
182 |
apply (assumption | rule rule_context)+
|
|
183 |
apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
|
|
184 |
apply (drule FiniteFun.dom_subset [THEN subsetD])
|
|
185 |
apply (drule Fin.dom_subset [THEN subsetD])
|
|
186 |
apply fast
|
|
187 |
done
|
|
188 |
qed
|
|
189 |
|
|
190 |
end
|