Theory Combinability

section ‹Combinability›

text ‹This section corresponds to Section 3 of the paper~\<^cite>‹"UnboundedSL"›.›

theory Combinability
  imports UnboundedLogic
begin

context logic
begin

text ‹The definition of combinable assertions corresponds to Definition 4 of the paper~\<^cite>‹"UnboundedSL"›.›

definition combinable :: "('d, 'c, 'a) interp ⇒ ('a, 'b, 'c, 'd) assertion ⇒ bool" where
  "combinable Δ A ⟷ (∀p q. Star (Mult p A) (Mult q A), Δ ⊢ Mult (sadd p q) A)"

lemma combinable_instantiate:
  assumes "combinable Δ A"
      and "a, s, Δ ⊨ A"
      and "b, s, Δ ⊨ A"
      and "Some x = p ⊙ a ⊕ q ⊙ b"
    shows "x, s, Δ ⊨ Mult (sadd p q) A"
  by (meson assms(1) assms(2) assms(3) assms(4) combinable_def entails_def logic.sat.simps(2) logic_axioms sat.simps(1))

lemma combinable_instantiate_one:
  assumes "combinable Δ A"
      and "a, s, Δ ⊨ A"
      and "b, s, Δ ⊨ A"
      and "Some x = p ⊙ a ⊕ q ⊙ b"
      and "sadd p q = one"
    shows "x, s, Δ ⊨ A"
  using assms(1) assms(2) assms(3) assms(4) assms(5) combinable_instantiate one_neutral by fastforce

lemma combinableI_old:
  assumes "⋀a b p q x σ s. a, s, Δ ⊨ A ∧ b, s, Δ ⊨ A ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = (sadd p q) ⊙ x ⟹ x, s, Δ ⊨ A"
  shows "combinable Δ A"
proof -
  have "⋀p q. Star (Mult p A) (Mult q A), Δ ⊢ Mult (sadd p q) A"
  proof (rule entailsI)
    fix p q σ s
    assume "σ, s, Δ ⊨ Star (Mult p A) (Mult q A)"
    then obtain a b where "a, s, Δ ⊨ A ∧ b, s, Δ ⊨ A ∧ Some σ = p ⊙ a ⊕ q ⊙ b"
      by auto
    moreover obtain x where "σ = (sadd p q) ⊙ x"
      using unique_inv by auto
    ultimately have "x, s, Δ ⊨ A" using assms
      by blast
    then show "σ, s, Δ ⊨ Mult (sadd p q) A"
      using ‹σ = sadd p q ⊙ x› by fastforce
    qed
  then show ?thesis
    by (simp add: combinable_def)
qed


lemma combinableI:
  assumes "⋀a b p q x σ s. a, s, Δ ⊨ A ∧ b, s, Δ ⊨ A ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one ⟹ x, s, Δ ⊨ A"
  shows "combinable Δ A"
proof (rule combinableI_old)
  fix a b p q x σ s
  assume "a, s, Δ ⊨ A ∧ b, s, Δ ⊨ A ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x"
  let ?p = "smult (sinv (sadd p q)) p"
  let ?q = "smult (sinv (sadd p q)) q"
  have "Some x = ?p ⊙ a ⊕ ?q ⊙ b"
  proof -
    have "Some ((smult (sinv (sadd p q)) (sadd p q)) ⊙ x) = ?p ⊙ a ⊕ ?q ⊙ b"
      by (metis ‹a, s, Δ ⊨ A ∧ b, s, Δ ⊨ A ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› double_mult logic.plus_mult logic_axioms)
    then show ?thesis
      by (simp add: one_neutral sinv_inverse smult_comm)
  qed
  moreover have "sadd ?p ?q = one"
    by (metis logic.smult_comm logic_axioms sinv_inverse smult_distrib)
  ultimately show "x, s, Δ ⊨ A"
    using ‹a, s, Δ ⊨ A ∧ b, s, Δ ⊨ A ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› assms by blast
qed


lemma combinable_wand:
  assumes "combinable Δ B"
    shows "combinable Δ (Wand A B)"
