# HG changeset patch
# User paulson
# Date 845636059 -7200
# Node ID 21266526ac42db3436e0ab1d87130c18300680ef
# Parent  3902e9af752f931d73c62d2c92c59a7b89f72f8b
Subst as modified by Konrad Slind

diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/AList.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/AList.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,34 @@
+(*  Title:      Substitutions/AList.ML
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For AList.thy.
+*)
+
+open AList;
+
+val al_rews = 
+  let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s 
+                            (fn _ => [Simp_tac 1])
+  in map mk_thm 
+     ["alist_rec [] c d = c",
+      "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)",
+      "assoc v d [] = d",
+      "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end;
+
+
+val prems = goal AList.thy
+    "[| P([]);   \
+\       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";
+by (list.induct_tac "l" 1);
+by (resolve_tac prems 1);
+by (rtac PairE 1);
+by (etac ssubst 1);
+by (resolve_tac prems 1);
+by (assume_tac 1);
+qed "alist_induct";
+
+(*Perform induction on xs. *)
+fun alist_ind_tac a M = 
+    EVERY [res_inst_tac [("l",a)] alist_induct M,
+           rename_last_tac a ["1"] (M+1)];
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/AList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/AList.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,21 @@
+(*  Title:      Substitutions/alist.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Association lists.
+*)
+
+AList = List + 
+
+consts
+
+  alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
+  assoc      :: "['a,'b,('a*'b) list] => 'b"
+
+rules
+
+  alist_rec_def "alist_rec al b c == list_rec b (split c) al"
+
+  assoc_def   "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
+
+end
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/NNF.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/NNF.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,11 @@
+goal HOL.thy "(~(!x. P x)) = (? x. ~(P x)) & \
+           \  (~(? x. P x)) = (!x. ~(P x)) & \
+           \  (~(x-->y)) = (x & (~ y))     & \
+           \  ((~ x) | y) = (x --> y)      & \
+           \  (~(x & y)) = ((~ x) | (~ y)) & \
+           \  (~(x | y)) = ((~ x) & (~ y)) & \
+           \  (~(~x)) = x";
+by (fast_tac HOL_cs 1);
+val NNF_rews = map (fn th => th RS eq_reflection)
+                   (Prim.Rules.CONJUNCTS (result()))
+
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/NNF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/NNF.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,1 @@
+NNF = HOL
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/README	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,11 @@
+A first order unification algorithm is formalized and proved in this
+directory. The files "ROOT.ML" and "ROOT1.ML" give instructions for
+running the proof. "ROOT1.ML" is will run on the current Isabelle release
+
+     "Isabelle-94 revision 5: January 96"
+
+while "ROOT.ML" builds on an internal release that Carsten Clasholm was
+maintaining. Features of this internal release will make their way into
+the public release (I hope). Eventually, the definition facility used to
+define the Unify algorithm will be incorporated into the syntax for
+".thy" files.
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/ROOT.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,35 @@
+(*  Title:      HOL/Subst/ROOT.ML
+    ID:         $Id$
+    Authors:     Martin Coen, Cambridge University Computer Laboratory
+                 Konrad Slind, TU Munich
+    Copyright   1993  University of Cambridge,
+                1996  TU Munich
+
+Substitution and Unification in Higher-Order Logic. 
+
+Implements Manna & Waldinger's formalization, with Paulson's simplifications,
+and some new simplifications by Slind.
+
+Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm. 
+SCP 1 (1981), 5-48
+
+L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
+
+Setplus      -  minor additions to HOL's set theory
+Alist        -  association lists
+Uterm        -  data type of terms
+Subst        -  substitutions
+Unify        -  specification of unification and conditions for 
+                correctness and termination
+
+To load, type use"ROOT.ML"; into an Isabelle-HOL that has TFL 
+also loaded. 
+*)
+
+HOL_build_completed;    (*Cause examples to fail if HOL did*)
+
+writeln"Root file for Substitutions and Unification";
+loadpath := "../../" :: !loadpath;
+use_thy "Unify";
+
+writeln"END: Root file for Substitutions and Unification";
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/ROOT1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/ROOT1.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,35 @@
+(*  Title:      HOL/Subst/ROOT.ML
+    ID:         $Id$
+    Authors:     Martin Coen, Cambridge University Computer Laboratory
+                 Konrad Slind, TU Munich
+    Copyright   1993  University of Cambridge,
+                1996  TU Munich
+
+Substitution and Unification in Higher-Order Logic. 
+
+Implements Manna & Waldinger's formalization, with Paulson's simplifications,
+and some new simplifications by Slind.
+
+Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm. 
+SCP 1 (1981), 5-48
+
+L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
+
+Setplus      -  minor additions to HOL's set theory
+Alist        -  association lists
+Uterm        -  data type of terms
+Subst        -  substitutions
+Unify        -  specification of unification and conditions for 
+                correctness and termination
+
+To load, type use"ROOT1.ML"; into an Isabelle-HOL that has TFL 
+also loaded. 
+*)
+
+HOL_build_completed;    (*Cause examples to fail if HOL did*)
+
+writeln"Root file for Substitutions and Unification";
+loadpath := "../../" :: !loadpath;  (* to get "WF1" *)
+use_thy "Unify1";
+
+writeln"END: Root file for Substitutions and Unification";
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Setplus.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Setplus.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,130 @@
+(*  Title:      Substitutions/setplus.ML
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For setplus.thy.
+Properties of subsets and empty sets.
+*)
+
+open Setplus;
+val eq_cs = claset_of "equalities";
+
+(*********)
+
+(*** Rules for subsets ***)
+
+goal Set.thy "A <= B =  (! t.t:A --> t:B)";
+by (fast_tac set_cs 1);
+qed "subset_iff";
+
+goalw Setplus.thy [ssubset_def] "A < B = ((A <= B) & ~(A=B))";
+by (rtac refl 1);
+qed "ssubset_iff";
+
+goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))";
+by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1);
+by (fast_tac set_cs 1);
+qed "subseteq_iff_subset_eq";
+
+(*Rule in Modus Ponens style*)
+goal Setplus.thy "A < B --> c:A --> c:B";
+by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1);
+by (fast_tac set_cs 1);
+qed "ssubsetD";
+
+(*********)
+
+goalw Setplus.thy [empty_def] "~ a : {}";
+by (fast_tac set_cs 1);
+qed "not_in_empty";
+
+goalw Setplus.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
+by (fast_tac (set_cs addIs [set_ext]) 1);
+qed "empty_iff";
+
+
+(*********)
+
+goal Set.thy "(~A=B)  = ((? x.x:A & ~x:B) | (? x.~x:A & x:B))";
+by (fast_tac (set_cs addIs [set_ext]) 1);
+qed "not_equal_iff";
+
+(*********)
+
+val setplus_rews = [ssubset_iff,not_in_empty,empty_iff];
+
+(*********)
+
+(*Case analysis for rewriting; P also gets rewritten*)
+val [prem1,prem2] = goal HOL.thy "[| P-->Q;  ~P-->Q |] ==> Q";
+by (rtac (excluded_middle RS disjE) 1);
+by (etac (prem2 RS mp) 1);
+by (etac (prem1 RS mp) 1);
+qed "imp_excluded_middle";
+
+fun imp_excluded_middle_tac s = res_inst_tac [("P",s)] imp_excluded_middle;
+
+
+goal Set.thy "(insert a A ~= insert a B) --> A ~= B";
+by (fast_tac set_cs 1);
+val insert_lim = result() RS mp;
+
+goal Set.thy "x~:A --> (A-{x} = A)";
+by (fast_tac eq_cs 1);
+val lem = result() RS mp;
+
+goal Nat.thy "B<=A --> B = Suc A --> P";
+by (strip_tac 1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+val leq_lem = standard(result() RS mp RS mp);
+
+goal Nat.thy "A<=B --> (A ~= Suc B)";
+by (strip_tac 1);
+by (rtac notI 1);
+by (rtac leq_lem 1);
+by (REPEAT (atac 1));
+val leq_lem1 = standard(result() RS mp);
+
+(* The following is an adaptation of the proof for the "<=" version 
+ * in Finite. *) 
+
+goalw Setplus.thy [ssubset_def]
+"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
+by (etac finite_induct 1);
+by (Simp_tac 1);
+by (fast_tac set_cs 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (case_tac "x:A" 1);
+(*1*)
+by (dtac mk_disjoint_insert 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (hyp_subst_tac 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (!simpset addsimps 
+                        [subset_insert_iff,finite_subset,lem]) 1);
+by (dtac insert_lim 1);
+by (Asm_full_simp_tac 1);
+(*2*)
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (!simpset addsimps 
+                       [subset_insert_iff,finite_subset,lem]) 1);
+by (case_tac "A=F" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (rtac leq_lem1 1);
+by (Asm_simp_tac 1);
+val ssubset_card = result() ;
+
+
+goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
+by (rtac iffI 1);
+by (simp_tac (HOL_ss addsimps [subset_iff]) 1);
+by (fast_tac set_cs 1);
+by (rtac subset_antisym 1);
+by (ALLGOALS Asm_simp_tac);
+val set_eq_subset = result();
+
+
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Setplus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Setplus.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,14 @@
+(*  Title:      Substitutions/setplus.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Minor additions to HOL's set theory
+*)
+
+Setplus = Finite + 
+
+rules
+
+  ssubset_def    "A < B == A <= B & ~ A=B"
+
+end
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Subst.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Subst.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,199 @@
+(*  Title:      HOL/Subst/subst.ML
+    ID:         $Id$
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For subst.thy.  
+*)
+
+open Subst;
+
+
+(**** Substitutions ****)
+
+goal Subst.thy "t <| [] = t";
+by (uterm.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps al_rews)));
+qed "subst_Nil";
+
+goal Subst.thy "t <: u --> t <| s <: u <| s";
+by (uterm.induct_tac "u" 1);
+by (ALLGOALS Asm_simp_tac);
+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);
+by (res_inst_tac [("P",
+    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
+    uterm.induct 2);
+by (ALLGOALS (simp_tac (!simpset addsimps al_rews)));
+by (fast_tac HOL_cs 1);
+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)";
+by (uterm.induct_tac "t" 1);
+by (REPEAT (etac rev_mp 3));
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (fast_tac HOL_cs));
+qed "agreement";
+
+goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
+by(simp_tac (!simpset addsimps (agreement::al_rews)
+                      setloop (split_tac [expand_if])) 1);
+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.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps al_rews)));
+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 1);
+qed "subst_eq_iff";
+
+
+local fun mk_thm s = prove_goal Subst.thy s
+                  (fn prems => [cut_facts_tac prems 1,
+                                REPEAT (etac rev_mp 1),
+                                simp_tac (!simpset addsimps [subst_eq_iff]) 1])
+in 
+  val subst_refl      = mk_thm "r = s ==> r =s= s";
+  val subst_sym       = mk_thm "r =s= s ==> s =s= r";
+  val subst_trans     = mk_thm "[| q =s= r; r =s= s |] ==> q =s= s";
+end;
+
+val eq::prems = goalw Subst.thy [subst_eq_def] 
+    "[| 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);
+qed "subst_subst2";
+
+val ssubst_subst2 = subst_sym RS subst_subst2;
+
+(**** Composition of Substitutions ****)
+
+local fun mk_thm s = 
+ prove_goalw Subst.thy [comp_def,sdom_def] s 
+   (fn _ => [simp_tac (simpset_of "UTerm" addsimps al_rews) 1])
+in 
+val subst_rews = 
+ map mk_thm 
+ [ "[] <> bl = bl",
+   "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
+   "sdom([]) = {}",
+   "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else (sdom al) Un {a})"]
+end;
+
+
+goal Subst.thy "s <> [] = s";
+by (alist_ind_tac "s" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps (subst_Nil::subst_rews))));
+qed "comp_Nil";
+
+goal Subst.thy "(t <| r <> s) = (t <| r <| s)";
+by (uterm.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps al_rews)));
+by (alist_ind_tac "r" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps (subst_Nil::(al_rews@subst_rews))
+                                     setloop (split_tac [expand_if]))));
+qed "subst_comp";
+
+
+goal Subst.thy "(q <> r) <> s =s= q <> (r <> s)";
+by (simp_tac (!simpset addsimps [subst_eq_iff,subst_comp]) 1);
+qed "comp_assoc";
+
+goal Subst.thy "(theta =s= theta1) --> \
+             \    (sigma =s= sigma1) --> \
+             \     ((theta <> sigma) =s= (theta1 <> sigma1))";
+by (simp_tac (!simpset addsimps [subst_eq_def,subst_comp]) 1);
+val subst_cong = result() RS mp RS mp;
+
+
+goal Subst.thy "(w,Var(w) <| s)#s =s= s"; 
+by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
+by (uterm.induct_tac "t" 1);
+by (REPEAT (etac rev_mp 3));
+by (ALLGOALS (simp_tac (!simpset addsimps al_rews
+                                 setloop (split_tac [expand_if]))));
+qed "Cons_trivial";
+
+
+val [prem] = goal Subst.thy "q <> r =s= s ==>  t <| q <| r = t <| s";
+by (simp_tac (!simpset addsimps [prem RS (subst_eq_iff RS iffD1),
+                                subst_comp RS sym]) 1);
+qed "comp_subst_subst";
+
+
+(****  Domain and range of Substitutions ****)
+
+goal Subst.thy  "(v : sdom(s)) = (~ Var(v) <| s = Var(v))";
+by (alist_ind_tac "s" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps (al_rews@subst_rews)
+                                     setloop (split_tac[expand_if]))));
+by (fast_tac HOL_cs 1);
+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);
+qed "srange_iff";
+
+goal Subst.thy  "(t <| s = t) = (sdom(s) Int vars_of(t) = {})";
+by (uterm.induct_tac "t" 1);
+by (REPEAT (etac rev_mp 3));
+by (ALLGOALS (simp_tac (!simpset addsimps 
+                        (sdom_iff::(subst_rews@al_rews@setplus_rews)))));
+by (ALLGOALS (fast_tac set_cs));
+qed "invariance";
+
+goal Subst.thy  "v : sdom(s) -->  ~v : srange(s) --> ~v : vars_of(t <| s)";
+by (uterm.induct_tac "t" 1);
+by (imp_excluded_middle_tac "a : sdom(s)" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [sdom_iff,srange_iff])));
+by (ALLGOALS (fast_tac set_cs));
+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));
+qed "Var_elim2";
+
+goal Subst.thy  "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
+by (uterm.induct_tac "t" 1);
+by (REPEAT_SOME (etac rev_mp ));
+by (ALLGOALS (simp_tac (!simpset addsimps [sdom_iff,srange_iff])));
+by (REPEAT (step_tac (set_cs addIs [vars_var_iff RS iffD1 RS sym]) 1));
+by (etac notE 1);
+by (etac subst 1);
+by (ALLGOALS (fast_tac set_cs));
+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 (!simpset addsimps [srange_iff]) 1);
+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 (!simpset addsimps setplus_rews) 1);
+by (fast_tac (set_cs addIs [Var_elim2] addEs [srangeE]) 1);
+qed "dom_range_disjoint";
+
+val asms = goal Subst.thy "~ u <| s = u --> (? x. x : sdom(s))";
+by (simp_tac (!simpset addsimps (invariance::setplus_rews)) 1);
+by (fast_tac set_cs 1);
+val subst_not_empty  = store_thm("subst_not_empty", result() RS mp);
+
+
+goal Subst.thy "(M <| [(x, Var x)]) = M";
+by (UTerm.uterm.induct_tac "M" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps (subst_rews@al_rews)
+                                     setloop (split_tac [expand_if]))));
+val id_subst_lemma = result();
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Subst.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Subst.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,39 @@
+(*  Title:      Substitutions/subst.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Substitutions on uterms
+*)
+
+Subst = Setplus + AList + UTerm +
+
+consts
+
+  "=s="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
+  "<|"   ::  "'a uterm => ('a * 'a uterm) list => 'a uterm"        (infixl 55)
+  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] 
+                 => ('a*('a uterm)) list"                          (infixl 56)
+  sdom   ::  "('a*('a uterm)) list => 'a set"
+  srange ::  "('a*('a uterm)) list => 'a set"
+
+
+primrec "op <|"   uterm
+  subst_Var      "(Var v <| s) = assoc v (Var v) s"
+  subst_Const  "(Const c <| s) = Const c"
+  subst_Comb  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
+
+
+rules 
+
+  subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
+
+  comp_def    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
+
+  sdom_def
+  "sdom(al) == alist_rec al {}  
+                (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
+
+  srange_def   
+   "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
+
+end
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/UTerm.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/UTerm.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,47 @@
+(*  Title:      HOL/Subst/UTerm.ML
+    ID:         $Id$
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Simple term structure for unifiation.
+Binary trees with leaves that are constants or variables.
+*)
+
+open UTerm;
+
+
+(**** vars_of lemmas  ****)
+
+goal UTerm.thy "(v : vars_of(Var(w))) = (w=v)";
+by (Simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed "vars_var_iff";
+
+goal UTerm.thy  "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)";
+by (uterm.induct_tac "t" 1);
+by (ALLGOALS Simp_tac);
+by (fast_tac HOL_cs 1);
+qed "vars_iff_occseq";
+
+
+(* Not used, but perhaps useful in other proofs *)
+goal UTerm.thy "M<:N --> vars_of(M) <= vars_of(N)";
+by (uterm.induct_tac "N" 1);
+by (ALLGOALS Asm_simp_tac);
+by (fast_tac set_cs 1);
+val occs_vars_subset = result();
+
+
+goal UTerm.thy 
+     "vars_of M Un vars_of N <= vars_of(Comb M P) Un vars_of(Comb N Q)";
+by (Simp_tac  1);
+by (fast_tac set_cs 1);
+val monotone_vars_of = result();
+
+goal UTerm.thy "finite(vars_of M)";
+by (uterm.induct_tac"M" 1);
+by (ALLGOALS Simp_tac);
+by (forward_tac [finite_UnI] 1);
+by (assume_tac 1);
+by (Asm_simp_tac 1);
+val finite_vars_of = result();
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/UTerm.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/UTerm.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,37 @@
+(*  Title:      Substitutions/UTerm.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Simple term structure for unification.
+Binary trees with leaves that are constants or variables.
+*)
+
+UTerm = Finite +
+
+datatype 'a uterm = Var ('a) 
+                  | Const ('a)
+                  | Comb ('a uterm) ('a uterm)
+
+consts
+  vars_of  ::  'a uterm => 'a set
+  "<:"     ::  'a uterm => 'a uterm => bool   (infixl 54) 
+uterm_size ::  'a uterm => nat
+
+
+primrec vars_of   uterm
+vars_of_Var   "vars_of (Var v) = {v}"
+vars_of_Const "vars_of (Const c) = {}"
+vars_of_Comb  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
+
+
+primrec "op <:"   uterm
+occs_Var   "u <: (Var v) = False"
+occs_Const "u <: (Const c) = False"
+occs_Comb  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
+
+primrec uterm_size  uterm
+uterm_size_Var   "uterm_size (Var v) = 0"
+uterm_size_Const "uterm_size (Const c) = 0"
+uterm_size_Comb  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
+
+end
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Unifier.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Unifier.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,114 @@
+(*  Title:      HOL/Subst/unifier.ML
+    ID:         $Id$
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For Unifier.thy.
+Properties of unifiers.
+*)
+
+open Unifier;
+
+val unify_defs = [Unifier_def,MoreGeneral_def,MGUnifier_def];
+
+val rews = subst_rews@al_rews@setplus_rews;
+
+(*---------------------------------------------------------------------------
+ * Unifiers 
+ *---------------------------------------------------------------------------*)
+
+goalw Unifier.thy [Unifier_def] "Unifier s t u = (t <| s = u <| s)";
+by (rtac refl 1);
+val Unifier_iff = result();
+
+goal Unifier.thy
+    "Unifier s (Comb t u) (Comb v w) --> Unifier s t v & Unifier s u w";
+by (simp_tac (!simpset addsimps [Unifier_iff]) 1);
+val 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 (!simpset addsimps [Unifier_iff,repl_invariance]) 1);
+val Cons_Unifier  = result() RS mp RS mp RS mp;
+
+
+(*---------------------------------------------------------------------------
+ * Most General Unifiers 
+ *---------------------------------------------------------------------------*)
+
+goalw Unifier.thy unify_defs "MGUnifier s t u = MGUnifier s u t";
+by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp]))));
+val mgu_sym = result();
+
+
+goalw Unifier.thy [MoreGeneral_def]  "r >> s = (EX q. s =s= r <> q)";
+by (rtac refl 1);
+val MoreGen_iff = result();
+
+
+goal Unifier.thy  "[] >> s";
+by (simp_tac (!simpset addsimps (MoreGen_iff::subst_rews)) 1);
+by (fast_tac (set_cs addIs [refl RS subst_refl]) 1);
+val MoreGen_Nil = result();
+
+
+goalw Unifier.thy unify_defs
+    "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)";
+by (REPEAT (ares_tac [iffI,allI] 1 ORELSE 
+            eresolve_tac [conjE,allE,mp,exE,ssubst_subst2] 1));
+by (asm_simp_tac (!simpset addsimps [subst_comp]) 1);
+by (fast_tac (set_cs addIs [comp_Nil RS sym RS subst_refl]) 1);
+val MGU_iff = result();
+
+
+val [prem] = goal Unifier.thy
+     "~ Var(v) <: t ==> MGUnifier [(v,t)] (Var v) t";
+by(simp_tac(HOL_ss addsimps([MGU_iff,MoreGen_iff,Unifier_iff]@rews))1);
+by (REPEAT_SOME (step_tac set_cs));
+by (etac subst 1);
+by (etac ssubst_subst2 2);
+by (rtac (Cons_trivial RS subst_sym) 1);
+by (simp_tac (!simpset addsimps ((prem RS Var_not_occs)::rews)) 1);
+val MGUnifier_Var = result();
+
+
+
+(*---------------------------------------------------------------------------
+ * Idempotence.
+ *---------------------------------------------------------------------------*)
+
+goalw Unifier.thy [Idem_def] "Idem([])";
+by (simp_tac (!simpset addsimps (refl RS subst_refl)::rews) 1);
+qed "Idem_Nil";
+
+goalw Unifier.thy [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})";
+by (simp_tac (!simpset addsimps [subst_eq_iff,subst_comp,
+                                 invariance,dom_range_disjoint])1);
+qed "Idem_iff";
+
+val rews = subst_rews@al_rews@setplus_rews;
+goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
+by (simp_tac (!simpset addsimps (vars_iff_occseq::Idem_iff::srange_iff::rews)
+                        setloop (split_tac [expand_if])) 1);
+by (fast_tac set_cs 1);
+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 (!simpset addsimps 
+              [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1);
+val Unifier_Idem_subst  = store_thm("Unifier_Idem_subst", result() RS mp);
+
+val [p1,p2,p3] = goal Unifier.thy
+     "[| Idem(r); Unifier s (t <| r) (u <| r); \
+\        (!q. Unifier q (t <| r) (u <| r) --> s <> q =s= q) \
+\     |] ==> Idem(r <> s)";
+
+by (cut_facts_tac [p1,
+                   p2 RS (p1 RS Unifier_Idem_subst RS (p3 RS spec RS mp))] 1);
+by (REPEAT_SOME (etac rev_mp));
+by (simp_tac (!simpset addsimps [Idem_def,subst_eq_iff,subst_comp]) 1);
+qed "Idem_comp";
+
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Unifier.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Unifier.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,24 @@
+(*  Title:      Subst/unifier.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Definition of most general unifier
+*)
+
+Unifier = Subst + 
+
+consts
+
+  Unifier    :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
+  ">>"       :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
+  MGUnifier  :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
+  Idem       :: "('a*('a uterm))list => bool"
+
+rules  (*Definitions*)
+
+  Unifier_def      "Unifier s t u == t <| s = u <| s"
+  MoreGeneral_def  "r >> s == ? q. s =s= r <> q"
+  MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
+                                       (!r. Unifier r t u --> s >> r)"
+  Idem_def         "Idem(s) == s <> s =s= s"
+end
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Unify.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Unify.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,571 @@
+(*---------------------------------------------------------------------------
+ * This file defines a nested unification algorithm, then proves that it 
+ * terminates, then proves 2 correctness theorems: that when the algorithm
+ * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
+ * Although the proofs may seem long, they are actually quite direct, in that
+ * the correctness and termination properties are not mingled as much as in 
+ * previous proofs of this algorithm. 
+ *
+ * Our approach for nested recursive functions is as follows: 
+ *
+ *    0. Prove the wellfoundedness of the termination relation.
+ *    1. Prove the non-nested termination conditions.
+ *    2. Eliminate (0) and (1) from the recursion equations and the 
+ *       induction theorem.
+ *    3. Prove the nested termination conditions by using the induction 
+ *       theorem from (2) and by using the recursion equations from (2). 
+ *       These are constrained by the nested termination conditions, but 
+ *       things work out magically (by wellfoundedness of the termination 
+ *       relation).
+ *    4. Eliminate the nested TCs from the results of (2).
+ *    5. Prove further correctness properties using the results of (4).
+ *
+ * Deeper nestings require iteration of steps (3) and (4).
+ *---------------------------------------------------------------------------*)
+
+(* This is just a wrapper for the definition mechanism. *)
+local fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
+in
+fun Rfunc thy R eqs =
+   let val read = term_of o cread thy;
+    in Tfl.Rfunction thy (read R) (read eqs)
+    end
+end;
+
+(*---------------------------------------------------------------------------
+ * The algorithm.
+ *---------------------------------------------------------------------------*)
+val {theory,induction,rules,tcs} =
+Rfunc Unify.thy "R"
+  "(Unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail))    & \
+\  (Unify(Const m, Comb M N) = Fail)                                 & \
+\  (Unify(Const m, Var v)    = Subst[(v,Const m)])                   & \
+\  (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & \
+\  (Unify(Comb M N, Const x) = Fail)                                 & \
+\  (Unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail  \
+\                             else Subst[(v,Comb M N)]))             & \
+\  (Unify(Comb M1 N1, Comb M2 N2) =  \
+\     (case Unify(M1,M2) \
+\       of Fail => Fail \
+\        | Subst theta => (case Unify(N1 <| theta, N2 <| theta) \
+\                           of Fail => Fail \
+\                             | Subst sigma => Subst (theta <> sigma))))";
+
+open Unify;
+
+(*---------------------------------------------------------------------------
+ * A slightly augmented strip_tac. 
+ *---------------------------------------------------------------------------*)
+fun my_strip_tac i = 
+   CHANGED (strip_tac i 
+             THEN REPEAT ((etac exE ORELSE' etac conjE) i)
+             THEN TRY (hyp_subst_tac i));
+
+(*---------------------------------------------------------------------------
+ * A slightly augmented fast_tac for sets. It handles the case where the 
+ * top connective is "=".
+ *---------------------------------------------------------------------------*)
+fun my_fast_set_tac i = (TRY(rtac set_ext i) THEN fast_tac set_cs i);
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of proper subset on finite sets.
+ *---------------------------------------------------------------------------*)
+goalw Unify.thy [R0_def] "wf(R0)";
+by (rtac ((wf_subset RS mp) RS mp) 1);
+by (rtac wf_measure 1);
+by(simp_tac(!simpset addsimps[measure_def,inv_image_def,symmetric less_def])1);
+by (my_strip_tac 1);
+by (forward_tac[ssubset_card] 1);
+by (fast_tac set_cs 1);
+val wf_R0 = result();
+
+
+(*---------------------------------------------------------------------------
+ * Tactic for selecting and working on the first projection of R.
+ *---------------------------------------------------------------------------*)
+fun R0_tac thms i =
+  (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def,
+               measure_def,inv_image_def,point_to_prod_def])) i THEN
+   REPEAT (rtac exI i) THEN
+   REPEAT ((rtac conjI THEN' rtac refl) i) THEN
+   rtac disjI1 i THEN
+   simp_tac (!simpset addsimps [R0_def,finite_vars_of]) i);
+
+
+
+(*---------------------------------------------------------------------------
+ * Tactic for selecting and working on the second projection of R.
+ *---------------------------------------------------------------------------*)
+fun R1_tac thms i = 
+   (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def,
+                 measure_def,inv_image_def,point_to_prod_def])) i THEN 
+    REPEAT (rtac exI i) THEN 
+    REPEAT ((rtac conjI THEN' rtac refl) i) THEN
+    rtac disjI2 i THEN
+    asm_simp_tac (!simpset addsimps [R1_def,rprod_def]) i);
+
+
+(*---------------------------------------------------------------------------
+ * The non-nested TC plus the wellfoundedness of R.
+ *---------------------------------------------------------------------------*)
+Tfl.tgoalw Unify.thy [] rules;
+by (rtac conjI 1);
+(* TC *)
+by (my_strip_tac 1);
+by (cut_facts_tac [monotone_vars_of] 1); 
+by (asm_full_simp_tac(!simpset addsimps [subseteq_iff_subset_eq]) 1);
+by (etac disjE 1);
+by (R0_tac[] 1);
+by (R1_tac[] 1);
+by (simp_tac
+     (!simpset addsimps [measure_def,inv_image_def,less_eq,less_add_Suc1]) 1);
+
+(* Wellfoundedness of R *)
+by (simp_tac (!simpset addsimps [Unify.R_def,Unify.R1_def]) 1);
+by (REPEAT (resolve_tac [wf_inv_image,wf_lex_prod,wf_R0,
+                         wf_rel_prod, wf_measure] 1));
+val tc0 = result();
+
+
+(*---------------------------------------------------------------------------
+ * Eliminate tc0 from the recursion equations and the induction theorem.
+ *---------------------------------------------------------------------------*)
+val [tc,wfr] = Prim.Rules.CONJUNCTS tc0;
+val rules1 = implies_intr_hyps rules;
+val rules2 = wfr RS rules1;
+
+val [a,b,c,d,e,f,g] = Prim.Rules.CONJUNCTS rules2;
+val g' = tc RS (g RS mp);
+val rules4 = standard (Prim.Rules.LIST_CONJ[a,b,c,d,e,f,g']);
+
+val induction1 = implies_intr_hyps induction;
+val induction2 = wfr RS induction1;
+val induction3 = tc RS induction2;
+
+val induction4 = standard
+ (rewrite_rule[fst_conv RS eq_reflection, snd_conv RS eq_reflection]
+   (induction3 RS (read_instantiate_sg (sign_of theory)
+      [("x","%p. Phi (fst p) (snd p)")] spec)));
+
+
+(*---------------------------------------------------------------------------
+ * Some theorems about transitivity of WF combinators. Only the last
+ * (transR) is used, in the proof of termination. The others are generic and
+ * should maybe go somewhere.
+ *---------------------------------------------------------------------------*)
+goalw WF1.thy [trans_def,lex_prod_def,mem_Collect_eq RS eq_reflection]
+           "trans R1 & trans R2 --> trans (R1 ** R2)";
+by (my_strip_tac 1);
+by (res_inst_tac [("x","a")] exI 1);
+by (res_inst_tac [("x","a'a")] exI 1);
+by (res_inst_tac [("x","b")] exI 1);
+by (res_inst_tac [("x","b'a")] exI 1);
+by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1));
+by (Simp_tac 1);
+by (REPEAT (etac disjE 1));
+by (rtac disjI1 1);
+by (ALLGOALS (fast_tac set_cs));
+val trans_lex_prod = result() RS mp;
+
+
+goalw WF1.thy [trans_def,rprod_def,mem_Collect_eq RS eq_reflection]
+           "trans R1 & trans R2 --> trans (rprod R1  R2)";
+by (my_strip_tac 1);
+by (res_inst_tac [("x","a")] exI 1);
+by (res_inst_tac [("x","a'a")] exI 1);
+by (res_inst_tac [("x","b")] exI 1);
+by (res_inst_tac [("x","b'a")] exI 1);
+by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1));
+by (Simp_tac 1);
+by (fast_tac set_cs 1);
+val trans_rprod = result() RS mp;
+
+
+goalw Unify.thy [trans_def,inv_image_def,mem_Collect_eq RS eq_reflection]
+ "trans r --> trans (inv_image r f)";
+by (rewrite_tac [fst_conv RS eq_reflection, snd_conv RS eq_reflection]);
+by (fast_tac set_cs 1);
+val trans_inv_image = result() RS mp;
+
+goalw Unify.thy [R0_def, trans_def, mem_Collect_eq RS eq_reflection]
+ "trans R0";
+by (rewrite_tac [fst_conv RS eq_reflection,snd_conv RS eq_reflection,
+                 ssubset_def, set_eq_subset RS eq_reflection]);
+by (fast_tac set_cs 1);
+val trans_R0 = result();
+
+goalw Unify.thy [R_def,R1_def,measure_def] "trans R";
+by (REPEAT (resolve_tac[trans_inv_image,trans_lex_prod,conjI, trans_R0,
+                        trans_rprod, trans_inv_image, trans_trancl] 1));
+val transR = result();
+
+
+(*---------------------------------------------------------------------------
+ * The following lemma is used in the last step of the termination proof for 
+ * the nested call in Unify. Loosely, it says that R doesn't care so much
+ * about term structure.
+ *---------------------------------------------------------------------------*)
+goalw Unify.thy [R_def,lex_prod_def, inv_image_def,point_to_prod_def]
+     "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : R --> \
+    \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : R";
+by (Simp_tac 1);
+by (rtac conjI 1);
+by (strip_tac 1);
+by (rtac disjI1 1);
+by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
+                \  (vars_of D Un vars_of E Un vars_of F)) = \
+                \ (vars_of A Un (vars_of B Un vars_of C) Un \
+                \  (vars_of D Un (vars_of E Un vars_of F)))" 1);
+by (my_fast_set_tac 2);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (rtac disjI2 1);
+by (etac conjE 1);
+by (Asm_simp_tac 1);
+by (rtac conjI 1);
+by (my_fast_set_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [R1_def, measure_def, rprod_def,
+                          less_eq, inv_image_def,add_assoc]) 1);
+val Rassoc = result() RS mp;
+
+(*---------------------------------------------------------------------------
+ * Rewriting support.
+ *---------------------------------------------------------------------------*)
+
+val termin_ss = (!simpset addsimps (srange_iff::(subst_rews@al_rews)));
+
+
+(*---------------------------------------------------------------------------
+ * This lemma proves the nested termination condition for the base cases 
+ * 3, 4, and 6. It's a clumsy formulation (requiring two conjuncts, each with
+ * exactly the same proof) of a more general theorem.
+ *---------------------------------------------------------------------------*)
+goal theory "(~(Var x <: M)) --> [(x, M)] = theta -->       \
+\ (! N1 N2. (((N1 <| theta, N2 <| theta), (Comb M N1, Comb (Var x) N2)) : R) \
+\       &   (((N1 <| theta, N2 <| theta), (Comb(Var x) N1, Comb M N2)) : R))";
+by (my_strip_tac 1);
+by (case_tac "Var x = M" 1);
+by (hyp_subst_tac 1);
+by (case_tac "x:(vars_of N1 Un vars_of N2)" 1);
+let val case1 = 
+   EVERY1[R1_tac[id_subst_lemma], rtac conjI, my_fast_set_tac,
+          REPEAT o (rtac exI), REPEAT o (rtac conjI THEN' rtac refl),
+          simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq])];
+in by (rtac conjI 1);
+   by case1;
+   by case1
+end;
+
+let val case2 = 
+   EVERY1[R0_tac[id_subst_lemma],
+          simp_tac (!simpset addsimps [ssubset_def,set_eq_subset]),
+          fast_tac set_cs]
+in by (rtac conjI 1);
+   by case2;
+   by case2
+end;
+
+let val case3 =  
+ EVERY1 [R0_tac[],
+        cut_inst_tac [("s2","[(x, M)]"), ("v2", "x"), ("t2","N1")] Var_elim] 
+ THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq]))
+ THEN cut_inst_tac [("s2","[(x, M)]"),("v2", "x"), ("t2","N2")] Var_elim 1
+ THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq]))
+ THEN EVERY1 [simp_tac (HOL_ss addsimps [ssubset_def]),
+             rtac conjI, simp_tac (HOL_ss addsimps [subset_iff]),
+             my_strip_tac, etac UnE, dtac Var_intro] 
+ THEN dtac Var_intro 2
+ THEN ALLGOALS (asm_full_simp_tac (termin_ss addsimps [set_eq_subset])) 
+ THEN TRYALL (fast_tac set_cs)
+in 
+  by (rtac conjI 1);
+  by case3;
+  by case3
+end;
+val var_elimR = result() RS mp RS mp RS spec RS spec;
+
+
+val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst");
+
+(*---------------------------------------------------------------------------
+ * Do a case analysis on something of type 'a subst. 
+ *---------------------------------------------------------------------------*)
+
+fun Subst_case_tac theta =
+(cut_inst_tac theta (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1 
+  THEN etac disjE 1 
+  THEN rotate_tac ~1 1 
+  THEN Asm_full_simp_tac 1 
+  THEN etac exE 1
+  THEN rotate_tac ~1 1 
+  THEN Asm_full_simp_tac 1);
+
+
+goals_limit := 1;
+
+(*---------------------------------------------------------------------------
+ * The nested TC. Proved by recursion induction.
+ *---------------------------------------------------------------------------*)
+goalw_cterm [] 
+     (hd(tl(tl(map (cterm_of (sign_of theory) o USyntax.mk_prop) tcs))));
+(*---------------------------------------------------------------------------
+ * The extracted TC needs the scope of its quantifiers adjusted, so our 
+ * first step is to restrict the scopes of N1 and N2.
+ *---------------------------------------------------------------------------*)
+by (subgoal_tac "!M1 M2 theta.  \
+ \     Unify (M1, M2) = Subst theta --> \
+ \    (!N1 N2. ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R)" 1);
+by (fast_tac HOL_cs 1);
+by (rtac allI 1); 
+by (rtac allI 1);
+(* Apply induction *)
+by (res_inst_tac [("xa","M1"),("x","M2")] 
+                 (standard (induction4 RS mp RS spec RS spec)) 1);
+by (simp_tac (!simpset addsimps (rules4::(subst_rews@al_rews))
+                       setloop (split_tac [expand_if])) 1);
+(* 1 *)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (R1_tac[subst_Nil] 1);
+by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1));
+by (simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq]) 1);
+
+(* 3 *)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1);
+by (Simp_tac 1);
+by (rtac refl 1);
+
+(* 4 *)
+by (rtac conjI 1);
+by (strip_tac 1);
+by (rtac (Prim.Rules.CONJUNCT2 var_elimR) 1);
+by (assume_tac 1);
+by (rtac refl 1);
+
+(* 6 *)
+by (rtac conjI 1);
+by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]);
+by (my_strip_tac 1);
+by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1);
+by (Asm_simp_tac 1);
+by (rtac refl 1);
+
+(* 7 *)
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (etac conjE 1);
+by (rename_tac "foo bar M1 N1 M2 N2" 1);
+by (Subst_case_tac [("v","Unify(M1, M2)")]);
+by (rename_tac "foo bar M1 N1 M2 N2 theta" 1);
+
+by (Subst_case_tac [("v","Unify(N1 <| theta, N2 <| theta)")]);
+by (rename_tac "foo bar M1 N1 M2 N2 theta sigma" 1);
+by (REPEAT (rtac allI 1));
+by (rename_tac "foo bar M1 N1 M2 N2 theta sigma P Q" 1); 
+by (simp_tac (HOL_ss addsimps [subst_comp]) 1);
+by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1);
+by (fast_tac HOL_cs 1);
+by (simp_tac (HOL_ss addsimps [symmetric (subst_Comb RS eq_reflection)]) 1);
+by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \
+                \ (Comb M1 (Comb N1 P), Comb M2 (Comb N2 Q))) :R" 1);
+by (asm_simp_tac HOL_ss 2);
+
+by (rtac Rassoc 1);
+by (assume_tac 1);
+val Unify_TC2 = result();
+
+
+(*---------------------------------------------------------------------------
+ * Now for elimination of nested TC from rules and induction. This step 
+ * would be easier if "rewrite_rule" used context.
+ *---------------------------------------------------------------------------*)
+goal theory 
+ "(Unify (Comb M1 N1, Comb M2 N2) =  \
+\   (case Unify (M1, M2) of Fail => Fail \
+\    | Subst theta => \
+\        (case if ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R \
+\              then Unify (N1 <| theta, N2 <| theta) else @ z. True of \
+\        Fail => Fail | Subst sigma => Subst (theta <> sigma)))) \
+\  = \
+\ (Unify (Comb M1 N1, Comb M2 N2) = \
+\   (case Unify (M1, M2)  \
+\      of Fail => Fail \
+\      | Subst theta => (case Unify (N1 <| theta, N2 <| theta) \
+\                          of Fail => Fail  \
+\                           | Subst sigma => Subst (theta <> sigma))))";
+by (cut_inst_tac [("v","Unify(M1, M2)")]
+                 (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1);
+by (etac disjE 1);
+by (Asm_simp_tac 1);
+by (etac exE 1);
+by (Asm_simp_tac 1);
+by (cut_inst_tac 
+     [("x","list"), ("xb","N1"), ("xa","N2"),("xc","M2"), ("xd","M1")]
+     (standard(Unify_TC2 RS spec RS spec RS spec RS spec RS spec)) 1);
+by (Asm_full_simp_tac 1);
+val Unify_rec_simpl = result() RS eq_reflection;
+
+val Unify_rules = rewrite_rule[Unify_rec_simpl] rules4;
+
+
+goal theory 
+ "(! M1 N1 M2 N2.  \
+\       (! theta.  \
+\           Unify (M1, M2) = Subst theta -->  \
+\           ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R -->  \
+\           ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 -->  \
+\       ?Phi (Comb M1 N1) (Comb M2 N2))  \
+\    =  \
+\ (! M1 N1 M2 N2.  \
+\       (! theta.  \
+\           Unify (M1, M2) = Subst theta -->  \
+\           ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 -->  \
+\       ?Phi (Comb M1 N1) (Comb M2 N2))";
+by (simp_tac (HOL_ss addsimps [Unify_TC2]) 1);
+val Unify_induction = rewrite_rule[result() RS eq_reflection] induction4;
+
+
+
+(*---------------------------------------------------------------------------
+ * Correctness. Notice that idempotence is not needed to prove that the 
+ * algorithm terminates and is not needed to prove the algorithm correct, 
+ * if you are only interested in an MGU. This is in contrast to the
+ * approach of M&W, who used idempotence and MGU-ness in the termination proof.
+ *---------------------------------------------------------------------------*)
+
+goal theory "!theta. Unify (P,Q) = Subst theta --> MGUnifier theta P Q";
+by (res_inst_tac [("xa","P"),("x","Q")] 
+                 (standard (Unify_induction RS mp RS spec RS spec)) 1);
+by (simp_tac (!simpset addsimps [Unify_rules] 
+                       setloop (split_tac [expand_if])) 1);
+(*1*)
+by (rtac conjI 1);
+by (REPEAT (rtac allI 1));
+by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
+by (my_strip_tac 1);
+by (rtac MoreGen_Nil 1);
+
+(*3*)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac (mgu_sym RS iffD1) 1);
+by (rtac MGUnifier_Var 1);
+by (Simp_tac 1);
+
+(*4*)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac MGUnifier_Var 1);
+by (assume_tac 1);
+
+(*6*)
+by (rtac conjI 1);
+by (rewrite_tac NNF_rews);
+by (my_strip_tac 1);
+by (rtac (mgu_sym RS iffD1) 1);
+by (rtac MGUnifier_Var 1);
+by (Asm_simp_tac 1);
+
+(*7*) 
+by (safe_tac HOL_cs);
+by (Subst_case_tac [("v","Unify(M1, M2)")]);
+by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1);
+by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*)
+
+by (prune_params_tac);
+by (safe_tac HOL_cs);
+by (rename_tac "M1 N1 M2 N2 theta sigma gamma" 1);
+
+by (rewrite_tac [MoreGeneral_def]);
+by (rotate_tac ~3 1);
+by (eres_inst_tac [("x","gamma")] allE 1);
+by (Asm_full_simp_tac 1);
+by (etac exE 1);
+by (rename_tac "M1 N1 M2 N2 theta sigma gamma delta" 1);
+by (eres_inst_tac [("x","delta")] allE 1);
+by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
+by (dtac mp 1);
+by (atac 1);
+by (etac exE 1);
+by (rename_tac "M1 N1 M2 N2 theta sigma gamma delta rho" 1);
+
+by (rtac exI 1);
+by (rtac subst_trans 1);
+by (assume_tac 1);
+
+by (rtac subst_trans 1);
+by (rtac (comp_assoc RS subst_sym) 2);
+by (rtac subst_cong 1);
+by (rtac (refl RS subst_refl) 1);
+by (assume_tac 1);
+
+by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff,subst_comp]) 1);
+by (forw_inst_tac [("x","N1")] spec 1);
+by (dres_inst_tac [("x","N2")] spec 1);
+by (Asm_full_simp_tac 1);
+val Unify_gives_MGU = standard(result() RS spec RS mp);
+
+
+(*---------------------------------------------------------------------------
+ * Unify returns idempotent substitutions, when it succeeds.
+ *---------------------------------------------------------------------------*)
+goal theory "!theta. Unify (P,Q) = Subst theta --> Idem theta";
+by (res_inst_tac [("xa","P"),("x","Q")] 
+                 (standard (Unify_induction RS mp RS spec RS spec)) 1);
+(* Blows away all base cases automatically *)
+by (simp_tac (!simpset addsimps [Unify_rules,Idem_Nil,Var_Idem] 
+                       setloop (split_tac [expand_if])) 1);
+
+(*7*)
+by (safe_tac HOL_cs);
+by (Subst_case_tac [("v","Unify(M1, M2)")]);
+by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
+by (hyp_subst_tac 1);
+by prune_params_tac;
+by (rename_tac "M1 N1 M2 N2 theta sigma" 1);
+
+by (dtac Unify_gives_MGU 1);
+by (dtac Unify_gives_MGU 1);
+by (rewrite_tac [MGUnifier_def]);
+by (my_strip_tac 1);
+by (rtac Idem_comp 1);
+by (atac 1);
+by (atac 1);
+
+by (my_strip_tac 1);
+by (eres_inst_tac [("x","q")] allE 1);
+by (Asm_full_simp_tac 1);
+by (rewrite_tac [MoreGeneral_def]);
+by (my_strip_tac 1);
+by (asm_full_simp_tac(termin_ss addsimps [subst_eq_iff,subst_comp,Idem_def])1);
+val Unify_gives_Idem = result() RS spec RS mp;
+
+
+
+(*---------------------------------------------------------------------------
+ * Exercise. The given algorithm is a bit inelegant. What about the
+ * following "improvement", which adds a few recursive calls in former
+ * base cases? It seems that the termination relation needs another
+ * case in the lexico. product.
+
+val {theory,induction,rules,tcs,typechecks} =
+Rfunc Unify.thy ??
+  `(Unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail))    &
+   (Unify(Const m, Comb M N) = Fail)                                 &
+   (Unify(Const m, Var v)    = Unify(Var v, Const m))                &
+   (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) &
+   (Unify(Comb M N, Const x) = Fail)                                 &
+   (Unify(Comb M N, Var v) = Unify(Var v, Comb M N))                 &
+   (Unify(Comb M1 N1, Comb M2 N2) = 
+      (case Unify(M1,M2)
+        of Fail => Fail
+         | Subst theta => (case Unify(N1 <| theta, N2 <| theta)
+                            of Fail => Fail
+                             | Subst sigma => Subst (theta <> sigma))))`;
+
+ *---------------------------------------------------------------------------*)
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Unify.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Unify.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,26 @@
+Unify = Unifier + WF1 + "NNF" + 
+
+datatype 'a subst = Fail | Subst ('a list)
+
+consts
+
+ "##"  :: "('a => 'b) => ('a => 'c) => 'a => ('b * 'c)"  (infixr 50)
+   R0  :: "('a set * 'a set) set"
+   R1  :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+   R   :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+
+
+rules
+
+  point_to_prod_def "(f ## g) x == (f x, g x)"
+
+  (* finite proper subset -- should go in WF1.thy maybe *)
+  R0_def "R0 == {p. fst p < snd p & finite(snd p)}"
+
+  R1_def "R1 == rprod (measure uterm_size) (measure uterm_size)"
+
+  (* The termination relation for the Unify function *)
+  R_def  "R == inv_image  (R0 ** R1)
+                          ((%(x,y). vars_of x Un vars_of y) ## (%x.x))"
+
+end
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Unify1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Unify1.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,637 @@
+(*---------------------------------------------------------------------------
+ * This file defines a nested unification algorithm, then proves that it 
+ * terminates, then proves 2 correctness theorems: that when the algorithm
+ * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
+ * Although the proofs may seem long, they are actually quite direct, in that
+ * the correctness and termination properties are not mingled as much as in 
+ * previous proofs of this algorithm. 
+ *
+ * Our approach for nested recursive functions is as follows: 
+ *
+ *    0. Prove the wellfoundedness of the termination relation.
+ *    1. Prove the non-nested termination conditions.
+ *    2. Eliminate (0) and (1) from the recursion equations and the 
+ *       induction theorem.
+ *    3. Prove the nested termination conditions by using the induction 
+ *       theorem from (2) and by using the recursion equations from (2). 
+ *       These are constrained by the nested termination conditions, but 
+ *       things work out magically (by wellfoundedness of the termination 
+ *       relation).
+ *    4. Eliminate the nested TCs from the results of (2).
+ *    5. Prove further correctness properties using the results of (4).
+ *
+ * Deeper nestings require iteration of steps (3) and (4).
+ *---------------------------------------------------------------------------*)
+
+Thry.add_datatype_facts
+   (UTerm.thy, ("uterm",["Var", "Const", "Comb"]), uterm.induct_tac);
+
+Thry.add_datatype_facts 
+   (Unify1.thy, ("subst",["Fail", "Subst"]), Unify1.subst.induct_tac);
+
+(* This is just a wrapper for the definition mechanism. *)
+local fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
+in
+fun Rfunc thy R eqs =
+   let val _ = reset_count()
+       val _ =  tych_counting true
+       val read = term_of o cread thy;
+       val {induction,rules,theory,tcs} = Tfl.Rfunction thy (read R) (read eqs)
+   in {induction=induction, rules=rules, theory=theory, 
+       typechecks = count(), tcs = tcs}
+   end
+end;
+
+(*---------------------------------------------------------------------------
+ * The algorithm.
+ *---------------------------------------------------------------------------*)
+val {theory,induction,rules,tcs,typechecks} =
+Rfunc Unify1.thy "R"
+  "(Unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail))    & \
+\  (Unify(Const m, Comb M N) = Fail)                                 & \
+\  (Unify(Const m, Var v)    = Subst[(v,Const m)])                   & \
+\  (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & \
+\  (Unify(Comb M N, Const x) = Fail)                                 & \
+\  (Unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail  \
+\                             else Subst[(v,Comb M N)]))             & \
+\  (Unify(Comb M1 N1, Comb M2 N2) =  \
+\     (case Unify(M1,M2) \
+\       of Fail => Fail \
+\        | Subst theta => (case Unify(N1 <| theta, N2 <| theta) \
+\                           of Fail => Fail \
+\                             | Subst sigma => Subst (theta <> sigma))))";
+
+
+
+open Unify1;
+
+(*---------------------------------------------------------------------------
+ * A slightly augmented strip_tac. 
+ *---------------------------------------------------------------------------*)
+(* Needs a correct "CHANGED" to work! This one taken from Carsten's version. *)
+(*Returns all changed states*)
+fun CHANGED tac st = 
+    let fun diff st' = not (eq_thm(st,st'))
+    in  Sequence.filters diff (tac st)  end;
+
+fun my_strip_tac i = 
+   CHANGED (strip_tac i 
+            THEN REPEAT ((etac exE ORELSE' etac conjE) i)
+            THEN TRY (hyp_subst_tac i));
+
+(*---------------------------------------------------------------------------
+ * A slightly augmented fast_tac for sets. It handles the case where the 
+ * top connective is "=".
+ *---------------------------------------------------------------------------*)
+fun my_fast_set_tac i = (TRY(rtac set_ext i) THEN fast_tac set_cs i);
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of proper subset on finite sets.
+ *---------------------------------------------------------------------------*)
+goalw Unify1.thy [R0_def] "wf(R0)";
+by (rtac ((wf_subset RS mp) RS mp) 1);
+by (rtac wf_measure 1);
+by(simp_tac(!simpset addsimps[measure_def,inv_image_def,symmetric less_def])1);
+by (my_strip_tac 1);
+by (forward_tac[ssubset_card] 1);
+by (fast_tac set_cs 1);
+val wf_R0 = result();
+
+
+(*---------------------------------------------------------------------------
+ * Tactic for selecting and working on the first projection of R.
+ *---------------------------------------------------------------------------*)
+fun R0_tac thms i =
+  (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def,
+               measure_def,inv_image_def,point_to_prod_def])) i THEN
+   REPEAT (rtac exI i) THEN
+   REPEAT ((rtac conjI THEN' rtac refl) i) THEN
+   rtac disjI1 i THEN
+   simp_tac (!simpset addsimps [R0_def,finite_vars_of]) i);
+
+
+
+(*---------------------------------------------------------------------------
+ * Tactic for selecting and working on the second projection of R.
+ *---------------------------------------------------------------------------*)
+fun R1_tac thms i = 
+   (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def,
+                 measure_def,inv_image_def,point_to_prod_def])) i THEN 
+    REPEAT (rtac exI i) THEN 
+    REPEAT ((rtac conjI THEN' rtac refl) i) THEN
+    rtac disjI2 i THEN
+    asm_simp_tac (!simpset addsimps [R1_def,rprod_def]) i);
+
+
+(*---------------------------------------------------------------------------
+ * The non-nested TC plus the wellfoundedness of R.
+ *---------------------------------------------------------------------------*)
+tgoalw Unify1.thy [] rules;
+by (rtac conjI 1);
+(* TC *)
+by (my_strip_tac 1);
+by (cut_facts_tac [monotone_vars_of] 1); 
+by (asm_full_simp_tac(!simpset addsimps [subseteq_iff_subset_eq]) 1);
+by (etac disjE 1);
+by (R0_tac[] 1);
+by (R1_tac[] 1);
+by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1));
+by (simp_tac
+     (!simpset addsimps [measure_def,inv_image_def,less_eq,less_add_Suc1]) 1);
+
+(* Wellfoundedness of R *)
+by (simp_tac (!simpset addsimps [Unify1.R_def,Unify1.R1_def]) 1);
+by (REPEAT (resolve_tac [wf_inv_image,wf_lex_prod,wf_R0,
+                         wf_rel_prod, wf_measure] 1));
+val tc0 = result();
+
+
+(*---------------------------------------------------------------------------
+ * Eliminate tc0 from the recursion equations and the induction theorem.
+ *---------------------------------------------------------------------------*)
+val [tc,wfr] = Prim.Rules.CONJUNCTS tc0;
+val rules1 = implies_intr_hyps rules;
+val rules2 = wfr RS rules1;
+
+val [a,b,c,d,e,f,g] = Prim.Rules.CONJUNCTS rules2;
+val g' = tc RS (g RS mp);
+val rules4 = standard (Prim.Rules.LIST_CONJ[a,b,c,d,e,f,g']);
+
+val induction1 = implies_intr_hyps induction;
+val induction2 = wfr RS induction1;
+val induction3 = tc RS induction2;
+
+val induction4 = standard
+ (rewrite_rule[fst_conv RS eq_reflection, snd_conv RS eq_reflection]
+   (induction3 RS (read_instantiate_sg (sign_of theory)
+      [("x","%p. Phi (fst p) (snd p)")] spec)));
+
+
+(*---------------------------------------------------------------------------
+ * Some theorems about transitivity of WF combinators. Only the last
+ * (transR) is used, in the proof of termination. The others are generic and
+ * should maybe go somewhere.
+ *---------------------------------------------------------------------------*)
+goalw WF1.thy [trans_def,lex_prod_def,mem_Collect_eq RS eq_reflection]
+           "trans R1 & trans R2 --> trans (R1 ** R2)";
+by (my_strip_tac 1);
+by (res_inst_tac [("x","a")] exI 1);
+by (res_inst_tac [("x","a'a")] exI 1);
+by (res_inst_tac [("x","b")] exI 1);
+by (res_inst_tac [("x","b'a")] exI 1);
+by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1));
+by (Simp_tac 1);
+by (REPEAT (etac disjE 1));
+by (rtac disjI1 1);
+by (ALLGOALS (fast_tac set_cs));
+val trans_lex_prod = result() RS mp;
+
+
+goalw WF1.thy [trans_def,rprod_def,mem_Collect_eq RS eq_reflection]
+           "trans R1 & trans R2 --> trans (rprod R1  R2)";
+by (my_strip_tac 1);
+by (res_inst_tac [("x","a")] exI 1);
+by (res_inst_tac [("x","a'a")] exI 1);
+by (res_inst_tac [("x","b")] exI 1);
+by (res_inst_tac [("x","b'a")] exI 1);
+by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1));
+by (Simp_tac 1);
+by (fast_tac set_cs 1);
+val trans_rprod = result() RS mp;
+
+
+goalw Unify1.thy [trans_def,inv_image_def,mem_Collect_eq RS eq_reflection]
+ "trans r --> trans (inv_image r f)";
+by (rewrite_tac [fst_conv RS eq_reflection, snd_conv RS eq_reflection]);
+by (fast_tac set_cs 1);
+val trans_inv_image = result() RS mp;
+
+goalw Unify1.thy [R0_def, trans_def, mem_Collect_eq RS eq_reflection]
+ "trans R0";
+by (rewrite_tac [fst_conv RS eq_reflection,snd_conv RS eq_reflection,
+                 ssubset_def, set_eq_subset RS eq_reflection]);
+by (fast_tac set_cs 1);
+val trans_R0 = result();
+
+goalw Unify1.thy [R_def,R1_def,measure_def] "trans R";
+by (REPEAT (resolve_tac[trans_inv_image,trans_lex_prod,conjI, trans_R0,
+                        trans_rprod, trans_inv_image, trans_trancl] 1));
+val transR = result();
+
+
+(*---------------------------------------------------------------------------
+ * The following lemma is used in the last step of the termination proof for 
+ * the nested call in Unify. Loosely, it says that R doesn't care so much
+ * about term structure.
+ *---------------------------------------------------------------------------*)
+goalw Unify1.thy [R_def,lex_prod_def, inv_image_def,point_to_prod_def]
+     "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : R --> \
+    \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : R";
+by (Simp_tac 1);
+by (my_strip_tac 1);
+by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1));
+by (etac disjE 1);
+by (rtac disjI1 1);
+by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
+                \  (vars_of D Un vars_of E Un vars_of F)) = \
+                \ (vars_of A Un (vars_of B Un vars_of C) Un \
+                \  (vars_of D Un (vars_of E Un vars_of F)))" 1);
+by (my_fast_set_tac 2);
+by (Asm_simp_tac 1);
+by (rtac disjI2 1);
+by (etac conjE 1);
+by (Asm_simp_tac 1);
+by (rtac conjI 1);
+by (my_fast_set_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [R1_def, measure_def, rprod_def,
+                                          less_eq, inv_image_def]) 1);
+by (my_strip_tac 1);
+by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1));
+by (asm_full_simp_tac (HOL_ss addsimps [uterm_size_Comb,
+                                        add_Suc_right,add_Suc,add_assoc]) 1);
+val Rassoc = result() RS mp;
+
+
+(*---------------------------------------------------------------------------
+ * Rewriting support.
+ *---------------------------------------------------------------------------*)
+
+val termin_ss = (!simpset addsimps (srange_iff::(subst_rews@al_rews)));
+
+
+(*---------------------------------------------------------------------------
+ * This lemma proves the nested termination condition for the base cases 
+ * 3, 4, and 6. It's a clumsy formulation (requiring two conjuncts, each with
+ * exactly the same proof) of a more general theorem.
+ *---------------------------------------------------------------------------*)
+goal theory "(~(Var x <: M)) --> [(x, M)] = theta -->       \
+\ (! N1 N2. (((N1 <| theta, N2 <| theta), (Comb M N1, Comb (Var x) N2)) : R) \
+\       &   (((N1 <| theta, N2 <| theta), (Comb(Var x) N1, Comb M N2)) : R))";
+by (my_strip_tac 1);
+by (case_tac "Var x = M" 1);
+by (hyp_subst_tac 1);
+by (case_tac "x:(vars_of N1 Un vars_of N2)" 1);
+let val case1 = 
+   EVERY1[R1_tac[id_subst_lemma], rtac conjI, my_fast_set_tac,
+          REPEAT o (rtac exI), REPEAT o (rtac conjI THEN' rtac refl),
+          simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq])];
+in by (rtac conjI 1);
+   by case1;
+   by case1
+end;
+
+let val case2 = 
+   EVERY1[R0_tac[id_subst_lemma],
+          simp_tac (!simpset addsimps [ssubset_def,set_eq_subset]),
+          fast_tac set_cs]
+in by (rtac conjI 1);
+   by case2;
+   by case2
+end;
+
+let val case3 =  
+ EVERY1 [R0_tac[],
+        cut_inst_tac [("s2","[(x, M)]"), ("v2", "x"), ("t2","N1")] Var_elim] 
+ THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq]))
+ THEN cut_inst_tac [("s2","[(x, M)]"),("v2", "x"), ("t2","N2")] Var_elim 1
+ THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq]))
+ THEN EVERY1 [simp_tac (HOL_ss addsimps [ssubset_def]),
+             rtac conjI, simp_tac (HOL_ss addsimps [subset_iff]),
+             my_strip_tac, etac UnE, dtac Var_intro] 
+ THEN dtac Var_intro 2
+ THEN ALLGOALS (asm_full_simp_tac (termin_ss addsimps [set_eq_subset])) 
+ THEN TRYALL (fast_tac set_cs)
+in 
+  by (rtac conjI 1);
+  by case3;
+  by case3
+end;
+val var_elimR = result() RS mp RS mp RS spec RS spec;
+
+
+val Some{nchotomy = subst_nchotomy,...} = 
+    assoc(Thry.datatype_facts theory,"subst");
+
+(*---------------------------------------------------------------------------
+ * Do a case analysis on something of type 'a subst. 
+ *---------------------------------------------------------------------------*)
+
+fun Subst_case_tac theta =
+(cut_inst_tac theta (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1 
+  THEN etac disjE 1 
+  THEN rotate_tac ~1 1 
+  THEN Asm_full_simp_tac 1 
+  THEN etac exE 1
+  THEN rotate_tac ~1 1 
+  THEN Asm_full_simp_tac 1);
+
+
+goals_limit := 1;
+
+(*---------------------------------------------------------------------------
+ * The nested TC. Proved by recursion induction.
+ *---------------------------------------------------------------------------*)
+goalw_cterm [] 
+     (hd(tl(tl(map (cterm_of (sign_of theory) o USyntax.mk_prop) tcs))));
+(*---------------------------------------------------------------------------
+ * The extracted TC needs the scope of its quantifiers adjusted, so our 
+ * first step is to restrict the scopes of N1 and N2.
+ *---------------------------------------------------------------------------*)
+by (subgoal_tac "!M1 M2 theta.  \
+ \     Unify (M1, M2) = Subst theta --> \
+ \    (!N1 N2. ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R)" 1);
+by (fast_tac HOL_cs 1);
+by (rtac allI 1); 
+by (rtac allI 1);
+(* Apply induction *)
+by (res_inst_tac [("xa","M1"),("x","M2")] 
+                 (standard (induction4 RS mp RS spec RS spec)) 1);
+by (simp_tac (!simpset addsimps (rules4::(subst_rews@al_rews))
+                       setloop (split_tac [expand_if])) 1);
+(* 1 *)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (R1_tac[subst_Nil] 1);
+by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1));
+by (simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq]) 1);
+
+(* 3 *)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1);
+by (Simp_tac 1);
+by (rtac refl 1);
+
+(* 4 *)
+by (rtac conjI 1);
+by (strip_tac 1);
+by (rtac (Prim.Rules.CONJUNCT2 var_elimR) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+
+(* 6 *)
+by (rtac conjI 1);
+by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]);
+by (my_strip_tac 1);
+by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1);
+by (assume_tac 1);
+by (rtac refl 1);
+
+(* 7 *)
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (etac conjE 1);
+by (Subst_case_tac [("v","Unify(M1a, M2a)")]);
+by (REPEAT (eres_inst_tac [("x","list")] allE 1));
+by (asm_full_simp_tac  HOL_ss 1);
+by (subgoal_tac "((N1 <| list, N2 <| list), Comb M1a N1, Comb M2a N2) : R" 1);
+by (asm_simp_tac HOL_ss 2);
+by (dtac mp 1);
+by (assume_tac 1);
+
+by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
+by (eres_inst_tac [("x","lista")] allE 1);
+by (asm_full_simp_tac  HOL_ss 1);
+
+by (rtac allI 1);
+by (rtac impI 1);
+
+by (hyp_subst_tac 1);
+by (REPEAT (rtac allI 1));
+by (rename_tac "foo bar M1 N1 M2 N2 theta sigma gamma P1 P2" 1);
+by (simp_tac (HOL_ss addsimps [subst_comp]) 1);
+by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1);
+by (fast_tac HOL_cs 1);
+by (simp_tac (HOL_ss addsimps [symmetric (subst_Comb RS eq_reflection)]) 1);
+by (subgoal_tac "((Comb N1 P1 <| theta, Comb N2 P2 <| theta), \
+                \ (Comb M1 (Comb N1 P1), Comb M2 (Comb N2 P2))) :R" 1);
+by (asm_simp_tac HOL_ss 2);
+by (rtac Rassoc 1);
+by (assume_tac 1);
+val Unify_TC2 = result();
+
+
+(*---------------------------------------------------------------------------
+ * Now for elimination of nested TC from rules and induction. This step 
+ * would be easier if "rewrite_rule" used context.
+ *---------------------------------------------------------------------------*)
+goal theory 
+ "(Unify (Comb M1 N1, Comb M2 N2) =  \
+\   (case Unify (M1, M2) of Fail => Fail \
+\    | Subst theta => \
+\        (case if ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R \
+\              then Unify (N1 <| theta, N2 <| theta) else @ z. True of \
+\        Fail => Fail | Subst sigma => Subst (theta <> sigma)))) \
+\  = \
+\ (Unify (Comb M1 N1, Comb M2 N2) = \
+\   (case Unify (M1, M2)  \
+\      of Fail => Fail \
+\      | Subst theta => (case Unify (N1 <| theta, N2 <| theta) \
+\                          of Fail => Fail  \
+\                           | Subst sigma => Subst (theta <> sigma))))";
+by (cut_inst_tac [("v","Unify(M1, M2)")]
+                 (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1);
+by (etac disjE 1);
+by (Asm_simp_tac 1);
+by (etac exE 1);
+by (Asm_simp_tac 1);
+by (cut_inst_tac 
+     [("x","list"), ("xb","N1"), ("xa","N2"),("xc","M2"), ("xd","M1")]
+     (standard(Unify_TC2 RS spec RS spec RS spec RS spec RS spec)) 1);
+by (Asm_full_simp_tac 1);
+val Unify_rec_simpl = result() RS eq_reflection;
+
+val Unify_rules = rewrite_rule[Unify_rec_simpl] rules4;
+
+
+goal theory 
+ "(! M1 N1 M2 N2.  \
+\       (! theta.  \
+\           Unify (M1, M2) = Subst theta -->  \
+\           ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R -->  \
+\           ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 -->  \
+\       ?Phi (Comb M1 N1) (Comb M2 N2))  \
+\    =  \
+\ (! M1 N1 M2 N2.  \
+\       (! theta.  \
+\           Unify (M1, M2) = Subst theta -->  \
+\           ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 -->  \
+\       ?Phi (Comb M1 N1) (Comb M2 N2))";
+by (simp_tac (HOL_ss addsimps [Unify_TC2]) 1);
+val Unify_induction = rewrite_rule[result() RS eq_reflection] induction4;
+
+
+
+(*---------------------------------------------------------------------------
+ * Correctness. Notice that idempotence is not needed to prove that the 
+ * algorithm terminates and is not needed to prove the algorithm correct, 
+ * if you are only interested in an MGU. This is in contrast to the
+ * approach of M&W, who used idempotence and MGU-ness in the termination proof.
+ *---------------------------------------------------------------------------*)
+
+goal theory "!theta. Unify (P,Q) = Subst theta --> MGUnifier theta P Q";
+by (res_inst_tac [("xa","P"),("x","Q")] 
+                 (standard (Unify_induction RS mp RS spec RS spec)) 1);
+by (simp_tac (!simpset addsimps [Unify_rules] 
+                       setloop (split_tac [expand_if])) 1);
+(*1*)
+by (rtac conjI 1);
+by (REPEAT (rtac allI 1));
+by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
+by (my_strip_tac 1);
+by (rtac MoreGen_Nil 1);
+
+(*3*)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac (mgu_sym RS iffD1) 1);
+by (rtac MGUnifier_Var 1);
+by (Simp_tac 1);
+
+(*4*)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac MGUnifier_Var 1);
+by (assume_tac 1);
+
+(*6*)
+by (rtac conjI 1);
+by (rewrite_tac NNF_rews);
+by (my_strip_tac 1);
+by (rtac (mgu_sym RS iffD1) 1);
+by (rtac MGUnifier_Var 1);
+by (Asm_simp_tac 1);
+
+(*7*)
+by (safe_tac HOL_cs);
+by (Subst_case_tac [("v","Unify(M1, M2)")]);
+by (REPEAT (eres_inst_tac[("x","list")] allE 1));
+by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
+by (eres_inst_tac[("x","lista")] allE 1);
+by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+by prune_params_tac;
+by (rename_tac "M1 N1 M2 N2 theta sigma" 1);
+
+by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1);
+by (rtac conjI 1);
+by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*)
+by (Simp_tac 1);
+by (safe_tac HOL_cs);
+by (rename_tac "M1 N1 M2 N2 theta sigma gamma" 1);
+
+by (rewrite_tac [MoreGeneral_def]);
+by (eres_inst_tac [("x","gamma")] allE 1);
+by (Asm_full_simp_tac 1);
+by (etac exE 1);
+by (rename_tac "M1 N1 M2 N2 theta sigma gamma theta1" 1);
+by (eres_inst_tac [("x","theta1")] allE 1);
+by (subgoal_tac "N1 <| theta <| theta1 = N2 <| theta <| theta1" 1);
+
+by (simp_tac (HOL_ss addsimps [subst_comp RS sym]) 2);
+by (rtac subst_subst2 2);
+by (assume_tac 3);
+by (assume_tac 2);
+
+by (dtac mp 1);
+by (assume_tac 1);
+by (etac exE 1);
+
+by (rename_tac "M1 N1 M2 N2 theta sigma gamma theta1 sigma1" 1);
+by (res_inst_tac [("x","sigma1")] exI 1);
+by (rtac subst_trans 1);
+by (assume_tac 1);
+by (rtac subst_trans 1);
+by (rtac subst_sym 2);
+by (rtac comp_assoc 2);
+by (rtac subst_cong 1);
+by (assume_tac 2);
+by (simp_tac (HOL_ss addsimps [subst_eq_def]) 1);
+val Unify_gives_MGU = standard(result() RS spec RS mp);
+
+
+(*---------------------------------------------------------------------------
+ * Unify returns idempotent substitutions, when it succeeds.
+ *---------------------------------------------------------------------------*)
+goal theory "!theta. Unify (P,Q) = Subst theta --> Idem theta";
+by (res_inst_tac [("xa","P"),("x","Q")] 
+                 (standard (Unify_induction RS mp RS spec RS spec)) 1);
+by (simp_tac (!simpset addsimps [Unify_rules] 
+                       setloop (split_tac [expand_if])) 1);
+(*1*)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac Idem_Nil 1);
+
+(*3*)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac Var_Idem 1);
+by (Simp_tac 1);
+
+(*4*)
+by (rtac conjI 1);
+by (my_strip_tac 1);
+by (rtac Var_Idem 1);
+by (atac 1);
+
+(*6*)
+by (rtac conjI 1);
+by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]);
+by (my_strip_tac 1);
+by (rtac Var_Idem 1);
+by (atac 1);
+
+(*7*)
+by (safe_tac HOL_cs);
+by (Subst_case_tac [("v","Unify(M1, M2)")]);
+by (REPEAT (eres_inst_tac[("x","list")] allE 1));
+by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
+by (eres_inst_tac[("x","lista")] allE 1);
+by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+by prune_params_tac;
+by (rename_tac "M1 N1 M2 N2 theta sigma" 1);
+
+by (dtac Unify_gives_MGU 1);
+by (dtac Unify_gives_MGU 1);
+by (rewrite_tac [MGUnifier_def]);
+by (my_strip_tac 1);
+by (rtac Idem_comp 1);
+by (atac 1);
+by (atac 1);
+
+by (rewrite_tac [MGUnifier_def]);
+by (my_strip_tac 1);
+by (eres_inst_tac [("x","q")] allE 1);
+by (Asm_full_simp_tac 1);
+by (rewrite_tac [MoreGeneral_def]);
+by (my_strip_tac 1);
+by (asm_full_simp_tac(termin_ss addsimps [subst_eq_iff,subst_comp,Idem_def])1);
+val Unify_gives_Idem = result();
+
+
+
+(*---------------------------------------------------------------------------
+ * Exercise. The given algorithm is a bit inelegant. What about the
+ * following "improvement", which adds a few recursive calls in former
+ * base cases? It seems that the termination relation needs another
+ * case in the lexico. product.
+
+val {theory,induction,rules,tcs,typechecks} =
+Rfunc Unify.thy ??
+  `(Unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail))    &
+   (Unify(Const m, Comb M N) = Fail)                                 &
+   (Unify(Const m, Var v)    = Unify(Var v, Const m))                &
+   (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) &
+   (Unify(Comb M N, Const x) = Fail)                                 &
+   (Unify(Comb M N, Var v) = Unify(Var v, Comb M N))                 &
+   (Unify(Comb M1 N1, Comb M2 N2) = 
+      (case Unify(M1,M2)
+        of Fail => Fail
+         | Subst theta => (case Unify(N1 <| theta, N2 <| theta)
+                            of Fail => Fail
+                             | Subst sigma => Subst (theta <> sigma))))`;
+
+ *---------------------------------------------------------------------------*)
diff -r 3902e9af752f -r 21266526ac42 TFL/examples/Subst/Unify1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Unify1.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,26 @@
+Unify1 = Unifier + WF1 + "NNF" + 
+
+datatype 'a subst = Fail | Subst ('a list)
+
+consts
+
+ "##"  :: "('a => 'b) => ('a => 'c) => 'a => ('b * 'c)"  (infixr 50)
+   R0  :: "('a set * 'a set) set"
+   R1  :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+   R   :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+
+
+rules
+
+  point_to_prod_def "(f ## g) x == (f x, g x)"
+
+  (* finite proper subset -- should go in WF1.thy maybe *)
+  R0_def "R0 == {p. fst p < snd p & finite(snd p)}"
+
+  R1_def "R1 == rprod (measure uterm_size) (measure uterm_size)"
+
+  (* The termination relation for the Unify function *)
+  R_def  "R == inv_image  (R0 ** R1)
+                          ((%(x,y). vars_of x Un vars_of y) ## (%x.x))"
+
+end