author | paulson |
Thu, 26 Sep 1996 15:49:54 +0200 | |
changeset 2034 | 5079fdf938dd |
parent 1461 | 6bcb44e4d6e5 |
child 2469 | b50b8c0eec01 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/Term.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
486 | 4 |
Copyright 1994 University of Cambridge |
0 | 5 |
|
6 |
Datatype definition of terms over an alphabet. |
|
7 |
Illustrates the list functor (essentially the same type as in Trees & Forests) |
|
8 |
*) |
|
9 |
||
515 | 10 |
open Term; |
0 | 11 |
|
434 | 12 |
goal Term.thy "term(A) = A * list(term(A))"; |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
13 |
let open term; val rew = rewrite_rule con_defs in |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
14 |
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs) |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
15 |
addEs [rew elim]) 1) |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
16 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
17 |
qed "term_unfold"; |
434 | 18 |
|
0 | 19 |
(*Induction on term(A) followed by induction on List *) |
20 |
val major::prems = goal Term.thy |
|
21 |
"[| t: term(A); \ |
|
22 |
\ !!x. [| x: A |] ==> P(Apply(x,Nil)); \ |
|
23 |
\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); P(Apply(x,zs)) \ |
|
24 |
\ |] ==> P(Apply(x, Cons(z,zs))) \ |
|
25 |
\ |] ==> P(t)"; |
|
515 | 26 |
by (rtac (major RS term.induct) 1); |
27 |
by (etac list.induct 1); |
|
0 | 28 |
by (etac CollectE 2); |
29 |
by (REPEAT (ares_tac (prems@[list_CollectD]) 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
30 |
qed "term_induct2"; |
0 | 31 |
|
32 |
(*Induction on term(A) to prove an equation*) |
|
515 | 33 |
val major::prems = goal Term.thy |
0 | 34 |
"[| t: term(A); \ |
35 |
\ !!x zs. [| x: A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==> \ |
|
36 |
\ f(Apply(x,zs)) = g(Apply(x,zs)) \ |
|
37 |
\ |] ==> f(t)=g(t)"; |
|
515 | 38 |
by (rtac (major RS term.induct) 1); |
0 | 39 |
by (resolve_tac prems 1); |
40 |
by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1)); |
|
760 | 41 |
qed "term_induct_eqn"; |
0 | 42 |
|
43 |
(** Lemmas to justify using "term" in other recursive type definitions **) |
|
44 |
||
515 | 45 |
goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)"; |
0 | 46 |
by (rtac lfp_mono 1); |
515 | 47 |
by (REPEAT (rtac term.bnd_mono 1)); |
0 | 48 |
by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
49 |
qed "term_mono"; |
0 | 50 |
|
51 |
(*Easily provable by induction also*) |
|
515 | 52 |
goalw Term.thy (term.defs@term.con_defs) "term(univ(A)) <= univ(A)"; |
0 | 53 |
by (rtac lfp_lowerbound 1); |
54 |
by (rtac (A_subset_univ RS univ_mono) 2); |
|
55 |
by (safe_tac ZF_cs); |
|
56 |
by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
57 |
qed "term_univ"; |
0 | 58 |
|
434 | 59 |
val term_subset_univ = |
60 |
term_mono RS (term_univ RSN (2,subset_trans)) |> standard; |
|
0 | 61 |
|
434 | 62 |
goal Term.thy "!!t A B. [| t: term(A); A <= univ(B) |] ==> t: univ(B)"; |
63 |
by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
64 |
qed "term_into_univ"; |
515 | 65 |
|
66 |
||
67 |
(*** term_rec -- by Vset recursion ***) |
|
68 |
||
69 |
(*Lemma: map works correctly on the underlying list of terms*) |
|
70 |
val [major,ordi] = goal list.thy |
|
71 |
"[| l: list(A); Ord(i) |] ==> \ |
|
72 |
\ rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)"; |
|
73 |
by (rtac (major RS list.induct) 1); |
|
74 |
by (simp_tac list_ss 1); |
|
75 |
by (rtac impI 1); |
|
76 |
by (forward_tac [rank_Cons1 RS lt_trans] 1); |
|
77 |
by (dtac (rank_Cons2 RS lt_trans) 1); |
|
78 |
by (asm_simp_tac (list_ss addsimps [ordi, VsetI]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
79 |
qed "map_lemma"; |
515 | 80 |
|
81 |
(*Typing premise is necessary to invoke map_lemma*) |
|
82 |
val [prem] = goal Term.thy |
|
83 |
"ts: list(A) ==> \ |
|
84 |
\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))"; |
|
85 |
by (rtac (term_rec_def RS def_Vrec RS trans) 1); |
|
86 |
by (rewrite_goals_tac term.con_defs); |
|
87 |
val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma]; |
|
88 |
by (simp_tac term_rec_ss 1); |
|
760 | 89 |
qed "term_rec"; |
515 | 90 |
|
91 |
(*Slightly odd typing condition on r in the second premise!*) |
|
92 |
val major::prems = goal Term.thy |
|
1461 | 93 |
"[| t: term(A); \ |
94 |
\ !!x zs r. [| x: A; zs: list(term(A)); \ |
|
95 |
\ r: list(UN t:term(A). C(t)) |] \ |
|
96 |
\ ==> d(x, zs, r): C(Apply(x,zs)) \ |
|
515 | 97 |
\ |] ==> term_rec(t,d) : C(t)"; |
98 |
by (rtac (major RS term.induct) 1); |
|
99 |
by (forward_tac [list_CollectD] 1); |
|
2034 | 100 |
by (stac term_rec 1); |
515 | 101 |
by (REPEAT (ares_tac prems 1)); |
102 |
by (etac list.induct 1); |
|
103 |
by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec]))); |
|
104 |
by (etac CollectE 1); |
|
105 |
by (REPEAT (ares_tac [list.Cons_I, UN_I] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
106 |
qed "term_rec_type"; |
515 | 107 |
|
108 |
val [rew,tslist] = goal Term.thy |
|
109 |
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \ |
|
110 |
\ j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))"; |
|
111 |
by (rewtac rew); |
|
112 |
by (rtac (tslist RS term_rec) 1); |
|
760 | 113 |
qed "def_term_rec"; |
515 | 114 |
|
115 |
val prems = goal Term.thy |
|
1461 | 116 |
"[| t: term(A); \ |
515 | 117 |
\ !!x zs r. [| x: A; zs: list(term(A)); r: list(C) |] \ |
1461 | 118 |
\ ==> d(x, zs, r): C \ |
515 | 119 |
\ |] ==> term_rec(t,d) : C"; |
120 |
by (REPEAT (ares_tac (term_rec_type::prems) 1)); |
|
121 |
by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1); |
|
760 | 122 |
qed "term_rec_simple_type"; |
515 | 123 |
|
124 |
||
125 |
(** term_map **) |
|
126 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
127 |
bind_thm ("term_map", (term_map_def RS def_term_rec)); |
515 | 128 |
|
129 |
val prems = goalw Term.thy [term_map_def] |
|
130 |
"[| t: term(A); !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)"; |
|
131 |
by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1)); |
|
760 | 132 |
qed "term_map_type"; |
515 | 133 |
|
134 |
val [major] = goal Term.thy |
|
135 |
"t: term(A) ==> term_map(f,t) : term({f(u). u:A})"; |
|
136 |
by (rtac (major RS term_map_type) 1); |
|
137 |
by (etac RepFunI 1); |
|
760 | 138 |
qed "term_map_type2"; |
515 | 139 |
|
140 |
||
141 |
(** term_size **) |
|
142 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
143 |
bind_thm ("term_size", (term_size_def RS def_term_rec)); |
515 | 144 |
|
145 |
goalw Term.thy [term_size_def] "!!t A. t: term(A) ==> term_size(t) : nat"; |
|
146 |
by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
147 |
qed "term_size_type"; |
515 | 148 |
|
149 |
||
150 |
(** reflect **) |
|
151 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
152 |
bind_thm ("reflect", (reflect_def RS def_term_rec)); |
515 | 153 |
|
154 |
goalw Term.thy [reflect_def] "!!t A. t: term(A) ==> reflect(t) : term(A)"; |
|
155 |
by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
156 |
qed "reflect_type"; |
515 | 157 |
|
158 |
(** preorder **) |
|
159 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
160 |
bind_thm ("preorder", (preorder_def RS def_term_rec)); |
515 | 161 |
|
162 |
goalw Term.thy [preorder_def] |
|
163 |
"!!t A. t: term(A) ==> preorder(t) : list(A)"; |
|
164 |
by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
165 |
qed "preorder_type"; |
515 | 166 |
|
167 |
||
168 |
(** Term simplification **) |
|
169 |
||
170 |
val term_typechecks = |
|
171 |
[term.Apply_I, term_map_type, term_map_type2, term_size_type, |
|
172 |
reflect_type, preorder_type]; |
|
173 |
||
174 |
(*map_type2 and term_map_type2 instantiate variables*) |
|
175 |
val term_ss = list_ss |
|
176 |
addsimps [term_rec, term_map, term_size, reflect, preorder] |
|
177 |
setsolver type_auto_tac (list_typechecks@term_typechecks); |
|
178 |
||
179 |
||
180 |
(** theorems about term_map **) |
|
181 |
||
182 |
goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t"; |
|
183 |
by (etac term_induct_eqn 1); |
|
184 |
by (asm_simp_tac (term_ss addsimps [map_ident]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
185 |
qed "term_map_ident"; |
515 | 186 |
|
187 |
goal Term.thy |
|
188 |
"!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)"; |
|
189 |
by (etac term_induct_eqn 1); |
|
190 |
by (asm_simp_tac (term_ss addsimps [map_compose]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
191 |
qed "term_map_compose"; |
515 | 192 |
|
193 |
goal Term.thy |
|
194 |
"!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; |
|
195 |
by (etac term_induct_eqn 1); |
|
196 |
by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
197 |
qed "term_map_reflect"; |
515 | 198 |
|
199 |
||
200 |
(** theorems about term_size **) |
|
201 |
||
202 |
goal Term.thy |
|
203 |
"!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)"; |
|
204 |
by (etac term_induct_eqn 1); |
|
205 |
by (asm_simp_tac (term_ss addsimps [map_compose]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
206 |
qed "term_size_term_map"; |
515 | 207 |
|
208 |
goal Term.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)"; |
|
209 |
by (etac term_induct_eqn 1); |
|
210 |
by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose, |
|
1461 | 211 |
list_add_rev]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
212 |
qed "term_size_reflect"; |
515 | 213 |
|
214 |
goal Term.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))"; |
|
215 |
by (etac term_induct_eqn 1); |
|
216 |
by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
217 |
qed "term_size_length"; |
515 | 218 |
|
219 |
||
220 |
(** theorems about reflect **) |
|
221 |
||
222 |
goal Term.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t"; |
|
223 |
by (etac term_induct_eqn 1); |
|
224 |
by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose, |
|
1461 | 225 |
map_ident, rev_rev_ident]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
226 |
qed "reflect_reflect_ident"; |
515 | 227 |
|
228 |
||
229 |
(** theorems about preorder **) |
|
230 |
||
231 |
goal Term.thy |
|
232 |
"!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; |
|
233 |
by (etac term_induct_eqn 1); |
|
234 |
by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
235 |
qed "preorder_term_map"; |
515 | 236 |
|
237 |
(** preorder(reflect(t)) = rev(postorder(t)) **) |
|
238 |
||
239 |
writeln"Reached end of file."; |