178 by (etac uterm.induct 1); |
179 by (etac uterm.induct 1); |
179 by (ALLGOALS (fast_tac uterm_cs)); |
180 by (ALLGOALS (fast_tac uterm_cs)); |
180 qed "COMB_D"; |
181 qed "COMB_D"; |
181 |
182 |
182 (*Basic ss with constructors and their freeness*) |
183 (*Basic ss with constructors and their freeness*) |
183 val uterm_free_simps = uterm.intrs @ |
184 Addsimps (uterm.intrs @ |
184 [Const_not_Comb,Comb_not_Var,Var_not_Const, |
185 [Const_not_Comb,Comb_not_Var,Var_not_Const, |
185 Comb_not_Const,Var_not_Comb,Const_not_Var, |
186 Comb_not_Const,Var_not_Comb,Const_not_Var, |
186 Var_Var_eq,Const_Const_eq,Comb_Comb_eq, |
187 Var_Var_eq,Const_Const_eq,Comb_Comb_eq, |
187 CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, |
188 CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, |
188 COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, |
189 COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, |
189 VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq]; |
190 VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq]); |
190 val uterm_free_ss = HOL_ss addsimps uterm_free_simps; |
|
191 |
191 |
192 goal UTerm.thy "!u. t~=Comb t u"; |
192 goal UTerm.thy "!u. t~=Comb t u"; |
193 by (uterm_ind_tac "t" 1); |
193 by (uterm_ind_tac "t" 1); |
194 by (rtac (Var_not_Comb RS allI) 1); |
194 by (rtac (Var_not_Comb RS allI) 1); |
195 by (rtac (Const_not_Comb RS allI) 1); |
195 by (rtac (Const_not_Comb RS allI) 1); |
196 by (asm_simp_tac uterm_free_ss 1); |
196 by (Asm_simp_tac 1); |
197 qed "t_not_Comb_t"; |
197 qed "t_not_Comb_t"; |
198 |
198 |
199 goal UTerm.thy "!t. u~=Comb t u"; |
199 goal UTerm.thy "!t. u~=Comb t u"; |
200 by (uterm_ind_tac "u" 1); |
200 by (uterm_ind_tac "u" 1); |
201 by (rtac (Var_not_Comb RS allI) 1); |
201 by (rtac (Var_not_Comb RS allI) 1); |
202 by (rtac (Const_not_Comb RS allI) 1); |
202 by (rtac (Const_not_Comb RS allI) 1); |
203 by (asm_simp_tac uterm_free_ss 1); |
203 by (Asm_simp_tac 1); |
204 qed "u_not_Comb_u"; |
204 qed "u_not_Comb_u"; |
205 |
205 |
206 |
206 |
207 (*** UTerm_rec -- by wf recursion on pred_sexp ***) |
207 (*** UTerm_rec -- by wf recursion on pred_sexp ***) |
208 |
208 |
211 |
211 |
212 (** conversion rules **) |
212 (** conversion rules **) |
213 |
213 |
214 goalw UTerm.thy [VAR_def] "UTerm_rec (VAR x) b c d = b(x)"; |
214 goalw UTerm.thy [VAR_def] "UTerm_rec (VAR x) b c d = b(x)"; |
215 by (rtac (UTerm_rec_unfold RS trans) 1); |
215 by (rtac (UTerm_rec_unfold RS trans) 1); |
216 by (simp_tac (HOL_ss addsimps [Case_In0]) 1); |
216 by (simp_tac (!simpset addsimps [Case_In0]) 1); |
217 qed "UTerm_rec_VAR"; |
217 qed "UTerm_rec_VAR"; |
218 |
218 |
219 goalw UTerm.thy [CONST_def] "UTerm_rec (CONST x) b c d = c(x)"; |
219 goalw UTerm.thy [CONST_def] "UTerm_rec (CONST x) b c d = c(x)"; |
220 by (rtac (UTerm_rec_unfold RS trans) 1); |
220 by (rtac (UTerm_rec_unfold RS trans) 1); |
221 by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1); |
221 by (simp_tac (!simpset addsimps [Case_In0,Case_In1]) 1); |
222 qed "UTerm_rec_CONST"; |
222 qed "UTerm_rec_CONST"; |
223 |
223 |
224 goalw UTerm.thy [COMB_def] |
224 goalw UTerm.thy [COMB_def] |
225 "!!M N. [| M: sexp; N: sexp |] ==> \ |
225 "!!M N. [| M: sexp; N: sexp |] ==> \ |
226 \ UTerm_rec (COMB M N) b c d = \ |
226 \ UTerm_rec (COMB M N) b c d = \ |
227 \ d M N (UTerm_rec M b c d) (UTerm_rec N b c d)"; |
227 \ d M N (UTerm_rec M b c d) (UTerm_rec N b c d)"; |
228 by (rtac (UTerm_rec_unfold RS trans) 1); |
228 by (rtac (UTerm_rec_unfold RS trans) 1); |
229 by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); |
229 by (simp_tac (!simpset addsimps [Split,Case_In1]) 1); |
230 by (asm_simp_tac (pred_sexp_ss addsimps [In1_def]) 1); |
230 by (asm_simp_tac (!simpset addsimps [In1_def]) 1); |
231 qed "UTerm_rec_COMB"; |
231 qed "UTerm_rec_COMB"; |
232 |
232 |
233 (*** uterm_rec -- by UTerm_rec ***) |
233 (*** uterm_rec -- by UTerm_rec ***) |
234 |
234 |
235 val Rep_uterm_in_sexp = |
235 val Rep_uterm_in_sexp = |
236 Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD); |
236 Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD); |
237 |
237 |
238 val uterm_rec_simps = |
238 Addsimps [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, |
239 uterm.intrs @ |
239 Abs_uterm_inverse, Rep_uterm_inverse, |
240 [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, |
240 Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp]; |
241 Abs_uterm_inverse, Rep_uterm_inverse, |
|
242 Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp]; |
|
243 val uterm_rec_ss = HOL_ss addsimps uterm_rec_simps; |
|
244 |
241 |
245 goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)"; |
242 goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)"; |
246 by (simp_tac uterm_rec_ss 1); |
243 by (Simp_tac 1); |
247 qed "uterm_rec_Var"; |
244 qed "uterm_rec_Var"; |
248 |
245 |
249 goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec (Const x) b c d = c(x)"; |
246 goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec (Const x) b c d = c(x)"; |
250 by (simp_tac uterm_rec_ss 1); |
247 by (Simp_tac 1); |
251 qed "uterm_rec_Const"; |
248 qed "uterm_rec_Const"; |
252 |
249 |
253 goalw UTerm.thy [uterm_rec_def, Comb_def] |
250 goalw UTerm.thy [uterm_rec_def, Comb_def] |
254 "uterm_rec (Comb u v) b c d = d u v (uterm_rec u b c d) (uterm_rec v b c d)"; |
251 "uterm_rec (Comb u v) b c d = d u v (uterm_rec u b c d) (uterm_rec v b c d)"; |
255 by (simp_tac uterm_rec_ss 1); |
252 by (Simp_tac 1); |
256 qed "uterm_rec_Comb"; |
253 qed "uterm_rec_Comb"; |
257 |
254 |
258 val uterm_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, |
255 Addsimps [uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb]; |
259 uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb]; |
|
260 val uterm_ss = uterm_free_ss addsimps uterm_simps; |
|
261 |
256 |
262 |
257 |
263 (**********) |
258 (**********) |
264 |
259 |
265 val uterm_rews = [uterm_rec_Var,uterm_rec_Const,uterm_rec_Comb, |
260 val uterm_rews = [t_not_Comb_t,u_not_Comb_u]; |
266 t_not_Comb_t,u_not_Comb_u, |
|
267 Const_not_Comb,Comb_not_Var,Var_not_Const, |
|
268 Comb_not_Const,Var_not_Comb,Const_not_Var, |
|
269 Var_Var_eq,Const_Const_eq,Comb_Comb_eq]; |
|
270 |
|