diff -r 6630488bbe44 -r 872f866e630f Subst/UTerm.ML --- a/Subst/UTerm.ML Mon Aug 22 12:00:02 1994 +0200 +++ b/Subst/UTerm.ML Wed Aug 24 18:49:29 1994 +0200 @@ -2,56 +2,48 @@ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -For uterm.thy. +Simple term structure for unifiation. +Binary trees with leaves that are constants or variables. *) open UTerm; +val uterm_con_defs = [VAR_def, CONST_def, COMB_def]; + +goal UTerm.thy "uterm(A) = A <+> A <+> (uterm(A) <*> uterm(A))"; +let val rew = rewrite_rule uterm_con_defs in +by (fast_tac (univ_cs addSIs (equalityI :: map rew uterm.intrs) + addEs [rew uterm.elim]) 1) +end; +val uterm_unfold = result(); + (** the uterm functional **) -goal UTerm.thy "mono(%Z. A <+> A <+> Z <*> Z)"; -by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono] 1)); -val UTerm_fun_mono = result(); +(*This justifies using uterm in other recursive type definitions*) +goalw UTerm.thy uterm.defs "!!A B. A<=B ==> uterm(A) <= uterm(B)"; +by (REPEAT (ares_tac (lfp_mono::basic_monos) 1)); +val uterm_mono = result(); -val UTerm_unfold = UTerm_fun_mono RS (UTerm_def RS def_lfp_Tarski); +(** Type checking rules -- uterm creates well-founded sets **) -(*This justifies using UTerm in other recursive type definitions*) -val prems = goalw UTerm.thy [UTerm_def] "[| A<=B |] ==> UTerm(A) <= UTerm(B)"; -by (REPEAT (ares_tac (prems@[monoI, subset_refl, lfp_mono, - usum_mono, uprod_mono]) 1)); -val UTerm_mono = result(); - -(** Type checking rules -- UTerm creates well-founded sets **) +goalw UTerm.thy (uterm_con_defs @ uterm.defs) "uterm(sexp) <= sexp"; +by (rtac lfp_lowerbound 1); +by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1); +val uterm_sexp = result(); -val prems = goalw UTerm.thy [UTerm_def] "UTerm(Sexp) <= Sexp"; -by (rtac lfp_lowerbound 1); -by (fast_tac (univ_cs addIs [Sexp_In0I,Sexp_In1I,Sexp_SconsI]) 1); -val UTerm_Sexp = result(); - -(* A <= Sexp ==> UTerm(A) <= Sexp *) -val UTerm_subset_Sexp = standard - (UTerm_mono RS (UTerm_Sexp RSN (2,subset_trans))); +(* A <= sexp ==> uterm(A) <= sexp *) +val uterm_subset_sexp = standard ([uterm_mono, uterm_sexp] MRS subset_trans); (** Induction **) -(*Induction for the set UTerm(A) *) -val major::prems = goalw UTerm.thy [VAR_def,CONST_def,COMB_def] - "[| M: UTerm(A); !!M.M : A ==> P(VAR(M)); !!M.M : A ==> P(CONST(M)); \ -\ !!M N. [| M: UTerm(A); N: UTerm(A); P(M); P(N) |] ==> P(COMB(M,N)) |] \ -\ ==> P(M)"; -by (rtac (major RS (UTerm_def RS def_induct)) 1); -by (rtac UTerm_fun_mono 1); -by (fast_tac (set_cs addIs prems addEs [usumE,uprodE]) 1); -val UTerm_induct = result(); - (*Induction for the type 'a uterm *) val prems = goalw UTerm.thy [Var_def,Const_def,Comb_def] "[| !!x.P(Var(x)); !!x.P(Const(x)); \ \ !!u v. [| P(u); P(v) |] ==> P(Comb(u,v)) |] ==> P(t)"; -by (rtac (Rep_UTerm_inverse RS subst) 1); (*types force good instantiation*) -by (rtac (Rep_UTerm RS UTerm_induct) 1); +by (rtac (Rep_uterm_inverse RS subst) 1); (*types force good instantiation*) +by (rtac (Rep_uterm RS uterm.induct) 1); by (REPEAT (ares_tac prems 1 - ORELSE eresolve_tac [rangeE, ssubst, Abs_UTerm_inverse RS subst] 1)); + ORELSE eresolve_tac [rangeE, ssubst, Abs_uterm_inverse RS subst] 1)); val uterm_induct = result(); (*Perform induction on xs. *) @@ -59,40 +51,22 @@ EVERY [res_inst_tac [("t",a)] uterm_induct M, rename_last_tac a ["1"] (M+1)]; -(** Introduction rules for UTerm constructors **) - -(* c : A <+> A <+> UTerm(A) <*> UTerm(A) ==> c : UTerm(A) *) -val UTermI = UTerm_unfold RS equalityD2 RS subsetD; - -(* Nil is a UTerm -- this also justifies the type definition*) -val prems = goalw UTerm.thy [VAR_def] "v:A ==> VAR(v) : UTerm(A)"; -by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I]@prems) 1)); -val VAR_I = result(); - -val prems = goalw UTerm.thy [CONST_def] "c:A ==> CONST(c) : UTerm(A)"; -by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I, usum_In1I]@prems) 1)); -val CONST_I = result(); - -val prems = goalw UTerm.thy [COMB_def] - "[| M:UTerm(A); N:UTerm(A) |] ==> COMB(M,N) : UTerm(A)"; -by (REPEAT (resolve_tac (prems@[UTermI, uprodI, usum_In1I]) 1)); -val COMB_I = result(); (*** Isomorphisms ***) -goal UTerm.thy "inj(Rep_UTerm)"; +goal UTerm.thy "inj(Rep_uterm)"; by (rtac inj_inverseI 1); -by (rtac Rep_UTerm_inverse 1); -val inj_Rep_UTerm = result(); +by (rtac Rep_uterm_inverse 1); +val inj_Rep_uterm = result(); -goal UTerm.thy "inj_onto(Abs_UTerm,UTerm(range(Leaf)))"; +goal UTerm.thy "inj_onto(Abs_uterm,uterm(range(Leaf)))"; by (rtac inj_onto_inverseI 1); -by (etac Abs_UTerm_inverse 1); -val inj_onto_Abs_UTerm = result(); +by (etac Abs_uterm_inverse 1); +val inj_onto_Abs_uterm = result(); (** Distinctness of constructors **) -goalw UTerm.thy [CONST_def,COMB_def] "~ CONST(c) = COMB(u,v)"; +goalw UTerm.thy uterm_con_defs "~ CONST(c) = COMB(u,v)"; by (rtac notI 1); by (etac (In1_inject RS (In0_not_In1 RS notE)) 1); val CONST_not_COMB = result(); @@ -100,14 +74,14 @@ val CONST_neq_COMB = standard (CONST_not_COMB RS notE); val COMB_neq_CONST = sym RS CONST_neq_COMB; -goalw UTerm.thy [COMB_def,VAR_def] "~ COMB(u,v) = VAR(x)"; +goalw UTerm.thy uterm_con_defs "~ COMB(u,v) = VAR(x)"; by (rtac In1_not_In0 1); val COMB_not_VAR = result(); val VAR_not_COMB = standard (COMB_not_VAR RS not_sym); val COMB_neq_VAR = standard (COMB_not_VAR RS notE); val VAR_neq_COMB = sym RS COMB_neq_VAR; -goalw UTerm.thy [VAR_def,CONST_def] "~ VAR(x) = CONST(c)"; +goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)"; by (rtac In0_not_In1 1); val VAR_not_CONST = result(); val CONST_not_VAR = standard (VAR_not_CONST RS not_sym); @@ -116,24 +90,24 @@ goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb(u,v)"; -by (rtac (CONST_not_COMB RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1); -by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1)); +by (rtac (CONST_not_COMB RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1); +by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1)); val Const_not_Comb = result(); val Comb_not_Const = standard (Const_not_Comb RS not_sym); val Const_neq_Comb = standard (Const_not_Comb RS notE); val Comb_neq_Const = sym RS Const_neq_Comb; goalw UTerm.thy [Comb_def,Var_def] "~ Comb(u,v) = Var(x)"; -by (rtac (COMB_not_VAR RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1); -by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1)); +by (rtac (COMB_not_VAR RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1); +by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1)); val Comb_not_Var = result(); val Var_not_Comb = standard (Comb_not_Var RS not_sym); val Comb_neq_Var = standard (Comb_not_Var RS notE); val Var_neq_Comb = sym RS Comb_neq_Var; goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)"; -by (rtac (VAR_not_CONST RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1); -by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1)); +by (rtac (VAR_not_CONST RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1); +by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1)); val Var_not_Const = result(); val Const_not_Var = standard (Var_not_Const RS not_sym); val Var_neq_Const = standard (Var_not_Const RS notE); @@ -163,66 +137,66 @@ (*For reasoning about abstract uterm constructors*) -val UTerm_cs = set_cs addIs [Rep_UTerm, VAR_I, CONST_I, COMB_I] - addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST, - COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR, - COMB_inject] - addSDs [VAR_inject,CONST_inject, - inj_onto_Abs_UTerm RS inj_ontoD, - inj_Rep_UTerm RS injD, Leaf_inject]; +val uterm_cs = set_cs addIs uterm.intrs @ [Rep_uterm] + addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST, + COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR, + COMB_inject] + addSDs [VAR_inject,CONST_inject, + inj_onto_Abs_uterm RS inj_ontoD, + inj_Rep_uterm RS injD, Leaf_inject]; goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)"; -by (fast_tac UTerm_cs 1); +by (fast_tac uterm_cs 1); val Var_Var_eq = result(); val Var_inject = standard (Var_Var_eq RS iffD1); goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)"; -by (fast_tac UTerm_cs 1); +by (fast_tac uterm_cs 1); val Const_Const_eq = result(); val Const_inject = standard (Const_Const_eq RS iffD1); goalw UTerm.thy [Comb_def] "(Comb(u,v)=Comb(x,y)) = (u=x & v=y)"; -by (fast_tac UTerm_cs 1); +by (fast_tac uterm_cs 1); val Comb_Comb_eq = result(); val Comb_inject = standard (Comb_Comb_eq RS iffD1 RS conjE); -val [major] = goal UTerm.thy "VAR(M): UTerm(A) ==> M : A"; +val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A"; by (rtac (major RS setup_induction) 1); -by (etac UTerm_induct 1); -by (ALLGOALS (fast_tac UTerm_cs)); +by (etac uterm.induct 1); +by (ALLGOALS (fast_tac uterm_cs)); val VAR_D = result(); -val [major] = goal UTerm.thy "CONST(M): UTerm(A) ==> M : A"; +val [major] = goal UTerm.thy "CONST(M): uterm(A) ==> M : A"; by (rtac (major RS setup_induction) 1); -by (etac UTerm_induct 1); -by (ALLGOALS (fast_tac UTerm_cs)); +by (etac uterm.induct 1); +by (ALLGOALS (fast_tac uterm_cs)); val CONST_D = result(); val [major] = goal UTerm.thy - "COMB(M,N): UTerm(A) ==> M: UTerm(A) & N: UTerm(A)"; + "COMB(M,N): uterm(A) ==> M: uterm(A) & N: uterm(A)"; by (rtac (major RS setup_induction) 1); -by (etac UTerm_induct 1); -by (ALLGOALS (fast_tac UTerm_cs)); +by (etac uterm.induct 1); +by (ALLGOALS (fast_tac uterm_cs)); val COMB_D = result(); (*Basic ss with constructors and their freeness*) -val uterm_free_simps = [Const_not_Comb,Comb_not_Var,Var_not_Const, - Comb_not_Const,Var_not_Comb,Const_not_Var, - Var_Var_eq,Const_Const_eq,Comb_Comb_eq, - CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, - COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, - VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq, - VAR_I, CONST_I, COMB_I]; +val uterm_free_simps = uterm.intrs @ + [Const_not_Comb,Comb_not_Var,Var_not_Const, + Comb_not_Const,Var_not_Comb,Const_not_Var, + Var_Var_eq,Const_Const_eq,Comb_Comb_eq, + CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, + COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, + VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq]; val uterm_free_ss = HOL_ss addsimps uterm_free_simps; -goal UTerm.thy "!u. ~(t=Comb(t,u))"; +goal UTerm.thy "!u. t~=Comb(t,u)"; by (uterm_ind_tac "t" 1); by (rtac (Var_not_Comb RS allI) 1); by (rtac (Const_not_Comb RS allI) 1); by (asm_simp_tac uterm_free_ss 1); val t_not_Comb_t = result(); -goal UTerm.thy "!t. ~(u=Comb(t,u))"; +goal UTerm.thy "!t. u~=Comb(t,u)"; by (uterm_ind_tac "u" 1); by (rtac (Var_not_Comb RS allI) 1); by (rtac (Const_not_Comb RS allI) 1); @@ -230,16 +204,16 @@ val u_not_Comb_u = result(); -(*** UTerm_rec -- by wf recursion on pred_Sexp ***) +(*** UTerm_rec -- by wf recursion on pred_sexp ***) val UTerm_rec_unfold = - wf_pred_Sexp RS wf_trancl RS (UTerm_rec_def RS def_wfrec); + [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec; (** conversion rules **) goalw UTerm.thy [VAR_def] "UTerm_rec(VAR(x),b,c,d) = b(x)"; by (rtac (UTerm_rec_unfold RS trans) 1); -by (rtac Case_In0 1); +by (simp_tac (HOL_ss addsimps [Case_In0]) 1); val UTerm_rec_VAR = result(); goalw UTerm.thy [CONST_def] "UTerm_rec(CONST(x),b,c,d) = c(x)"; @@ -247,23 +221,25 @@ by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1); val UTerm_rec_CONST = result(); -val prems = goalw UTerm.thy [COMB_def] - "[| M: Sexp; N: Sexp |] ==> \ -\ UTerm_rec(COMB(M,N), b, c, d) = \ -\ d(M, N, UTerm_rec(M,b,c,d), UTerm_rec(N,b,c,d))"; +goalw UTerm.thy [COMB_def] + "!!M N. [| M: sexp; N: sexp |] ==> \ +\ UTerm_rec(COMB(M,N), b, c, d) = \ +\ d(M, N, UTerm_rec(M,b,c,d), UTerm_rec(N,b,c,d))"; by (rtac (UTerm_rec_unfold RS trans) 1); by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); -by (simp_tac (pred_Sexp_ss addsimps (In1_def::prems)) 1); +by (asm_simp_tac (pred_sexp_ss addsimps [In1_def]) 1); val UTerm_rec_COMB = result(); (*** uterm_rec -- by UTerm_rec ***) -val Rep_UTerm_in_Sexp = - Rep_UTerm RS (range_Leaf_subset_Sexp RS UTerm_subset_Sexp RS subsetD); +val Rep_uterm_in_sexp = + Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD); -val uterm_rec_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, - Abs_UTerm_inverse, Rep_UTerm_inverse, VAR_I, CONST_I, COMB_I, - Rep_UTerm, rangeI, inj_Leaf, Inv_f_f, Rep_UTerm_in_Sexp]; +val uterm_rec_simps = + uterm.intrs @ + [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, + Abs_uterm_inverse, Rep_uterm_inverse, + Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp]; val uterm_rec_ss = HOL_ss addsimps uterm_rec_simps; goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec(Var(x),b,c,d) = b(x)"; @@ -283,22 +259,6 @@ uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb]; val uterm_ss = uterm_free_ss addsimps uterm_simps; -(*Type checking. Useful?*) -val major::A_subset_Sexp::prems = goal UTerm.thy - "[| M: UTerm(A); \ -\ A<=Sexp; \ -\ !!x.x:A ==> b(x): C(VAR(x)); \ -\ !!x.x:A ==> c(x): C(CONST(x)); \ -\ !!x y q r. [| x: UTerm(A); y: UTerm(A); q: C(x); r: C(y) |] ==> \ -\ d(x,y,q,r): C(COMB(x,y)) \ -\ |] ==> UTerm_rec(M,b,c,d) : C(M)"; -val Sexp_UTermA_I = A_subset_Sexp RS UTerm_subset_Sexp RS subsetD; -val Sexp_A_I = A_subset_Sexp RS subsetD; -by (rtac (major RS UTerm_induct) 1); -by (ALLGOALS - (asm_simp_tac (uterm_ss addsimps ([Sexp_A_I,Sexp_UTermA_I] @ prems)))); -val UTerm_rec_type = result(); - (**********) @@ -308,13 +268,3 @@ Comb_not_Const,Var_not_Comb,Const_not_Var, Var_Var_eq,Const_Const_eq,Comb_Comb_eq]; -(* -val prems = goal Subst.thy - "[| !!x.P(Var(x)); !!x.P(Const(x)); \ -\ !!u v. P(u) --> P(v) --> P(Comb(u,v)) |] ==> P(a)"; -by (uterm_ind_tac "a" 1); -by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs)); -val uterm_induct2 = result(); - -add_inds uterm_induct2; -*)