--- a/src/HOL/IsaMakefile Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/IsaMakefile Sun Aug 21 22:13:04 2011 +0200
@@ -70,7 +70,6 @@
HOL-SPARK-Examples \
HOL-Word-SMT_Examples \
HOL-Statespace \
- HOL-Subst \
TLA-Buffer \
TLA-Inc \
TLA-Memory \
@@ -496,15 +495,6 @@
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
-## HOL-Subst
-
-HOL-Subst: HOL $(LOG)/HOL-Subst.gz
-
-$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \
- Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
-
-
## HOL-Induct
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
@@ -1754,7 +1744,7 @@
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
$(LOG)/HOL-Word-SMT_Examples.gz \
$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \
- $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
+ $(LOG)/HOL-Statespace.gz \
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \
$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \
--- a/src/HOL/Subst/AList.thy Sun Aug 21 22:13:04 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/Subst/AList.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-*)
-
-header {* Association Lists *}
-
-theory AList
-imports Main
-begin
-
-primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
-where
- "alist_rec [] c d = c"
-| "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
-
-primrec assoc :: "['a,'b,('a*'b) list] => 'b"
-where
- "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 [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
- by (induct l) auto
-
-
-
-end
--- a/src/HOL/Subst/ROOT.ML Sun Aug 21 22:13:04 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: HOL/Subst/ROOT.ML
- 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,
-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
-
-AList - association lists
-UTerm - data type of terms
-Subst - substitutions
-Unifier - specification of unification and conditions for
- correctness and termination
-Unify - the unification function
-
-*)
-
-use_thys ["Unify"];
--- a/src/HOL/Subst/Subst.thy Sun Aug 21 22:13:04 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,196 +0,0 @@
-(* Title: HOL/Subst/Subst.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-*)
-
-header {* Substitutions on uterms *}
-
-theory Subst
-imports AList UTerm
-begin
-
-primrec
- subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl "<|" 55)
-where
- 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)"
-
-notation (xsymbols)
- subst (infixl "\<lhd>" 55)
-
-definition
- subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52)
- where "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
-
-notation (xsymbols)
- subst_eq (infixr "\<doteq>" 52)
-
-definition
- comp :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> ('a* 'a uterm) list"
- (infixl "<>" 56)
- where "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl) # g)"
-
-notation (xsymbols)
- comp (infixl "\<lozenge>" 56)
-
-definition
- sdom :: "('a*('a uterm)) list => 'a set" where
- "sdom al = alist_rec al {} (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
-
-definition
- srange :: "('a*('a uterm)) list => 'a set" where
- "srange al = Union({y. \<exists>x \<in> sdom(al). y = vars_of(Var(x) \<lhd> al)})"
-
-
-
-subsection {* Basic Laws *}
-
-lemma subst_Nil [simp]: "t \<lhd> [] = t"
- by (induct t) auto
-
-lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
- by (induct u) auto
-
-lemma Var_not_occs: "~ (Var(v) \<prec> t) \<Longrightarrow> t \<lhd> (v,t \<lhd> s) # s = t \<lhd> s"
- apply (case_tac "t = Var v")
- prefer 2
- apply (erule rev_mp)+
- apply (rule_tac P = "%x. x \<noteq> Var v \<longrightarrow> ~(Var v \<prec> x) \<longrightarrow> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s"
- in uterm.induct)
- apply auto
- done
-
-lemma agreement: "(t\<lhd>r = t\<lhd>s) = (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
- by (induct t) auto
-
-lemma repl_invariance: "~ v: vars_of t ==> t \<lhd> (v,u)#s = t \<lhd> s"
- by (simp add: agreement)
-
-lemma Var_in_subst:
- "v \<in> vars_of(t) --> w \<in> vars_of(t \<lhd> (v,Var(w))#s)"
- by (induct t) auto
-
-
-subsection{*Equality between Substitutions*}
-
-lemma subst_eq_iff: "r \<doteq> s = (\<forall>t. t \<lhd> r = t \<lhd> s)"
- by (simp add: subst_eq_def)
-
-lemma subst_refl [iff]: "r \<doteq> r"
- by (simp add: subst_eq_iff)
-
-lemma subst_sym: "r \<doteq> s ==> s \<doteq> r"
- by (simp add: subst_eq_iff)
-
-lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s"
- by (simp add: subst_eq_iff)
-
-lemma subst_subst2:
- "[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
- by (simp add: subst_eq_def)
-
-lemma ssubst_subst2:
- "[| s \<doteq> r; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
- by (simp add: subst_eq_def)
-
-
-subsection{*Composition of Substitutions*}
-
-lemma [simp]:
- "[] \<lozenge> bl = bl"
- "((a,b)#al) \<lozenge> bl = (a,b \<lhd> bl) # (al \<lozenge> 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 \<lozenge> [] = s"
- by (induct s) auto
-
-lemma subst_comp_Nil: "s \<doteq> s \<lozenge> []"
- by simp
-
-lemma subst_comp [simp]: "(t \<lhd> r \<lozenge> s) = (t \<lhd> r \<lhd> s)"
- apply (induct t)
- apply simp_all
- apply (induct r)
- apply auto
- done
-
-lemma comp_assoc: "(q \<lozenge> r) \<lozenge> s \<doteq> q \<lozenge> (r \<lozenge> s)"
- by (simp add: subst_eq_iff)
-
-lemma subst_cong:
- "[| theta \<doteq> theta1; sigma \<doteq> sigma1|]
- ==> (theta \<lozenge> sigma) \<doteq> (theta1 \<lozenge> sigma1)"
- by (simp add: subst_eq_def)
-
-
-lemma Cons_trivial: "(w, Var(w) \<lhd> s) # s \<doteq> s"
- apply (simp add: subst_eq_iff)
- apply (rule allI)
- apply (induct_tac t)
- apply simp_all
- done
-
-
-lemma comp_subst_subst: "q \<lozenge> r \<doteq> s ==> t \<lhd> q \<lhd> r = t \<lhd> s"
- by (simp add: subst_eq_iff)
-
-
-subsection{*Domain and range of Substitutions*}
-
-lemma sdom_iff: "(v \<in> sdom(s)) = (Var(v) \<lhd> s ~= Var(v))"
- apply (induct s)
- apply (case_tac [2] a)
- apply auto
- done
-
-
-lemma srange_iff:
- "v \<in> srange(s) = (\<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s))"
- by (auto simp add: srange_def)
-
-lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
- unfolding empty_def by blast
-
-lemma invariance: "(t \<lhd> s = t) = (sdom(s) Int vars_of(t) = {})"
- apply (induct t)
- apply (auto simp add: empty_iff_all_not sdom_iff)
- done
-
-lemma Var_in_srange:
- "v \<in> sdom(s) \<Longrightarrow> v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s)"
- apply (induct t)
- apply (case_tac "a \<in> sdom s")
- apply (auto simp add: sdom_iff srange_iff)
- done
-
-lemma Var_elim: "[| v \<in> sdom(s); v \<notin> srange(s) |] ==> v \<notin> vars_of(t \<lhd> s)"
- by (blast intro: Var_in_srange)
-
-lemma Var_intro:
- "v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s) | v \<in> vars_of(t)"
- apply (induct t)
- apply (auto simp add: sdom_iff srange_iff)
- apply (rule_tac x=a in exI)
- apply auto
- done
-
-lemma srangeD: "v \<in> srange(s) ==> \<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s)"
- by (simp add: srange_iff)
-
-lemma dom_range_disjoint:
- "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t \<lhd> s) = {})"
- apply (simp add: empty_iff_all_not)
- apply (force intro: Var_in_srange dest: srangeD)
- done
-
-lemma subst_not_empty: "~ u \<lhd> s = u ==> (\<exists>x. x \<in> sdom(s))"
- by (auto simp add: empty_iff_all_not invariance)
-
-
-lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M"
- by (induct M) auto
-
-end
--- a/src/HOL/Subst/UTerm.thy Sun Aug 21 22:13:04 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/Subst/UTerm.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-*)
-
-header {* Simple Term Structure for Unification *}
-
-theory UTerm
-imports Main
-begin
-
-text {* Binary trees with leaves that are constants or variables. *}
-
-datatype 'a uterm =
- Var 'a
- | Const 'a
- | Comb "'a uterm" "'a uterm"
-
-primrec vars_of :: "'a uterm => 'a set"
-where
- 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 occs :: "'a uterm => 'a uterm => bool" (infixl "<:" 54)
-where
- 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)"
-
-notation (xsymbols)
- occs (infixl "\<prec>" 54)
-
-primrec uterm_size :: "'a uterm => nat"
-where
- 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 \<in> vars_of (Var w)) = (w = v)"
- by auto
-
-lemma vars_iff_occseq: "(x \<in> vars_of t) = (Var x \<prec> t | Var x = t)"
- by (induct t) auto
-
-
-text{* Not used, but perhaps useful in other proofs *}
-lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
- by (induct N) auto
-
-
-lemma monotone_vars_of:
- "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
- by blast
-
-lemma finite_vars_of: "finite (vars_of M)"
- by (induct M) auto
-
-end
--- a/src/HOL/Subst/Unifier.thy Sun Aug 21 22:13:04 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title: HOL/Subst/Unifier.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-*)
-
-header {* Definition of Most General Unifier *}
-
-theory Unifier
-imports Subst
-begin
-
-definition
- Unifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
- where "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
-
-definition
- MoreGeneral :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> bool" (infixr ">>" 52)
- where "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
-
-definition
- MGUnifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
- where "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
-
-definition
- Idem :: "('a * 'a uterm)list => bool" where
- "Idem s \<longleftrightarrow> (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 \<notin> vars_of t \<Longrightarrow> v \<notin> vars_of u \<Longrightarrow> Unifier s t u \<Longrightarrow> 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 [intro!]: "~ 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
-
-
-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) \<Longrightarrow> Unifier s (t<|r) (u<|r) \<Longrightarrow>
- Unifier (r <> s) (t <| r) (u <| r)"
- by (simp add: Idem_def Unifier_def comp_subst_subst)
-
-lemma Idem_comp:
- "Idem r \<Longrightarrow> Unifier s (t <| r) (u <| r) \<Longrightarrow>
- (!!q. Unifier q (t <| r) (u <| r) \<Longrightarrow> s <> q =$= q) \<Longrightarrow>
- 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.thy Sun Aug 21 22:13:04 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,235 +0,0 @@
-(* Title: HOL/Subst/Unify.thy
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-header {* Unification Algorithm *}
-
-theory Unify
-imports Unifier "~~/src/HOL/Library/Old_Recdef"
-begin
-
-subsection {* Substitution and Unification in Higher-Order Logic. *}
-
-text {*
-NB: This theory is already quite old.
-You might want to look at the newer Isar formalization of
-unification in HOL/ex/Unification.thy.
-
-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
-*}
-
-definition
- unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
- "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) *}
-
-
-text{* Wellfoundedness of unifyRel *}
-lemma wf_unifyRel [iff]: "wf unifyRel"
- by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
-
-consts unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
-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 \<prec> 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 \<prec> 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 \<lhd> theta, N2 \<lhd> theta)
- of None => None
- | Some sigma => Some (theta \<lozenge> sigma)))"
- (hints recdef_wf: wf_unifyRel)
-
-
-text{* 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).*}
-recdef_tc unify_tc1: unify (1)
- by (auto simp: unifyRel_def finite_psubset_def finite_vars_of)
-
-
-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))) \<in> unifyRel ==>
- ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
- by (simp add: less_eq 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 \<prec> M) ==>
- ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) \<in> unifyRel
- & ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) \<in> unifyRel"
-apply (case_tac "Var x = M", clarify, simp)
-apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
-txt{*@{text uterm_less} case*}
-apply (simp add: less_eq unifyRel_def lex_prod_def)
-apply blast
-txt{*@{text finite_psubset} case*}
-apply (simp add: unifyRel_def lex_prod_def)
-apply (simp add: finite_psubset_def finite_vars_of psubset_eq)
-apply blast
-txt{*Final case, also @{text finite_psubset}*}
-apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_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. The (2) requests the second one.
- Proved by recursion induction.*}
-recdef_tc unify_tc2: unify (2)
-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\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) \<in> 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 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 \<lhd> theta, N2 \<lhd> theta)
- of None => None
- | Some sigma => Some (theta \<lozenge> sigma)))"
-by (simp add: unify_tc2 unify_simps0 split add: option.split)
-
-lemma unify_induct:
- "(\<And>m n. P (Const m) (Const n)) \<Longrightarrow>
- (\<And>m M N. P (Const m) (Comb M N)) \<Longrightarrow>
- (\<And>m v. P (Const m) (Var v)) \<Longrightarrow>
- (\<And>v M. P (Var v) M) \<Longrightarrow>
- (\<And>M N x. P (Comb M N) (Const x)) \<Longrightarrow>
- (\<And>M N v. P (Comb M N) (Var v)) \<Longrightarrow>
- (\<And>M1 N1 M2 N2.
- \<forall>theta. unify (M1, M2) = Some theta \<longrightarrow> P (N1 \<lhd> theta) (N2 \<lhd> theta) \<Longrightarrow>
- P M1 M2 \<Longrightarrow> P (Comb M1 N1) (Comb M2 N2)) \<Longrightarrow>
- P u v"
-by (rule unify_induct0) (simp_all add: unify_tc2)
-
-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))
- txt{*Const-Const case*}
- apply (simp add: MGUnifier_def Unifier_def)
- txt{*Const-Var case*}
- apply (subst mgu_sym)
- apply (simp add: MGUnifier_Var)
- txt{*Var-M case*}
- apply (simp add: MGUnifier_Var)
- txt{*Comb-Var case*}
- apply (subst mgu_sym)
- apply (simp add: MGUnifier_Var)
-txt{*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 \<lhd> theta \<lhd> delta = N2 \<lhd> theta \<lhd> 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