7 Binary trees with leaves that are constants or variables. |
7 Binary trees with leaves that are constants or variables. |
8 *) |
8 *) |
9 |
9 |
10 open UTerm; |
10 open UTerm; |
11 |
11 |
12 val uterm_con_defs = [VAR_def, CONST_def, COMB_def]; |
|
13 |
12 |
14 goal UTerm.thy "uterm(A) = A <+> A <+> (uterm(A) <*> uterm(A))"; |
13 (**** vars_of lemmas ****) |
15 let val rew = rewrite_rule uterm_con_defs in |
|
16 by (fast_tac (!claset addSIs (map rew uterm.intrs) |
|
17 addEs [rew uterm.elim]) 1) |
|
18 end; |
|
19 qed "uterm_unfold"; |
|
20 |
14 |
21 (** the uterm functional **) |
15 goal UTerm.thy "(v : vars_of(Var(w))) = (w=v)"; |
|
16 by (Simp_tac 1); |
|
17 by (fast_tac HOL_cs 1); |
|
18 qed "vars_var_iff"; |
22 |
19 |
23 (*This justifies using uterm in other recursive type definitions*) |
20 goal UTerm.thy "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; |
24 goalw UTerm.thy uterm.defs "!!A B. A<=B ==> uterm(A) <= uterm(B)"; |
21 by (induct_tac "t" 1); |
25 by (REPEAT (ares_tac (lfp_mono::basic_monos) 1)); |
22 by (ALLGOALS Simp_tac); |
26 qed "uterm_mono"; |
23 by (fast_tac HOL_cs 1); |
27 |
24 qed "vars_iff_occseq"; |
28 (** Type checking rules -- uterm creates well-founded sets **) |
|
29 |
|
30 goalw UTerm.thy (uterm_con_defs @ uterm.defs) "uterm(sexp) <= sexp"; |
|
31 by (rtac lfp_lowerbound 1); |
|
32 by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1); |
|
33 qed "uterm_sexp"; |
|
34 |
|
35 (* A <= sexp ==> uterm(A) <= sexp *) |
|
36 bind_thm ("uterm_subset_sexp", ([uterm_mono, uterm_sexp] MRS subset_trans)); |
|
37 |
|
38 (** Induction **) |
|
39 |
|
40 (*Induction for the type 'a uterm *) |
|
41 val prems = goalw UTerm.thy [Var_def,Const_def,Comb_def] |
|
42 "[| !!x.P(Var(x)); !!x.P(Const(x)); \ |
|
43 \ !!u v. [| P(u); P(v) |] ==> P(Comb u v) |] ==> P(t)"; |
|
44 by (rtac (Rep_uterm_inverse RS subst) 1); (*types force good instantiation*) |
|
45 by (rtac (Rep_uterm RS uterm.induct) 1); |
|
46 by (REPEAT (ares_tac prems 1 |
|
47 ORELSE eresolve_tac [rangeE, ssubst, Abs_uterm_inverse RS subst] 1)); |
|
48 qed "uterm_induct"; |
|
49 |
|
50 (*Perform induction on xs. *) |
|
51 fun uterm_ind_tac a M = |
|
52 EVERY [res_inst_tac [("t",a)] uterm_induct M, |
|
53 rename_last_tac a ["1"] (M+1)]; |
|
54 |
25 |
55 |
26 |
56 (*** Isomorphisms ***) |
27 (* Not used, but perhaps useful in other proofs *) |
57 |
28 goal UTerm.thy "M<:N --> vars_of(M) <= vars_of(N)"; |
58 goal UTerm.thy "inj(Rep_uterm)"; |
29 by (induct_tac "N" 1); |
59 by (rtac inj_inverseI 1); |
30 by (ALLGOALS Asm_simp_tac); |
60 by (rtac Rep_uterm_inverse 1); |
31 by (fast_tac set_cs 1); |
61 qed "inj_Rep_uterm"; |
32 val occs_vars_subset = result(); |
62 |
|
63 goal UTerm.thy "inj_onto Abs_uterm (uterm (range Leaf))"; |
|
64 by (rtac inj_onto_inverseI 1); |
|
65 by (etac Abs_uterm_inverse 1); |
|
66 qed "inj_onto_Abs_uterm"; |
|
67 |
|
68 (** Distinctness of constructors **) |
|
69 |
|
70 goalw UTerm.thy uterm_con_defs "~ CONST(c) = COMB u v"; |
|
71 by (rtac notI 1); |
|
72 by (etac (In1_inject RS (In0_not_In1 RS notE)) 1); |
|
73 qed "CONST_not_COMB"; |
|
74 bind_thm ("COMB_not_CONST", (CONST_not_COMB RS not_sym)); |
|
75 bind_thm ("CONST_neq_COMB", (CONST_not_COMB RS notE)); |
|
76 val COMB_neq_CONST = sym RS CONST_neq_COMB; |
|
77 |
|
78 goalw UTerm.thy uterm_con_defs "~ COMB u v = VAR(x)"; |
|
79 by (rtac In1_not_In0 1); |
|
80 qed "COMB_not_VAR"; |
|
81 bind_thm ("VAR_not_COMB", (COMB_not_VAR RS not_sym)); |
|
82 bind_thm ("COMB_neq_VAR", (COMB_not_VAR RS notE)); |
|
83 val VAR_neq_COMB = sym RS COMB_neq_VAR; |
|
84 |
|
85 goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)"; |
|
86 by (rtac In0_not_In1 1); |
|
87 qed "VAR_not_CONST"; |
|
88 bind_thm ("CONST_not_VAR", (VAR_not_CONST RS not_sym)); |
|
89 bind_thm ("VAR_neq_CONST", (VAR_not_CONST RS notE)); |
|
90 val CONST_neq_VAR = sym RS VAR_neq_CONST; |
|
91 |
33 |
92 |
34 |
93 goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb u v"; |
35 goal UTerm.thy "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"; |
94 by (rtac (CONST_not_COMB RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1); |
36 by (Blast_tac 1); |
95 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1)); |
37 val monotone_vars_of = result(); |
96 qed "Const_not_Comb"; |
|
97 bind_thm ("Comb_not_Const", (Const_not_Comb RS not_sym)); |
|
98 bind_thm ("Const_neq_Comb", (Const_not_Comb RS notE)); |
|
99 val Comb_neq_Const = sym RS Const_neq_Comb; |
|
100 |
38 |
101 goalw UTerm.thy [Comb_def,Var_def] "~ Comb u v = Var(x)"; |
39 goal UTerm.thy "finite(vars_of M)"; |
102 by (rtac (COMB_not_VAR RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1); |
40 by (induct_tac"M" 1); |
103 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1)); |
41 by (ALLGOALS Simp_tac); |
104 qed "Comb_not_Var"; |
42 by (forward_tac [finite_UnI] 1); |
105 bind_thm ("Var_not_Comb", (Comb_not_Var RS not_sym)); |
43 by (assume_tac 1); |
106 bind_thm ("Comb_neq_Var", (Comb_not_Var RS notE)); |
|
107 val Var_neq_Comb = sym RS Comb_neq_Var; |
|
108 |
|
109 goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)"; |
|
110 by (rtac (VAR_not_CONST RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1); |
|
111 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1)); |
|
112 qed "Var_not_Const"; |
|
113 bind_thm ("Const_not_Var", (Var_not_Const RS not_sym)); |
|
114 bind_thm ("Var_neq_Const", (Var_not_Const RS notE)); |
|
115 val Const_neq_Var = sym RS Var_neq_Const; |
|
116 |
|
117 |
|
118 (** Injectiveness of CONST and Const **) |
|
119 |
|
120 val inject_cs = HOL_cs addSEs [Scons_inject] |
|
121 addSDs [In0_inject,In1_inject]; |
|
122 |
|
123 goalw UTerm.thy [VAR_def] "(VAR(M)=VAR(N)) = (M=N)"; |
|
124 by (fast_tac inject_cs 1); |
|
125 qed "VAR_VAR_eq"; |
|
126 |
|
127 goalw UTerm.thy [CONST_def] "(CONST(M)=CONST(N)) = (M=N)"; |
|
128 by (fast_tac inject_cs 1); |
|
129 qed "CONST_CONST_eq"; |
|
130 |
|
131 goalw UTerm.thy [COMB_def] "(COMB K L = COMB M N) = (K=M & L=N)"; |
|
132 by (fast_tac inject_cs 1); |
|
133 qed "COMB_COMB_eq"; |
|
134 |
|
135 bind_thm ("VAR_inject", (VAR_VAR_eq RS iffD1)); |
|
136 bind_thm ("CONST_inject", (CONST_CONST_eq RS iffD1)); |
|
137 bind_thm ("COMB_inject", (COMB_COMB_eq RS iffD1 RS conjE)); |
|
138 |
|
139 |
|
140 (*For reasoning about abstract uterm constructors*) |
|
141 val uterm_cs = set_cs addIs uterm.intrs @ [Rep_uterm] |
|
142 addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST, |
|
143 COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR, |
|
144 COMB_inject] |
|
145 addSDs [VAR_inject,CONST_inject, |
|
146 inj_onto_Abs_uterm RS inj_ontoD, |
|
147 inj_Rep_uterm RS injD, Leaf_inject]; |
|
148 |
|
149 goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)"; |
|
150 by (fast_tac uterm_cs 1); |
|
151 qed "Var_Var_eq"; |
|
152 bind_thm ("Var_inject", (Var_Var_eq RS iffD1)); |
|
153 |
|
154 goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)"; |
|
155 by (fast_tac uterm_cs 1); |
|
156 qed "Const_Const_eq"; |
|
157 bind_thm ("Const_inject", (Const_Const_eq RS iffD1)); |
|
158 |
|
159 goalw UTerm.thy [Comb_def] "(Comb u v =Comb x y) = (u=x & v=y)"; |
|
160 by (fast_tac uterm_cs 1); |
|
161 qed "Comb_Comb_eq"; |
|
162 bind_thm ("Comb_inject", (Comb_Comb_eq RS iffD1 RS conjE)); |
|
163 |
|
164 val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A"; |
|
165 by (rtac (major RS setup_induction) 1); |
|
166 by (etac uterm.induct 1); |
|
167 by (ALLGOALS (fast_tac uterm_cs)); |
|
168 qed "VAR_D"; |
|
169 |
|
170 val [major] = goal UTerm.thy "CONST(M): uterm(A) ==> M : A"; |
|
171 by (rtac (major RS setup_induction) 1); |
|
172 by (etac uterm.induct 1); |
|
173 by (ALLGOALS (fast_tac uterm_cs)); |
|
174 qed "CONST_D"; |
|
175 |
|
176 val [major] = goal UTerm.thy |
|
177 "COMB M N: uterm(A) ==> M: uterm(A) & N: uterm(A)"; |
|
178 by (rtac (major RS setup_induction) 1); |
|
179 by (etac uterm.induct 1); |
|
180 by (ALLGOALS (fast_tac uterm_cs)); |
|
181 qed "COMB_D"; |
|
182 |
|
183 (*Basic ss with constructors and their freeness*) |
|
184 Addsimps (uterm.intrs @ |
|
185 [Const_not_Comb,Comb_not_Var,Var_not_Const, |
|
186 Comb_not_Const,Var_not_Comb,Const_not_Var, |
|
187 Var_Var_eq,Const_Const_eq,Comb_Comb_eq, |
|
188 CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, |
|
189 COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, |
|
190 VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq]); |
|
191 |
|
192 goal UTerm.thy "!u. t~=Comb t u"; |
|
193 by (uterm_ind_tac "t" 1); |
|
194 by (rtac (Var_not_Comb RS allI) 1); |
|
195 by (rtac (Const_not_Comb RS allI) 1); |
|
196 by (Asm_simp_tac 1); |
44 by (Asm_simp_tac 1); |
197 qed "t_not_Comb_t"; |
45 val finite_vars_of = result(); |
198 |
|
199 goal UTerm.thy "!t. u~=Comb t u"; |
|
200 by (uterm_ind_tac "u" 1); |
|
201 by (rtac (Var_not_Comb RS allI) 1); |
|
202 by (rtac (Const_not_Comb RS allI) 1); |
|
203 by (Asm_simp_tac 1); |
|
204 qed "u_not_Comb_u"; |
|
205 |
|
206 |
|
207 (*** UTerm_rec -- by wf recursion on pred_sexp ***) |
|
208 |
|
209 goal UTerm.thy |
|
210 "(%M. UTerm_rec M b c d) = wfrec (trancl pred_sexp) \ |
|
211 \ (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y)))))"; |
|
212 by (simp_tac (HOL_ss addsimps [UTerm_rec_def]) 1); |
|
213 bind_thm("UTerm_rec_unfold", (wf_pred_sexp RS wf_trancl) RS |
|
214 ((result() RS eq_reflection) RS def_wfrec)); |
|
215 |
|
216 (*--------------------------------------------------------------------------- |
|
217 * Old: |
|
218 * val UTerm_rec_unfold = |
|
219 * [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec; |
|
220 *---------------------------------------------------------------------------*) |
|
221 |
|
222 (** conversion rules **) |
|
223 |
|
224 goalw UTerm.thy [VAR_def] "UTerm_rec (VAR x) b c d = b(x)"; |
|
225 by (rtac (UTerm_rec_unfold RS trans) 1); |
|
226 by (simp_tac (!simpset addsimps [Case_In0]) 1); |
|
227 qed "UTerm_rec_VAR"; |
|
228 |
|
229 goalw UTerm.thy [CONST_def] "UTerm_rec (CONST x) b c d = c(x)"; |
|
230 by (rtac (UTerm_rec_unfold RS trans) 1); |
|
231 by (simp_tac (!simpset addsimps [Case_In0,Case_In1]) 1); |
|
232 qed "UTerm_rec_CONST"; |
|
233 |
|
234 goalw UTerm.thy [COMB_def] |
|
235 "!!M N. [| M: sexp; N: sexp |] ==> \ |
|
236 \ UTerm_rec (COMB M N) b c d = \ |
|
237 \ d M N (UTerm_rec M b c d) (UTerm_rec N b c d)"; |
|
238 by (rtac (UTerm_rec_unfold RS trans) 1); |
|
239 by (simp_tac (!simpset addsimps [Split,Case_In1]) 1); |
|
240 by (asm_simp_tac (!simpset addsimps [In1_def]) 1); |
|
241 qed "UTerm_rec_COMB"; |
|
242 |
|
243 (*** uterm_rec -- by UTerm_rec ***) |
|
244 |
|
245 val Rep_uterm_in_sexp = |
|
246 Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD); |
|
247 |
|
248 Addsimps [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, |
|
249 Abs_uterm_inverse, Rep_uterm_inverse, |
|
250 Rep_uterm, rangeI, inj_Leaf, inv_f_f, Rep_uterm_in_sexp]; |
|
251 |
|
252 goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)"; |
|
253 by (Simp_tac 1); |
|
254 qed "uterm_rec_Var"; |
|
255 |
|
256 goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec (Const x) b c d = c(x)"; |
|
257 by (Simp_tac 1); |
|
258 qed "uterm_rec_Const"; |
|
259 |
|
260 goalw UTerm.thy [uterm_rec_def, Comb_def] |
|
261 "uterm_rec (Comb u v) b c d = d u v (uterm_rec u b c d) (uterm_rec v b c d)"; |
|
262 by (Simp_tac 1); |
|
263 qed "uterm_rec_Comb"; |
|
264 |
|
265 Addsimps [uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb]; |
|
266 |
|
267 |
|
268 (**********) |
|
269 |
|
270 val uterm_rews = [t_not_Comb_t,u_not_Comb_u]; |
|