# HG changeset patch
# User clasohm
# Date 795788548 -3600
# Node ID 3cdaa87241757cde87670648c63e83e72dd02823
# Parent  bfcb53497a99050710535730535b760bcd461113
converted Subst with curried function application

diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/AList.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/AList.ML	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,33 @@
+(*  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 list_ss 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 bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/AList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/AList.thy	Tue Mar 21 13:22:28 1995 +0100
@@ -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 bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/ROOT.ML	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,37 @@
+(*  Title: 	CHOL/Subst
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Substitution and Unification in Higher-Order Logic. 
+
+Implements Manna & Waldinger's formalization, with Paulson's simplifications:
+
+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        -  inductive data type of terms
+utlemmas     -  definition of occurs and vars_of for terms
+subst        -  substitutions
+unifier      -  specification of unification and conditions for 
+                correctness and termination
+
+To load, go to the parent directory and type use"Subst/ROOT.ML";
+*)
+
+CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
+
+writeln"Root file for Substitutions and Unification";
+loadpath := ["Subst"];
+use_thy "Subst/Setplus";
+
+use_thy "Subst/AList";
+use_thy "Subst/UTerm";
+use_thy "Subst/UTLemmas";
+
+use_thy "Subst/Subst";
+use_thy "Subst/Unifier";
+writeln"END: Root file for Substitutions and Unification";
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/Setplus.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Setplus.ML	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,64 @@
+(*  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;
+
+(*********)
+
+(*** 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 (set_ss 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 (set_ss 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;
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/Setplus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Setplus.thy	Tue Mar 21 13:22:28 1995 +0100
@@ -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 = Set + 
+
+rules
+
+  ssubset_def    "A < B == A <= B & ~ A=B"
+
+end
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/Subst.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Subst.ML	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,186 @@
+(*  Title: 	Substitutions/subst.ML
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For subst.thy.  
+*)
+
+open Subst;
+
+(***********)
+
+val subst_defs = [subst_def,comp_def,sdom_def];
+
+val raw_subst_ss = utlemmas_ss addsimps al_rews;
+
+local fun mk_thm s = prove_goalw Subst.thy subst_defs s 
+                                 (fn _ => [simp_tac raw_subst_ss 1])
+in val subst_rews = map mk_thm 
+["Const(c) <| al = Const(c)",
+ "Comb t u <| al = Comb (t <| al) (u <| al)",
+ "[] <> bl = bl",
+ "(<a,b>#al) <> bl = <a,b <| bl> # (al <> bl)",
+ "sdom([]) = {}",
+ "sdom(<a,b>#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
+\                               else (sdom al) Un {a})"
+];
+   (* This rewrite isn't always desired *)
+   val Var_subst = mk_thm "Var(x) <| al = assoc x (Var x) al";
+end;
+
+val subst_ss = raw_subst_ss addsimps subst_rews;
+
+(**** Substitutions ****)
+
+goal Subst.thy "t <| [] = t";
+by (uterm_ind_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
+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  = 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 (subst_ss addsimps [Var_subst])));
+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_ind_tac "t" 1);
+by (REPEAT (etac rev_mp 3));
+by (ALLGOALS (asm_simp_tac subst_ss));
+by (ALLGOALS (fast_tac HOL_cs));
+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  = 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  = 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);
+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 (subst_ss 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 ****)
+
+goal Subst.thy "s <> [] = s";
+by (alist_ind_tac "s" 1);
+by (ALLGOALS (asm_simp_tac (subst_ss addsimps [subst_Nil])));
+qed "comp_Nil";
+
+goal Subst.thy "(t <| r <> s) = (t <| r <| s)";
+by (uterm_ind_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
+by (alist_ind_tac "r" 1);
+by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst,subst_Nil]
+                                     setloop (split_tac [expand_if]))));
+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);
+qed "comp_assoc";
+
+goal Subst.thy "<w,Var(w) <| s>#s =s= s"; 
+by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
+by (uterm_ind_tac "t" 1);
+by (REPEAT (etac rev_mp 3));
+by (ALLGOALS (simp_tac (subst_ss addsimps[Var_subst]
+                                 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 (subst_ss 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 (subst_ss addsimps [Var_subst]
+                            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_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));
+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  = 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_ind_tac "t" 1);
+by (REPEAT_SOME (etac rev_mp ));
+by (ALLGOALS (simp_tac (subst_ss 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 (subst_ss 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 subst_ss 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 (subst_ss addsimps [invariance]) 1);
+by (fast_tac set_cs 1);
+val subst_not_empty  = store_thm("subst_not_empty", result() RS mp);
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/Subst.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Subst.thy	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,37 @@
+(*  Title: 	Substitutions/subst.thy
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Substitutions on uterms
+*)
+
+Subst = Setplus + AList + UTLemmas +
+
+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"
+
+rules 
+
+  subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
+
+  subst_def    
+  "t <| al == uterm_rec t (%x.assoc x (Var x) al)	\
+\                         (%x.Const(x))			\
+\                         (%u v q r.Comb q r)"
+
+  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 Int Compl({x}) else g Un {x})"
+  srange_def   
+  "srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
+
+end
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/UTLemmas.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/UTLemmas.ML	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,77 @@
+(*  Title: 	Substitutions/UTLemmas.ML
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For UTLemmas.thy.  
+*)
+
+open UTLemmas;
+
+(***********)
+
+val utlemmas_defs = [vars_of_def,occs_def];
+
+local fun mk_thm s = prove_goalw UTLemmas.thy utlemmas_defs s 
+                                 (fn _ => [simp_tac uterm_ss 1])
+in val utlemmas_rews = map mk_thm 
+      ["vars_of(Const(c)) = {}",
+       "vars_of(Var(x)) = {x}",
+       "vars_of(Comb t u) = vars_of(t) Un vars_of(u)",
+       "t <: Const(c) = False",
+       "t <: Var(x) = False",
+       "t <: Comb u v = (t=u | t=v | t <: u | t <: v)"];
+end;
+
+val utlemmas_ss = prod_ss addsimps (setplus_rews @ uterm_rews @ utlemmas_rews);
+
+(****  occs irrefl ****)
+
+goal UTLemmas.thy  "t <: u & u <: v --> t <: v";
+by (uterm_ind_tac "v" 1);
+by (ALLGOALS (simp_tac utlemmas_ss));
+by (fast_tac HOL_cs 1);
+val occs_trans  = store_thm("occs_trans", conjI RS (result() RS mp));
+
+goal UTLemmas.thy   "~ t <: v --> ~ t <: u | ~ u <: v";
+by (fast_tac (HOL_cs addIs [occs_trans]) 1);
+val contr_occs_trans  = store_thm("contr_occs_trans", result() RS mp);
+
+goal UTLemmas.thy   "t <: Comb t u";
+by (simp_tac utlemmas_ss 1);
+qed "occs_Comb1";
+
+goal UTLemmas.thy  "u <: Comb t u";
+by (simp_tac utlemmas_ss 1);
+qed "occs_Comb2";
+
+goal HOL.thy  "(~(P|Q)) = (~P & ~Q)";
+by (fast_tac HOL_cs 1);
+qed "demorgan_disj";
+
+goal UTLemmas.thy  "~ t <: t";
+by (uterm_ind_tac "t" 1);
+by (ALLGOALS (simp_tac (utlemmas_ss addsimps [demorgan_disj])));
+by (REPEAT (resolve_tac [impI,conjI] 1 ORELSE
+            (etac contrapos 1 THEN etac subst 1 THEN 
+             resolve_tac [occs_Comb1,occs_Comb2] 1) ORELSE
+            (etac (contr_occs_trans RS disjE) 1 THEN assume_tac 2) ORELSE
+            eresolve_tac ([occs_Comb1,occs_Comb2] RLN(2,[notE])) 1));
+qed "occs_irrefl";
+
+goal UTLemmas.thy  "t <: u --> ~t=u";
+by (fast_tac (HOL_cs addEs [occs_irrefl RS notE]) 1);
+val occs_irrefl2  = store_thm("occs_irrefl2", result() RS mp);
+
+
+(**** vars_of lemmas  ****)
+
+goal UTLemmas.thy "(v : vars_of(Var(w))) = (w=v)";
+by (simp_tac utlemmas_ss 1);
+by (fast_tac HOL_cs 1);
+qed "vars_var_iff";
+
+goal UTLemmas.thy  "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)";
+by (uterm_ind_tac "t" 1);
+by (ALLGOALS (simp_tac utlemmas_ss));
+by (fast_tac HOL_cs 1);
+qed "vars_iff_occseq";
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/UTLemmas.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/UTLemmas.thy	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,20 @@
+(*  Title: 	Substitutions/utermlemmas.thy
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Additional definitions for uterms that are not part of the basic inductive definition.
+*)
+
+UTLemmas = UTerm + Setplus +
+
+consts
+
+  vars_of       ::   "'a uterm=>'a set"
+  "<:"          ::   "['a uterm,'a uterm]=>bool"   (infixl 54) 
+
+rules  (*Definitions*)
+
+  vars_of_def   "vars_of(t) == uterm_rec t (%x.{x}) (%x.{}) (%u v q r.q Un r)"
+  occs_def      "s <: t == uterm_rec t (%x.False) (%x.False) (%u v q r.s=u | s=v | q | r)"
+
+end
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/UTerm.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/UTerm.ML	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,270 @@
+(*  Title: 	Substitutions/uterm.ML
+    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;
+
+val uterm_con_defs = [VAR_def, CONST_def, COMB_def];
+
+goal UTerm.thy "uterm(A) = A <+> A <+> (uterm(A) <*> uterm(A))";
+let val rew = rewrite_rule uterm_con_defs in  
+by (fast_tac (univ_cs addSIs (equalityI :: map rew uterm.intrs)
+                      addEs [rew uterm.elim]) 1)
+end;
+qed "uterm_unfold";
+
+(** the uterm functional **)
+
+(*This justifies using uterm in other recursive type definitions*)
+goalw UTerm.thy uterm.defs "!!A B. A<=B ==> uterm(A) <= uterm(B)";
+by (REPEAT (ares_tac (lfp_mono::basic_monos) 1));
+qed "uterm_mono";
+
+(** Type checking rules -- uterm creates well-founded sets **)
+
+goalw UTerm.thy (uterm_con_defs @ uterm.defs) "uterm(sexp) <= sexp";
+by (rtac lfp_lowerbound 1);
+by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
+qed "uterm_sexp";
+
+(* A <= sexp ==> uterm(A) <= sexp *)
+bind_thm ("uterm_subset_sexp", ([uterm_mono, uterm_sexp] MRS subset_trans));
+
+(** Induction **)
+
+(*Induction for the type 'a uterm *)
+val prems = goalw UTerm.thy [Var_def,Const_def,Comb_def]
+    "[| !!x.P(Var(x));  !!x.P(Const(x));  \
+\       !!u v. [|  P(u);  P(v) |] ==> P(Comb u v) |]  ==> P(t)";
+by (rtac (Rep_uterm_inverse RS subst) 1);   (*types force good instantiation*)
+by (rtac (Rep_uterm RS uterm.induct) 1);
+by (REPEAT (ares_tac prems 1
+     ORELSE eresolve_tac [rangeE, ssubst, Abs_uterm_inverse RS subst] 1));
+qed "uterm_induct";
+
+(*Perform induction on xs. *)
+fun uterm_ind_tac a M = 
+    EVERY [res_inst_tac [("t",a)] uterm_induct M,
+	   rename_last_tac a ["1"] (M+1)];
+
+
+(*** Isomorphisms ***)
+
+goal UTerm.thy "inj(Rep_uterm)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_uterm_inverse 1);
+qed "inj_Rep_uterm";
+
+goal UTerm.thy "inj_onto Abs_uterm (uterm (range Leaf))";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_uterm_inverse 1);
+qed "inj_onto_Abs_uterm";
+
+(** Distinctness of constructors **)
+
+goalw UTerm.thy uterm_con_defs "~ CONST(c) = COMB u v";
+by (rtac notI 1);
+by (etac (In1_inject RS (In0_not_In1 RS notE)) 1);
+qed "CONST_not_COMB";
+bind_thm ("COMB_not_CONST", (CONST_not_COMB RS not_sym));
+bind_thm ("CONST_neq_COMB", (CONST_not_COMB RS notE));
+val COMB_neq_CONST = sym RS CONST_neq_COMB;
+
+goalw UTerm.thy uterm_con_defs "~ COMB u v = VAR(x)";
+by (rtac In1_not_In0 1);
+qed "COMB_not_VAR";
+bind_thm ("VAR_not_COMB", (COMB_not_VAR RS not_sym));
+bind_thm ("COMB_neq_VAR", (COMB_not_VAR RS notE));
+val VAR_neq_COMB = sym RS COMB_neq_VAR;
+
+goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)";
+by (rtac In0_not_In1 1);
+qed "VAR_not_CONST";
+bind_thm ("CONST_not_VAR", (VAR_not_CONST RS not_sym));
+bind_thm ("VAR_neq_CONST", (VAR_not_CONST RS notE));
+val CONST_neq_VAR = sym RS VAR_neq_CONST;
+
+
+goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb u v";
+by (rtac (CONST_not_COMB RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
+qed "Const_not_Comb";
+bind_thm ("Comb_not_Const", (Const_not_Comb RS not_sym));
+bind_thm ("Const_neq_Comb", (Const_not_Comb RS notE));
+val Comb_neq_Const = sym RS Const_neq_Comb;
+
+goalw UTerm.thy [Comb_def,Var_def] "~ Comb u v = Var(x)";
+by (rtac (COMB_not_VAR RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
+qed "Comb_not_Var";
+bind_thm ("Var_not_Comb", (Comb_not_Var RS not_sym));
+bind_thm ("Comb_neq_Var", (Comb_not_Var RS notE));
+val Var_neq_Comb = sym RS Comb_neq_Var;
+
+goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)";
+by (rtac (VAR_not_CONST RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
+qed "Var_not_Const";
+bind_thm ("Const_not_Var", (Var_not_Const RS not_sym));
+bind_thm ("Var_neq_Const", (Var_not_Const RS notE));
+val Const_neq_Var = sym RS Var_neq_Const;
+
+
+(** Injectiveness of CONST and Const **)
+
+val inject_cs = HOL_cs addSEs [Scons_inject] 
+                       addSDs [In0_inject,In1_inject];
+
+goalw UTerm.thy [VAR_def] "(VAR(M)=VAR(N)) = (M=N)";
+by (fast_tac inject_cs 1);
+qed "VAR_VAR_eq";
+
+goalw UTerm.thy [CONST_def] "(CONST(M)=CONST(N)) = (M=N)";
+by (fast_tac inject_cs 1);
+qed "CONST_CONST_eq";
+
+goalw UTerm.thy [COMB_def] "(COMB K L = COMB M N) = (K=M & L=N)";
+by (fast_tac inject_cs 1);
+qed "COMB_COMB_eq";
+
+bind_thm ("VAR_inject", (VAR_VAR_eq RS iffD1));
+bind_thm ("CONST_inject", (CONST_CONST_eq RS iffD1));
+bind_thm ("COMB_inject", (COMB_COMB_eq RS iffD1 RS conjE));
+
+
+(*For reasoning about abstract uterm constructors*)
+val uterm_cs = set_cs addIs uterm.intrs @ [Rep_uterm]
+	              addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST,
+			      COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR,
+			      COMB_inject]
+		      addSDs [VAR_inject,CONST_inject,
+			      inj_onto_Abs_uterm RS inj_ontoD,
+			      inj_Rep_uterm RS injD, Leaf_inject];
+
+goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)";
+by (fast_tac uterm_cs 1);
+qed "Var_Var_eq";
+bind_thm ("Var_inject", (Var_Var_eq RS iffD1));
+
+goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)";
+by (fast_tac uterm_cs 1);
+qed "Const_Const_eq";
+bind_thm ("Const_inject", (Const_Const_eq RS iffD1));
+
+goalw UTerm.thy [Comb_def] "(Comb u v =Comb x y) = (u=x & v=y)";
+by (fast_tac uterm_cs 1);
+qed "Comb_Comb_eq";
+bind_thm ("Comb_inject", (Comb_Comb_eq RS iffD1 RS conjE));
+
+val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A";
+by (rtac (major RS setup_induction) 1);
+by (etac uterm.induct 1);
+by (ALLGOALS (fast_tac uterm_cs));
+qed "VAR_D";
+
+val [major] = goal UTerm.thy "CONST(M): uterm(A) ==> M : A";
+by (rtac (major RS setup_induction) 1);
+by (etac uterm.induct 1);
+by (ALLGOALS (fast_tac uterm_cs));
+qed "CONST_D";
+
+val [major] = goal UTerm.thy
+    "COMB M N: uterm(A) ==> M: uterm(A) & N: uterm(A)";
+by (rtac (major RS setup_induction) 1);
+by (etac uterm.induct 1);
+by (ALLGOALS (fast_tac uterm_cs));
+qed "COMB_D";
+
+(*Basic ss with constructors and their freeness*)
+val uterm_free_simps = uterm.intrs @
+                       [Const_not_Comb,Comb_not_Var,Var_not_Const,
+			Comb_not_Const,Var_not_Comb,Const_not_Var,
+			Var_Var_eq,Const_Const_eq,Comb_Comb_eq,
+			CONST_not_COMB,COMB_not_VAR,VAR_not_CONST,
+			COMB_not_CONST,VAR_not_COMB,CONST_not_VAR,
+			VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq];
+val uterm_free_ss = HOL_ss addsimps uterm_free_simps;
+
+goal UTerm.thy "!u. t~=Comb t u";
+by (uterm_ind_tac "t" 1);
+by (rtac (Var_not_Comb RS allI) 1);
+by (rtac (Const_not_Comb RS allI) 1);
+by (asm_simp_tac uterm_free_ss 1);
+qed "t_not_Comb_t";
+
+goal UTerm.thy "!t. u~=Comb t u";
+by (uterm_ind_tac "u" 1);
+by (rtac (Var_not_Comb RS allI) 1);
+by (rtac (Const_not_Comb RS allI) 1);
+by (asm_simp_tac uterm_free_ss 1);
+qed "u_not_Comb_u";
+
+
+(*** UTerm_rec -- by wf recursion on pred_sexp ***)
+
+val UTerm_rec_unfold =
+    [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
+
+(** conversion rules **)
+
+goalw UTerm.thy [VAR_def] "UTerm_rec (VAR x) b c d = b(x)";
+by (rtac (UTerm_rec_unfold RS trans) 1);
+by (simp_tac (HOL_ss addsimps [Case_In0]) 1);
+qed "UTerm_rec_VAR";
+
+goalw UTerm.thy [CONST_def] "UTerm_rec (CONST x) b c d = c(x)";
+by (rtac (UTerm_rec_unfold RS trans) 1);
+by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1);
+qed "UTerm_rec_CONST";
+
+goalw UTerm.thy [COMB_def]
+    "!!M N. [| M: sexp;  N: sexp |] ==> 	\
+\           UTerm_rec (COMB M N) b c d = \
+\           d M N (UTerm_rec M b c d) (UTerm_rec N b c d)";
+by (rtac (UTerm_rec_unfold RS trans) 1);
+by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1);
+by (asm_simp_tac (pred_sexp_ss addsimps [In1_def]) 1);
+qed "UTerm_rec_COMB";
+
+(*** uterm_rec -- by UTerm_rec ***)
+
+val Rep_uterm_in_sexp =
+    Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD);
+
+val uterm_rec_simps = 
+    uterm.intrs @
+    [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, 
+     Abs_uterm_inverse, Rep_uterm_inverse, 
+     Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp];
+val uterm_rec_ss = HOL_ss addsimps uterm_rec_simps;
+
+goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)";
+by (simp_tac uterm_rec_ss 1);
+qed "uterm_rec_Var";
+
+goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec (Const x) b c d = c(x)";
+by (simp_tac uterm_rec_ss 1);
+qed "uterm_rec_Const";
+
+goalw UTerm.thy [uterm_rec_def, Comb_def]
+   "uterm_rec (Comb u v) b c d = d u v (uterm_rec u b c d) (uterm_rec v b c d)";
+by (simp_tac uterm_rec_ss 1);
+qed "uterm_rec_Comb";
+
+val uterm_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB,
+		 uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb];
+val uterm_ss = uterm_free_ss addsimps uterm_simps;
+
+
+(**********)
+
+val uterm_rews = [uterm_rec_Var,uterm_rec_Const,uterm_rec_Comb,
+		  t_not_Comb_t,u_not_Comb_u,
+                  Const_not_Comb,Comb_not_Var,Var_not_Const,
+                  Comb_not_Const,Var_not_Comb,Const_not_Var,
+                  Var_Var_eq,Const_Const_eq,Comb_Comb_eq];
+
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/UTerm.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/UTerm.thy	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,65 @@
+(*  Title: 	Substitutions/UTerm.thy
+    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.
+*)
+
+UTerm = Sexp +
+
+types uterm 1
+
+arities 
+  uterm     :: (term)term
+
+consts
+  uterm     :: "'a item set => 'a item set"
+  Rep_uterm :: "'a uterm => 'a item"
+  Abs_uterm :: "'a item => 'a uterm"
+  VAR       :: "'a item => 'a item"
+  CONST     :: "'a item => 'a item"
+  COMB      :: "['a item, 'a item] => 'a item"
+  Var       :: "'a => 'a uterm"
+  Const     :: "'a => 'a uterm"
+  Comb      :: "['a uterm, 'a uterm] => 'a uterm"
+  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, \
+\                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
+  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, \
+\                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
+
+defs
+     (*defining the concrete constructors*)
+  VAR_def  	"VAR(v) == In0(v)"
+  CONST_def  	"CONST(v) == In1(In0(v))"
+  COMB_def 	"COMB t u == In1(In1(t $ u))"
+
+inductive "uterm(A)"
+  intrs
+    VAR_I	   "v:A ==> VAR(v) : uterm(A)"
+    CONST_I  "c:A ==> CONST(c) : uterm(A)"
+    COMB_I   "[| M:uterm(A);  N:uterm(A) |] ==> COMB M N : uterm(A)"
+
+rules
+    (*faking a type definition...*)
+  Rep_uterm 		"Rep_uterm(xs): uterm(range(Leaf))"
+  Rep_uterm_inverse 	"Abs_uterm(Rep_uterm(xs)) = xs"
+  Abs_uterm_inverse 	"M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
+
+defs
+     (*defining the abstract constructors*)
+  Var_def  	"Var(v) == Abs_uterm(VAR(Leaf(v)))"
+  Const_def  	"Const(c) == Abs_uterm(CONST(Leaf(c)))"
+  Comb_def 	"Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
+
+     (*uterm recursion*)
+  UTerm_rec_def	
+   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M \
+\          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
+
+  uterm_rec_def
+   "uterm_rec t b c d == \
+\   UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) \
+\                           (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
+
+end
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/Unifier.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Unifier.ML	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,299 @@
+(*  Title: 	Substitutions/unifier.ML
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For unifier.thy.
+Properties of unifiers.
+Cases for partial correctness of algorithm and conditions for termination.
+*)
+
+open Unifier;
+
+val unify_defs =
+    [Idem_def,Unifier_def,MoreGeneral_def,MGUnifier_def,MGIUnifier_def];
+
+(**** Unifiers ****)
+
+goalw Unifier.thy [Unifier_def] "Unifier s t u = (t <| s = u <| s)";
+by (rtac refl 1);
+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  = 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  = 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);
+qed "MoreGen_iff";
+
+goal Unifier.thy  "[] >> s";
+by (simp_tac (subst_ss addsimps [MoreGen_iff]) 1);
+by (fast_tac (set_cs addIs [refl RS subst_refl]) 1);
+qed "MoreGen_Nil";
+
+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 (subst_ss addsimps [subst_comp]) 1);
+by (fast_tac (set_cs addIs [comp_Nil RS sym RS subst_refl]) 1);
+qed "MGU_iff";
+
+val [prem] = goal Unifier.thy
+     "~ Var(v) <: t ==> MGUnifier [<v,t>] (Var v) t";
+by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 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 (subst_ss addsimps [prem RS Var_not_occs,Var_subst]) 1);
+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  = 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);
+qed "MGIU_iff";
+
+(**** Idempotence ****)
+
+goalw Unifier.thy unify_defs "Idem(s) = (s <> s =s= s)";
+by (rtac refl 1);
+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);
+qed "Idem_iff";
+
+goal Unifier.thy "Idem([])";
+by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
+qed "Idem_Nil";
+
+goal Unifier.thy "~ (Var(v) <: t) --> Idem([<v,t>])";
+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  = 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  = 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  = 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 ***)
+
+val [prem] = goal Unifier.thy
+    "~ 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);
+qed "lemma_lemma";
+
+val prems = goal Unifier.thy 
+    "x : sdom(s) -->  ~x : srange(s) --> \
+\   ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
+\      vars_of(Var(x) <| <x,Var(x)>#s)";
+by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
+by (REPEAT (resolve_tac [impI,disjI2] 1));
+by(res_inst_tac [("x","x")] exI 1);
+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 = 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);
+by (asm_simp_tac (subst_ss addsimps [MGIU_iff,Idem_iff,subset_iff]) 1);
+by (safe_tac set_cs);
+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  = 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);
+qed "not_cong";
+
+val prems = goal Unifier.thy 
+   "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
+\   ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
+\   vars_of(Var(w) <| <x,Var(w)>#s)";
+by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
+by (REPEAT (resolve_tac [impI,disjI1] 1));
+by(res_inst_tac [("x","w")] exI 1);
+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  = 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);
+by (asm_simp_tac (subst_ss addsimps [MGIU_iff,srange_iff,subset_iff]) 1);
+by (simp_tac (subst_ss addsimps [Idem_iff]) 1);
+by (safe_tac set_cs);
+by (eresolve_tac ([spec] RL [impE]) 1);
+by (rtac Cons_Unifier 1);
+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 = store_thm("MGIU_srange", result() RS mp);
+
+(*************** Correctness of a simple unification algorithm ***************)
+(*                                                                           *)
+(*  fun unify Const(m) Const(n) = if m=n then Nil else Fail                  *)
+(*    | unify Const(m) _        = Fail                                       *)
+(*    | unify Var(v)   t        = if Var(v)<:t then Fail else <v,t>#Nil      *)
+(*    | unify Comb(t,u) Const(n) = Fail                                      *)
+(*    | unify Comb(t,u) Var(v)  = if Var(v) <: Comb(t,u) then Fail           *)
+(*                                               else <v,Comb(t,u>#Nil       *)
+(*    | unify Comb(t,u) Comb(v,w) = let s = unify t v                        *)
+(*                                  in if s=Fail then Fail                   *)
+(*                                               else unify (u<|s) (w<|s);   *)
+
+(**** Cases for the partial correctness of the algorithm ****)
+
+goalw Unifier.thy unify_defs "MGIUnifier s t u = MGIUnifier s u t";
+by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp]))));
+qed "Unify_comm";
+
+goal Unifier.thy "MGIUnifier [] (Const n) (Const n)";
+by (simp_tac (subst_ss addsimps
+	      [MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1);
+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 = store_thm("Unify2", result() RS mp);
+
+val [prem] = goalw Unifier.thy [MGIUnifier_def] 
+ "~Var(v) <: t ==> MGIUnifier [<v,t>] (Var v) t";
+by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
+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);
+qed "Unify4";
+
+goal Unifier.thy "ALL l.~Unifier l (Const m) (Comb t u)";
+by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
+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 = 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 = store_thm("Unify7", result() RS mp 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 (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp]) 1);
+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); \
+\      (! q.Unifier q (u <| r) (w <| r) --> s <> q =s= q) |] ==> \
+\   r <> s <> q =s= q";
+val pp = p1 RS (p3 RS spec RS mp);
+by (cut_facts_tac [pp,
+		   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);
+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)";
+by (simp_tac (subst_ss addsimps [MGIU_iff,subst_comp,comp_assoc]) 1);
+by (safe_tac HOL_cs);
+by (REPEAT (etac rev_mp 2));
+by (simp_tac (subst_ss addsimps 
+	      [Unifier_iff,MGIU_iff,subst_comp,comp_assoc]) 2);
+by (ALLGOALS (fast_tac (set_cs addEs 
+			[Unifier_Comb,Unify8_lemma1,Unify8_lemma2])));
+qed "Unify8";
+
+
+(********************** Termination of the algorithm *************************)
+(*                                                                           *)
+(*UWFD is a well-founded relation that orders the 2 recursive calls in unify *)
+(*                   NB well-foundedness of UWFD isn't proved                *)
+
+
+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);
+qed "UnifyWFD1";
+
+val [prem] = goal Unifier.thy 
+     "MGIUnifier s t t' ==> vars_of(u <| s) Un vars_of(u' <| s) <= \
+\                           vars_of (Comb t u) Un vars_of (Comb t' u')";
+by (subgoal_tac "vars_of(u <| s) Un vars_of(u' <| s) <= \
+\                srange(s) Un vars_of(u) Un srange(s) Un vars_of(u')" 1);
+by (etac subset_trans 1);
+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])));
+qed "UWFD2_lemma1";
+
+val [major,minor] = goal Unifier.thy 
+     "[| MGIUnifier s t t';  ~ u <| s = u |] ==> \
+\     ~ vars_of(u <| s) Un vars_of(u' <| s) =  \
+\         (vars_of(t) Un vars_of(u)) Un (vars_of(t') Un vars_of(u'))";
+by (cut_facts_tac 
+    [major RS (MGIU_iff RS iffD1) RS conjunct1 RS (Idem_iff RS iffD1)] 1);
+by (rtac (minor RS subst_not_empty RS exE) 1);
+by (rtac (make_elim ((major RS MGIU_sdom) RS subsetD)) 1 THEN assume_tac 1);
+by (rtac (disjI2 RS (not_equal_iff RS iffD2)) 1);
+by (REPEAT (etac rev_mp 1));
+by (asm_simp_tac subst_ss 1);
+by (fast_tac (set_cs addIs [Var_elim2]) 1);
+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')";
+by (cut_facts_tac 
+    [prem RS UWFD2_lemma1 RS (subseteq_iff_subset_eq RS iffD1)] 1);
+by (imp_excluded_middle_tac "u <| s = u" 1);
+by (simp_tac (set_ss addsimps [occs_Comb2] ) 1);
+by (rtac impI 1 THEN etac subst 1 THEN assume_tac 1);
+by (rtac impI 1);
+by (rtac (conjI RS (ssubset_iff RS iffD2) RS disjI1) 1);
+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);
+qed "UnifyWFD2";
diff -r bfcb53497a99 -r 3cdaa8724175 src/HOL/Subst/Unifier.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Unifier.thy	Tue Mar 21 13:22:28 1995 +0100
@@ -0,0 +1,33 @@
+(*  Title: 	Subst/unifier.thy
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Definition of most general idempotent unifier
+*)
+
+Unifier = Subst +
+
+consts
+
+  Idem       :: "('a*('a uterm))list=> bool"
+  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"
+  MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
+  UWFD       :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool"
+
+rules  (*Definitions*)
+
+  Idem_def         "Idem(s) == s <> s =s= s"
+  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)"
+  MGIUnifier_def   "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
+
+  UWFD_def
+  "UWFD x y x' y' == \
+\    (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  \
+\    (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
+
+end