author | paulson |
Mon, 28 Dec 1998 16:54:01 +0100 | |
changeset 6046 | 2c8a8be36c94 |
parent 5147 | 825877190618 |
child 6112 | 5e4871c5136b |
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 |
|
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); |
75 |
by (asm_simp_tac (simpset() addsimps [VsetI]) 1); |
|
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); |
|
6046 | 85 |
by (asm_simp_tac (simpset() addsimps [Ord_rank, 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); |
|
96 |
by (forward_tac [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]))); |
515 | 101 |
by (etac CollectE 1); |
102 |
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
|
103 |
qed "term_rec_type"; |
515 | 104 |
|
6046 | 105 |
val [rew,tslist] = Goal |
515 | 106 |
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \ |
3840 | 107 |
\ j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))"; |
515 | 108 |
by (rewtac rew); |
109 |
by (rtac (tslist RS term_rec) 1); |
|
760 | 110 |
qed "def_term_rec"; |
515 | 111 |
|
6046 | 112 |
val prems = Goal |
1461 | 113 |
"[| t: term(A); \ |
515 | 114 |
\ !!x zs r. [| x: A; zs: list(term(A)); r: list(C) |] \ |
1461 | 115 |
\ ==> d(x, zs, r): C \ |
515 | 116 |
\ |] ==> term_rec(t,d) : C"; |
117 |
by (REPEAT (ares_tac (term_rec_type::prems) 1)); |
|
118 |
by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1); |
|
760 | 119 |
qed "term_rec_simple_type"; |
515 | 120 |
|
121 |
||
122 |
(** term_map **) |
|
123 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
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 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
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"; |
515 | 142 |
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
|
143 |
qed "term_size_type"; |
515 | 144 |
|
145 |
||
146 |
(** reflect **) |
|
147 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
148 |
bind_thm ("reflect", (reflect_def RS def_term_rec)); |
515 | 149 |
|
5137 | 150 |
Goalw [reflect_def] "t: term(A) ==> reflect(t) : term(A)"; |
515 | 151 |
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
|
152 |
qed "reflect_type"; |
515 | 153 |
|
154 |
(** preorder **) |
|
155 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
156 |
bind_thm ("preorder", (preorder_def RS def_term_rec)); |
515 | 157 |
|
5068 | 158 |
Goalw [preorder_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
159 |
"t: term(A) ==> preorder(t) : list(A)"; |
515 | 160 |
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
|
161 |
qed "preorder_type"; |
515 | 162 |
|
163 |
||
164 |
(** Term simplification **) |
|
165 |
||
166 |
val term_typechecks = |
|
167 |
[term.Apply_I, term_map_type, term_map_type2, term_size_type, |
|
168 |
reflect_type, preorder_type]; |
|
169 |
||
170 |
(*map_type2 and term_map_type2 instantiate variables*) |
|
4091 | 171 |
simpset_ref() := simpset() |
515 | 172 |
addsimps [term_rec, term_map, term_size, reflect, preorder] |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2496
diff
changeset
|
173 |
setSolver type_auto_tac (list_typechecks@term_typechecks); |
515 | 174 |
|
175 |
||
176 |
(** theorems about term_map **) |
|
177 |
||
5137 | 178 |
Goal "t: term(A) ==> term_map(%u. u, t) = t"; |
515 | 179 |
by (etac term_induct_eqn 1); |
4091 | 180 |
by (asm_simp_tac (simpset() addsimps [map_ident]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
181 |
qed "term_map_ident"; |
515 | 182 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
183 |
Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)"; |
515 | 184 |
by (etac term_induct_eqn 1); |
4091 | 185 |
by (asm_simp_tac (simpset() addsimps [map_compose]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
186 |
qed "term_map_compose"; |
515 | 187 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
188 |
Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; |
515 | 189 |
by (etac term_induct_eqn 1); |
4091 | 190 |
by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
191 |
qed "term_map_reflect"; |
515 | 192 |
|
193 |
||
194 |
(** theorems about term_size **) |
|
195 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
196 |
Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)"; |
515 | 197 |
by (etac term_induct_eqn 1); |
4091 | 198 |
by (asm_simp_tac (simpset() addsimps [map_compose]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
199 |
qed "term_size_term_map"; |
515 | 200 |
|
5137 | 201 |
Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)"; |
515 | 202 |
by (etac term_induct_eqn 1); |
4091 | 203 |
by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose, |
1461 | 204 |
list_add_rev]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
205 |
qed "term_size_reflect"; |
515 | 206 |
|
5137 | 207 |
Goal "t: term(A) ==> term_size(t) = length(preorder(t))"; |
515 | 208 |
by (etac term_induct_eqn 1); |
4091 | 209 |
by (asm_simp_tac (simpset() addsimps [length_flat, map_compose]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
210 |
qed "term_size_length"; |
515 | 211 |
|
212 |
||
213 |
(** theorems about reflect **) |
|
214 |
||
5137 | 215 |
Goal "t: term(A) ==> reflect(reflect(t)) = t"; |
515 | 216 |
by (etac term_induct_eqn 1); |
4091 | 217 |
by (asm_simp_tac (simpset() addsimps [rev_map_distrib, map_compose, |
1461 | 218 |
map_ident, rev_rev_ident]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
219 |
qed "reflect_reflect_ident"; |
515 | 220 |
|
221 |
||
222 |
(** theorems about preorder **) |
|
223 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
224 |
Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; |
515 | 225 |
by (etac term_induct_eqn 1); |
4091 | 226 |
by (asm_simp_tac (simpset() addsimps [map_compose, map_flat]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
227 |
qed "preorder_term_map"; |
515 | 228 |
|
229 |
(** preorder(reflect(t)) = rev(postorder(t)) **) |
|
230 |
||
231 |
writeln"Reached end of file."; |