Theory Unifiers_More

subsubsection ‹Sets of Unifiers›

theory Unifiers_More
  imports
    First_Order_Terms.Term_More
    First_Order_Terms.Unifiers
begin

lemma is_mguI:
  fixes σ :: "('f, 'v) subst"
  assumes "∀(s, t) ∈ E. s ⋅ σ = t ⋅ σ"
    and "⋀τ :: ('f, 'v) subst. ∀(s, t) ∈ E. s ⋅ τ = t ⋅ τ ⟹ ∃γ :: ('f, 'v) subst. τ = σ ∘⇩s γ"
  shows "is_mgu σ E"
  using assms by (fastforce simp: is_mgu_def unifiers_def)

lemma subst_set_insert [simp]:
  "subst_set σ (insert e E) = insert (fst e ⋅ σ, snd e ⋅ σ) (subst_set σ E)"
  by (auto simp: subst_set_def)

lemma unifiable_UnD [dest]:
  "unifiable (M ∪ N) ⟹ unifiable M ∧ unifiable N"
  by (auto simp: unifiable_def)

lemma supt_imp_not_unifiable:
  assumes "s ⊳ t"
  shows "¬ unifiable {(t, s)}"
proof
  assume "unifiable {(t, s)}"
  then obtain σ where "σ ∈ unifiers {(t, s)}"
    by (auto simp: unifiable_def)
  then have "t ⋅ σ = s ⋅ σ" by (auto)
  moreover have "s ⋅ σ ⊳ t ⋅ σ"
    using assms by (metis instance_no_supt_imp_no_supt)
  ultimately show False by auto
qed

lemma unifiable_insert_Var_swap [simp]:
  "unifiable (insert (t, Var x) E) ⟷ unifiable (insert (Var x, t) E)"
  by (rule unifiable_insert_swap)

lemma unifiers_Int1 [simp]:
  "(s, t) ∈ E ⟹ unifiers {(s, t)} ∩ unifiers E = unifiers E"
  by (auto simp: unifiers_def)

lemma imgu_linear_var_disjoint:
  assumes "is_imgu σ {(l2 |_ p, l1)}"
    and "p ∈ poss l2"
    and "linear_term l2"
    and "vars_term l1 ∩ vars_term l2 = {}"
    and "q ∈ poss l2"
    and "parallel_pos p q"
  shows "l2 |_ q = l2 |_ q ⋅ σ"
  using assms
proof (induct p arbitrary: q l2)
  case (Cons i p)
  from this(3) obtain f ls where 
    l2[simp]: "l2 = Fun f ls" and 
    i: "i < length ls" and 
    p: "p ∈ poss (ls ! i)"
    by (cases l2) (auto)
  then have l2i: "l2 |_ ((i # p)) = ls ! i |_ p" by auto
  have "linear_term (ls ! i)" using Cons(4) l2 i by simp
  moreover have "vars_term l1 ∩ vars_term (ls ! i) = {}" using Cons(5) l2 i by force
  ultimately have IH: "⋀q. q ∈ poss (ls ! i) ⟹ p ⊥ q ⟹ ls ! i |_ q = ls ! i |_ q ⋅ σ" 
    using Cons(1)[OF Cons(2)[unfolded l2i] p] by blast
  from Cons(7) obtain j q' where q: "q = j # q'" by (cases q) auto
  show ?case
  proof (cases "j = i") 
    case True with Cons(6,7) IH q show ?thesis by simp
  next
    case False
    from Cons(6) q have j: "j < length ls" by simp 
    { fix y
      assume y: "y ∈ vars_term (l2 |_ q)"
      let ?τ = "λx. if x = y then Var y else σ x"
      from y Cons(6) q j have yj:"y ∈ vars_term (ls ! j)" 
        by simp (meson subt_at_imp_supteq subteq_Var_imp_in_vars_term supteq_Var supteq_trans)
      { fix i j
        assume j:"j < length ls" and i:"i < length ls" and neq: "i ≠ j"
        from j Cons(4) have "∀i < j. vars_term (ls ! i) ∩ vars_term (ls ! j) = {}"
          by (auto simp : is_partition_def)
        moreover from i Cons(4) have "∀j < i. vars_term (ls ! i) ∩ vars_term (ls ! j) = {}"
          by (auto simp : is_partition_def)
        ultimately have "vars_term (ls ! i) ∩ vars_term (ls ! j) = {}" 
          using neq by (cases "i < j") auto
      }
      from this[OF i j False] have "y ∉ vars_term (ls ! i)" using yj by auto
      then have "y ∉ vars_term (l2 |_ ((i # p)))"
        by (metis l2i p subt_at_imp_supteq subteq_Var_imp_in_vars_term supteq_Var supteq_trans)
      then have "∀x ∈ vars_term (l2 |_ ((i # p))). ?τ x = σ x" by auto
      then have l2τσ: "l2 |_ ((i # p)) ⋅ ?τ = l2 |_ ((i # p)) ⋅ σ" using term_subst_eq[of _ σ ?τ] by simp
      from Cons(5) have "y ∉ vars_term l1" using y Cons(6) vars_term_subt_at by fastforce
      then have "∀x ∈ vars_term l1. ?τ x = σ x" by auto
      then have l1τσ:"l1 ⋅ ?τ = l1 ⋅ σ" using term_subst_eq[of _ σ ?τ] by simp
      have "l1 ⋅ σ = l2 |_ (i # p) ⋅ σ" using Cons(2) unfolding is_imgu_def by auto
      then have "l1 ⋅ ?τ = l2 |_ (i # p) ⋅ ?τ"  using l1τσ l2τσ by simp
      then have "?τ ∈ unifiers {(l2 |_ (i # p), l1)}" unfolding unifiers_def by simp
      with Cons(2) have τσ:"?τ = σ ∘⇩s ?τ" unfolding is_imgu_def by blast
      have "Var y = Var y ⋅ σ"
      proof (rule ccontr)
        let ?x = "Var y ⋅ σ"
        assume *:"Var y ≠ ?x"
        have "Var y = Var y ⋅ ?τ" by auto
        also have "... = (Var y ⋅ σ) ⋅ ?τ" using τσ subst_subst by metis 
        finally have xy:"?x ⋅ σ = Var y" using * by (cases "σ y") auto 
        have "σ ∘⇩s σ = σ" using Cons(2) unfolding is_imgu_def by auto
        then have "?x ⋅ (σ ∘⇩s σ) = Var y" using xy by auto
        moreover have "?x ⋅ σ ⋅ σ = ?x" using xy by auto
        ultimately show False using * by auto
      qed
    }
    then show ?thesis by (simp add: term_subst_eq)
  qed
qed auto

end