Subst/Subst.ML

--- a/Subst/Subst.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/Subst/Subst.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -34,12 +34,12 @@
 goal Subst.thy "t <| Nil = t";
 by (uterm_ind_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
-val subst_Nil = result();
+qed "subst_Nil";
 
 goal Subst.thy "t <: u --> t <| s <: u <| s";
 by (uterm_ind_tac "u" 1);
 by (ALLGOALS (asm_simp_tac subst_ss));
-val subst_mono = result() RS mp;
+val subst_mono  = store_thm("subst_mono", result() RS mp);
 
 goal Subst.thy  "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
 by (imp_excluded_middle_tac "t = Var(v)" 1);
@@ -48,7 +48,7 @@
     uterm_induct 2);
 by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
 by (fast_tac HOL_cs 1);
-val Var_not_occs = result() RS mp;
+val Var_not_occs  = store_thm("Var_not_occs", result() RS mp);
 
 goal Subst.thy
     "(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
@@ -56,24 +56,24 @@
 by (REPEAT (etac rev_mp 3));
 by (ALLGOALS (asm_simp_tac subst_ss));
 by (ALLGOALS (fast_tac HOL_cs));
-val agreement = result();
+qed "agreement";
 
 goal Subst.thy   "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
 by(simp_tac(subst_ss addsimps [agreement,Var_subst]
                      setloop (split_tac [expand_if])) 1);
-val repl_invariance = result() RS mp;
+val repl_invariance  = store_thm("repl_invariance", result() RS mp);
 
 val asms = goal Subst.thy 
      "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
 by (uterm_ind_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
-val Var_in_subst = result() RS mp;
+val Var_in_subst  = store_thm("Var_in_subst", result() RS mp);
 
 (**** Equality between Substitutions ****)
 
 goalw Subst.thy [subst_eq_def] "r =s= s = (! t.t <| r = t <| s)";
 by (simp_tac subst_ss 1);
-val subst_eq_iff = result();
+qed "subst_eq_iff";
 
 local fun mk_thm s = prove_goal Subst.thy s
                   (fn prems => [cut_facts_tac prems 1,
@@ -89,7 +89,7 @@
     "[| r =s= s; P(t <| r,u <| r) |] ==> P(t <| s,u <| s)";
 by (resolve_tac [eq RS spec RS subst] 1);
 by (resolve_tac (prems RL [eq RS spec RS subst]) 1);
-val subst_subst2 = result();
+qed "subst_subst2";
 
 val ssubst_subst2 = subst_sym RS subst_subst2;
 
@@ -98,7 +98,7 @@
 goal Subst.thy "s <> Nil = s";
 by (alist_ind_tac "s" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [subst_Nil])));
-val comp_Nil = result();
+qed "comp_Nil";
 
 goal Subst.thy "(t <| r <> s) = (t <| r <| s)";
 by (uterm_ind_tac "t" 1);
@@ -106,11 +106,11 @@
 by (alist_ind_tac "r" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst,subst_Nil]
                                      setloop (split_tac [expand_if]))));
-val subst_comp = result();
+qed "subst_comp";
 
 goal Subst.thy "q <> r <> s =s= q <> (r <> s)";
 by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
-val comp_assoc = result();
+qed "comp_assoc";
 
 goal Subst.thy "<w,Var(w) <| s>#s =s= s"; 
 by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
@@ -118,12 +118,12 @@
 by (REPEAT (etac rev_mp 3));
 by (ALLGOALS (simp_tac (subst_ss addsimps[Var_subst]
                                  setloop (split_tac [expand_if]))));
-val Cons_trivial = result();
+qed "Cons_trivial";
 
 val [prem] = goal Subst.thy "q <> r =s= s ==>  t <| q <| r = t <| s";
 by (simp_tac (subst_ss addsimps [prem RS (subst_eq_iff RS iffD1),
 				subst_comp RS sym]) 1);
-val comp_subst_subst = result();
+qed "comp_subst_subst";
 
 (****  Domain and range of Substitutions ****)
 
@@ -132,31 +132,31 @@
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst]
                             setloop (split_tac[expand_if]))));
 by (fast_tac HOL_cs 1);
-val sdom_iff = result();
+qed "sdom_iff";
 
 goalw Subst.thy [srange_def]  
    "v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
 by (fast_tac set_cs 1);
-val srange_iff = result();
+qed "srange_iff";
 
 goal Subst.thy  "(t <| s = t) = (sdom(s) Int vars_of(t) = {})";
 by (uterm_ind_tac "t" 1);
 by (REPEAT (etac rev_mp 3));
 by (ALLGOALS (simp_tac (subst_ss addsimps [sdom_iff,Var_subst])));
 by (ALLGOALS (fast_tac set_cs));
-val invariance = result();
+qed "invariance";
 
 goal Subst.thy  "v : sdom(s) -->  ~v : srange(s) --> ~v : vars_of(t <| s)";
 by (uterm_ind_tac "t" 1);
 by (imp_excluded_middle_tac "x : sdom(s)" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [sdom_iff,srange_iff])));
 by (ALLGOALS (fast_tac set_cs));
-val Var_elim = result() RS mp RS mp;
+val Var_elim  = store_thm("Var_elim", result() RS mp RS mp);
 
 val asms = goal Subst.thy 
      "[| v : sdom(s); v : vars_of(t <| s) |] ==>  v : srange(s)";
 by (REPEAT (ares_tac (asms @ [Var_elim RS swap RS classical]) 1));
-val Var_elim2 = result();
+qed "Var_elim2";
 
 goal Subst.thy  "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
 by (uterm_ind_tac "t" 1);
@@ -166,20 +166,20 @@
 by (etac notE 1);
 by (etac subst 1);
 by (ALLGOALS (fast_tac set_cs));
-val Var_intro = result() RS mp;
+val Var_intro  = store_thm("Var_intro", result() RS mp);
 
 goal Subst.thy
     "v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
 by (simp_tac (subst_ss addsimps [srange_iff]) 1);
-val srangeE = make_elim (result() RS mp);
+val srangeE  = store_thm("srangeE", make_elim (result() RS mp));
 
 val asms = goal Subst.thy
    "sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})";
 by (simp_tac subst_ss 1);
 by (fast_tac (set_cs addIs [Var_elim2] addEs [srangeE]) 1);
-val dom_range_disjoint = result();
+qed "dom_range_disjoint";
 
 val asms = goal Subst.thy "~ u <| s = u --> (? x.x : sdom(s))";
 by (simp_tac (subst_ss addsimps [invariance]) 1);
 by (fast_tac set_cs 1);
-val subst_not_empty = result() RS mp;
+val subst_not_empty  = store_thm("subst_not_empty", result() RS mp);