# HG changeset patch
# User paulson
# Date 863692801 -7200
# Node ID a75558a4ed3773790bb894b3119f054472ce7fb5
# Parent  14bd6e5985f1b1d15084e16f5ed6ca18662124ad
New version, modified by Konrad Slind and LCP for TFL

diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/AList.ML
--- a/src/HOL/Subst/AList.ML	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/AList.ML	Thu May 15 12:40:01 1997 +0200
@@ -7,24 +7,26 @@
 
 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;
+let fun prove s = prove_goalw AList.thy [alist_rec_def,assoc_def] s 
+			  (fn _ => [Simp_tac 1])
+in 
+Addsimps 
+ (
+   map prove 
+   ["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);
+by (induct_tac "l" 1);
+by (split_all_tac 2);
+by (REPEAT (ares_tac prems 1));
 qed "alist_induct";
 
 (*Perform induction on xs. *)
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/AList.thy
--- a/src/HOL/Subst/AList.thy	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/AList.thy	Thu May 15 12:40:01 1997 +0200
@@ -12,7 +12,7 @@
   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
   assoc      :: "['a,'b,('a*'b) list] => 'b"
 
-rules
+defs
 
   alist_rec_def "alist_rec al b c == list_rec b (split c) al"
 
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/ROOT.ML
--- a/src/HOL/Subst/ROOT.ML	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/ROOT.ML	Thu May 15 12:40:01 1997 +0200
@@ -1,32 +1,34 @@
 (*  Title:      HOL/Subst/ROOT.ML
     ID:         $Id$
-    Author:     Martin Coen, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    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:
+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        -  inductive data type of terms
-utlemmas     -  definition of occurs and vars_of for terms
-subst        -  substitutions
-unifier      -  specification of unification and conditions for 
+AList        -  association lists
+UTerm        -  data type of terms
+Subst        -  substitutions
+Unifier      -  specification of unification and conditions for 
                 correctness and termination
+Unify        -  the unification function
 
-To load, go to the parent directory and type use"Subst/ROOT.ML";
+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";
-
-use_thy "Unifier";
+use_thy "Unify";
 
 writeln"END: Root file for Substitutions and Unification";
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Setplus.ML
--- a/src/HOL/Subst/Setplus.ML	Thu May 15 12:29:59 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  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 (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;
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Setplus.thy
--- a/src/HOL/Subst/Setplus.thy	Thu May 15 12:29:59 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  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 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Subst.ML
--- a/src/HOL/Subst/Subst.ML	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/Subst.ML	Thu May 15 12:40:01 1997 +0200
@@ -8,88 +8,73 @@
 
 open Subst;
 
-(***********)
-
-val subst_defs = [subst_def,comp_def,sdom_def];
-
-val raw_subst_ss = simpset_of "UTLemmas" 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 
-                            delsimps [de_Morgan_conj, de_Morgan_disj];
 
 (**** Substitutions ****)
 
 goal Subst.thy "t <| [] = t";
-by (uterm_ind_tac "t" 1);
-by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
+by (induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "subst_Nil";
 
+Addsimps [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);
+by (induct_tac "u" 1);
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp "subst_mono";
 
-goal Subst.thy  "~ (Var(v) <: t) --> t <| (v,t <| s)#s = t <| s";
-by (imp_excluded_middle_tac "t = Var(v)" 1);
+goal Subst.thy  "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
+by (case_tac "t = Var(v)" 1);
+be rev_mp 2;
 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);
+    uterm.induct 2);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+qed_spec_mp "Var_not_occs";
 
 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));
+by (induct_tac "t" 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Blast_tac);
 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);
+by(simp_tac (!simpset addsimps [agreement]
+                      setloop (split_tac [expand_if])) 1);
+qed_spec_mp"repl_invariance";
 
 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);
+by (induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp"Var_in_subst";
+
 
 (**** Equality between Substitutions ****)
 
-goalw Subst.thy [subst_eq_def] "r =s= s = (! t.t <| r = t <| s)";
-by (simp_tac subst_ss 1);
+goalw Subst.thy [subst_eq_def] "r =$= s = (! t.t <| r = t <| s)";
+by (Simp_tac 1);
 qed "subst_eq_iff";
 
-local fun mk_thm s = prove_goal Subst.thy s
+
+local fun prove 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])
+                                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";
+  val subst_refl      = prove "r =$= r";
+  val subst_sym       = prove "r =$= s ==> s =$= r";
+  val subst_trans     = prove "[| q =$= r; r =$= s |] ==> q =$= s";
 end;
 
