author | paulson |
Thu, 23 May 2002 17:05:21 +0200 | |
changeset 13175 | 81082cfa5618 |
parent 12788 | 6842f90972da |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
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) == |
|
12610 | 37 |
Vrecursor(\<lambda>pr. ntree_case(\<lambda>x h. b(x, h, \<lambda>i \<in> domain(h). pr`(h`i))))" |
12229 | 38 |
|
39 |
constdefs |
|
40 |
ntree_copy :: "i => i" |
|
12610 | 41 |
"ntree_copy(z) == ntree_rec(\<lambda>x h r. Branch(x,r), z)" |
12229 | 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))" |
|
12788 | 49 |
by (blast intro: ntree.intros [unfolded ntree.con_defs] |
12229 | 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 |
||
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12788
diff
changeset
|
117 |
lemma ntree_rec_Branch: |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12788
diff
changeset
|
118 |
"function(h) ==> |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12788
diff
changeset
|
119 |
ntree_rec(b, Branch(x,h)) = b(x, h, \<lambda>i \<in> domain(h). ntree_rec(b, h`i))" |
12229 | 120 |
apply (rule ntree_rec_def [THEN def_Vrecursor, THEN trans]) |
121 |
apply (simp add: ntree.con_defs rank_pair2 [THEN [2] lt_trans] rank_apply) |
|
122 |
done |
|
123 |
||
124 |
lemma ntree_copy_Branch [simp]: |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12788
diff
changeset
|
125 |
"function(h) ==> |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12788
diff
changeset
|
126 |
ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))" |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12788
diff
changeset
|
127 |
by (simp add: ntree_copy_def ntree_rec_Branch) |
12229 | 128 |
|
129 |
lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z" |
|
130 |
apply (induct_tac z) |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12788
diff
changeset
|
131 |
apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function) |
12229 | 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 |