Quelle Unification.thy Sprache: Isabelle

(*  Title:      HOL/ex/Unification.thy
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Author:     Konrad Slind, TUM & Cambridge University Computer Laboratory
    Author:     Alexander Krauss, TUM
*)

section \<open>Substitution and Unification\<close>

theory Unification
imports Main
begin

text \<open>
  Implements Manna \& Waldinger's formalization, with Paulson's
  simplifications, and some new simplifications by Slind and Krauss.

  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

  K Slind, Reasoning about Terminating Functional Programs,
  Ph.D. thesis, TUM, 1999, Sect. 5.8

  A Krauss, Partial and Nested Recursive Function Definitions in
  Higher-Order Logic, JAR 44(4):303-336, 2010. Sect. 6.3
\<close>

subsection \<open>Terms\<close>

text \<open>Binary trees with leaves that are constants or variables.\<close>

datatype 'a trm =
  Var 'a
  | Const 'a
  | Comb "'a trm" "'a trm" (infix \<open>\<cdot>\<close> 60)

primrec vars_of :: "'a trm \ 'a set"
where
  "vars_of (Var v) = {v}"
| "vars_of (Const c) = {}"
| "vars_of (M \ N) = vars_of M \ vars_of N"

fun occs :: "'a trm \ 'a trm \ bool" (infixl \\\ 54)
where
  "u \ Var v \ False"
| "u \ Const c \ False"
| "u \ M \ N \ u = M \ u = N \ u \ M \ u \ N"

lemma finite_vars_of[intro]: "finite (vars_of t)"
  by (induct t) simp_all

lemma vars_iff_occseq: "x \ vars_of t \ Var x \ t \ Var x = t"
  by (induct t) auto

lemma occs_vars_subset: "M \ N \ vars_of M \ vars_of N"
  by (induct N) auto

lemma size_less_size_if_occs: "t \ u \ size t < size u"
proof (induction u arbitrary: t)
  case (Comb u1 u2)
  thus ?case by fastforce
qed simp_all

corollary neq_if_occs: "t \ u \ t \ u"
  using size_less_size_if_occs by auto

subsection \<open>Substitutions\<close>

type_synonym 'a subst = "('a \<times> 'a trm) list"

fun assoc :: "'a \ 'b \ ('a \ 'b) list \ 'b"
where
  "assoc x d [] = d"
| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"

primrec subst :: "'a trm \ 'a subst \ 'a trm" (infixl \\\ 55)
where
  "(Var v) \ s = assoc v (Var v) s"
| "(Const c) \ s = (Const c)"
| "(M \ N) \ s = (M \ s) \ (N \ s)"

definition subst_eq (infixr \<open>\<doteq>\<close> 52)
where
  "s1 \ s2 \ (\t. t \ s1 = t \ s2)"

fun comp :: "'a subst \ 'a subst \ 'a subst" (infixl \\\ 56)
where
  "[] \ bl = bl"
| "((a,b) # al) \ bl = (a, b \ bl) # (al \ bl)"

lemma subst_Nil[simp]: "t \ [] = t"
by (induct t) auto

lemma subst_mono: "t \ u \ t \ s \ u \ s"
by (induct u) auto

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 remove_var: "v \ vars_of s \ v \ vars_of (t \ [(v, s)])"
by (induct t) simp_all

lemma subst_refl[iff]: "s \ s"
  by (auto simp:subst_eq_def)

lemma subst_sym[sym]: "\s1 \ s2\ \ s2 \ s1"
  by (auto simp:subst_eq_def)

lemma subst_trans[trans]: "\s1 \ s2; s2 \ s3\ \ s1 \ s3"
  by (auto simp:subst_eq_def)

lemma subst_no_occs: "\ Var v \ t \ Var v \ t
  \<Longrightarrow> t \<lhd> [(v,s)] = t"
by (induct t) auto

lemma comp_Nil[simp]: "\ \ [] = \"
by (induct \<sigma>) auto

lemma subst_comp[simp]: "t \ (r \ s) = t \ r \ s"
proof (induct t)
  case (Var v) thus ?case
    by (induct r) auto
qed auto

lemma subst_eq_intro[intro]: "(\t. t \ \ = t \ \) \ \ \ \"
  by (auto simp:subst_eq_def)

lemma subst_eq_dest[dest]: "s1 \ s2 \ t \ s1 = t \ s2"
  by (auto simp:subst_eq_def)

