diff -r 4d0545e93c0d -r c533bc92e882 Subst/UTerm.ML --- a/Subst/UTerm.ML Wed Dec 14 10:32:07 1994 +0100 +++ b/Subst/UTerm.ML Wed Dec 14 11:17:18 1994 +0100 @@ -32,7 +32,7 @@ qed "uterm_sexp"; (* A <= sexp ==> uterm(A) <= sexp *) -val uterm_subset_sexp = standard ([uterm_mono, uterm_sexp] MRS subset_trans); +bind_thm ("uterm_subset_sexp", ([uterm_mono, uterm_sexp] MRS subset_trans)); (** Induction **) @@ -70,22 +70,22 @@ by (rtac notI 1); by (etac (In1_inject RS (In0_not_In1 RS notE)) 1); qed "CONST_not_COMB"; -val COMB_not_CONST = standard (CONST_not_COMB RS not_sym); -val CONST_neq_COMB = standard (CONST_not_COMB RS notE); +bind_thm ("COMB_not_CONST", (CONST_not_COMB RS not_sym)); +bind_thm ("CONST_neq_COMB", (CONST_not_COMB RS notE)); val COMB_neq_CONST = sym RS CONST_neq_COMB; goalw UTerm.thy uterm_con_defs "~ COMB(u,v) = VAR(x)"; by (rtac In1_not_In0 1); qed "COMB_not_VAR"; -val VAR_not_COMB = standard (COMB_not_VAR RS not_sym); -val COMB_neq_VAR = standard (COMB_not_VAR RS notE); +bind_thm ("VAR_not_COMB", (COMB_not_VAR RS not_sym)); +bind_thm ("COMB_neq_VAR", (COMB_not_VAR RS notE)); val VAR_neq_COMB = sym RS COMB_neq_VAR; goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)"; by (rtac In0_not_In1 1); qed "VAR_not_CONST"; -val CONST_not_VAR = standard (VAR_not_CONST RS not_sym); -val VAR_neq_CONST = standard (VAR_not_CONST RS notE); +bind_thm ("CONST_not_VAR", (VAR_not_CONST RS not_sym)); +bind_thm ("VAR_neq_CONST", (VAR_not_CONST RS notE)); val CONST_neq_VAR = sym RS VAR_neq_CONST; @@ -93,24 +93,24 @@ 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)); qed "Const_not_Comb"; -val Comb_not_Const = standard (Const_not_Comb RS not_sym); -val Const_neq_Comb = standard (Const_not_Comb RS notE); +bind_thm ("Comb_not_Const", (Const_not_Comb RS not_sym)); +bind_thm ("Const_neq_Comb", (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 (uterm.intrs @ [rangeI, Rep_uterm]) 1)); qed "Comb_not_Var"; -val Var_not_Comb = standard (Comb_not_Var RS not_sym); -val Comb_neq_Var = standard (Comb_not_Var RS notE); +bind_thm ("Var_not_Comb", (Comb_not_Var RS not_sym)); +bind_thm ("Comb_neq_Var", (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 (uterm.intrs @ [rangeI, Rep_uterm]) 1)); qed "Var_not_Const"; -val Const_not_Var = standard (Var_not_Const RS not_sym); -val Var_neq_Const = standard (Var_not_Const RS notE); +bind_thm ("Const_not_Var", (Var_not_Const RS not_sym)); +bind_thm ("Var_neq_Const", (Var_not_Const RS notE)); val Const_neq_Var = sym RS Var_neq_Const; @@ -131,9 +131,9 @@ by (fast_tac inject_cs 1); qed "COMB_COMB_eq"; -val VAR_inject = standard (VAR_VAR_eq RS iffD1); -val CONST_inject = standard (CONST_CONST_eq RS iffD1); -val COMB_inject = standard (COMB_COMB_eq RS iffD1 RS conjE); +bind_thm ("VAR_inject", (VAR_VAR_eq RS iffD1)); +bind_thm ("CONST_inject", (CONST_CONST_eq RS iffD1)); +bind_thm ("COMB_inject", (COMB_COMB_eq RS iffD1 RS conjE)); (*For reasoning about abstract uterm constructors*) @@ -148,17 +148,17 @@ goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)"; by (fast_tac uterm_cs 1); qed "Var_Var_eq"; -val Var_inject = standard (Var_Var_eq RS iffD1); +bind_thm ("Var_inject", (Var_Var_eq RS iffD1)); goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)"; by (fast_tac uterm_cs 1); qed "Const_Const_eq"; -val Const_inject = standard (Const_Const_eq RS iffD1); +bind_thm ("Const_inject", (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); qed "Comb_Comb_eq"; -val Comb_inject = standard (Comb_Comb_eq RS iffD1 RS conjE); +bind_thm ("Comb_inject", (Comb_Comb_eq RS iffD1 RS conjE)); val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A"; by (rtac (major RS setup_induction) 1);