+
+AddIffs [subst_refl];
+
+
 val eq::prems = goalw Subst.thy [subst_eq_def] 
-    "[| r =s= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)";
+    "[| r =$= 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";
@@ -98,91 +83,128 @@
 
 (**** Composition of Substitutions ****)
 
+let fun prove s = 
+ prove_goalw Subst.thy [comp_def,sdom_def] s (fn _ => [Simp_tac 1])
+in 
+Addsimps
+ (
+   map prove 
+   [ "[] <> 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 (subst_ss addsimps [subst_Nil])));
+by (ALLGOALS Asm_simp_tac);
 qed "comp_Nil";
 
+Addsimps [comp_Nil];
+
+goal Subst.thy "s =$= s <> []";
+by (Simp_tac 1);
+qed "subst_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 (induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
 by (alist_ind_tac "r" 1);
-by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst,subst_Nil]
-                                     setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset 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);
+Addsimps [subst_comp];
+
+goal Subst.thy "(q <> r) <> s =$= q <> (r <> s)";
+by (simp_tac (!simpset addsimps [subst_eq_iff]) 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]))));
+goal Subst.thy "!!s. [| theta =$= theta1; sigma =$= sigma1|] ==> \
+             \       (theta <> sigma) =$= (theta1 <> sigma1)";
+by (asm_full_simp_tac (!simpset addsimps [subst_eq_def]) 1);
+qed "subst_cong";
+
+
+goal Subst.thy "(w, Var(w) <| s) # s =$= s"; 
+by (simp_tac (!simpset addsimps [subst_eq_iff]) 1);
+by (rtac allI 1);
+by (induct_tac "t" 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset 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);
+
+goal Subst.thy "!!s. q <> r =$= s ==>  t <| q <| r = t <| s";
+by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff]) 1);
 qed "comp_subst_subst";
 
+
 (****  Domain and range of Substitutions ****)
 
-goal Subst.thy  "(v : sdom(s)) = (~ Var(v) <| s = Var(v))";
+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);
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
+by (Blast_tac 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);
+by (Blast_tac 1);
 qed "srange_iff";
 
+goalw Set.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
+by (Blast_tac 1);
+qed "empty_iff_all_not";
+
 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));
+by (induct_tac "t" 1);
+by (ALLGOALS
+    (asm_full_simp_tac (!simpset addsimps [empty_iff_all_not, sdom_iff])));
+by (ALLGOALS Blast_tac);
 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);
+goal Subst.thy  "v : sdom(s) -->  v : vars_of(t <| s) --> v : srange(s)";
+by (induct_tac "t" 1);
+by (case_tac "a : sdom(s)" 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff, srange_iff])));
+by (ALLGOALS Blast_tac);
+qed_spec_mp "Var_in_srange";
 
-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. [| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
+by (blast_tac (!claset addIs [Var_in_srange]) 1);
+qed "Var_elim";
 
 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);
+by (induct_tac "t" 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff,srange_iff])));
+by (Blast_tac 2);
+by (REPEAT (step_tac (!claset addIs [vars_var_iff RS iffD1 RS sym]) 1));
+by (Auto_tac());
+qed_spec_mp "Var_intro";
 
 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));
+by (simp_tac (!simpset addsimps [srange_iff]) 1);
+qed_spec_mp "srangeD";
 
-val asms = goal Subst.thy
+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);
+by (simp_tac (!simpset addsimps [empty_iff_all_not]) 1);
+by (fast_tac (!claset addIs [Var_in_srange] addDs [srangeD]) 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);
+goal Subst.thy "!!u. ~ u <| s = u ==> (? x. x : sdom(s))";
+by (full_simp_tac (!simpset addsimps [empty_iff_all_not, invariance]) 1);
+by (Blast_tac 1);
+qed "subst_not_empty";
+
+
+goal Subst.thy "(M <| [(x, Var x)]) = M";
+by (induct_tac "M" 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed "id_subst_lemma";
+
+Addsimps [id_subst_lemma];
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/Subst.thy	Thu May 15 12:40:01 1997 +0200
@@ -5,33 +5,35 @@
 Substitutions on uterms
 *)
 