lemma comp_assoc: "(a \ b) \ c \ a \ (b \ c)"
  by auto

lemma subst_cong: "\\ \ \'; \ \ \'\ \ (\ \ \) \ (\' \ \')"
  by (auto simp: subst_eq_def)

lemma var_self: "[(v, Var v)] \ []"
proof
  fix t show "t \ [(v, Var v)] = t \ []"
    by (induct t) simp_all
qed

lemma var_same[simp]: "[(v, t)] \ [] \ t = Var v"
by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)

lemma vars_of_subst_conv_Union: "vars_of (t \ \) = \(vars_of ` (\x. Var x \ \) ` vars_of t)"
  by (induction t) simp_all

lemma domain_comp: "fst ` set (\ \ \) = fst ` (set \ \ set \)"
  by (induction \<sigma> \<theta> rule: comp.induct) auto

subsection \<open>Unifiers and Most General Unifiers\<close>

definition Unifier :: "'a subst \ 'a trm \ 'a trm \ bool"
  where "Unifier \ t u \ (t \ \ = u \ \)"

lemma not_occs_if_Unifier:
  assumes "Unifier \ t u"
  shows "\ (t \ u) \ \ (u \ t)"
proof -
  from assms have "t \ \ = u \ \"
    unfolding Unifier_def by simp
  thus ?thesis
    using neq_if_occs subst_mono by metis
qed

definition MGU :: "'a subst \ 'a trm \ 'a trm \ bool" where
  "MGU \ t u \
   Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"

lemma MGUI[intro]:
  "\t \ \ = u \ \; \\. t \ \ = u \ \ \ \\. \ \ \ \ \\
  \<Longrightarrow> MGU \<sigma> t u"
  by (simp only:Unifier_def MGU_def, auto)

lemma MGU_sym[sym]:
  "MGU \ s t \ MGU \ t s"
  by (auto simp:MGU_def Unifier_def)

lemma MGU_is_Unifier: "MGU \ t u \ Unifier \ t u"
unfolding MGU_def by (rule conjunct1)

lemma MGU_Var:
  assumes "\ Var v \ t"
  shows "MGU [(v,t)] (Var v) t"
proof (intro MGUI exI)
  show "Var v \ [(v,t)] = t \ [(v,t)]" using assms
    by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
next
  fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>"
  show "\ \ [(v,t)] \ \"
  proof
    fix s show "s \ \ = s \ [(v,t)] \ \" using th
      by (induct s) auto
  qed
qed

lemma MGU_Const: "MGU [] (Const c) (Const d) \ c = d"
  by (auto simp: MGU_def Unifier_def)


subsection \<open>The unification algorithm\<close>

function unify :: "'a trm \ 'a trm \ 'a subst option"
where
  "unify (Const c) (M \ N) = None"
| "unify (M \ N) (Const c) = None"
| "unify (Const c) (Var v) = Some [(v, Const c)]"
| "unify (M \ N) (Var v) = (if Var v \ M \ N
                                        then None
                                        else Some [(v, M \<cdot> N)])"
| "unify (Var v) M = (if Var v \ M
                                        then None
                                        else Some [(v, M)])"
| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
| "unify (M \ N) (M' \ N') = (case unify M M' of
                                    None \<Rightarrow> None |
                                    Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
                                      of None \<Rightarrow> None |
                                         Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
  by pat_completeness auto

subsection \<open>Properties used in termination proof\<close>

text \<open>Elimination of variables by a substitution:\<close>

definition
  "elim \ v \ \t. v \ vars_of (t \ \)"

lemma elim_intro[intro]: "(\t. v \ vars_of (t \ \)) \ elim \ v"
  by (auto simp:elim_def)

lemma elim_dest[dest]: "elim \ v \ v \ vars_of (t \ \)"
  by (auto simp:elim_def)

lemma elim_eq: "\ \ \ \ elim \ x = elim \ x"
  by (auto simp:elim_def subst_eq_def)

lemma occs_elim: "\ Var v \ t
  \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
by (metis elim_intro remove_var var_same vars_iff_occseq)

text \<open>The result of a unification never introduces new variables:\<close>

declare unify.psimps[simp]

lemma unify_vars:
  assumes "unify_dom (M, N)"
  assumes "unify M N = Some \"
  shows "vars_of (t \ \) \ vars_of M \ vars_of N \ vars_of t"
  (is "?P M N \ t")
using assms
proof (induct M N arbitrary:\<sigma> t)
  case (3 c v)
  hence "\ = [(v, Const c)]" by simp
  thus ?case by (induct t) auto
