diff -r 3a8d722fd3ff -r 16c4ea954511 Subst/Unifier.ML
--- a/Subst/Unifier.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/Subst/Unifier.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -16,29 +16,29 @@
 
 goalw Unifier.thy [Unifier_def] "Unifier(s,t,u) = (t <| s = u <| s)";
 by (rtac refl 1);
-val Unifier_iff = result();
+qed "Unifier_iff";
 
 goal Unifier.thy
     "Unifier(s,Comb(t,u),Comb(v,w)) --> Unifier(s,t,v) & Unifier(s,u,w)";
 by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
-val Unifier_Comb = result() RS mp RS conjE;
+val Unifier_Comb  = store_thm("Unifier_Comb", result() RS mp RS conjE);
 
 goal Unifier.thy
   "~v : vars_of(t) --> ~v : vars_of(u) -->Unifier(s,t,u) --> \
 \  Unifier(<v,r>#s,t,u)";
 by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
-val Cons_Unifier = result() RS mp RS mp RS mp;
+val Cons_Unifier  = store_thm("Cons_Unifier", result() RS mp RS mp RS mp);
 
 (**** Most General Unifiers ****)
 
 goalw Unifier.thy [MoreGeneral_def]  "r >> s = (EX q. s =s= r <> q)";
 by (rtac refl 1);
-val MoreGen_iff = result();
+qed "MoreGen_iff";
 
 goal Unifier.thy  "Nil >> s";
 by (simp_tac (subst_ss addsimps [MoreGen_iff]) 1);
 by (fast_tac (set_cs addIs [refl RS subst_refl]) 1);
-val MoreGen_Nil = result();
+qed "MoreGen_Nil";
 
 goalw Unifier.thy unify_defs
     "MGUnifier(s,t,u) = (ALL r.Unifier(r,t,u) = s >> r)";
@@ -46,7 +46,7 @@
             eresolve_tac [conjE,allE,mp,exE,ssubst_subst2] 1));
 by (asm_simp_tac (subst_ss addsimps [subst_comp]) 1);
 by (fast_tac (set_cs addIs [comp_Nil RS sym RS subst_refl]) 1);
-val MGU_iff = result();
+qed "MGU_iff";
 
 val [prem] = goal Unifier.thy
      "~ Var(v) <: t ==> MGUnifier(<v,t>#Nil,Var(v),t)";
@@ -56,52 +56,52 @@
 by (etac ssubst_subst2 2);
 by (rtac (Cons_trivial RS subst_sym) 1);
 by (simp_tac (subst_ss addsimps [prem RS Var_not_occs,Var_subst]) 1);
-val MGUnifier_Var = result();
+qed "MGUnifier_Var";
 
 (**** Most General Idempotent Unifiers ****)
 
 goal Unifier.thy "r <> r =s= r --> s =s= r <> q --> r <> s =s= s";
 by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
-val MGIU_iff_lemma = result() RS mp RS mp;
+val MGIU_iff_lemma  = store_thm("MGIU_iff_lemma", result() RS mp RS mp);
 
 goalw Unifier.thy unify_defs
  "MGIUnifier(s,t,u) = \
 \  (Idem(s) & Unifier(s,t,u) & (ALL r.Unifier(r,t,u) --> s<>r=s=r))";
 by (fast_tac (set_cs addEs [subst_sym,MGIU_iff_lemma]) 1);
-val MGIU_iff = result();
+qed "MGIU_iff";
 
 (**** Idempotence ****)
 
 goalw Unifier.thy unify_defs "Idem(s) = (s <> s =s= s)";
 by (rtac refl 1);
-val raw_Idem_iff = result();
+qed "raw_Idem_iff";
 
 goal Unifier.thy "Idem(s) = (sdom(s) Int srange(s) = {})";
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp,
                                 invariance,dom_range_disjoint])1);
-val Idem_iff = result();
+qed "Idem_iff";
 
 goal Unifier.thy "Idem(Nil)";
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
-val Idem_Nil = result();
+qed "Idem_Nil";
 
 goal Unifier.thy "~ (Var(v) <: t) --> Idem(<v,t>#Nil)";
 by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
                        setloop (split_tac [expand_if])) 1);
 by (fast_tac set_cs 1);