-Subst = Setplus + AList + UTLemmas +
+Subst = 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)
+  "=$="  ::  "[('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"
+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)"
 
-  subst_def    
-  "t <| al == uterm_rec t (%x.assoc x (Var x) al)       
-                         (%x.Const(x))                  
-                         (%u v q r.Comb q r)"
+
+defs 
 
-  comp_def    "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
+  subst_eq_def  "r =$= 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 Int Compl({x}) else g Un {x})"
+                (%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)})"
+   "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
 
 end
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/UTLemmas.ML
--- a/src/HOL/Subst/UTLemmas.ML	Thu May 15 12:29:59 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(*  Title:      HOL/Subst/UTLemmas.ML
-    ID:         $Id$
-    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 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;
-
-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);
-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 1);
-qed "occs_Comb1";
-
-goal UTLemmas.thy  "u <: Comb t u";
-by (Simp_tac 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 (!simpset 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 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);
-by (fast_tac HOL_cs 1);
-qed "vars_iff_occseq";
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/UTLemmas.thy
--- a/src/HOL/Subst/UTLemmas.thy	Thu May 15 12:29:59 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  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 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/UTerm.ML
--- a/src/HOL/Subst/UTerm.ML	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/UTerm.ML	Thu May 15 12:40:01 1997 +0200
@@ -9,262 +9,37 @@
 
 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 (!claset addSIs (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 (!claset 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 **)
+(**** vars_of lemmas  ****)
 
-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;
+goal UTerm.thy "(v : vars_of(Var(w))) = (w=v)";
+by (Simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed "vars_var_iff";
 
-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));
+goal UTerm.thy  "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)";
+by (induct_tac "t" 1);
+by (ALLGOALS Simp_tac);
+by (fast_tac HOL_cs 1);
+qed "vars_iff_occseq";
 
 
-(*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*)
-Addsimps (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]);
-
-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 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 1);
-qed "u_not_Comb_u";
+(* Not used, but perhaps useful in other proofs *)
+goal UTerm.thy "M<:N --> vars_of(M) <= vars_of(N)";
+by (induct_tac "N" 1);
+by (ALLGOALS Asm_simp_tac);
+by (fast_tac set_cs 1);
+val occs_vars_subset = result();
 
 
-(*** UTerm_rec -- by wf recursion on pred_sexp ***)
-
-goal UTerm.thy
-   "(%M. UTerm_rec M b c d) = wfrec (trancl pred_sexp) \
-   \ (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y)))))";
-by (simp_tac (HOL_ss addsimps [UTerm_rec_def]) 1);
-bind_thm("UTerm_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
-                            ((result() RS eq_reflection) RS def_wfrec));
-
-(*---------------------------------------------------------------------------
- * Old:
- * 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 (!simpset 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 (!simpset addsimps [Case_In0,Case_In1]) 1);
-qed "UTerm_rec_CONST";
+goal UTerm.thy "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)";
+by (Blast_tac 1);
+val monotone_vars_of = result();
 
-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 (!simpset addsimps [Split,Case_In1]) 1);
-by (asm_simp_tac (!simpset 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);
-
-Addsimps [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];
-
-goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)";
-by (Simp_tac 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 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 1);
-qed "uterm_rec_Comb";
-
-Addsimps [uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb];
-
-
-(**********)
-
-val uterm_rews = [t_not_Comb_t,u_not_Comb_u];
+goal UTerm.thy "finite(vars_of M)";
+by (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 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/UTerm.thy	Thu May 15 12:40:01 1997 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Substitutions/UTerm.thy
+(*  Title:      Subst/UTerm.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -6,60 +6,32 @@
 Binary trees with leaves that are constants or variables.
 *)
 
-UTerm = Sexp +
+UTerm = Finite + 
 
-types uterm 1
-
-arities 
-  uterm     :: (term)term
+datatype 'a uterm = Var ('a) 
+                  | Const ('a)
+                  | Comb ('a uterm) ('a uterm)
 
 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
+  vars_of  ::  'a uterm => 'a set
+  "<:"     ::  'a uterm => 'a uterm => bool   (infixl 54) 
+uterm_size ::  'a uterm => nat
+
 
-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))"
+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))"
 