next
  case (4 M N v)
  hence "\ Var v \ M \ N" by auto
  with 4 have "\ = [(v, M\N)]" by simp
  thus ?case by (induct t) auto
next
  case (5 v M)
  hence "\ Var v \ M" by auto
  with 5 have "\ = [(v, M)]" by simp
  thus ?case by (induct t) auto
next
  case (7 M N M' N' \<sigma>)
  then obtain \<theta>1 \<theta>2
    where "unify M M' = Some \1"
    and "unify (N \ \1) (N' \ \1) = Some \2"
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
    and ih1: "\t. ?P M M' \1 t"
    and ih2: "\t. ?P (N\\1) (N'\\1) \2 t"
    by (auto split:option.split_asm)

  show ?case
  proof
    fix v assume a: "v \ vars_of (t \ \)"

    show "v \ vars_of (M \ N) \ vars_of (M' \ N') \ vars_of t"
    proof (cases "v \ vars_of M \ v \ vars_of M'
        \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
      case True
      with ih1 have l:"\t. v \ vars_of (t \ \1) \ v \ vars_of t"
        by auto

      from a and ih2[where t="t \ \1"]
      have "v \ vars_of (N \ \1) \ vars_of (N' \ \1)
        \<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
        by auto
      hence "v \ vars_of t"
      proof
        assume "v \ vars_of (N \ \1) \ vars_of (N' \ \1)"
        with True show ?thesis by (auto dest:l)
      next
        assume "v \ vars_of (t \ \1)"
        thus ?thesis by (rule l)
      qed

      thus ?thesis by auto
    qed auto
  qed
qed (auto split: if_split_asm)

text \<open>The result of a unification is either the identity
substitution or it eliminates a variable from one of the terms:\<close>

lemma unify_eliminates:
  assumes "unify_dom (M, N)"
  assumes "unify M N = Some \"
  shows "(\v\vars_of M \ vars_of N. elim \ v) \ \ \ []"
  (is "?P M N \")
using assms
proof (induct M N arbitrary:\<sigma>)
  case 1 thus ?case by simp
next
  case 2 thus ?case by simp
next
  case (3 c v)
  have no_occs: "\ Var v \ Const c" by simp
  with 3 have "\ = [(v, Const c)]" by simp
  with occs_elim[OF no_occs]
  show ?case by auto
next
  case (4 M N v)
  hence no_occs: "\ Var v \ M \ N" by auto
  with 4 have "\ = [(v, M\N)]" by simp
  with occs_elim[OF no_occs]
  show ?case by auto
next
  case (5 v M)
  hence no_occs: "\ Var v \ M" by auto
  with 5 have "\ = [(v, M)]" by simp
  with occs_elim[OF no_occs]
  show ?case by auto
next
  case (6 c d) thus ?case
    by (cases "c = d") auto
next
  case (7 M N M' N' \<sigma>)
  then obtain \<theta>1 \<theta>2
    where "unify M M' = Some \1"
    and "unify (N \ \1) (N' \ \1) = Some \2"
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
    and ih1: "?P M M' \1"
    and ih2: "?P (N\\1) (N'\\1) \2"
    by (auto split:option.split_asm)

  from \<open>unify_dom (M \<cdot> N, M' \<cdot> N')\<close>
  have "unify_dom (M, M')"
    by (rule accp_downward) (rule unify_rel.intros)
  hence no_new_vars:
    "\t. vars_of (t \ \1) \ vars_of M \ vars_of M' \ vars_of t"
    by (rule unify_vars) (rule \<open>unify M M' = Some \<theta>1\<close>)

  from ih2 show ?case
  proof
    assume "\v\vars_of (N \ \1) \ vars_of (N' \ \1). elim \2 v"
    then obtain v
      where "v\vars_of (N \ \1) \ vars_of (N' \ \1)"
      and el: "elim \2 v" by auto
    with no_new_vars show ?thesis unfolding \<sigma>
      by (auto simp:elim_def)
  next
    assume empty[simp]: "\2 \ []"

    have "\ \ (\1 \ [])" unfolding \
      by (rule subst_cong) auto
    also have "\ \ \1" by auto
    finally have "\ \ \1" .

    from ih1 show ?thesis
    proof
      assume "\v\vars_of M \ vars_of M'. elim \1 v"
      with elim_eq[OF \<open>\<sigma> \<doteq> \<theta>1\<close>]
      show ?thesis by auto
    next
      note \<open>\<sigma> \<doteq> \<theta>1\<close>
      also assume "\1 \ []"
      finally show ?thesis ..
    qed
  qed
qed

declare unify.psimps[simp del]

subsection \<open>Termination proof\<close>

termination unify
proof
  let ?R = "measures [\(M,N). card (vars_of M \ vars_of N),
                           \<lambda>(M, N). size M]"
  show "wf ?R" by simp

  fix M N M' N' :: "'a trm"
  show "((M, M'), (M \ N, M' \ N')) \ ?R" \ \Inner call\
    by (rule measures_lesseq) (auto intro: card_mono)

  fix \<theta>                                   \<comment> \<open>Outer call\<close>
  assume inner: "unify_dom (M, M')"
    "unify M M' = Some \"

  from unify_eliminates[OF inner]
  show "((N \ \, N' \ \), (M \ N, M' \ N')) \?R"
  proof
    \<comment> \<open>Either a variable is eliminated \ldots\<close>
    assume "(\v\vars_of M \ vars_of M'. elim \ v)"
    then obtain v
      where "elim \ v"
      and "v\vars_of M \ vars_of M'" by auto
    with unify_vars[OF inner]
    have "vars_of (N\\) \ vars_of (N'\\)
      \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
      by auto

    thus ?thesis
      by (auto intro!: measures_less intro: psubset_card_mono)
  next
    \<comment> \<open>Or the substitution is empty\<close>
    assume "\ \ []"
    hence "N \ \ = N"
      and "N' \ \ = N'" by auto
    thus ?thesis
       by (auto intro!: measures_less intro: psubset_card_mono)
  qed
qed

subsection \<open>Unification returns a Most General Unifier\<close>

lemma unify_computes_MGU:
  "unify M N = Some \ \ MGU \ M N"
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
  case (7 M N M' N' \<sigma>) \<comment> \<open>The interesting case\<close>

  then obtain \<theta>1 \<theta>2
    where "unify M M' = Some \1"
    and "unify (N \ \1) (N' \ \1) = Some \2"
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
    and MGU_inner: "MGU \1 M M'"
    and MGU_outer: "MGU \2 (N \ \1) (N' \ \1)"
    by (auto split:option.split_asm)

  show ?case
  proof
    from MGU_inner and MGU_outer
    have "M \ \1 = M' \ \1"
      and "N \ \1 \ \2 = N' \ \1 \ \2"
      unfolding MGU_def Unifier_def
      by auto
    thus "M \ N \ \ = M' \ N' \ \" unfolding \
      by simp
  next
    fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
    hence "M \ \' = M' \ \'"
      and Ns: "N \ \' = N' \ \'" by auto

    with MGU_inner obtain \<delta>
      where eqv: "\' \ \1 \ \"
      unfolding MGU_def Unifier_def
      by auto

    from Ns have "N \ \1 \ \ = N' \ \1 \ \"
      by (simp add:subst_eq_dest[OF eqv])

    with MGU_outer obtain \<rho>
      where eqv2: "\ \ \2 \ \"
      unfolding MGU_def Unifier_def
      by auto

    have "\' \ \ \ \" unfolding \
      by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
    thus "\\. \' \ \ \ \" ..
  qed
qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: if_split_asm)

subsection \<open>Unification returns Idempotent Substitution\<close>

definition Idem :: "'a subst \ bool"
where "Idem s \ (s \ s) \ s"

lemma Idem_Nil [iff]: "Idem []"
  by (simp add: Idem_def)

lemma Var_Idem:
  assumes "~ (Var v \ t)" shows "Idem [(v,t)]"
  unfolding Idem_def
proof
  from assms have [simp]: "t \ [(v, t)] = t"
    by (metis assoc.simps(2) subst.simps(1) subst_no_occs)

  fix s show "s \ [(v, t)] \ [(v, t)] = s \ [(v, t)]"
    by (induct s) auto
qed

lemma Unifier_Idem_subst:
  "Idem(r) \ Unifier s (t \ r) (u \ r) \
    Unifier (r \<lozenge> s) (t \<lhd> r) (u \<lhd> r)"
by (simp add: Idem_def Unifier_def subst_eq_def)

lemma Idem_comp:
  "Idem r \ Unifier s (t \ r) (u \ r) \
      (!!q. Unifier q (t \<lhd> r) (u \<lhd> r) \<Longrightarrow> s \<lozenge> q \<doteq> q) \<Longrightarrow>
    Idem (r \<lozenge> s)"
  apply (frule Unifier_Idem_subst, blast)
  apply (force simp add: Idem_def subst_eq_def)
  done

theorem unify_gives_Idem:
  "unify M N = Some \ \ Idem \"
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
  case (7 M M' N N' \<sigma>)

  then obtain \<theta>1 \<theta>2
    where "unify M N = Some \1"
    and \<theta>2: "unify (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
    and "Idem \1"
    and "Idem \2"
    by (auto split: option.split_asm)

  from \<theta>2 have "Unifier \<theta>2 (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
    by (rule unify_computes_MGU[THEN MGU_is_Unifier])

  with \<open>Idem \<theta>1\<close>
  show "Idem \" unfolding \
  proof (rule Idem_comp)
    fix \<sigma> assume "Unifier \<sigma> (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
    with \<theta>2 obtain \<gamma> where \<sigma>: "\<sigma> \<doteq> \<theta>2 \<lozenge> \<gamma>"
      using unify_computes_MGU MGU_def by blast

    have "\2 \ \ \ \2 \ (\2 \ \)" by (rule subst_cong) (auto simp: \)
    also have "... \ (\2 \ \2) \ \" by (rule comp_assoc[symmetric])
    also have "... \ \2 \ \" by (rule subst_cong) (auto simp: \Idem \2\[unfolded Idem_def])
    also have "... \ \" by (rule \[symmetric])
    finally show "\2 \ \ \ \" .
  qed
qed (auto intro!: Var_Idem split: option.splits if_splits)

subsection \<open>Unification Returns Substitution With Minimal Domain And Range\<close>

definition range_vars where
  "range_vars \ = \ {vars_of (Var x \ \) |x. Var x \ \ \ Var x}"

lemma vars_of_subst_subset: "vars_of (N \ \) \ vars_of N \ range_vars \"
proof (rule subsetI)
  fix x assume "x \ vars_of (N \ \)"
  thus "x \ vars_of N \ range_vars \"
  proof (induction N)
    case (Var y)
    thus ?case
      unfolding range_vars_def vars_of.simps by force
  next
    case (Const y)
    thus ?case
      by simp
  next
    case (Comb N1 N2)
    thus ?case
      by auto
  qed
qed

lemma range_vars_comp_subset: "range_vars (\\<^sub>1 \ \\<^sub>2) \ range_vars \\<^sub>1 \ range_vars \\<^sub>2"
proof (rule subsetI)
  fix x assume "x \ range_vars (\\<^sub>1 \ \\<^sub>2)"
  then obtain x' where
    x'_\\<^sub>1_\\<^sub>2: "Var x' \ \\<^sub>1 \ \\<^sub>2 \ Var x'" and x_in: "x \ vars_of (Var x' \ \\<^sub>1 \ \\<^sub>2)"
    unfolding range_vars_def by auto

  show "x \ range_vars \\<^sub>1 \ range_vars \\<^sub>2"
  proof (cases "Var x' \ \\<^sub>1 = Var x'")
    case True
    with x'_\\<^sub>1_\\<^sub>2 x_in show ?thesis
      unfolding range_vars_def by auto
  next
    case x'_\\<^sub>1_neq: False
    show ?thesis
    proof (cases "Var x' \ \\<^sub>1 \ \\<^sub>2 = Var x' \ \\<^sub>1")
      case True
      with x'_\\<^sub>1_\\<^sub>2 x_in x'_\\<^sub>1_neq show ?thesis
        unfolding range_vars_def by auto
    next
      case False
      with x_in obtain y where "y \ vars_of (Var x' \ \\<^sub>1)" and "x \ vars_of (Var y \ \\<^sub>2)"
        by (metis (no_types, lifting) UN_E UN_simps(10) vars_of_subst_conv_Union)
      with x'_\\<^sub>1_neq show ?thesis
        unfolding range_vars_def by force
    qed
  qed