proof (rule combinableI_old)
  fix a b p q x σ s
  assume "a, s, Δ ⊨ Wand A B ∧ b, s, Δ ⊨ Wand A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x"
  show "x, s, Δ ⊨ Wand A B"
  proof (rule sat_wand)
    fix aa σ'
    assume "aa, s, Δ ⊨ A ∧ Some σ' = x ⊕ aa"
    then have "Some ((sadd p q) ⊙ σ') = σ ⊕ ((sadd p q) ⊙ aa)"
      by (simp add: ‹a, s, Δ ⊨ Wand A B ∧ b, s, Δ ⊨ Wand A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› plus_mult)
    moreover have "Some ((sadd p q) ⊙ aa) = p ⊙ aa ⊕ q ⊙ aa"
      by (simp add: distrib_mult)
    moreover have "a ## aa"
    proof -
      have "p ⊙ a ## (sadd p q) ⊙ aa"
        by (metis ‹a, s, Δ ⊨ Wand A B ∧ b, s, Δ ⊨ Wand A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› asso2 calculation(1) commutative compatible_def option.discI)
      then show ?thesis
        using compatible_multiples by blast
    qed
    then obtain aaa where "Some aaa = a ⊕ aa"
      using compatible_def by auto
    moreover have "b ## aa"
    proof -
      have "q ⊙ b ## (sadd p q) ⊙ aa"
        by (metis ‹a, s, Δ ⊨ Wand A B ∧ b, s, Δ ⊨ Wand A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› asso2 calculation(1) compatible_def option.discI)
      then show ?thesis
        using compatible_multiples by blast
    qed
    then obtain baa where "Some baa = b ⊕ aa"
      using compatible_def by auto
    ultimately have "Some (mult (sadd p q) σ') = p ⊙ aaa ⊕ q ⊙ baa"
    proof -
      obtain a1 where "Some a1 = σ ⊕ (p ⊙ aa)"
        by (metis ‹Some (sadd p q ⊙ σ') = σ ⊕ sadd p q ⊙ aa› compatible_multiples option.exhaust_sel pre_logic.compatible_def unique_inv)
      then obtain a2 where "Some a2 = p ⊙ a ⊕ (p ⊙ aa)"
        by (meson ‹⋀thesis. (⋀aaa. Some aaa = a ⊕ aa ⟹ thesis) ⟹ thesis› plus_mult)
      then have "Some a1 = a2 ⊕ q ⊙ b"
      proof -
        obtain bc where "q ⊙ b ⊕ p ⊙ aa = Some bc"
          by (metis ‹b ## aa› compatible_iff compatible_multiples one_neutral option.exhaust_sel pre_logic.compatible_def)
        then have "σ ⊕ p ⊙ aa = p ⊙ a ⊕ bc"
          using asso1[of "p ⊙ a" "q ⊙ b" σ "p ⊙ aa" bc]
          by (metis ‹a, s, Δ ⊨ Wand A B ∧ b, s, Δ ⊨ Wand A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x›)
        then show ?thesis
          by (metis ‹Some a1 = σ ⊕ p ⊙ aa› ‹Some a2 = p ⊙ a ⊕ p ⊙ aa› ‹q ⊙ b ⊕ p ⊙ aa = Some bc› asso1 commutative)
      qed
      moreover have "a2 = p ⊙ aaa"
        by (metis ‹Some a2 = p ⊙ a ⊕ p ⊙ aa› ‹Some aaa = a ⊕ aa› option.inject plus_mult)
      moreover have "Some (q ⊙ baa) = q ⊙ b ⊕ q ⊙ aa"
        by (simp add: ‹Some baa = b ⊕ aa› plus_mult)
      ultimately show ?thesis
        by (metis ‹Some (sadd p q ⊙ σ') = σ ⊕ sadd p q ⊙ aa› ‹Some (sadd p q ⊙ aa) = p ⊙ aa ⊕ q ⊙ aa› ‹Some a1 = σ ⊕ p ⊙ aa› asso1)
    qed
    moreover have "aaa, s, Δ ⊨ B ∧ baa, s, Δ ⊨ B"
      using ‹Some aaa = a ⊕ aa› ‹Some baa = b ⊕ aa› ‹a, s, Δ ⊨ Wand A B ∧ b, s, Δ ⊨ Wand A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› ‹aa, s, Δ ⊨ A ∧ Some σ' = x ⊕ aa› by auto
    ultimately have "mult (sadd p q) σ', s, Δ ⊨ Mult (sadd p q) B"
      by (meson assms logic.combinable_def logic.entails_def logic_axioms sat.simps(1) sat.simps(2))
    then show "σ', s, Δ ⊨ B"
      using can_divide sat.simps(1) by metis
  qed
qed

lemma combinable_star:
  assumes "combinable Δ A"
      and "combinable Δ B"
    shows "combinable Δ (Star A B)"
proof (rule combinableI_old)
  fix a b p q x σ s
  assume "a, s, Δ ⊨ Star A B ∧ b, s, Δ ⊨ Star A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x"
  then obtain aa ab ba bb where "Some a = aa ⊕ ab" "Some b = ba ⊕ bb" "aa, s, Δ ⊨ A"
   "ab, s, Δ ⊨ B" "ba, s, Δ ⊨ A" "bb, s, Δ ⊨ B"
    by auto
  then obtain xa xb where "Some xa = p ⊙ aa ⊕ q ⊙ ba" "Some xb = p ⊙ ab ⊕ q ⊙ bb"
    by (metis ‹a, s, Δ ⊨ Star A B ∧ b, s, Δ ⊨ Star A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› asso2 commutative compatible_iff compatible_multiples one_neutral option.discI option.exhaust_sel pre_logic.compatible_def)
  then have "xa, s, Δ ⊨ Mult (sadd p q) A"
    by (meson ‹aa, s, Δ ⊨ A› ‹ba, s, Δ ⊨ A› assms(1) entails_def logic.combinable_def logic.sat.simps(1) logic.sat.simps(2) logic_axioms)
  moreover have "xb, s, Δ ⊨ Mult (sadd p q) B"
    by (meson ‹Some xb = p ⊙ ab ⊕ q ⊙ bb› ‹ab, s, Δ ⊨ B› ‹bb, s, Δ ⊨ B› assms(2) combinable_def entails_def sat.simps(1) sat.simps(2))
  moreover have "Some σ = xa ⊕ xb"
    using ‹Some a = aa ⊕ ab› ‹Some b = ba ⊕ bb› ‹Some xa = p ⊙ aa ⊕ q ⊙ ba› ‹Some xb = p ⊙ ab ⊕ q ⊙ bb› ‹a, s, Δ ⊨ Star A B ∧ b, s, Δ ⊨ Star A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› move_sum plus_mult by blast
  then obtain xa' xb' where "Some x = xa' ⊕ xb'" "xa = sadd p q ⊙ xa'" "xb = sadd p q ⊙ xb'"
    by (metis ‹a, s, Δ ⊨ Star A B ∧ b, s, Δ ⊨ Star A B ∧ Some σ = p ⊙ a ⊕ q ⊙ b ∧ σ = sadd p q ⊙ x› plus_mult unique_inv)
  ultimately show "x, s, Δ ⊨ Star A B"
    by (metis logic.can_divide logic_axioms sat.simps(1) sat.simps(2))
qed

lemma combinable_mult:
  assumes "combinable Δ A"
  shows "combinable Δ (Mult π A)"
proof (rule combinableI)
  fix a b p q x σ s
  assume asm: "a, s, Δ ⊨ Mult π A ∧ b, s, Δ ⊨ Mult π A ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
  then obtain a' b' where "a', s, Δ ⊨ A" "b', s, Δ ⊨ A" "a = π ⊙ a'" "b = π ⊙ b'" by auto

  let ?p = "smult p π"
  let ?q = "smult q π"

  have "Some x = ?p ⊙ a' ⊕ ?q ⊙ b'"
    by (simp add: ‹a = π ⊙ a'› ‹b = π ⊙ b'› asm double_mult)
  moreover have "sadd ?p ?q = π"
    using asm smult_comm smult_distrib sone_neutral by force
  ultimately show "x, s, Δ ⊨ Mult π A"
    by (metis ‹a', s, Δ ⊨ A› ‹b', s, Δ ⊨ A› assms combinable_instantiate)
qed

lemma combinable_and:
  assumes "combinable Δ A"
      and "combinable Δ B"
    shows "combinable Δ (And A B)"
proof (rule combinableI)
  fix a b p q x σ s
  assume "a, s, Δ ⊨ And A B ∧ b, s, Δ ⊨ And A B ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
  then obtain "a, s, Δ ⊨ A" "b, s, Δ ⊨ A" "a, s, Δ ⊨ B" "b, s, Δ ⊨ B" by auto
  then show "x, s, Δ ⊨ And A B"
    by (meson ‹a, s, Δ ⊨ And A B ∧ b, s, Δ ⊨ And A B ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one› assms(1) assms(2) combinable_instantiate_one sat.simps(7))
qed


lemma combinable_forall:
  assumes "combinable Δ A"
    shows "combinable Δ (Forall x A)"
proof (rule combinableI)
  fix a b p q y σ s
  assume "a, s, Δ ⊨ Forall x A ∧ b, s, Δ ⊨ Forall x A ∧ Some y = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
  show "y, s, Δ ⊨ Forall x A"
  proof (rule sat_forall)
    fix v show "y, s(x := v), Δ ⊨ A"
      by (meson ‹a, s, Δ ⊨ Forall x A ∧ b, s, Δ ⊨ Forall x A ∧ Some y = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one› assms combinable_instantiate_one sat.simps(9))
  qed
qed




definition unambiguous where
  "unambiguous Δ A x ⟷ (∀σ1 σ2 v1 v2 s. σ1 ## σ2 ∧ σ1, s(x := v1), Δ ⊨ A ∧ σ2, s(x := v2), Δ ⊨ A ⟶ v1 = v2)"

lemma unambiguousI:
  assumes "⋀σ1 σ2 v1 v2 s. σ1 ## σ2 ∧ σ1, s(x := v1), Δ ⊨ A ∧ σ2, s(x := v2), Δ ⊨ A ⟹ v1 = v2"
  shows "unambiguous Δ A x"
  by (simp add: assms unambiguous_def)

lemma unambiguous_star:
  assumes "unambiguous Δ A x"
  shows "unambiguous Δ (Star A B) x"
proof (rule unambiguousI)
  fix σ1 σ2 v1 v2 s
  assume "σ1 ## σ2 ∧ σ1, s(x := v1), Δ ⊨ Star A B ∧ σ2, s(x := v2), Δ ⊨ Star A B"
  then obtain a1 b1 a2 b2 where "Some σ1 = a1 ⊕ b1" "Some σ2 = a2 ⊕ b2" "a1, s(x := v1), Δ ⊨ A"
 "a2, s(x := v2), Δ ⊨ A" "b1, s(x := v1), Δ ⊨ B" "b2, s(x := v2), Δ ⊨ B" by auto
  then have "a1 ## a2"
    by (metis ‹σ1 ## σ2 ∧ σ1, s(x := v1), Δ ⊨ Star A B ∧ σ2, s (x := v2), Δ ⊨ Star A B› asso2 asso3 commutative)
  then show "v1 = v2"
    using ‹a1, s(x := v1), Δ ⊨ A› ‹a2, s(x := v2), Δ ⊨ A› assms unambiguous_def by fastforce
qed


lemma combinable_exists:
  assumes "combinable Δ A"
      and "unambiguous Δ A x"
    shows "combinable Δ (Exists x A)"
proof (rule combinableI)
  fix a b p q y σ s
  assume "a, s, Δ ⊨ Exists x A ∧ b, s, Δ ⊨ Exists x A ∧ Some y = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
  then have "a ## b"
    by (metis logic.compatible_multiples logic_axioms option.discI pre_logic.compatible_def)
  moreover obtain v1 v2 where "a, s(x := v1), Δ ⊨ A" "b, s(x := v2), Δ ⊨ A"
    using ‹a, s, Δ ⊨ Exists x A ∧ b, s, Δ ⊨ Exists x A ∧ Some y = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one› by auto
  ultimately have "v1 = v2"
    using assms(2) unambiguous_def by force
  then show "y, s, Δ ⊨ Exists x A"
    by (metis (mono_tags, opaque_lifting) ‹a, s(x := v1), Δ ⊨ A› ‹a, s, Δ ⊨ Exists x A ∧ b, s, Δ ⊨ Exists x A ∧ Some y = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one› ‹b, s(x := v2), Δ ⊨ A› assms(1) combinable_instantiate_one logic.sat.simps(8) logic_axioms)
qed

lemma combinable_pure:
  assumes "pure A"
  shows "combinable Δ A"
  using assms combinableI_old pure_def by blast


lemma combinable_imp:
  assumes "pure A"
      and "combinable Δ B"
  shows "combinable Δ (Imp A B)"
proof (rule combinableI)
  fix a b p q x σ s
  assume "a, s, Δ ⊨ Imp A B ∧ b, s, Δ ⊨ Imp A B ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
  then show "x, s, Δ ⊨ Imp A B"
    using assms(1) assms(2) combinable_instantiate_one pure_def sat.simps(5)
    by metis
qed


lemma combinable_wildcard:
  assumes "combinable Δ A"
  shows "combinable Δ (Wildcard A)"
proof (rule combinableI)
  fix a b p q x σ s
  assume asm: "a, s, Δ ⊨ Wildcard A ∧ b, s, Δ ⊨ Wildcard A ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
  then obtain a' b' pa pb where "a', s, Δ ⊨ A" "b', s, Δ ⊨ A" "a = pa ⊙ a'" "b = pb ⊙ b'" by auto
  then have "Some x = (smult p pa) ⊙ a' ⊕ (smult q pb) ⊙ b'"
    by (simp add: asm double_mult)
  then have "x, s, Δ ⊨ Mult (sadd (smult p pa) (smult q pb)) A"
    using ‹a', s, Δ ⊨ A› ‹b', s, Δ ⊨ A› assms combinable_instantiate by blast
  then show "x, s, Δ ⊨ Wildcard A"
    by fastforce
qed


end


end