-val Var_Idem = result() RS mp;
+val Var_Idem  = store_thm("Var_Idem", result() RS mp);
 
 val [prem] = goalw Unifier.thy [Idem_def]
      "Idem(r) ==>  Unifier(s,t <| r,u <| r) --> Unifier(r <> s,t <| r,u <| r)";
 by (simp_tac (subst_ss addsimps 
 	      [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1);
-val Unifier_Idem_subst = result() RS mp;
+val Unifier_Idem_subst  = store_thm("Unifier_Idem_subst", result() RS mp);
 
 val [prem] = goal Unifier.thy 
      "r <> s =s= s ==>  Unifier(s,t,u) --> Unifier(s,t <| r,u <| r)";
 by (simp_tac (subst_ss addsimps 
 	      [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1);
-val Unifier_comp_subst = result() RS mp;
+val Unifier_comp_subst  = store_thm("Unifier_comp_subst", result() RS mp);
 
 (*** The domain of a MGIU is a subset of the variables in the terms ***)
 (***      NB this and one for range are only needed for termination ***)
@@ -110,7 +110,7 @@
     "~ vars_of(Var(x) <| r) = vars_of(Var(x) <| s) ==> ~r =s= s";
 by (rtac (prem RS contrapos) 1);
 by (fast_tac (set_cs addEs [subst_subst2]) 1);
-val lemma_lemma = result();
+qed "lemma_lemma";
 
 val prems = goal Unifier.thy 
     "x : sdom(s) -->  ~x : srange(s) --> \
@@ -122,7 +122,7 @@
 br conjI 1;
 by (asm_simp_tac (subst_ss addsimps [Var_elim,subst_comp,repl_invariance]) 1);
 by (asm_simp_tac (subst_ss addsimps [Var_subst]) 1);
-val MGIU_sdom_lemma = result() RS mp RS mp RS lemma_lemma RS notE;;
+val MGIU_sdom_lemma = store_thm("MGIU_sdom_lemma", result() RS mp RS mp RS lemma_lemma RS notE);
 
 goal Unifier.thy "MGIUnifier(s,t,u) --> sdom(s) <= vars_of(t) Un vars_of(u)";
 by (subgoal_tac "! P Q.(P | Q) = (~( ~P & ~Q))" 1);
@@ -131,13 +131,13 @@
 by (eresolve_tac ([spec] RL [impE]) 1);
 by (rtac Cons_Unifier 1);
 by (ALLGOALS (fast_tac (set_cs addIs [Cons_Unifier,MGIU_sdom_lemma])));
-val MGIU_sdom = result() RS mp;
+val MGIU_sdom  = store_thm("MGIU_sdom", result() RS mp);
 
 (*** The range of a MGIU is a subset of the variables in the terms ***)
 
 val prems = goal HOL.thy  "P = Q ==> (~P) = (~Q)";
 by (simp_tac (set_ss addsimps prems) 1);
-val not_cong = result();
+qed "not_cong";
 
 val prems = goal Unifier.thy 
    "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
@@ -149,7 +149,7 @@
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps  [Var_elim,subst_comp,
                 vars_var_iff RS not_cong RS iffD2 RS repl_invariance]) ));
 by (fast_tac (set_cs addIs [Var_in_subst]) 1);
-val MGIU_srange_lemma =result() RS mp RS mp RS mp RS mp RS lemma_lemma RS notE;
+val MGIU_srange_lemma  = store_thm("MGIU_srange_lemma", result() RS mp RS mp RS mp RS mp RS lemma_lemma RS notE);
 
 goal Unifier.thy "MGIUnifier(s,t,u) --> srange(s) <= vars_of(t) Un vars_of(u)";
 by (subgoal_tac "! P Q.(P | Q) = (~( ~P & ~Q))" 1);
@@ -161,7 +161,7 @@
 by (imp_excluded_middle_tac "w=ta" 4);
 by (fast_tac (set_cs addEs [MGIU_srange_lemma]) 5);
 by (ALLGOALS (fast_tac (set_cs addIs [Var_elim2])));
-val MGIU_srange = result() RS mp;
+val MGIU_srange = store_thm("MGIU_srange", result() RS mp);
 
 (*************** Correctness of a simple unification algorithm ***************)
 (*                                                                           *)
@@ -179,41 +179,41 @@
 
 goalw Unifier.thy unify_defs "MGIUnifier(s,t,u) = MGIUnifier(s,u,t)";
 by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp]))));