qed

theorem unify_gives_minimal_range:
  "unify M N = Some \ \ range_vars \ \ vars_of M \ vars_of N"
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
  case (1 c M N)
  thus ?case by simp
next
  case (2 M N c)
  thus ?case by simp
next
  case (3 c v)
  hence "\ = [(v, Const c)]"
    by simp
  thus ?case
    by (simp add: range_vars_def)
next
  case (4 M N v)
  hence "\ = [(v, M \ N)]"
    by (metis option.discI option.sel unify.simps(4))
  thus ?case
    by (auto simp: range_vars_def)
next
  case (5 v M)
  hence "\ = [(v, M)]"
    by (metis option.discI option.inject unify.simps(5))
  thus ?case
    by (auto simp: range_vars_def)
next
  case (6 c d)
  hence "\ = []"
    by (metis option.distinct(1) option.sel unify.simps(6))
  thus ?case
    by (simp add: range_vars_def)
next
  case (7 M N M' N')
  from "7.prems" obtain \<theta>\<^sub>1 \<theta>\<^sub>2 where
    "unify M M' = Some \\<^sub>1" and "unify (N \ \\<^sub>1) (N' \ \\<^sub>1) = Some \\<^sub>2" and "\ = \\<^sub>1 \ \\<^sub>2"
    apply simp
    by (metis (no_types, lifting) option.case_eq_if option.collapse option.discI option.sel)

  from "7.hyps"(1) have range_\<theta>\<^sub>1: "range_vars \<theta>\<^sub>1 \<subseteq> vars_of M \<union> vars_of M'"
    using \<open>unify M M' = Some \<theta>\<^sub>1\<close> by simp

  from "7.hyps"(2) have "range_vars \\<^sub>2 \ vars_of (N \ \\<^sub>1) \ vars_of (N' \ \\<^sub>1)"
    using \<open>unify M M' = Some \<theta>\<^sub>1\<close> \<open>unify (N \<lhd> \<theta>\<^sub>1) (N' \<lhd> \<theta>\<^sub>1) = Some \<theta>\<^sub>2\<close> by simp
  hence range_\<theta>\<^sub>2: "range_vars \<theta>\<^sub>2 \<subseteq> vars_of N \<union> vars_of N' \<union> range_vars \<theta>\<^sub>1"
    using vars_of_subst_subset[of _ \<theta>\<^sub>1] by auto

  have "range_vars \ = range_vars (\\<^sub>1 \ \\<^sub>2)"
    unfolding \<open>\<sigma> = \<theta>\<^sub>1 \<lozenge> \<theta>\<^sub>2\<close> by simp
  also have "... \ range_vars \\<^sub>1 \ range_vars \\<^sub>2"
    by (rule range_vars_comp_subset)
  also have "... \ range_vars \\<^sub>1 \ vars_of N \ vars_of N'"
    using range_\<theta>\<^sub>2 by auto
  also have "... \ vars_of M \ vars_of M' \ vars_of N \ vars_of N'"
    using range_\<theta>\<^sub>1 by auto
  finally show ?case
    by auto
