src/HOL/Subst/Unify.thy

-(*  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