author | paulson |
Thu, 13 Jan 2000 17:36:02 +0100 | |
changeset 8126 | 6244be18fa55 |
parent 7499 | 23e090051cb8 |
child 11316 | b4e71bd751e4 |
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 |
||
6160 | 10 |
AddTCs [term.Apply_I]; |
11 |
||
5068 | 12 |
Goal "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 |
4091 | 14 |
by (fast_tac (claset() addSIs (map rew intrs) 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
|
15 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
16 |
qed "term_unfold"; |
434 | 17 |
|
0 | 18 |
(*Induction on term(A) followed by induction on List *) |
6046 | 19 |
val major::prems = Goal |
0 | 20 |
"[| t: term(A); \ |
21 |
\ !!x. [| x: A |] ==> P(Apply(x,Nil)); \ |
|
22 |
\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); P(Apply(x,zs)) \ |
|
23 |
\ |] ==> P(Apply(x, Cons(z,zs))) \ |
|
24 |
\ |] ==> P(t)"; |
|
515 | 25 |
by (rtac (major RS term.induct) 1); |
26 |
by (etac list.induct 1); |
|
0 | 27 |
by (etac CollectE 2); |
28 |
by (REPEAT (ares_tac (prems@[list_CollectD]) 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
29 |
qed "term_induct2"; |
0 | 30 |
|
31 |
(*Induction on term(A) to prove an equation*) |
|
6046 | 32 |
val major::prems = Goal |
0 | 33 |
"[| t: term(A); \ |
34 |
\ !!x zs. [| x: A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==> \ |
|
35 |
\ f(Apply(x,zs)) = g(Apply(x,zs)) \ |
|
36 |
\ |] ==> f(t)=g(t)"; |
|
515 | 37 |
by (rtac (major RS term.induct) 1); |
0 | 38 |
by (resolve_tac prems 1); |
39 |
by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1)); |
|
760 | 40 |
qed "term_induct_eqn"; |
0 | 41 |
|
42 |
(** Lemmas to justify using "term" in other recursive type definitions **) |
|
43 |
||
5137 | 44 |
Goalw term.defs "A<=B ==> term(A) <= term(B)"; |
0 | 45 |
by (rtac lfp_mono 1); |
515 | 46 |
by (REPEAT (rtac term.bnd_mono 1)); |
0 | 47 |
by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
48 |
qed "term_mono"; |
0 | 49 |
|
50 |
(*Easily provable by induction also*) |
|
5068 | 51 |
Goalw (term.defs@term.con_defs) "term(univ(A)) <= univ(A)"; |
0 | 52 |
by (rtac lfp_lowerbound 1); |
53 |
by (rtac (A_subset_univ RS univ_mono) 2); |
|
4152 | 54 |
by Safe_tac; |
0 | 55 |
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
|
56 |
qed "term_univ"; |
0 | 57 |
|
434 | 58 |
val term_subset_univ = |
59 |
term_mono RS (term_univ RSN (2,subset_trans)) |> standard; |
|
0 | 60 |
|
5137 | 61 |
Goal "[| t: term(A); A <= univ(B) |] ==> t: univ(B)"; |
434 | 62 |
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
|
63 |
qed "term_into_univ"; |
515 | 64 |
|
65 |
||
66 |
(*** term_rec -- by Vset recursion ***) |
|
67 |
||
68 |
(*Lemma: map works correctly on the underlying list of terms*) |
|
6046 | 69 |
Goal "[| l: list(A); Ord(i) |] ==> \ |
70 |
\ rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)"; |
|
71 |
by (etac list.induct 1); |
|
2469 | 72 |
by (Simp_tac 1); |
515 | 73 |
by (rtac impI 1); |
6046 | 74 |
by (subgoal_tac "rank(a)<i & rank(l) < i" 1); |
8126 | 75 |
by (asm_simp_tac (simpset() addsimps [rank_of_Ord]) 1); |
6046 | 76 |
by (full_simp_tac (simpset() addsimps list.con_defs) 1); |
77 |
by (blast_tac (claset() addDs (rank_rls RL [lt_trans])) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
78 |
qed "map_lemma"; |
515 | 79 |
|
80 |
(*Typing premise is necessary to invoke map_lemma*) |
|
6046 | 81 |
Goal "ts: list(A) ==> \ |
82 |
\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))"; |
|
515 | 83 |
by (rtac (term_rec_def RS def_Vrec RS trans) 1); |
84 |
by (rewrite_goals_tac term.con_defs); |
|
8126 | 85 |
by (asm_simp_tac (simpset() addsimps [rank_pair2, map_lemma]) 1);; |
760 | 86 |
qed "term_rec"; |
515 | 87 |
|
88 |
(*Slightly odd typing condition on r in the second premise!*) |
|
6046 | 89 |
val major::prems = Goal |
1461 | 90 |
"[| t: term(A); \ |
91 |
\ !!x zs r. [| x: A; zs: list(term(A)); \ |
|
92 |
\ r: list(UN t:term(A). C(t)) |] \ |
|
93 |
\ ==> d(x, zs, r): C(Apply(x,zs)) \ |
|
515 | 94 |
\ |] ==> term_rec(t,d) : C(t)"; |
95 |
by (rtac (major RS term.induct) 1); |
|
7499 | 96 |
by (ftac list_CollectD 1); |
2034 | 97 |
by (stac term_rec 1); |
515 | 98 |
by (REPEAT (ares_tac prems 1)); |
99 |
by (etac list.induct 1); |
|
4091 | 100 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [term_rec]))); |
6160 | 101 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
102 |
qed "term_rec_type"; |
515 | 103 |
|
6046 | 104 |
val [rew,tslist] = Goal |
515 | 105 |
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \ |
3840 | 106 |
\ j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))"; |
515 | 107 |
by (rewtac rew); |
108 |
by (rtac (tslist RS term_rec) 1); |
|
760 | 109 |
qed "def_term_rec"; |
515 | 110 |
|
6046 | 111 |
val prems = Goal |
1461 | 112 |
"[| t: term(A); \ |
515 | 113 |
\ !!x zs r. [| x: A; zs: list(term(A)); r: list(C) |] \ |
1461 | 114 |
\ ==> d(x, zs, r): C \ |
515 | 115 |
\ |] ==> term_rec(t,d) : C"; |
116 |
by (REPEAT (ares_tac (term_rec_type::prems) 1)); |
|
117 |
by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1); |
|
760 | 118 |
qed "term_rec_simple_type"; |
515 | 119 |
|
6160 | 120 |
AddTCs [term_rec_simple_type]; |
515 | 121 |
|
122 |
(** term_map **) |
|
123 |
||
6112 | 124 |
bind_thm ("term_map", term_map_def RS def_term_rec); |
515 | 125 |
|
6046 | 126 |
val prems = Goalw [term_map_def] |
515 | 127 |
"[| t: term(A); !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)"; |
128 |
by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1)); |
|
760 | 129 |
qed "term_map_type"; |
515 | 130 |
|
6046 | 131 |
Goal "t: term(A) ==> term_map(f,t) : term({f(u). u:A})"; |
132 |
by (etac term_map_type 1); |
|
515 | 133 |
by (etac RepFunI 1); |
760 | 134 |
qed "term_map_type2"; |
515 | 135 |
|
136 |
||
137 |
(** term_size **) |
|
138 |
||
6112 | 139 |
bind_thm ("term_size", term_size_def RS def_term_rec); |
515 | 140 |
|
5137 | 141 |
Goalw [term_size_def] "t: term(A) ==> term_size(t) : nat"; |
6160 | 142 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
143 |
qed "term_size_type"; |
515 | 144 |
|
145 |
||
146 |
(** reflect **) |
|
147 |
||
6112 | 148 |
bind_thm ("reflect", reflect_def RS def_term_rec); |
515 | 149 |
|
5137 | 150 |
Goalw [reflect_def] "t: term(A) ==> reflect(t) : term(A)"; |
6160 | 151 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
152 |
qed "reflect_type"; |
515 | 153 |
|
154 |
(** preorder **) |
|
155 |
||
6112 | 156 |
bind_thm ("preorder", preorder_def RS def_term_rec); |
515 | 157 |
|
6160 | 158 |
Goalw [preorder_def] "t: term(A) ==> preorder(t) : list(A)"; |
159 |
by Auto_tac; |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
160 |
qed "preorder_type"; |
515 | 161 |
|
6112 | 162 |
(** postorder **) |
163 |
||
164 |
bind_thm ("postorder", postorder_def RS def_term_rec); |
|
165 |
||
6160 | 166 |
Goalw [postorder_def] "t: term(A) ==> postorder(t) : list(A)"; |
167 |
by Auto_tac; |
|
6112 | 168 |
qed "postorder_type"; |
169 |
||
515 | 170 |
|
171 |
(** Term simplification **) |
|
172 |
||
6160 | 173 |
AddTCs [term_map_type, term_map_type2, term_size_type, |
6153 | 174 |
reflect_type, preorder_type, postorder_type]; |
515 | 175 |
|
176 |
(*map_type2 and term_map_type2 instantiate variables*) |
|
6153 | 177 |
Addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]; |
515 | 178 |
|
179 |
||
180 |
(** theorems about term_map **) |
|
181 |
||
6112 | 182 |
Addsimps [thm "List.map_compose"]; (*there is also TF.map_compose*) |
183 |
||
5137 | 184 |
Goal "t: term(A) ==> term_map(%u. u, t) = t"; |
515 | 185 |
by (etac term_induct_eqn 1); |
6112 | 186 |
by (Asm_simp_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
187 |
qed "term_map_ident"; |
515 | 188 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
189 |
Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)"; |
515 | 190 |
by (etac term_induct_eqn 1); |
6160 | 191 |
by (Asm_simp_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
192 |
qed "term_map_compose"; |
515 | 193 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
194 |
Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; |
515 | 195 |
by (etac term_induct_eqn 1); |
6112 | 196 |
by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym]) 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 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
202 |
Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)"; |
515 | 203 |
by (etac term_induct_eqn 1); |
6160 | 204 |
by (Asm_simp_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
205 |
qed "term_size_term_map"; |
515 | 206 |
|
5137 | 207 |
Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)"; |
515 | 208 |
by (etac term_induct_eqn 1); |
6112 | 209 |
by (asm_simp_tac(simpset() addsimps [rev_map_distrib RS sym, list_add_rev]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
210 |
qed "term_size_reflect"; |
515 | 211 |
|
5137 | 212 |
Goal "t: term(A) ==> term_size(t) = length(preorder(t))"; |
515 | 213 |
by (etac term_induct_eqn 1); |
6112 | 214 |
by (asm_simp_tac (simpset() addsimps [length_flat]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
215 |
qed "term_size_length"; |
515 | 216 |
|
217 |
||
218 |
(** theorems about reflect **) |
|
219 |
||
5137 | 220 |
Goal "t: term(A) ==> reflect(reflect(t)) = t"; |
515 | 221 |
by (etac term_induct_eqn 1); |
6112 | 222 |
by (asm_simp_tac (simpset() addsimps [rev_map_distrib]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
223 |
qed "reflect_reflect_ident"; |
515 | 224 |
|
225 |
||
226 |
(** theorems about preorder **) |
|
227 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
228 |
Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; |
515 | 229 |
by (etac term_induct_eqn 1); |
6112 | 230 |
by (asm_simp_tac (simpset() addsimps [map_flat]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
231 |
qed "preorder_term_map"; |
515 | 232 |
|
6112 | 233 |
Goal "t: term(A) ==> preorder(reflect(t)) = rev(postorder(t))"; |
234 |
by (etac term_induct_eqn 1); |
|
235 |
by (asm_simp_tac(simpset() addsimps [rev_app_distrib, rev_flat, |
|
236 |
rev_map_distrib RS sym]) 1); |
|
237 |
qed "preorder_reflect_eq_rev_postorder"; |
|
238 |
||
515 | 239 |
|
240 |
writeln"Reached end of file."; |