qed

theorem unify_gives_minimal_domain:
  "unify M N = Some \ \ fst ` set \ \ vars_of M \ vars_of N"
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
  case (1 c M N)
  thus ?case
    by simp
next
  case (2 M N c)
  thus ?case
    by simp
next
  case (3 c v)
  hence "\ = [(v, Const c)]"
    by simp
  thus ?case
    by (simp add: dom_def)
next
  case (4 M N v)
  hence "\ = [(v, M \ N)]"
    by (metis option.distinct(1) option.inject unify.simps(4))
  thus ?case
    by (simp add: dom_def)
next
  case (5 v M)
  hence "\ = [(v, M)]"
    by (metis option.distinct(1) option.inject unify.simps(5))
  thus ?case
    by (simp add: dom_def)
next
  case (6 c d)
  hence "\ = []"
    by (metis option.distinct(1) option.sel unify.simps(6))
  thus ?case
    by simp
next
  case (7 M N M' N')
  from "7.prems" obtain \<theta>\<^sub>1 \<theta>\<^sub>2 where
    "unify M M' = Some \\<^sub>1" and "unify (N \ \\<^sub>1) (N' \ \\<^sub>1) = Some \\<^sub>2" and "\ = \\<^sub>1 \ \\<^sub>2"
    apply simp
    by (metis (no_types, lifting) option.case_eq_if option.collapse option.discI option.sel)

  from "7.hyps"(1) have dom_\<theta>\<^sub>1: "fst ` set \<theta>\<^sub>1 \<subseteq> vars_of M \<union> vars_of M'"
    using \<open>unify M M' = Some \<theta>\<^sub>1\<close> by simp

  from "7.hyps"(2) have "fst ` set \\<^sub>2 \ vars_of (N \ \\<^sub>1) \ vars_of (N' \ \\<^sub>1)"
    using \<open>unify M M' = Some \<theta>\<^sub>1\<close> \<open>unify (N \<lhd> \<theta>\<^sub>1) (N' \<lhd> \<theta>\<^sub>1) = Some \<theta>\<^sub>2\<close> by simp
  hence dom_\<theta>\<^sub>2: "fst ` set \<theta>\<^sub>2 \<subseteq> vars_of N \<union> vars_of N' \<union> range_vars \<theta>\<^sub>1"
    using vars_of_subst_subset[of _ \<theta>\<^sub>1] by auto

  have "fst ` set \ = fst ` set (\\<^sub>1 \ \\<^sub>2)"
    unfolding \<open>\<sigma> = \<theta>\<^sub>1 \<lozenge> \<theta>\<^sub>2\<close> by simp
  also have "... = fst ` set \\<^sub>1 \ fst ` set \\<^sub>2"
    by (auto simp: domain_comp)
  also have "... \ vars_of M \ vars_of M' \ fst ` set \\<^sub>2"
    using dom_\<theta>\<^sub>1 by auto
  also have "... \ vars_of M \ vars_of M' \ vars_of N \ vars_of N' \ range_vars \\<^sub>1"
    using dom_\<theta>\<^sub>2 by auto
  also have "... \ vars_of M \ vars_of M' \ vars_of N \ vars_of N'"
    using unify_gives_minimal_range[OF \<open>unify M M' = Some \<theta>\<^sub>1\<close>] by auto
  finally show ?case
    by auto
qed

subsection \<open>Idempotent Most General Unifier\<close>

definition IMGU :: "'a subst \ 'a trm \ 'a trm \ bool" where
  "IMGU \ t u \ Unifier \ t u \ (\\. Unifier \ t u \ \ \ \ \ \)"

lemma IMGU_iff_Idem_and_MGU: "IMGU \ t u \ Idem \ \ MGU \ t u"
  unfolding IMGU_def Idem_def MGU_def
  by (meson Unification.comp_assoc subst_cong subst_refl subst_sym subst_trans)

lemma unify_computes_IMGU:
  "unify M N = Some \ \ IMGU \ M N"
  by (simp add: IMGU_iff_Idem_and_MGU unify_computes_MGU unify_gives_Idem)

subsection \<open>Unification is complete\<close>

lemma unify_eq_Some_if_Unifier:
  assumes "Unifier \ t u"
  shows "\\. unify t u = Some \"
  using assms
proof (induction t u rule: unify.induct)
  case (1 c M N)
  thus ?case
    by (simp add: Unifier_def)
next
  case (2 M N c)
  thus ?case
    by (simp add: Unifier_def)
next
  case (3 c v)
  thus ?case
    by simp
next
  case (4 M N v)
  hence "\ (Var v \ M \ N)"
    by (auto dest: not_occs_if_Unifier)
  thus ?case
    by simp
next
  case (5 v M)
  thus ?case
    by (auto dest: not_occs_if_Unifier)
next
  case (6 c d)
  thus ?case
    by (simp add: Unifier_def)
next
  case (7 M N M' N')
  from "7.prems" have "Unifier \ M M'"
    by (simp add: Unifier_def)
  with "7.IH"(1) obtain \<tau> where \<tau>: "unify M M' = Some \<tau>"
    by auto
  then have "Unifier \ (N \ \) (N' \ \)"
    unfolding Unifier_def
    by (metis "7.prems" IMGU_def Unifier_def subst.simps(3) subst_comp subst_eq_def trm.distinct(3) trm.distinct(5) trm.exhaust trm.inject(3) unify_computes_IMGU)
  with \<tau> show ?case
    using "7.IH"(2) by auto
qed

definition subst_domain where
  "subst_domain \ = {x. Var x \ \ \ Var x}"

lemma subst_domain_subset_list_domain: "subst_domain \ \ fst ` set \"
proof (rule Set.subsetI)
  fix x assume "x \ subst_domain \"
  hence "Var x \ \ \ Var x"
    by (simp add: subst_domain_def)
  then show "x \ fst ` set \"
  proof (induction \<sigma>)
    case Nil
    thus ?case
      by simp
  next
    case (Cons p \<sigma>)
    show ?case
    proof (cases "x = fst p")
      case True
      thus ?thesis
        by simp
    next
      case False
      with Cons.IH Cons.prems show ?thesis
        by (cases p) simp
    qed
  qed
qed

lemma subst_apply_eq_Var:
  assumes "s \ \ = Var x"
  obtains y where "s = Var y" and "Var y \ \ = Var x"
  using assms by (induct s) auto

lemma mem_range_varsI:
  assumes "Var x \ \ = Var y" and "x \ y"
  shows "y \ range_vars \"
  using assms unfolding range_vars_def
  by (metis (mono_tags, lifting) UnionI mem_Collect_eq trm.inject(1) vars_iff_occseq)

lemma IMGU_subst_domain_subset:
  assumes "IMGU \ t u"
  shows "subst_domain \ \ vars_of t \ vars_of u"
proof (rule Set.subsetI)
  from assms have "Unifier \ t u"
    by (simp add: IMGU_def)
  then obtain \<upsilon> where "unify t u = Some \<upsilon>"
    using unify_eq_Some_if_Unifier by metis
  hence "Unifier \ t u"
    using MGU_def unify_computes_MGU by blast
  with assms have "\ \ \ \ \"
    by (simp add: IMGU_def)

  fix x assume "x \ subst_domain \"
  hence "Var x \ \ \ Var x"
    by (simp add: subst_domain_def)

  show "x \ vars_of t \ vars_of u"
  proof (cases "x \ subst_domain \")
    case True
    hence "x \ fst ` set \"
      using subst_domain_subset_list_domain by fast
    thus ?thesis
      using unify_gives_minimal_domain[OF \<open>unify t u = Some \<upsilon>\<close>] by auto
  next
    case False
    hence "Var x \ \ = Var x"
      by (simp add: subst_domain_def)
    hence "Var x \ \ \ \ = Var x"
      using \<open>\<upsilon> \<doteq> \<mu> \<lozenge> \<upsilon>\<close>
      by (metis subst_comp subst_eq_dest)
    then show ?thesis
      apply (rule subst_apply_eq_Var)
      using \<open>Var x \<lhd> \<mu> \<noteq> Var x\<close>
      using unify_gives_minimal_range[OF \<open>unify t u = Some \<upsilon>\<close>]
      using mem_range_varsI
      by force
  qed
qed

lemma IMGU_range_vars_subset:
  assumes "IMGU \ t u"
  shows "range_vars \ \ vars_of t \ vars_of u"
proof (rule Set.subsetI)
  from assms have "Unifier \ t u"
    by (simp add: IMGU_def)
  then obtain \<upsilon> where "unify t u = Some \<upsilon>"
    using unify_eq_Some_if_Unifier by metis
  hence "Unifier \ t u"
    using MGU_def unify_computes_MGU by blast
  with assms have "\ \ \ \ \"
    by (simp add: IMGU_def)

  have ball_subst_dom: "\x \ subst_domain \. vars_of (Var x \ \) \ vars_of t \ vars_of u"
    using unify_gives_minimal_range[OF \<open>unify t u = Some \<upsilon>\<close>]
    using range_vars_def subst_domain_def by fastforce

  fix x assume "x \ range_vars \"
  then obtain y where "x \ vars_of (Var y \ \)" and "Var y \ \ \ Var y"
    by (auto simp: range_vars_def)

  have vars_of_y_\<upsilon>: "vars_of (Var y \<lhd> \<upsilon>) \<subseteq> vars_of t \<union> vars_of u"
    using ball_subst_dom
    by (metis (mono_tags, lifting) IMGU_subst_domain_subset \<open>Var y \<lhd> \<mu> \<noteq> Var y\<close> assms empty_iff
        insert_iff mem_Collect_eq subset_eq subst_domain_def vars_of.simps(1))

  show "x \ vars_of t \ vars_of u"
  proof (rule ccontr)
    assume "x \ vars_of t \ vars_of u"
    hence "x \ vars_of (Var y \ \)"
      using vars_of_y_\<upsilon> by blast
    moreover have "x \ vars_of (Var y \ \ \ \)"
    proof -
      have "Var x \ \ = Var x"
        using \<open>x \<notin> vars_of t \<union> vars_of u\<close>
        using IMGU_subst_domain_subset \<open>unify t u = Some \<upsilon>\<close> subst_domain_def unify_computes_IMGU
        by fastforce
      thus ?thesis
        by (metis \<open>x \<in> vars_of (Var y \<lhd> \<mu>)\<close> subst_mono vars_iff_occseq)
    qed
    ultimately show False
      using \<open>\<upsilon> \<doteq> \<mu> \<lozenge> \<upsilon>\<close>
      by (metis subst_comp subst_eq_dest)
  qed
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.