author | paulson |
Mon, 28 Dec 1998 16:54:01 +0100 | |
changeset 6046 | 2c8a8be36c94 |
parent 5147 | 825877190618 |
child 6153 | bff90585cce5 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/tf.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Trees & forests, a mutually recursive type definition. |
|
7 |
*) |
|
8 |
||
6046 | 9 |
Addsimps tree_forest.intrs; |
0 | 10 |
|
11 |
(** tree_forest(A) as the union of tree(A) and forest(A) **) |
|
12 |
||
739 | 13 |
val [_, tree_def, forest_def] = tree_forest.defs; |
14 |
||
5068 | 15 |
Goalw [tree_def] "tree(A) <= tree_forest(A)"; |
0 | 16 |
by (rtac Part_subset 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
17 |
qed "tree_subset_TF"; |
0 | 18 |
|
5068 | 19 |
Goalw [forest_def] "forest(A) <= tree_forest(A)"; |
0 | 20 |
by (rtac Part_subset 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
21 |
qed "forest_subset_TF"; |
0 | 22 |
|
5068 | 23 |
Goal "tree(A) Un forest(A) = tree_forest(A)"; |
739 | 24 |
by (safe_tac (subset_cs addSIs [equalityI, tree_subset_TF, forest_subset_TF])); |
4091 | 25 |
by (fast_tac (claset() addSIs tree_forest.intrs addEs [tree_forest.elim]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
26 |
qed "TF_equals_Un"; |
0 | 27 |
|
28 |
(** NOT useful, but interesting... **) |
|
29 |
||
5068 | 30 |
Goalw [tree_def, forest_def] |
434 | 31 |
"tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))"; |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
32 |
let open tree_forest; |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
33 |
val rew = rewrite_rule (con_defs @ tl defs) in |
4091 | 34 |
by (fast_tac (claset() addSIs (map rew intrs RL [PartD1]) addEs [rew elim]) 1) |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
35 |
end; |
760 | 36 |
qed "tree_forest_unfold"; |
434 | 37 |
|
739 | 38 |
val tree_forest_unfold' = rewrite_rule [tree_def, forest_def] |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
39 |
tree_forest_unfold; |
434 | 40 |
|
5068 | 41 |
Goalw [tree_def, forest_def] |
515 | 42 |
"tree(A) = {Inl(x). x: A*forest(A)}"; |
438 | 43 |
by (rtac (Part_Inl RS subst) 1); |
44 |
by (rtac (tree_forest_unfold' RS subst_context) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
45 |
qed "tree_unfold"; |
0 | 46 |
|
5068 | 47 |
Goalw [tree_def, forest_def] |
515 | 48 |
"forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}"; |
438 | 49 |
by (rtac (Part_Inr RS subst) 1); |
50 |
by (rtac (tree_forest_unfold' RS subst_context) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
51 |
qed "forest_unfold"; |
0 | 52 |
|
434 | 53 |
|
6046 | 54 |
(** Type checking for recursor: Not needed; possibly interesting (??) **) |
515 | 55 |
|
56 |
val major::prems = goal TF.thy |
|
57 |
"[| z: tree_forest(A); \ |
|
1461 | 58 |
\ !!x f r. [| x: A; f: forest(A); r: C(f) \ |
59 |
\ |] ==> b(x,f,r): C(Tcons(x,f)); \ |
|
60 |
\ c : C(Fnil); \ |
|
515 | 61 |
\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: C(f) \ |
1461 | 62 |
\ |] ==> d(t,f,r1,r2): C(Fcons(t,f)) \ |
6046 | 63 |
\ |] ==> tree_forest_rec(b,c,d,z) : C(z)"; |
515 | 64 |
by (rtac (major RS tree_forest.induct) 1); |
4091 | 65 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
760 | 66 |
qed "TF_rec_type"; |
515 | 67 |
|
68 |
(*Mutually recursive version*) |
|
69 |
val prems = goal TF.thy |
|
1461 | 70 |
"[| !!x f r. [| x: A; f: forest(A); r: D(f) \ |
71 |
\ |] ==> b(x,f,r): C(Tcons(x,f)); \ |
|
72 |
\ c : D(Fnil); \ |
|
515 | 73 |
\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: D(f) \ |
1461 | 74 |
\ |] ==> d(t,f,r1,r2): D(Fcons(t,f)) \ |
6046 | 75 |
\ |] ==> (ALL t:tree(A). tree_forest_rec(b,c,d,t) : C(t)) & \ |
76 |
\ (ALL f: forest(A). tree_forest_rec(b,c,d,f) : D(f))"; |
|
515 | 77 |
by (rewtac Ball_def); |
78 |
by (rtac tree_forest.mutual_induct 1); |
|
4091 | 79 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
80 |
qed "tree_forest_rec_type"; |
515 | 81 |
|
82 |
||
6046 | 83 |
(** list_of_TF and of_list **) |
515 | 84 |
|
6046 | 85 |
Goal "z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))"; |
86 |
by (etac tree_forest.induct 1); |
|
87 |
by (ALLGOALS Asm_simp_tac); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
88 |
qed "list_of_TF_type"; |
515 | 89 |
|
6046 | 90 |
Goal "l: list(tree(A)) ==> of_list(l) : forest(A)"; |
91 |
by (etac list.induct 1); |
|
92 |
by (ALLGOALS Asm_simp_tac); |
|
93 |
qed "of_list_type"; |
|
515 | 94 |
|
95 |
||
6046 | 96 |
(** map **) |
515 | 97 |
|
6046 | 98 |
val prems = Goal |
515 | 99 |
"[| !!x. x: A ==> h(x): B |] ==> \ |
6046 | 100 |
\ (ALL t:tree(A). map(h,t) : tree(B)) & \ |
101 |
\ (ALL f: forest(A). map(h,f) : forest(B))"; |
|
102 |
by (rewtac Ball_def); |
|
103 |
by (rtac tree_forest.mutual_induct 1); |
|
104 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
|
105 |
qed "map_type"; |
|
515 | 106 |
|
107 |
||
6046 | 108 |
(** size **) |
515 | 109 |
|
6046 | 110 |
Goal "z: tree_forest(A) ==> size(z) : nat"; |
111 |
by (etac tree_forest.induct 1); |
|
112 |
by (ALLGOALS Asm_simp_tac); |
|
113 |
qed "size_type"; |
|
515 | 114 |
|
115 |
||
6046 | 116 |
(** preorder **) |
515 | 117 |
|
6046 | 118 |
Goal "z: tree_forest(A) ==> preorder(z) : list(A)"; |
119 |
by (etac tree_forest.induct 1); |
|
120 |
by (ALLGOALS Asm_simp_tac); |
|
121 |
qed "preorder_type"; |
|
515 | 122 |
|
123 |
||
124 |
(** Term simplification **) |
|
125 |
||
126 |
val treeI = tree_subset_TF RS subsetD |
|
127 |
and forestI = forest_subset_TF RS subsetD; |
|
128 |
||
6046 | 129 |
val typechecks = |
130 |
[treeI, forestI, |
|
131 |
list_of_TF_type, map_type, size_type, preorder_type]; |
|
515 | 132 |
|
6046 | 133 |
Addsimps typechecks; |
515 | 134 |
|
6046 | 135 |
(** theorems about list_of_TF and of_list **) |
515 | 136 |
|
137 |
(*essentially the same as list induction*) |
|
6046 | 138 |
val major::prems = Goal |
1461 | 139 |
"[| f: forest(A); \ |
515 | 140 |
\ R(Fnil); \ |
141 |
\ !!t f. [| t: tree(A); f: forest(A); R(f) |] ==> R(Fcons(t,f)) \ |
|
142 |
\ |] ==> R(f)"; |
|
143 |
by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1); |
|
144 |
by (REPEAT (ares_tac (TrueI::prems) 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
145 |
qed "forest_induct"; |
515 | 146 |
|
6046 | 147 |
Goal "f: forest(A) ==> of_list(list_of_TF(f)) = f"; |
515 | 148 |
by (etac forest_induct 1); |
2469 | 149 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
150 |
qed "forest_iso"; |
515 | 151 |
|
6046 | 152 |
Goal "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts"; |
515 | 153 |
by (etac list.induct 1); |
2469 | 154 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
155 |
qed "tree_list_iso"; |
515 | 156 |
|
6046 | 157 |
(** theorems about map **) |
515 | 158 |
|
6046 | 159 |
Goal "z: tree_forest(A) ==> map(%u. u, z) = z"; |
515 | 160 |
by (etac tree_forest.induct 1); |
2469 | 161 |
by (ALLGOALS Asm_simp_tac); |
6046 | 162 |
qed "map_ident"; |
515 | 163 |
|
6046 | 164 |
Goal "z: tree_forest(A) ==> map(h, map(j,z)) = map(%u. h(j(u)), z)"; |
165 |
by (etac tree_forest.induct 1); |
|
166 |
by (ALLGOALS Asm_simp_tac); |
|
167 |
qed "map_compose"; |
|
168 |
||
169 |
(** theorems about size **) |
|
170 |
||
171 |
Goal "z: tree_forest(A) ==> size(map(h,z)) = size(z)"; |
|
515 | 172 |
by (etac tree_forest.induct 1); |
2469 | 173 |
by (ALLGOALS Asm_simp_tac); |
6046 | 174 |
qed "size_map"; |
515 | 175 |
|
6046 | 176 |
Goal "z: tree_forest(A) ==> size(z) = length(preorder(z))"; |
515 | 177 |
by (etac tree_forest.induct 1); |
6046 | 178 |
by (ALLGOALS (*TYPECHECKING: why so explicit?*) |
179 |
(asm_simp_tac |
|
180 |
(simpset() addsimps [treeI RS preorder_type RS length_app]))); |
|
181 |
qed "size_length"; |
|
515 | 182 |
|
6046 | 183 |
(** theorems about preorder **) |
515 | 184 |
|
6046 | 185 |
Goal "z: tree_forest(A) ==> preorder(TF.map(h,z)) = List.map(h, preorder(z))"; |
515 | 186 |
by (etac tree_forest.induct 1); |
6046 | 187 |
by (ALLGOALS (*TYPECHECKING: why so explicit?*) |
188 |
(asm_simp_tac |
|
189 |
(simpset() addsimps [treeI RS preorder_type RS map_app_distrib]))); |
|
190 |
qed "preorder_map"; |