--- /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)];
--- /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
--- /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";
--- /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;
--- /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
--- /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);
--- /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
--- /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";
--- /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
--- /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];
+
--- /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
--- /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";
--- /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