# HG changeset patch # User krauss # Date 1313957584 -7200 # Node ID 0b217404522a576e0ea934b8f3808122f614dbe0 # Parent 7321d628b57d4a3cbacda26f0b47b1f65e197ce0 removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy diff -r 7321d628b57d -r 0b217404522a src/HOL/IsaMakefile --- 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 \ diff -r 7321d628b57d -r 0b217404522a src/HOL/Subst/AList.thy --- 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 [] \ (!!x y xs. P xs \ P ((x,y) # xs)) \ P l" - by (induct l) auto - - - -end diff -r 7321d628b57d -r 0b217404522a src/HOL/Subst/ROOT.ML --- 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"]; diff -r 7321d628b57d -r 0b217404522a src/HOL/Subst/Subst.thy --- 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 "\" 55) - -definition - subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52) - where "r =$= s \ (\t. t \ r = t \ s)" - -notation (xsymbols) - subst_eq (infixr "\" 52) - -definition - comp :: "('a * 'a uterm) list \ ('a * 'a uterm) list \ ('a* 'a uterm) list" - (infixl "<>" 56) - where "al <> bl = alist_rec al bl (%x y xs g. (x,y \ bl) # g)" - -notation (xsymbols) - comp (infixl "\" 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. \x \ sdom(al). y = vars_of(Var(x) \ al)})" - - - -subsection {* Basic Laws *} - -lemma subst_Nil [simp]: "t \ [] = t" - by (induct t) auto - -lemma subst_mono: "t \ u \ t \ s \ u \ s" - by (induct u) auto - -lemma Var_not_occs: "~ (Var(v) \ t) \ t \ (v,t \ s) # s = t \ s" - apply (case_tac "t = Var v") - prefer 2 - apply (erule rev_mp)+ - apply (rule_tac 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) = (\v \ vars_of t. Var v \ r = Var v \ s)" - by (induct t) auto - -lemma repl_invariance: "~ v: vars_of t ==> t \ (v,u)#s = t \ s" - by (simp add: agreement) - -lemma Var_in_subst: - "v \ vars_of(t) --> w \ vars_of(t \ (v,Var(w))#s)" - by (induct t) auto - - -subsection{*Equality between Substitutions*} - -lemma subst_eq_iff: "r \ s = (\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) - -lemma ssubst_subst2: - "[| s \ r; P (t \ r) (u \ r) |] ==> P (t \ s) (u \ s)" - by (simp add: subst_eq_def) - - -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 t) - apply simp_all - apply (induct r) - apply auto - done - -lemma comp_assoc: "(q \ r) \ s \ q \ (r \ s)" - by (simp add: subst_eq_iff) - -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) - apply 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) - apply auto - done - - -lemma srange_iff: - "v \ srange(s) = (\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)" - unfolding empty_def by blast - -lemma invariance: "(t \ 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 \ sdom(s) \ v \ vars_of(t \ s) \ v \ srange(s)" - apply (induct 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: - "v \ vars_of(t \ s) \ v \ srange(s) | v \ 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 \ srange(s) ==> \w. w \ sdom(s) & v \ vars_of(Var(w) \ s)" - by (simp add: srange_iff) - -lemma dom_range_disjoint: - "sdom(s) Int srange(s) = {} = (\t. sdom(s) Int vars_of(t \ s) = {})" - apply (simp add: empty_iff_all_not) - apply (force intro: Var_in_srange dest: srangeD) - done - -lemma subst_not_empty: "~ u \ s = u ==> (\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 M) auto - -end diff -r 7321d628b57d -r 0b217404522a src/HOL/Subst/UTerm.thy --- 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 "\" 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 \ vars_of (Var w)) = (w = v)" - by auto - -lemma vars_iff_occseq: "(x \ vars_of t) = (Var x \ t | Var x = t)" - by (induct t) auto - - -text{* Not used, but perhaps useful in other proofs *} -lemma occs_vars_subset: "M \ N \ vars_of M \ vars_of N" - by (induct 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 M) auto - -end diff -r 7321d628b57d -r 0b217404522a src/HOL/Subst/Unifier.thy --- 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 \ 'a uterm \ 'a uterm \ bool" - where "Unifier s t u \ t <| s = u <| s" - -definition - MoreGeneral :: "('a * 'a uterm) list \ ('a * 'a uterm) list \ bool" (infixr ">>" 52) - where "r >> s \ (\q. s =$= r <> q)" - -definition - MGUnifier :: "('a * 'a uterm) list \ 'a uterm \ 'a uterm \ bool" - where "MGUnifier s t u \ Unifier s t u & (\r. Unifier r t u --> s >> r)" - -definition - Idem :: "('a * 'a uterm)list => bool" where - "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 [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) \ 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 diff -r 7321d628b57d -r 0b217404522a src/HOL/Subst/Unify.thy --- 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 \ 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) - - -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))) \ unifyRel ==> - ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \ 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 \ 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{*@{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 "\M1 M2 theta. unify (M1, M2) = Some theta --> - (\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 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) - -lemma unify_induct: - "(\m n. P (Const m) (Const n)) \ - (\m M N. P (Const m) (Comb M N)) \ - (\m v. P (Const m) (Var v)) \ - (\v M. P (Var v) M) \ - (\M N x. P (Comb M N) (Const x)) \ - (\M N v. P (Comb M N) (Var v)) \ - (\M1 N1 M2 N2. - \theta. unify (M1, M2) = Some theta \ P (N1 \ theta) (N2 \ theta) \ - P M1 M2 \ P (Comb M1 N1) (Comb M2 N2)) \ - 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]: - "\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 \ 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]: - "\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