--- a/src/HOL/IsaMakefile Mon Mar 28 16:19:56 2005 +0200
+++ b/src/HOL/IsaMakefile Tue Mar 29 12:30:48 2005 +0200
@@ -191,9 +191,8 @@
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
-$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.ML Subst/AList.thy \
- Subst/ROOT.ML Subst/Subst.ML Subst/Subst.thy Subst/UTerm.ML \
- Subst/UTerm.thy Subst/Unifier.ML Subst/Unifier.thy Subst/Unify.ML \
+$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy \
+ Subst/ROOT.ML Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy \
Subst/Unify.thy
@$(ISATOOL) usedir $(OUT)/HOL Subst
--- a/src/HOL/Subst/AList.ML Mon Mar 28 16:19:56 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: Subst/AList.ML
- ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Association lists.
-*)
-
-open AList;
-
-val prems = goal AList.thy
- "[| P([]); \
-\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)";
-by (induct_tac "l" 1);
-by (split_all_tac 2);
-by (REPEAT (ares_tac prems 1));
-qed "alist_induct";
-
-(*Perform induction on xs. *)
-fun alist_ind_tac a M =
- EVERY [induct_thm_tac alist_induct a M,
- rename_last_tac a ["1"] (M+1)];
--- a/src/HOL/Subst/AList.thy Mon Mar 28 16:19:56 2005 +0200
+++ b/src/HOL/Subst/AList.thy Tue Mar 29 12:30:48 2005 +0200
@@ -1,12 +1,14 @@
-(* Title: Subst/AList.thy
- ID: $Id$
+(* ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Association lists.
*)
-AList = Main +
+header{*Association Lists*}
+
+theory AList
+imports Main
+begin
consts
alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
@@ -20,4 +22,10 @@
"assoc v d [] = d"
"assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
+
+lemma alist_induct:
+ "[| P([]);
+ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"
+by (induct_tac "l", auto)
+
end
--- a/src/HOL/Subst/Subst.ML Mon Mar 28 16:19:56 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,205 +0,0 @@
-(* Title: HOL/Subst/Subst.ML
- ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Substitutions on uterms
-*)
-
-open Subst;
-
-
-(**** Substitutions ****)
-
-Goal "t <| [] = t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "subst_Nil";
-
-Addsimps [subst_Nil];
-
-Goal "t <: u --> t <| s <: u <| s";
-by (induct_tac "u" 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "subst_mono";
-
-Goal "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
-by (case_tac "t = Var(v)" 1);
-by (etac 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 Asm_simp_tac);
-by (Blast_tac 1);
-qed_spec_mp "Var_not_occs";
-
-Goal "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (ALLGOALS Blast_tac);
-qed "agreement";
-
-Goal "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
-by (simp_tac (simpset() addsimps [agreement]) 1);
-qed_spec_mp"repl_invariance";
-
-val asms = goal Subst.thy
- "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp"Var_in_subst";
-
-
-(**** Equality between Substitutions ****)
-
-Goalw [subst_eq_def] "r =$= s = (! t. t <| r = t <| s)";
-by (Simp_tac 1);
-qed "subst_eq_iff";
-
-
-local fun prove s = prove_goal Subst.thy s
- (fn prems => [cut_facts_tac prems 1,
- REPEAT (etac rev_mp 1),
- simp_tac (simpset() addsimps [subst_eq_iff]) 1])
-in
- val subst_refl = 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; 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 ****)
-
-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 "s <> [] = s";
-by (alist_ind_tac "s" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "comp_Nil";
-
-Addsimps [comp_Nil];
-
-Goal "s =$= s <> []";
-by (Simp_tac 1);
-qed "subst_comp_Nil";
-
-Goal "(t <| r <> s) = (t <| r <| s)";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-by (alist_ind_tac "r" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "subst_comp";
-
-Addsimps [subst_comp];
-
-Goal "(q <> r) <> s =$= q <> (r <> s)";
-by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
-qed "comp_assoc";
-
-Goal "[| theta =$= theta1; sigma =$= sigma1|] ==> \
-\ (theta <> sigma) =$= (theta1 <> sigma1)";
-by (asm_full_simp_tac (simpset() addsimps [subst_eq_def]) 1);
-qed "subst_cong";
-
-
-Goal "(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);
-qed "Cons_trivial";
-
-
-Goal "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 "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
-by (alist_ind_tac "s" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "sdom_iff";
-
-
-Goalw [srange_def]
- "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
-by (Blast_tac 1);
-qed "srange_iff";
-
-Goalw [empty_def] "(A = {}) = (ALL a.~ a:A)";
-by (Blast_tac 1);
-qed "empty_iff_all_not";
-
-Goal "(t <| s = t) = (sdom(s) Int vars_of(t) = {})";
-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 "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";
-
-Goal "[| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)";
-by (blast_tac (claset() addIs [Var_in_srange]) 1);
-qed "Var_elim";
-
-Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
-by (induct_tac "t" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff])));
-by (Blast_tac 2);
-by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym]));
-by Auto_tac;
-qed_spec_mp "Var_intro";
-
-Goal "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
-by (simp_tac (simpset() addsimps [srange_iff]) 1);
-qed_spec_mp "srangeD";
-
-Goal "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
-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";
-
-Goal "~ 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 "(M <| [(x, Var x)]) = M";
-by (induct_tac "M" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "id_subst_lemma";
-
-Addsimps [id_subst_lemma];
--- a/src/HOL/Subst/Subst.thy Mon Mar 28 16:19:56 2005 +0200
+++ b/src/HOL/Subst/Subst.thy Tue Mar 29 12:30:48 2005 +0200
@@ -2,11 +2,13 @@
ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-
-Substitutions on uterms
*)
-Subst = AList + UTerm +
+header{*Substitutions on uterms*}
+
+theory Subst
+imports AList UTerm
+begin
consts
@@ -19,22 +21,170 @@
primrec
- 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_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)"
defs
- subst_eq_def "r =$= s == ALL t. t <| r = t <| s"
+ 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)"
+ comp_def: "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
- sdom_def
+ sdom_def:
"sdom(al) == alist_rec al {}
(%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
- srange_def
+ srange_def:
"srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
+
+
+subsection{*Basic Laws*}
+
+lemma subst_Nil [simp]: "t <| [] = t"
+by (induct_tac "t", auto)
+
+lemma subst_mono [rule_format]: "t <: u --> t <| s <: u <| s"
+by (induct_tac "u", auto)
+
+lemma Var_not_occs [rule_format]:
+ "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s"
+apply (case_tac "t = Var v")
+apply (erule_tac [2] rev_mp)
+apply (rule_tac [2] P = "%x.~x=Var (v) --> ~ (Var (v) <: x) --> x <| (v,t<|s) #s=x<|s" in uterm.induct)
+apply auto
+done
+
+lemma agreement: "(t <|r = t <|s) = (\<forall>v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"
+by (induct_tac "t", auto)
+
+lemma repl_invariance: "~ v: vars_of(t) ==> t <| (v,u)#s = t <| s"
+by (simp add: agreement)
+
+lemma Var_in_subst [rule_format]:
+ "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"
+by (induct_tac "t", auto)
+
+
+subsection{*Equality between Substitutions*}
+
+lemma subst_eq_iff: "r =$= s = (\<forall>t. t <| r = t <| s)"
+by (simp add: subst_eq_def)
+
+lemma subst_refl [iff]: "r =$= r"
+by (simp add: subst_eq_iff)
+
+lemma subst_sym: "r =$= s ==> s =$= r"
+by (simp add: subst_eq_iff)
+
+lemma subst_trans: "[| q =$= r; r =$= s |] ==> q =$= s"
+by (simp add: subst_eq_iff)
+
+lemma subst_subst2:
+ "[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)"
+by (simp add: subst_eq_def)
+
+lemmas ssubst_subst2 = subst_sym [THEN subst_subst2]
+
+
+subsection{*Composition of Substitutions*}
+
+lemma [simp]:
+ "[] <> 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})"
+by (simp_all add: comp_def sdom_def)
+
+lemma comp_Nil [simp]: "s <> [] = s"
+by (induct "s", auto)
+
+lemma subst_comp_Nil: "s =$= s <> []"
+by simp
+
+lemma subst_comp [simp]: "(t <| r <> s) = (t <| r <| s)"
+apply (induct_tac "t")
+apply (simp_all (no_asm_simp))
+apply (induct "r", auto)
+done
+
+lemma comp_assoc: "(q <> r) <> s =$= q <> (r <> s)"
+apply (simp (no_asm) add: subst_eq_iff)
+done
+
+lemma subst_cong:
+ "[| theta =$= theta1; sigma =$= sigma1|]
+ ==> (theta <> sigma) =$= (theta1 <> sigma1)"
+by (simp add: subst_eq_def)
+
+
+lemma Cons_trivial: "(w, Var(w) <| s) # s =$= s"
+apply (simp add: subst_eq_iff)
+apply (rule allI)
+apply (induct_tac "t", simp_all)
+done
+
+
+lemma comp_subst_subst: "q <> r =$= s ==> t <| q <| r = t <| s"
+by (simp add: subst_eq_iff)
+
+
+subsection{*Domain and range of Substitutions*}
+
+lemma sdom_iff: "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"
+apply (induct "s")
+apply (case_tac [2] a, auto)
+done
+
+
+lemma srange_iff:
+ "v : srange(s) = (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))"
+by (auto simp add: srange_def)
+
+lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
+by (unfold empty_def, blast)
+
+lemma invariance: "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"
+apply (induct_tac "t")
+apply (auto simp add: empty_iff_all_not sdom_iff)
+done
+
+lemma Var_in_srange [rule_format]:
+ "v : sdom(s) --> v : vars_of(t <| s) --> v : srange(s)"
+apply (induct_tac "t")
+apply (case_tac "a : sdom (s) ")
+apply (auto simp add: sdom_iff srange_iff)
+done
+
+lemma Var_elim: "[| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)"
+by (blast intro: Var_in_srange)
+
+lemma Var_intro [rule_format]:
+ "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"
+apply (induct_tac "t")
+apply (auto simp add: sdom_iff srange_iff)
+apply (rule_tac x=a in exI, auto)
+done
+
+lemma srangeD [rule_format]:
+ "v : srange(s) --> (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))"
+apply (simp (no_asm) add: srange_iff)
+done
+
+lemma dom_range_disjoint:
+ "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t <| s) = {})"
+apply (simp (no_asm) add: empty_iff_all_not)
+apply (force intro: Var_in_srange dest: srangeD)
+done
+
+lemma subst_not_empty: "~ u <| s = u ==> (\<exists>x. x : sdom(s))"
+by (auto simp add: empty_iff_all_not invariance)
+
+
+lemma id_subst_lemma [simp]: "(M <| [(x, Var x)]) = M"
+by (induct_tac "M", auto)
+
+
end
--- a/src/HOL/Subst/UTerm.ML Mon Mar 28 16:19:56 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOL/Subst/UTerm.ML
- ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Simple term structure for unifiation.
-Binary trees with leaves that are constants or variables.
-*)
-
-open UTerm;
-
-
-(**** vars_of lemmas ****)
-
-Goal "(v : vars_of(Var(w))) = (w=v)";
-by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
-qed "vars_var_iff";
-
-Goal "(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";
-
-
-(* Not used, but perhaps useful in other proofs *)
-Goal "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();
-
-
-Goal "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();
-
-Goal "finite(vars_of M)";
-by (induct_tac"M" 1);
-by (ALLGOALS Simp_tac);
-by (ftac finite_UnI 1);
-by (assume_tac 1);
-by (Asm_simp_tac 1);
-val finite_vars_of = result();
--- a/src/HOL/Subst/UTerm.thy Mon Mar 28 16:19:56 2005 +0200
+++ b/src/HOL/Subst/UTerm.thy Tue Mar 29 12:30:48 2005 +0200
@@ -1,38 +1,61 @@
-(* Title: Subst/UTerm.thy
- ID: $Id$
+(* ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-
-Simple term structure for unification.
-Binary trees with leaves that are constants or variables.
*)
-UTerm = Main +
+header{*Simple Term Structure for Unification*}
+
+theory UTerm
+imports Main
-datatype 'a uterm = Var ('a)
- | Const ('a)
- | Comb ('a uterm) ('a uterm)
+begin
+
+text{*Binary trees with leaves that are constants or variables.*}
+
+datatype 'a uterm = Var 'a
+ | Const 'a
+ | Comb "'a uterm" "'a uterm"
consts
- vars_of :: 'a uterm => 'a set
- "<:" :: 'a uterm => 'a uterm => bool (infixl 54)
-uterm_size :: 'a uterm => nat
+ vars_of :: "'a uterm => 'a set"
+ "<:" :: "'a uterm => 'a uterm => bool" (infixl 54)
+uterm_size :: "'a uterm => nat"
+
+
+primrec
+ vars_of_Var: "vars_of (Var v) = {v}"
+ vars_of_Const: "vars_of (Const c) = {}"
+ vars_of_Comb: "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
primrec
- 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))"
-
+ occs_Var: "u <: (Var v) = False"
+ occs_Const: "u <: (Const c) = False"
+ occs_Comb: "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
primrec
- 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_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)"
+
+
+lemma vars_var_iff: "(v : vars_of(Var(w))) = (w=v)"
+by auto
+
+lemma vars_iff_occseq: "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"
+by (induct_tac "t", auto)
+
-primrec
- 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)"
+(* Not used, but perhaps useful in other proofs *)
+lemma occs_vars_subset: "M<:N --> vars_of(M) <= vars_of(N)"
+by (induct_tac "N", auto)
+
+
+lemma monotone_vars_of: "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"
+by blast
+
+lemma finite_vars_of: "finite(vars_of M)"
+by (induct_tac "M", auto)
+
end
--- a/src/HOL/Subst/Unifier.ML Mon Mar 28 16:19:56 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: HOL/Subst/Unifier.ML
- ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Properties of unifiers.
-*)
-
-open Unifier;
-
-val unify_defs = [Unifier_def, MoreGeneral_def, MGUnifier_def];
-
-(*---------------------------------------------------------------------------
- * Unifiers
- *---------------------------------------------------------------------------*)
-
-Goal "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";
-
-AddIffs [Unifier_Comb];
-
-Goal "[| 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";
-
-
-(*---------------------------------------------------------------------------
- * Most General Unifiers
- *---------------------------------------------------------------------------*)
-
-Goalw unify_defs "MGUnifier s t u = MGUnifier s u t";
-by (blast_tac (claset() addIs [sym]) 1);
-qed "mgu_sym";
-
-
-Goal "[] >> s";
-by (simp_tac (simpset() addsimps [MoreGeneral_def]) 1);
-by (Blast_tac 1);
-qed "MoreGen_Nil";
-
-AddIffs [MoreGen_Nil];
-
-Goalw unify_defs
- "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";
-
-
-Goal "~ 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 Safe_tac;
-by (rtac 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";
-
-AddSIs [MGUnifier_Var];
-
-
-(*---------------------------------------------------------------------------
- * Idempotence.
- *---------------------------------------------------------------------------*)
-
-Goalw [Idem_def] "Idem([])";
-by (Simp_tac 1);
-qed "Idem_Nil";
-
-AddIffs [Idem_Nil];
-
-Goalw [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";
-
-Goal "~ (Var(v) <: t) --> Idem([(v,t)])";
-by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff,
- empty_iff_all_not]) 1);
-qed_spec_mp "Var_Idem";
-
-AddSIs [Var_Idem];
-
-Goalw [Idem_def]
- "[| 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 Mon Mar 28 16:19:56 2005 +0200
+++ b/src/HOL/Subst/Unifier.thy Tue Mar 29 12:30:48 2005 +0200
@@ -1,12 +1,15 @@
-(* Title: Subst/Unifier.thy
- ID: $Id$
+(* ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Definition of most general unifier
*)
-Unifier = Subst +
+header{*Definition of Most General Unifier*}
+
+theory Unifier
+imports Subst
+
+begin
consts
@@ -17,9 +20,76 @@
defs
- Unifier_def "Unifier s t u == t <| s = u <| s"
- 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)"
- Idem_def "Idem(s) == (s <> s) =$= s"
+ Unifier_def: "Unifier s t u == t <| s = u <| s"
+ 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)"
+ Idem_def: "Idem(s) == (s <> s) =$= s"
+
+
+
+lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
+
+
+subsection{*Unifiers*}
+
+lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
+by (simp add: Unifier_def)
+
+
+lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u"
+by (simp add: Unifier_def repl_invariance)
+
+
+subsection{* Most General Unifiers*}
+
+lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
+by (simp add: unify_defs eq_commute)
+
+
+lemma MoreGen_Nil [iff]: "[] >> s"
+by (auto simp add: MoreGeneral_def)
+
+lemma MGU_iff: "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"
+apply (unfold unify_defs)
+apply (auto intro: ssubst_subst2 subst_comp_Nil)
+done
+
+lemma MGUnifier_Var: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"
+apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var)
+apply safe
+apply (rule exI)
+apply (erule subst, rule Cons_trivial [THEN subst_sym])
+apply (erule ssubst_subst2)
+apply (simp (no_asm_simp) add: Var_not_occs)
+done
+
+declare MGUnifier_Var [intro!]
+
+
+subsection{*Idempotence*}
+
+lemma Idem_Nil [iff]: "Idem([])"
+by (simp add: Idem_def)
+
+lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})"
+by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
+
+lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])"
+by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
+
+lemma Unifier_Idem_subst:
+ "[| Idem(r); Unifier s (t<|r) (u<|r) |]
+ ==> Unifier (r <> s) (t <| r) (u <| r)"
+by (simp add: Idem_def Unifier_def comp_subst_subst)
+
+lemma Idem_comp:
+ "[| Idem(r); Unifier s (t <| r) (u <| r);
+ !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q
+ |] ==> Idem(r <> s)"
+apply (frule Unifier_Idem_subst, blast)
+apply (force simp add: Idem_def subst_eq_iff)
+done
+
+
end
--- a/src/HOL/Subst/Unify.ML Mon Mar 28 16:19:56 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,251 +0,0 @@
-(* Title: Subst/Unify
- ID: $Id$
- 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).
- *---------------------------------------------------------------------------*)
-
-(*---------------------------------------------------------------------------
- * The non-nested TC plus the wellfoundedness of unifyRel.
- *---------------------------------------------------------------------------*)
-Tfl.tgoalw Unify.thy [] unify.simps;
-(* Wellfoundedness of unifyRel *)
-by (simp_tac (simpset() addsimps [unifyRel_def,
- wf_inv_image, wf_lex_prod, wf_finite_psubset,
- wf_measure]) 1);
-(* TC *)
-by Safe_tac;
-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 [less_eq, less_add_Suc1]) 1);
-qed "tc0";
-
-
-(*---------------------------------------------------------------------------
- * Termination proof.
- *---------------------------------------------------------------------------*)
-
-Goalw [unifyRel_def, measure_def] "trans unifyRel";
-by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod,
- trans_finite_psubset, trans_less_than,
- trans_inv_image] 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 [unifyRel_def,lex_prod_def, inv_image_def]
- "((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 [measure_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 "~(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, 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]) 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])));
-by (ALLGOALS
- (fast_tac (claset() addEs [Var_intro RS disjE]
- addss (simpset() addsimps [srange_iff]))));
-qed "var_elimR";
-
-
-(*---------------------------------------------------------------------------
- * Eliminate tc0 from the recursion equations and the induction theorem.
- *---------------------------------------------------------------------------*)
-val wfr = tc0 RS conjunct1
-and tc = tc0 RS conjunct2;
-val unifyRules0 = map (rule_by_tactic (rtac wfr 1 THEN TRY(rtac tc 1)))
- unify.simps;
-
-val unifyInduct0 = [wfr,tc] MRS unify.induct;
-
-
-(*---------------------------------------------------------------------------
- * The nested TC. Proved by recursion induction.
- *---------------------------------------------------------------------------*)
-val [_,_,tc3] = unify.tcs;
-goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop 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) = Some 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 [("u","M1"),("v","M2")] unifyInduct0 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0))));
-(*Const-Const case*)
-by (simp_tac
- (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
- inv_image_def, less_eq]) 1);
-(** LEVEL 7 **)
-(*Comb-Comb case*)
-by (asm_simp_tac (simpset() addsplits [option.split]) 1);
-by (strip_tac 1);
-by (rtac (trans_unifyRel RS transD) 1);
-by (Blast_tac 1);
-by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
-by (rtac Rassoc 1);
-by (Blast_tac 1);
-qed_spec_mp "unify_TC";
-
-
-(*---------------------------------------------------------------------------
- * Now for elimination of nested TC from unify.simps and induction.
- *---------------------------------------------------------------------------*)
-
-(*Desired rule, copied from the theory file. Could it be made available?*)
-Goal "unify(Comb M1 N1, Comb M2 N2) = \
-\ (case unify(M1,M2) \
-\ of None => None \
-\ | Some theta => (case unify(N1 <| theta, N2 <| theta) \
-\ of None => None \
-\ | Some sigma => Some (theta <> sigma)))";
-by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
- addsplits [option.split]) 1);
-qed "unifyCombComb";
-
-
-val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
-
-Addsimps unifyRules;
-
-bind_thm ("unifyInduct",
- rule_by_tactic
- (ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC])))
- unifyInduct0);
-
-
-(*---------------------------------------------------------------------------
- * 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 "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
-by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
-by (ALLGOALS Asm_simp_tac);
-(*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);
-(** LEVEL 8 **)
-(*Comb-Comb case*)
-by (asm_simp_tac (simpset() addsplits [option.split]) 1);
-by (strip_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
-by (Safe_tac THEN rename_tac "theta sigma gamma" 1);
-by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
-by (etac exE 1 THEN 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
- THEN 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 "!theta. unify(M,N) = Some theta --> Idem theta";
-by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps [Var_Idem] addsplits [option.split])));
-(*Comb-Comb case*)
-by Safe_tac;
-by (REPEAT (dtac spec 1 THEN mp_tac 1));
-by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
-by (rtac Idem_comp 1);
-by (atac 1);
-by (atac 1);
-by (best_tac (claset() addss (simpset() addsimps
- [MoreGeneral_def, subst_eq_iff, Idem_def])) 1);
-qed_spec_mp "unify_gives_Idem";
-
--- a/src/HOL/Subst/Unify.thy Mon Mar 28 16:19:56 2005 +0200
+++ b/src/HOL/Subst/Unify.thy Tue Mar 29 12:30:48 2005 +0200
@@ -1,12 +1,26 @@
-(* Title: Subst/Unify
- ID: $Id$
+(* ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-Unification algorithm
*)
-Unify = Unifier +
+header{*Unification Algorithm*}
+
+theory Unify
+imports Unifier
+begin
+
+text{*
+Substitution and Unification in Higher-Order Logic.
+
+Implements Manna and Waldinger's formalization, with Paulson's simplifications,
+and some new simplifications by Slind.
+
+Z Manna and 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
+*}
consts
@@ -14,26 +28,218 @@
unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
defs
+ unifyRel_def:
+ "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
+ (%(M,N). (vars_of M Un vars_of N, M))"
+ --{*Termination relation for the Unify function:
+ either the set of variables decreases,
+ or the first argument does (in fact, both do) *}
- (*Termination relation for the Unify function:
- --either the set of variables decreases
- --or the first argument does (in fact, both do)
- *)
- unifyRel_def "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
- (%(M,N). (vars_of M Un vars_of N, M))"
+text{* Wellfoundedness of unifyRel *}
+lemma wf_unifyRel [iff]: "wf unifyRel"
+by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
-recdef unify "unifyRel"
- "unify(Const m, Const n) = (if (m=n) then Some[] else None)"
- "unify(Const m, Comb M N) = None"
- "unify(Const m, Var v) = Some[(v,Const m)]"
- "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])"
- "unify(Comb M N, Const x) = None"
- "unify(Comb M N, Var v) = (if (Var v <: Comb M N) then None
- else Some[(v,Comb M N)])"
+
+recdef (permissive) unify "unifyRel"
+ unify_CC: "unify(Const m, Const n) = (if (m=n) then Some[] else None)"
+ unify_CB: "unify(Const m, Comb M N) = None"
+ unify_CV: "unify(Const m, Var v) = Some[(v,Const m)]"
+ unify_V: "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])"
+ unify_BC: "unify(Comb M N, Const x) = None"
+ unify_BV: "unify(Comb M N, Var v) = (if (Var v <: Comb M N) then None
+ else Some[(v,Comb M N)])"
+ unify_BB:
"unify(Comb M1 N1, Comb M2 N2) =
(case unify(M1,M2)
of None => None
| Some theta => (case unify(N1 <| theta, N2 <| theta)
of None => None
| Some sigma => Some (theta <> sigma)))"
+ (hints recdef_wf: wf_unifyRel)
+
+
+
+(*---------------------------------------------------------------------------
+ * 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).
+ *---------------------------------------------------------------------------*)
+
+text{*The non-nested TC (terminiation condition). This declaration form
+only seems to return one subgoal outstanding from the recdef.*}
+recdef_tc unify_tc1: unify
+apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe)
+apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def inv_image_def)
+apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]])
+done
+
+
+
+
+text{*Termination proof.*}
+
+lemma trans_unifyRel: "trans unifyRel"
+by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod
+ trans_finite_psubset)
+
+
+text{*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.*}
+lemma Rassoc:
+ "((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 (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc
+ unifyRel_def lex_prod_def)
+
+
+text{*This lemma proves the nested termination condition for the base cases
+ * 3, 4, and 6.*}
+lemma var_elimR:
+ "~(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"
+apply (case_tac "Var x = M", clarify, simp)
+apply (case_tac "x: (vars_of N1 Un vars_of N2) ")
+txt{*uterm_less case*}
+apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def)
+apply blast
+txt{*@{text finite_psubset} case*}
+apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def)
+apply (simp add: finite_psubset_def finite_vars_of psubset_def)
+apply blast
+txt{*Final case, also {text finite_psubset}*}
+apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def measure_def inv_image_def)
+apply (cut_tac s = "[ (x,M) ]" and v = x and t = N2 in Var_elim)
+apply (cut_tac [3] s = "[ (x,M) ]" and v = x and t = N1 in Var_elim)
+apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
+apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff)
+done
+
+
+text{*Eliminate tc1 from the recursion equations and the induction theorem.*}
+
+lemmas unify_nonrec [simp] =
+ unify_CC unify_CB unify_CV unify_V unify_BC unify_BV
+
+lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1]
+
+lemmas unify_induct0 = unify.induct [OF unify_tc1]
+
+text{*The nested TC. Proved by recursion induction.*}
+lemma unify_tc2:
+ "\<forall>M1 M2 N1 N2 theta.
+ unify (M1, M2) = Some theta \<longrightarrow>
+ ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) \<in> unifyRel"
+txt{*The extracted TC needs the scope of its quantifiers adjusted, so our
+ first step is to restrict the scopes of N1 and N2.*}
+apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta -->
+ (\<forall>N1 N2.((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)")
+apply blast
+apply (rule allI)
+apply (rule allI)
+txt{*Apply induction on this still-quantified formula*}
+apply (rule_tac u = M1 and v = M2 in unify_induct0)
+apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
+txt{*Const-Const case*}
+apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq)
+txt{*Comb-Comb case*}
+apply (simp (no_asm_simp) split add: option.split)
+apply (intro strip)
+apply (rule trans_unifyRel [THEN transD], blast)
+apply (simp only: subst_Comb [symmetric])
+apply (rule Rassoc, blast)
+done
+
+
+text{* Now for elimination of nested TC from unify.simps and induction.*}
+
+text{*Desired rule, copied from the theory file.*}
+lemma unifyCombComb [simp]:
+ "unify(Comb M1 N1, Comb M2 N2) =
+ (case unify(M1,M2)
+ of None => None
+ | Some theta => (case unify(N1 <| theta, N2 <| theta)
+ of None => None
+ | Some sigma => Some (theta <> sigma)))"
+by (simp add: unify_tc2 unify_simps0 split add: option.split)
+
+text{*The ML version had this, but it can't be used: we get
+*** exception THM raised: transfer: not a super theory
+All we can do is state the desired induction rule in full and prove it.*}
+ML{*
+bind_thm ("unify_induct",
+ rule_by_tactic
+ (ALLGOALS (full_simp_tac (simpset() addsimps [thm"unify_tc2"])))
+ (thm"unify_induct0"));
+*}
+
+
+text{*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.*}
+
+theorem unify_gives_MGU [rule_format]:
+ "\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N"
+apply (rule_tac u = M and v = N in unify_induct0)
+apply (simp_all (no_asm_simp))
+(*Const-Const case*)
+apply (simp (no_asm) add: MGUnifier_def Unifier_def)
+(*Const-Var case*)
+apply (subst mgu_sym)
+apply (simp (no_asm) add: MGUnifier_Var)
+(*Var-M case*)
+apply (simp (no_asm) add: MGUnifier_Var)
+(*Comb-Var case*)
+apply (subst mgu_sym)
+apply (simp (no_asm) add: MGUnifier_Var)
+(** LEVEL 8 **)
+(*Comb-Comb case*)
+apply (simp add: unify_tc2)
+apply (simp (no_asm_simp) split add: option.split)
+apply (intro strip)
+apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def)
+apply (safe, rename_tac theta sigma gamma)
+apply (erule_tac x = gamma in allE, erule (1) notE impE)
+apply (erule exE, rename_tac delta)
+apply (erule_tac x = delta in allE)
+apply (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta")
+ apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym])
+apply (simp add: subst_eq_iff)
+done
+
+
+text{*Unify returns idempotent substitutions, when it succeeds.*}
+theorem unify_gives_Idem [rule_format]:
+ "\<forall>theta. unify(M,N) = Some theta --> Idem theta"
+apply (rule_tac u = M and v = N in unify_induct0)
+apply (simp_all add: Var_Idem unify_tc2 split add: option.split)
+txt{*Comb-Comb case*}
+apply safe
+apply (drule spec, erule (1) notE impE)+
+apply (safe dest!: unify_gives_MGU [unfolded MGUnifier_def])
+apply (rule Idem_comp, assumption+)
+apply (force simp add: MoreGeneral_def subst_eq_iff Idem_def)
+done
+
end