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