-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))"
+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)"
 
-     (*uterm recursion*)
-  UTerm_rec_def 
-   "UTerm_rec M b c d == wfrec (trancl pred_sexp) 
-    (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y))))) M"
-
-  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)"
+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 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Unifier.ML
--- a/src/HOL/Subst/Unifier.ML	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/Unifier.ML	Thu May 15 12:40:01 1997 +0200
@@ -3,322 +3,103 @@
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For unifier.thy.
+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];
+val unify_defs = [Unifier_def, MoreGeneral_def, MGUnifier_def];
+
+(*---------------------------------------------------------------------------
+ * Unifiers 
+ *---------------------------------------------------------------------------*)
 
-(**** Unifiers ****)
+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_def]) 1);
+qed "Unifier_Comb";
 
-goalw Unifier.thy [Unifier_def] "Unifier s t u = (t <| s = u <| s)";
-by (rtac refl 1);
-qed "Unifier_iff";
+AddIffs [Unifier_Comb];
 
 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);
+  "!!v. [| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
+\       Unifier ((v,r)#s) t u";
+by (asm_full_simp_tac (!simpset addsimps [Unifier_def, repl_invariance]) 1);
+qed "Cons_Unifier";
+
 
-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 
+ *---------------------------------------------------------------------------*)
 
-(**** Most General Unifiers ****)
+goalw Unifier.thy unify_defs "MGUnifier s t u = MGUnifier s u t";
+by (blast_tac (!claset addIs [sym]) 1);
+qed "mgu_sym";
 
-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);
+by (simp_tac (!simpset addsimps [MoreGeneral_def]) 1);
+by (Blast_tac 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);
+AddIffs [MoreGen_Nil];
 
 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]
-		       delsimps (empty_iff::mem_simps)) 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);
-by (rtac 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);
-
-
-(** COULD REPLACE THE TWO THEOREMS ABOVE BY THE FOLLOWING, IN THE PRESENCE
-    OF DEMORGAN LAWS.  DON'T KNOW WHAT TO DO WITH THE SIMILAR PROOF BELOW.
-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);
-by (rtac conjI 1);
-by (asm_simp_tac (subst_ss addsimps [Var_elim,subst_comp,repl_invariance]) 1);
-by (asm_simp_tac (subst_ss addsimps [Var_subst]) 1);
-val MGIU_sdom_lemma = result() RS mp RS mp RS lemma_lemma RSN (2, rev_notE);
-
-goal Unifier.thy "MGIUnifier s t u --> sdom(s) <= vars_of(t) Un vars_of(u)";
-by (asm_simp_tac (subst_ss addsimps [MGIU_iff,Idem_iff,subset_iff]) 1);
-by (deepen_tac (set_cs addIs [Cons_Unifier] addEs [MGIU_sdom_lemma]) 3 1);
-val MGIU_sdom  = store_thm("MGIU_sdom", result() RS mp);
-**)
+    "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)";
+by (auto_tac (!claset addIs [ssubst_subst2, subst_comp_Nil], !simpset));
+qed "MGU_iff";
 
 
-(*** 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 (subst_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);
+goal Unifier.thy
+     "!!v. ~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
+by (simp_tac(!simpset addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
+	              delsimps [subst_Var]) 1);
+by (Step_tac 1);
+br exI 1;
+by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
+by (etac ssubst_subst2 1);
+by (asm_simp_tac (!simpset addsimps [Var_not_occs]) 1);
+qed "MGUnifier_Var";
 
-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";
+AddSIs [MGUnifier_Var];
 
 
-(********************** 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";
+(*---------------------------------------------------------------------------
+ * Idempotence.
+ *---------------------------------------------------------------------------*)
 
-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";
+goalw Unifier.thy [Idem_def] "Idem([])";
+by (Simp_tac 1);
+qed "Idem_Nil";
+
+AddIffs [Idem_Nil];
+
+goalw Unifier.thy [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})";
+by (simp_tac (!simpset addsimps [subst_eq_iff, invariance, 
+				 dom_range_disjoint]) 1);
+qed "Idem_iff";
 
-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";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
+by (simp_tac (!simpset addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
+				 empty_iff_all_not]
+                       setloop (split_tac [expand_if])) 1);
+by (Blast_tac 1);
+qed_spec_mp "Var_Idem";
+
+AddSIs [Var_Idem];
 