-val Unify_comm = result();
+qed "Unify_comm";
 
 goal Unifier.thy "MGIUnifier(Nil,Const(n),Const(n))";
 by (simp_tac (subst_ss addsimps
 	      [MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1);
-val Unify1 = result();
+qed "Unify1";
 
 goal Unifier.thy "~m=n --> (ALL l.~Unifier(l,Const(m),Const(n)))";
 by (simp_tac (subst_ss addsimps[Unifier_iff]) 1);
-val Unify2 = result() RS mp;
+val Unify2 = store_thm("Unify2", result() RS mp);
 
 val [prem] = goalw Unifier.thy [MGIUnifier_def] 
  "~Var(v) <: t ==> MGIUnifier(<v,t>#Nil,Var(v),t)";
 by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
-val Unify3 = result();
+qed "Unify3";
 
 val [prem] = goal Unifier.thy "Var(v) <: t ==> (ALL l.~Unifier(l,Var(v),t))";
 by (simp_tac (subst_ss addsimps
 	      [Unifier_iff,prem RS subst_mono RS occs_irrefl2]) 1);
-val Unify4 = result();
+qed "Unify4";
 
 goal Unifier.thy "ALL l.~Unifier(l,Const(m),Comb(t,u))";
 by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
-val Unify5 = result();
+qed "Unify5";
 
 goal Unifier.thy
     "(ALL l.~Unifier(l,t,v)) --> (ALL l.~Unifier(l,Comb(t,u),Comb(v,w)))";
 by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
-val Unify6 = result() RS mp;
+val Unify6 = store_thm("Unify6", result() RS mp);
 
 goal Unifier.thy "MGIUnifier(s,t,v) --> (ALL l.~Unifier(l,u <| s,w <| s)) --> \
 \                                     (ALL l.~Unifier(l,Comb(t,u),Comb(v,w)))";
 by (simp_tac (subst_ss addsimps [MGIU_iff]) 1);
 by (fast_tac (set_cs addIs [Unifier_comp_subst] addSEs [Unifier_Comb]) 1);
-val Unify7 = result() RS mp RS mp;
+val Unify7 = store_thm("Unify7", result() RS mp RS mp);
 
 val [p1,p2,p3] = goal Unifier.thy
      "[| Idem(r); Unifier(s,t <| r,u <| r); \
@@ -223,7 +223,7 @@
 		   p2 RS (p1 RS Unifier_Idem_subst RS (p3 RS spec RS mp))] 1);
 by (REPEAT_SOME (etac rev_mp));
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp]) 1);
-val Unify8_lemma1 = result();
+qed "Unify8_lemma1";
 
 val [p1,p2,p3,p4] = goal Unifier.thy
    "[| Unifier(q,t,v); Unifier(q,u,w); (! q.Unifier(q,t,v) --> r <> q =s= q); \
@@ -234,7 +234,7 @@
 		   p2 RS (pp RS Unifier_comp_subst) RS (p4 RS spec RS mp)] 1);
 by (REPEAT_SOME (etac rev_mp));
 by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
-val Unify8_lemma2 = result();
+qed "Unify8_lemma2";
 
 goal Unifier.thy  "MGIUnifier(r,t,v) -->  MGIUnifier(s,u <| r,w <| r) --> \
 \                MGIUnifier(r <> s,Comb(t,u),Comb(v,w))";
@@ -245,7 +245,7 @@
 	      [Unifier_iff,MGIU_iff,subst_comp,comp_assoc]) 2);
 by (ALLGOALS (fast_tac (set_cs addEs 
 			[Unifier_Comb,Unify8_lemma1,Unify8_lemma2])));
-val Unify8 = result();
+qed "Unify8";
 
 
 (********************** Termination of the algorithm *************************)
@@ -257,7 +257,7 @@
 goalw Unifier.thy [UWFD_def]  "UWFD(t,t',Comb(t,u),Comb(t',u'))";
 by (simp_tac subst_ss 1);
 by (fast_tac set_cs 1);
-val UnifyWFD1 = result();
+qed "UnifyWFD1";
 
 val [prem] = goal Unifier.thy 
      "MGIUnifier(s,t,t') ==> vars_of(u <| s) Un vars_of(u' <| s) <= \
@@ -268,7 +268,7 @@
 by (ALLGOALS (simp_tac (subst_ss addsimps [Var_intro,subset_iff])));
 by (ALLGOALS (fast_tac (set_cs addDs 
 			[Var_intro,prem RS MGIU_srange RS subsetD])));
-val UWFD2_lemma1 = result();
+qed "UWFD2_lemma1";
 
 val [major,minor] = goal Unifier.thy 
      "[| MGIUnifier(s,t,t');  ~ u <| s = u |] ==> \
@@ -282,7 +282,7 @@
 by (REPEAT (etac rev_mp 1));
 by (asm_simp_tac subst_ss 1);
 by (fast_tac (set_cs addIs [Var_elim2]) 1);
-val UWFD2_lemma2 = result();
+qed "UWFD2_lemma2";
 
 val [prem] = goalw Unifier.thy [UWFD_def]  
   "MGIUnifier(s,t,t') ==> UWFD(u <| s,u' <| s,Comb(t,u),Comb(t',u'))";
@@ -296,4 +296,4 @@
 by (asm_simp_tac (set_ss addsimps [subseteq_iff_subset_eq]) 1);
 by (asm_simp_tac subst_ss 1);
 by (fast_tac (set_cs addDs [prem RS UWFD2_lemma2]) 1);
-val UnifyWFD2 = result();
+qed "UnifyWFD2";