author | lcp |
Thu, 18 Aug 1994 12:48:03 +0200 | |
changeset 114 | b7f57e0ab47c |
parent 48 | 21291189b51e |
child 127 | d9527f97246e |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: HOL/ex/term |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
For term.thy. illustrates List functor |
|
7 |
(essentially the same type as in Trees & Forests) |
|
8 |
*) |
|
9 |
||
10 |
open Term; |
|
11 |
||
12 |
(*** Monotonicity and unfolding of the function ***) |
|
13 |
||
14 |
goal Term.thy "mono(%Z. A <*> List(Z))"; |
|
15 |
by (REPEAT (ares_tac [monoI, subset_refl, List_mono, uprod_mono] 1)); |
|
16 |
val Term_fun_mono = result(); |
|
17 |
||
18 |
val Term_unfold = Term_fun_mono RS (Term_def RS def_lfp_Tarski); |
|
19 |
||
20 |
(*This justifies using Term in other recursive type definitions*) |
|
21 |
goalw Term.thy [Term_def] "!!A B. A<=B ==> Term(A) <= Term(B)"; |
|
22 |
by (REPEAT (ares_tac [lfp_mono, subset_refl, List_mono, uprod_mono] 1)); |
|
23 |
val Term_mono = result(); |
|
24 |
||
25 |
(** Type checking rules -- Term creates well-founded sets **) |
|
26 |
||
27 |
val prems = goalw Term.thy [Term_def] "Term(Sexp) <= Sexp"; |
|
28 |
by (rtac lfp_lowerbound 1); |
|
29 |
by (fast_tac (univ_cs addIs [Sexp_SconsI, List_Sexp RS subsetD]) 1); |
|
30 |
val Term_Sexp = result(); |
|
31 |
||
32 |
(* A <= Sexp ==> Term(A) <= Sexp *) |
|
33 |
val Term_subset_Sexp = standard |
|
34 |
(Term_mono RS (Term_Sexp RSN (2,subset_trans))); |
|
35 |
||
36 |
||
37 |
(** Elimination -- structural induction on the set Term(A) **) |
|
38 |
||
39 |
(*Induction for the set Term(A) *) |
|
40 |
val [major,minor] = goal Term.thy |
|
41 |
"[| M: Term(A); \ |
|
42 |
\ !!x zs. [| x: A; zs: List(Term(A)); zs: List({x.R(x)}) \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
43 |
\ |] ==> R(x$zs) \ |
0 | 44 |
\ |] ==> R(M)"; |
45 |
by (rtac (major RS (Term_def RS def_induct)) 1); |
|
46 |
by (rtac Term_fun_mono 1); |
|
47 |
by (REPEAT (eresolve_tac ([uprodE, ssubst, minor] @ |
|
48 |
([Int_lower1,Int_lower2] RL [List_mono RS subsetD])) 1)); |
|
49 |
val Term_induct = result(); |
|
50 |
||
51 |
(*Induction on Term(A) followed by induction on List *) |
|
52 |
val major::prems = goal Term.thy |
|
53 |
"[| M: Term(A); \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
54 |
\ !!x. [| x: A |] ==> R(x$NIL); \ |
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
55 |
\ !!x z zs. [| x: A; z: Term(A); zs: List(Term(A)); R(x$zs) \ |
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
56 |
\ |] ==> R(x $ CONS(z,zs)) \ |
0 | 57 |
\ |] ==> R(M)"; |
58 |
by (rtac (major RS Term_induct) 1); |
|
59 |
by (etac List_induct 1); |
|
60 |
by (REPEAT (ares_tac prems 1)); |
|
61 |
val Term_induct2 = result(); |
|
62 |
||
63 |
(*** Structural Induction on the abstract type 'a term ***) |
|
64 |
||
65 |
val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons]; |
|
66 |
||
67 |
val Rep_Term_in_Sexp = |
|
68 |
Rep_Term RS (range_Leaf_subset_Sexp RS Term_subset_Sexp RS subsetD); |
|
69 |
||
70 |
(*Induction for the abstract type 'a term*) |
|
71 |
val prems = goalw Term.thy [App_def,Rep_TList_def,Abs_TList_def] |
|
72 |
"[| !!x ts. list_all(R,ts) ==> R(App(x,ts)) \ |
|
73 |
\ |] ==> R(t)"; |
|
74 |
by (rtac (Rep_Term_inverse RS subst) 1); (*types force good instantiation*) |
|
75 |
by (res_inst_tac [("P","Rep_Term(t) : Sexp")] conjunct2 1); |
|
76 |
by (rtac (Rep_Term RS Term_induct) 1); |
|
77 |
by (REPEAT (ares_tac [conjI, Sexp_SconsI, Term_subset_Sexp RS |
|
78 |
List_subset_Sexp,range_Leaf_subset_Sexp] 1 |
|
79 |
ORELSE etac rev_subsetD 1)); |
|
80 |
by (eres_inst_tac [("A1","Term(?u)"), ("f1","Rep_Term"), ("g1","Abs_Term")] |
|
81 |
(Abs_map_inverse RS subst) 1); |
|
82 |
by (rtac (range_Leaf_subset_Sexp RS Term_subset_Sexp) 1); |
|
83 |
by (etac Abs_Term_inverse 1); |
|
84 |
by (etac rangeE 1); |
|
85 |
by (hyp_subst_tac 1); |
|
86 |
by (resolve_tac prems 1); |
|
87 |
by (etac List_induct 1); |
|
88 |
by (etac CollectE 2); |
|
89 |
by (stac Abs_map_CONS 2); |
|
90 |
by (etac conjunct1 2); |
|
91 |
by (etac rev_subsetD 2); |
|
92 |
by (rtac List_subset_Sexp 2); |
|
93 |
by (fast_tac set_cs 2); |
|
94 |
by (ALLGOALS (asm_simp_tac list_all_ss)); |
|
95 |
val term_induct = result(); |
|
96 |
||
97 |
(*Induction for the abstract type 'a term*) |
|
98 |
val prems = goal Term.thy |
|
99 |
"[| !!x. R(App(x,Nil)); \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
100 |
\ !!x t ts. R(App(x,ts)) ==> R(App(x, t#ts)) \ |
0 | 101 |
\ |] ==> R(t)"; |
102 |
by (rtac term_induct 1); (*types force good instantiation*) |
|
103 |
by (etac rev_mp 1); |
|
104 |
by (rtac list_induct 1); (*types force good instantiation*) |
|
105 |
by (ALLGOALS (asm_simp_tac (list_all_ss addsimps prems))); |
|
106 |
val term_induct2 = result(); |
|
107 |
||
108 |
(*Perform induction on xs. *) |
|
109 |
fun term_ind2_tac a i = |
|
110 |
EVERY [res_inst_tac [("t",a)] term_induct2 i, |
|
111 |
rename_last_tac a ["1","s"] (i+1)]; |
|
112 |
||
113 |
||
114 |
(** Introduction rule for Term **) |
|
115 |
||
116 |
(* c : A <*> List(Term(A)) ==> c : Term(A) *) |
|
117 |
val TermI = standard (Term_unfold RS equalityD2 RS subsetD); |
|
118 |
||
119 |
(*The constant APP is not declared; it is simply . *) |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
120 |
val prems = goal Term.thy "[| M: A; N : List(Term(A)) |] ==> M$N : Term(A)"; |
0 | 121 |
by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1)); |
122 |
val APP_I = result(); |
|
123 |
||
124 |
||
125 |
(*** Term_rec -- by wf recursion on pred_Sexp ***) |
|
126 |
||
127 |
val Term_rec_unfold = |
|
128 |
wf_pred_Sexp RS wf_trancl RS (Term_rec_def RS def_wfrec); |
|
129 |
||
130 |
(** conversion rules **) |
|
131 |
||
132 |
val [prem] = goal Term.thy |
|
133 |
"N: List(Term(A)) ==> \ |
|
134 |
\ !M. <N,M>: pred_Sexp^+ --> \ |
|
135 |
\ Abs_map(cut(h, pred_Sexp^+, M), N) = \ |
|
136 |
\ Abs_map(h,N)"; |
|
137 |
by (rtac (prem RS List_induct) 1); |
|
138 |
by (simp_tac list_all_ss 1); |
|
139 |
by (strip_tac 1); |
|
140 |
by (etac (pred_Sexp_CONS_D RS conjE) 1); |
|
141 |
by (asm_simp_tac (list_all_ss addsimps [trancl_pred_SexpD1, cut_apply]) 1); |
|
142 |
val Abs_map_lemma = result(); |
|
143 |
||
144 |
val [prem1,prem2,A_subset_Sexp] = goal Term.thy |
|
145 |
"[| M: Sexp; N: List(Term(A)); A<=Sexp |] ==> \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
146 |
\ Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))"; |
0 | 147 |
by (rtac (Term_rec_unfold RS trans) 1); |
148 |
by (simp_tac (HOL_ss addsimps |
|
114 | 149 |
[Split, |
150 |
prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl, |
|
0 | 151 |
prem1, prem2 RS rev_subsetD, List_subset_Sexp, |
152 |
Term_subset_Sexp, A_subset_Sexp])1); |
|
153 |
val Term_rec = result(); |
|
154 |
||
155 |
(*** term_rec -- by Term_rec ***) |
|
156 |
||
157 |
local |
|
158 |
val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy) |
|
159 |
[("f","Rep_Term")] Rep_map_type; |
|
160 |
val Rep_TList = Rep_Term RS Rep_map_type1; |
|
161 |
val Rep_Term_rec = range_Leaf_subset_Sexp RSN (2,Rep_TList RSN(2,Term_rec)); |
|
162 |
||
163 |
(*Now avoids conditional rewriting with the premise N: List(Term(A)), |
|
164 |
since A will be uninstantiated and will cause rewriting to fail. *) |
|
165 |
val term_rec_ss = HOL_ss |
|
166 |
addsimps [Rep_TList RS (rangeI RS APP_I RS Abs_Term_inverse), |
|
167 |
Rep_Term_in_Sexp, Rep_Term_rec, Rep_Term_inverse, |
|
168 |
inj_Leaf, Inv_f_f, |
|
169 |
Abs_Rep_map, map_ident, Sexp_LeafI] |
|
170 |
in |
|
171 |
||
172 |
val term_rec = prove_goalw Term.thy |
|
173 |
[term_rec_def, App_def, Rep_TList_def, Abs_TList_def] |
|
174 |
"term_rec(App(f,ts), d) = d(f, ts, map (%t. term_rec(t,d), ts))" |
|
175 |
(fn _ => [simp_tac term_rec_ss 1]) |
|
176 |
||
177 |
end; |