-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 (subst_ss delsimps (ssubset_iff :: utlemmas_rews)
-                       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 (subst_ss delsimps (ssubset_iff :: utlemmas_rews) 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";
+goalw Unifier.thy [Idem_def]
+  "!!r. [| Idem(r); Unifier s (t<|r) (u<|r) |]       \
+\       ==> Unifier (r <> s) (t <| r) (u <| r)";
+by (asm_full_simp_tac (!simpset addsimps [Unifier_def, comp_subst_subst]) 1);
+qed "Unifier_Idem_subst";
+
+val [idemr,unifier,minor] = goal Unifier.thy
+     "[| Idem(r);  Unifier s (t <| r) (u <| r); \
+\        !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q \
+\     |] ==> Idem(r <> s)";
+by (cut_facts_tac [idemr,
+                   unifier RS (idemr RS Unifier_Idem_subst RS minor)] 1);
+by (asm_full_simp_tac (!simpset addsimps [Idem_def, subst_eq_iff]) 1);
+qed "Idem_comp";
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Unifier.thy
--- a/src/HOL/Subst/Unifier.thy	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/Unifier.thy	Thu May 15 12:40:01 1997 +0200
@@ -2,32 +2,23 @@
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Definition of most general idempotent unifier
+Definition of most general unifier
 *)
 
-Unifier = Subst +
+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
+  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*)
+defs
 
