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