-  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"
+  MoreGeneral_def  "r >> s == ? q. 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')"
-
+                                       (!r. Unifier r t u --> s >> r)"
+  Idem_def         "Idem(s) == (s <> s) =$= s"
 end
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Unify.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Unify.ML	Thu May 15 12:40:01 1997 +0200
@@ -0,0 +1,323 @@
+(*  Title:      Subst/Unify
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Unification algorithm
+*)
+
+(*---------------------------------------------------------------------------
+ * 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).
+ *---------------------------------------------------------------------------*)
+
+open Unify;
+
+
+
+(*---------------------------------------------------------------------------
+ * The non-nested TC plus the wellfoundedness of unifyRel.
+ *---------------------------------------------------------------------------*)
+Tfl.tgoalw Unify.thy [] unify.rules;
+(* Wellfoundedness of unifyRel *)
+by (simp_tac (!simpset addsimps [unifyRel_def, uterm_less_def,
+				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
+				 wf_rel_prod, wf_measure]) 1);
+(* TC *)
+by (Step_tac 1);
+by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
+				 lex_prod_def, measure_def,
+				 inv_image_def]) 1);
+by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
+by (Blast_tac 1);
+by (asm_simp_tac (!simpset addsimps [rprod_def, less_eq, less_add_Suc1]) 1);
+qed "tc0";
+
+
+(*---------------------------------------------------------------------------
+ * Eliminate tc0 from the recursion equations and the induction theorem.
+ *---------------------------------------------------------------------------*)
+val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
+val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
+                     unify.rules;
+
+val unifyInduct0 = [wfr,tc] MRS unify.induct 
+                  |> read_instantiate [("P","split Q")]
+                  |> rewrite_rule [split RS eq_reflection]
+                  |> standard;
+
+
+(*---------------------------------------------------------------------------
+ * Termination proof.
+ *---------------------------------------------------------------------------*)
+
+goalw Unify.thy [trans_def,inv_image_def]
+    "!!r. trans r ==> trans (inv_image r f)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_inv_image";
+
+goalw Unify.thy [finite_psubset_def, trans_def] "trans finite_psubset";
+by (simp_tac (!simpset addsimps [psubset_def]) 1);
+by (Blast_tac 1);
+qed "trans_finite_psubset";
+
+goalw Unify.thy [unifyRel_def,uterm_less_def,measure_def] "trans unifyRel";
+by (REPEAT (resolve_tac [trans_inv_image,trans_lex_prod,conjI, 
+			 trans_finite_psubset,
+			 trans_rprod, trans_inv_image, trans_trancl] 1));
+qed "trans_unifyRel";
+
+
+(*---------------------------------------------------------------------------
+ * The following lemma is used in the last step of the termination proof for 
+ * the nested call in Unify.  Loosely, it says that unifyRel doesn't care
+ * about term structure.
+ *---------------------------------------------------------------------------*)
+goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
+     "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
+    \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
+by (asm_full_simp_tac (!simpset addsimps [uterm_less_def, measure_def, rprod_def,
+                          less_eq, inv_image_def,add_assoc]) 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 (Blast_tac 2);
+by (Asm_simp_tac 1);
+qed "Rassoc";
+
+
+(*---------------------------------------------------------------------------
+ * This lemma proves the nested termination condition for the base cases 
+ * 3, 4, and 6. 
+ *---------------------------------------------------------------------------*)
+goal Unify.thy
+ "!!x. ~(Var x <: M) ==>        \
+\   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
+\ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
+by (case_tac "Var x = M" 1);
+by (hyp_subst_tac 1);
+by (Simp_tac 1);
+by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
+(*uterm_less case*)
+by (asm_simp_tac
+    (!simpset addsimps [less_eq, unifyRel_def, uterm_less_def,
+			rprod_def, lex_prod_def,
+			measure_def, inv_image_def]) 1);
+by (Blast_tac 1);
+(*finite_psubset case*)
+by (simp_tac
+    (!simpset addsimps [unifyRel_def, lex_prod_def,
+			measure_def, inv_image_def]) 1);
+by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
+				 psubset_def, set_eq_subset]) 1);
+by (Blast_tac 1);
+(** LEVEL 9 **)
+(*Final case, also finite_psubset*)
+by (simp_tac
+    (!simpset addsimps [finite_vars_of, unifyRel_def, finite_psubset_def,
+			lex_prod_def, measure_def, inv_image_def]) 1);
+by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1);
+by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3);
+by (ALLGOALS (asm_simp_tac(!simpset addsimps [srange_iff, vars_iff_occseq])));
+by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI]));
+by (ALLGOALS (asm_full_simp_tac 
+	      (!simpset addsimps [srange_iff, set_eq_subset]))); 
+by (ALLGOALS
+    (fast_tac (!claset addEs [Var_intro RS disjE]
+	               unsafe_addss (!simpset addsimps [srange_iff]))));
+qed "var_elimR";
+
+
+val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst");
+
+(*---------------------------------------------------------------------------
+ * Do a case analysis on something of type 'a subst. 
+ *---------------------------------------------------------------------------*)
+
+fun subst_case_tac t =
+(cut_inst_tac [("x",t)] (subst_nchotomy RS spec) 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);
+
+
+(*---------------------------------------------------------------------------
+ * The nested TC. Proved by recursion induction.
+ *---------------------------------------------------------------------------*)
+val [tc1,tc2,tc3] = unify.tcs;
+goalw_cterm [] (cterm_of (sign_of Unify.thy) (USyntax.mk_prop tc3));
+(*---------------------------------------------------------------------------
+ * 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) : unifyRel)" 1);
+by (Blast_tac 1);
+by (rtac allI 1); 
+by (rtac allI 1);
+(* Apply induction *)
+by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
+			    setloop (split_tac [expand_if]))));
+(*Const-Const case*)
+by (simp_tac
+    (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
+			inv_image_def, less_eq, uterm_less_def, rprod_def]) 1);
+(** LEVEL 7 **)
+(*Comb-Comb case*)
+by (subst_case_tac "unify(M1a, M2a)");
+by (rename_tac "theta" 1);
+by (subst_case_tac "unify(N1 <| theta, N2 <| theta)");
+by (rename_tac "sigma" 1);
+by (REPEAT (rtac allI 1));
+by (rename_tac "P Q" 1); 
+by (rtac (trans_unifyRel RS transD) 1);
+by (Blast_tac 1);
+by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
+by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \
+                \ (Comb M1a (Comb N1 P), Comb M2a (Comb N2 Q))) :unifyRel" 1);
+by (asm_simp_tac HOL_ss 2);
+by (rtac Rassoc 1);
+by (Blast_tac 1);
+qed_spec_mp "unify_TC2";
+
+
+(*---------------------------------------------------------------------------
+ * Now for elimination of nested TC from unify.rules and induction. 
+ *---------------------------------------------------------------------------*)
+
+(*Desired rule, copied from the theory file.  Could it be made available?*)
+goal Unify.thy 
+  "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 (asm_simp_tac (!simpset addsimps unifyRules0) 1);
+by (subst_case_tac "unify(M1, M2)");
+by (asm_simp_tac (!simpset addsimps [unify_TC2]) 1);
+qed "unifyCombComb";
+
+
+val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
+
+Addsimps unifyRules;
+
+val prems = goal Unify.thy 
+"   [| !!m n. Q (Const m) (Const n);      \
+\      !!m M N. Q (Const m) (Comb M N); !!m x. Q (Const m) (Var x);     \
+\      !!x M. Q (Var x) M; !!M N x. Q (Comb M N) (Const x);     \
+\      !!M N x. Q (Comb M N) (Var x);   \
+\      !!M1 N1 M2 N2.   \
+\         (! theta.     \
+\             unify (M1, M2) = Subst theta -->  \
+\             Q (N1 <| theta) (N2 <| theta)) & Q M1 M2   \
+\         ==> Q (Comb M1 N1) (Comb M2 N2) |] ==> Q M1 M2";
+by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps (unify_TC2::prems))));
+qed "unifyInduct";
+
+
+
+(*---------------------------------------------------------------------------
+ * 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 Unify.thy "!theta. unify(P,Q) = Subst theta --> MGUnifier theta P Q";
+by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+(*Const-Const case*)
+by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
+(*Const-Var case*)
+by (stac mgu_sym 1);
+by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
+(*Var-M case*)
+by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
+(*Comb-Var case*)
+by (stac mgu_sym 1);
+by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
+(*Comb-Comb case*)
+by (safe_tac (!claset));
+by (subst_case_tac "unify(M1, M2)");
+by (subst_case_tac "unify(N1<|list, N2<|list)");
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [MGUnifier_def, Unifier_def])1);
+(** LEVEL 13 **)
+by (safe_tac (!claset));
+by (rename_tac "theta sigma gamma" 1);
+by (rewrite_goals_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 "delta" 1);
+by (eres_inst_tac [("x","delta")] allE 1);
+by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
+(*Proving the subgoal*)
+by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2);
+by (blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
+by (blast_tac (!claset addIs [subst_trans, subst_cong, 
+			      comp_assoc RS subst_sym]) 1);
+qed_spec_mp "unify_gives_MGU";
+
+
+(*---------------------------------------------------------------------------
+ * Unify returns idempotent substitutions, when it succeeds.
+ *---------------------------------------------------------------------------*)
+goal Unify.thy "!theta. unify(P,Q) = Subst theta --> Idem theta";
+by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem] 
+			             setloop split_tac[expand_if])));
+(*Comb-Comb case*)
+by (safe_tac (!claset));
+by (subst_case_tac "unify(M1, M2)");
+by (subst_case_tac "unify(N1 <| list, N2 <| list)");
+by (hyp_subst_tac 1);
+by prune_params_tac;
+by (rename_tac "theta sigma" 1);
+(** LEVEL 8 **)
+by (dtac unify_gives_MGU 1);
+by (dtac unify_gives_MGU 1);
+by (rewrite_tac [MGUnifier_def]);
+by (safe_tac (!claset));
+by (rtac Idem_comp 1);
+by (atac 1);
+by (atac 1);
+
+by (eres_inst_tac [("x","q")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [MoreGeneral_def]) 1);
+by (safe_tac (!claset));
+by (asm_full_simp_tac
+    (!simpset addsimps [srange_iff, subst_eq_iff, Idem_def]) 1);
+qed_spec_mp "unify_gives_Idem";
+
diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Unify.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Subst/Unify.thy	Thu May 15 12:40:01 1997 +0200
@@ -0,0 +1,41 @@
+(*  Title:      Subst/Unify
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Unification algorithm
+*)
+
+Unify = Unifier + WF_Rel + 
+
+datatype 'a subst = Fail | Subst ('a list)
+
+consts
+
+   uterm_less :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+   unifyRel   :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+   unify      :: "'a uterm * 'a uterm => ('a * 'a uterm) subst"
+
+defs
+
+  uterm_less_def "uterm_less == rprod (measure uterm_size) 
+                                      (measure uterm_size)"
+  
+  (* Termination relation for the Unify function *)
+  unifyRel_def  "unifyRel == inv_image  (finite_psubset ** uterm_less)
+                               (%(x,y). (vars_of x Un vars_of y, (x,y)))"
+
+recdef unify "unifyRel"
+  "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)))"
+end