Theory Distributivity

section ‹Distributivity and Factorisability›

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

theory Distributivity
  imports UnboundedLogic
begin

context logic
begin

subsection DotPos

lemma DotPos:
  "A, Δ ⊢ B ⟷ (Mult π A, Δ ⊢ Mult π B)" (is "?A ⟷ ?B")
proof
  show "?A ⟹ ?B"
    by (metis (no_types, lifting) entails_def sat.simps(1))
  show "?B ⟹ ?A"
    using can_divide entails_def sat.simps(1)
    by metis
qed

text ‹Only one direction holds with a wildcard›

lemma WildPos:
  "A, Δ ⊢ B ⟹ (Wildcard A, Δ ⊢ Wildcard B)"
  by (metis (no_types, lifting) entails_def sat.simps(12))

subsection DotDot

lemma dot_mult1:
  "Mult p (Mult q A), Δ ⊢ Mult (smult p q) A"
proof (rule entailsI)
  fix σ s
  assume "σ, s, Δ ⊨ Mult p (Mult q A)"
  then show "σ, s, Δ ⊨ Mult (smult p q) A"
    using double_mult by auto
qed

lemma dot_mult2:
  "Mult (smult p q) A, Δ ⊢ Mult p (Mult q A)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult (smult p q) A"
  then obtain a where "a, s, Δ ⊨ A" "σ = (smult p q) ⊙ a"
    by auto
  then have "q ⊙ a, s, Δ ⊨ Mult q A" by auto
  then show "σ, s, Δ ⊨ Mult p (Mult q A)"  
    by (metis ‹σ = smult p q ⊙ a› double_mult sat.simps(1))
qed

lemma DotDot:
  "Mult p (Mult q A), Δ ≡ Mult (smult p q) A"
  by (simp add: dot_mult1 dot_mult2 equivalent_def)

lemma can_factorize:
  "∃r. q = smult r p"
  by (metis sinv_inverse smult_asso smult_comm sone_neutral)

lemma WildDot:
  "Wildcard (Mult p A), Δ ≡ Wildcard A"
proof (rule equivalentI)
  show "⋀σ s. σ, s, Δ ⊨ Wildcard (Mult p A) ⟹ σ, s, Δ ⊨ Wildcard A"
    using double_mult by fastforce
  fix σ s
  assume asm0: "σ, s, Δ ⊨ Wildcard A"
  then obtain q a where "σ = q ⊙ a" "a, s, Δ ⊨ A"
    using sat.simps(12) by blast
  then obtain r where "q = smult r p"
    using can_factorize by blast
  then have "σ = r ⊙ (p ⊙ a)"
    by (simp add: ‹σ = q ⊙ a› double_mult)
  then show "σ, s, Δ ⊨ Wildcard (Mult p A)"
    using ‹a, s, Δ ⊨ A› sat.simps(1) sat.simps(12) by blast
qed

lemma DotWild:
  "Mult p (Wildcard A), Δ ≡ Wildcard A"
proof (rule equivalentI)
  show "⋀σ s. σ, s, Δ ⊨ Mult p (Wildcard A) ⟹ σ, s, Δ ⊨ Wildcard A"
    using double_mult by fastforce
  fix σ s
  assume asm0: "σ, s, Δ ⊨ Wildcard A"
  then obtain q a where "σ = q ⊙ a" "a, s, Δ ⊨ A"
    by force
  then obtain r where "q = smult p r"
    using can_factorize smult_comm by presburger
  then have "σ = p ⊙ (r ⊙ a)"
    by (simp add: ‹σ = q ⊙ a› double_mult)
  then show "σ, s, Δ ⊨ Mult p (Wildcard A)"
    using ‹a, s, Δ ⊨ A› by auto
qed

lemma WildWild:
  "Wildcard (Wildcard A), Δ ≡ Wildcard A"
proof (rule equivalentI)
  show "⋀σ s. σ, s, Δ ⊨ Wildcard (Wildcard A) ⟹ σ, s, Δ ⊨ Wildcard A"
    using double_mult by fastforce
  show "⋀σ s. σ, s, Δ ⊨ Wildcard A ⟹ σ, s, Δ ⊨ Wildcard (Wildcard A)"
    by (metis one_neutral sat.simps(12))
qed




subsection DotStar

lemma dot_star1:
  "Mult p (Star A B), Δ ⊢ Star (Mult p A) (Mult p B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult p (Star A B)"
  then obtain a b x where "σ = p ⊙ x" "Some x = a ⊕ b" "a, s, Δ ⊨ A" "b, s, Δ ⊨ B"
    by auto
  then show "σ, s, Δ ⊨ Star (Mult p A) (Mult p B)"
    using plus_mult by auto
qed


lemma dot_star2:
  "Star (Mult p A) (Mult p B), Δ ⊢ Mult p (Star A B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Star (Mult p A) (Mult p B)"
  then obtain a b where "Some σ = (p ⊙ a) ⊕ (p ⊙ b)" "a, s, Δ ⊨ A" "b, s, Δ ⊨ B"
    by auto
  then obtain x where "Some x = a ⊕ b"
    by (metis plus_mult unique_inv)
  then have "σ = p ⊙ x"
    by (metis ‹Some σ = p ⊙ a ⊕ p ⊙ b› option.sel plus_mult)
  then show "σ, s, Δ ⊨ Mult p (Star A B)"
    using ‹Some x = a ⊕ b› ‹a, s, Δ ⊨ A› ‹b, s, Δ ⊨ B› by auto
qed

lemma DotStar:
  "Mult p (Star A B), Δ ≡ Star (Mult p A) (Mult p B)"
  by (simp add: dot_star1 dot_star2 equivalent_def)

lemma WildStar1:
  "Wildcard (Star A B), Δ ⊢ Star (Wildcard A) (Wildcard B)"
proof (rule entailsI)
  fix σ s assume asm0: "σ, s, Δ ⊨ Wildcard (Star A B)"
  then obtain p ab a b where "σ = p ⊙ ab" "Some ab = a ⊕ b" "a, s, Δ ⊨ A" "b, s, Δ ⊨ B"
    by auto
  then have "Some σ = (p ⊙ a) ⊕ (p ⊙ b)"
    using plus_mult by blast
  then show "σ, s, Δ ⊨ Star (Wildcard A) (Wildcard B)"
    using ‹a, s, Δ ⊨ A› ‹b, s, Δ ⊨ B› by auto
qed


subsection DotWand


lemma dot_wand1:
  "Mult p (Wand A B), Δ ⊢ Wand (Mult p A) (Mult p B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult p (Wand A B)"
  then obtain x where "σ = p ⊙ x" "x, s, Δ ⊨ Wand A B"
    by auto
  show "σ, s, Δ ⊨ Wand (Mult p A) (Mult p B)"
  proof (rule sat_wand)
    fix a σ'
    assume "a, s, Δ ⊨ Mult p A ∧ Some σ' = σ ⊕ a"
    then obtain aa where "aa, s, Δ ⊨ A" "a = p ⊙ aa"
      by auto
    then obtain b where "Some b = x ⊕ aa"
      by (metis ‹σ = p ⊙ x› ‹a, s, Δ ⊨ Mult p A ∧ Some σ' = σ ⊕ a› compatible_def compatible_iff option.exhaust_sel)
    then have "b, s, Δ ⊨ B"
      using ‹aa, s, Δ ⊨ A› ‹x, s, Δ ⊨ Wand A B› by auto
    then show "σ', s, Δ ⊨ Mult p B"
      by (metis ‹Some b = x ⊕ aa› ‹σ = p ⊙ x› ‹a = p ⊙ aa› ‹a, s, Δ ⊨ Mult p A ∧ Some σ' = σ ⊕ a› can_divide option.inject plus_mult sat_mult)
  qed
qed

lemma dot_wand2:
  "Wand (Mult p A) (Mult p B), Δ ⊢ Mult p (Wand A B)"
proof (rule entailsI)
  fix σ s Δ
  assume asm: "σ, s, Δ ⊨ Wand (Mult p A) (Mult p B)"
  show "σ, s, Δ ⊨ Mult p (Wand A B)"
  proof (rule sat_mult)
    fix a assume "σ = p ⊙ a"
    show "a, s, Δ ⊨ Wand A B"
    proof (rule sat_wand)
      fix aa σ'
      assume "aa, s, Δ ⊨ A ∧ Some σ' = a ⊕ aa"
      then have "p ⊙ aa, s, Δ ⊨ Mult p A" by auto
      then have "Some (p ⊙ σ') = σ ⊕ p ⊙ aa"
        by (simp add: ‹σ = p ⊙ a› ‹aa, s, Δ ⊨ A ∧ Some σ' = a ⊕ aa› plus_mult)
      then have "p ⊙ σ', s, Δ ⊨ Mult p B"
        using ‹p ⊙ aa, s, Δ ⊨ Mult p A› asm by force
      then show "σ', s, Δ ⊨ B"
        by (metis can_divide sat.simps(1))
    qed
  qed
qed

lemma DotWand:
  "Mult p (Wand A B), Δ ≡ Wand (Mult p A) (Mult p B)"
  by (simp add: dot_wand1 dot_wand2 equivalent_def)


(* Again: Need intuitionism
lemma WildWand:
  "Wildcard (Wand A B), Δ ⊢ Wand (Wildcard A) (Wildcard B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Wildcard (Wand A B)"
  then obtain x p where "σ = p ⊙ x" "x, s, Δ ⊨ Wand A B"
    by auto
  show "σ, s, Δ ⊨ Wand (Wildcard A) (Wildcard B)"
  proof (rule sat_wand)
    fix a σ'
    assume "a, s, Δ ⊨ Wildcard A ∧ Some σ' = σ ⊕ a"
    then obtain aa q where "aa, s, Δ ⊨ A" "a = q ⊙ aa"
      by auto
    then obtain b where "Some b = x ⊕ aa"
      by (metis ‹σ = p ⊙ x› ‹a, s, Δ ⊨ Wildcard A ∧ Some σ' = σ ⊕ a› compatible_def compatible_multiples not_None_eq)



    then have "b, s, Δ ⊨ B"
      using ‹aa, s, Δ ⊨ A› ‹x, s, Δ ⊨ Wand A B› by auto


    then show "σ', s, Δ ⊨ Wildcard B"
      
      by (metis ‹Some b = x ⊕ aa› ‹σ = p ⊙ x› ‹a = p ⊙ aa› ‹a, s, Δ ⊨ Mult p A ∧ Some σ' = σ ⊕ a› can_divide option.inject plus_mult sat_mult)
  qed
qed

*)



subsection DotOr

lemma dot_or1:
  "Mult p (Or A B), Δ ⊢ Or (Mult p A) (Mult p B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult p (Or A B)"
  then obtain x where "σ = p ⊙ x" "x, s, Δ ⊨ A ∨ x, s, Δ ⊨ B"
    by auto
  then show "σ, s, Δ ⊨ Or (Mult p A) (Mult p B)"
  proof (cases "x, s, Δ ⊨ A")
    case True
    then show ?thesis 
      using ‹σ = p ⊙ x› by auto
  next
    case False
    then show ?thesis
      using ‹σ = p ⊙ x› ‹x, s, Δ ⊨ A ∨ x, s, Δ ⊨ B› by auto
  qed
qed

lemma dot_or2:
  "Or (Mult p A) (Mult p B), Δ ⊢ Mult p (Or A B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Or (Mult p A) (Mult p B)"
  then show "σ, s, Δ ⊨ Mult p (Or A B)"
  proof (cases "σ, s, Δ ⊨ Mult p A")
    case True
    then show ?thesis by auto
  next
    case False
    then show ?thesis
      using ‹σ, s, Δ ⊨ Or (Mult p A) (Mult p B)› by auto
  qed
qed

lemma DotOr:
  "Mult p (Or A B), Δ ≡ Or (Mult p A) (Mult p B)"
  by (simp add: dot_or1 dot_or2 equivalent_def)

lemma WildOr:
  "Wildcard (Or A B), Δ ≡ Or (Wildcard A) (Wildcard B)"
proof (rule equivalentI)
  show "⋀σ s. σ, s, Δ ⊨ Wildcard (Or A B) ⟹ σ, s, Δ ⊨ Or (Wildcard A) (Wildcard B)"
    by auto
  show "⋀σ s. σ, s, Δ ⊨ Or (Wildcard A) (Wildcard B) ⟹ σ, s, Δ ⊨ Wildcard (Or A B)"
    by auto
qed


subsection DotAnd

lemma dot_and1:
  "Mult p (And A B), Δ ⊢ And (Mult p A) (Mult p B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult p (And A B)"
  then obtain x where "σ = p ⊙ x" "x, s, Δ ⊨ A" "x, s, Δ ⊨ B"
    by auto
  then show "σ, s, Δ ⊨ And (Mult p A) (Mult p B)"
    by auto
qed

lemma dot_and2:
  "And (Mult p A) (Mult p B), Δ ⊢ Mult p (And A B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ And (Mult p A) (Mult p B)"
  then show "σ, s, Δ ⊨ Mult p (And A B)"
    using logic.can_divide logic_axioms by fastforce
qed

lemma DotAnd:
  "And (Mult p A) (Mult p B), Δ ≡ Mult p (And A B)"
  by (simp add: dot_and1 dot_and2 equivalent_def)

lemma WildAnd:
  "Wildcard (And A B), Δ ⊢ And (Wildcard A) (Wildcard B)"
  using entails_def by fastforce



subsection DotImp


lemma dot_imp1:
  "Imp (Mult p A) (Mult p B), Δ ⊢ Mult p (Imp A B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Imp (Mult p A) (Mult p B)"
  then show "σ, s, Δ ⊨ Mult p (Imp A B)"
    using sat_mult by force
qed

lemma dot_imp2:
  "Mult p (Imp A B), Δ ⊢ Imp (Mult p A) (Mult p B)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult p (Imp A B)"
  then show "σ, s, Δ ⊨ Imp (Mult p A) (Mult p B)"
    using can_divide by auto
qed

lemma DotImp:
  "Mult p (Imp A B), Δ ≡ Imp (Mult p A) (Mult p B)"
  by (simp add: dot_imp1 dot_imp2 equivalent_def)

subsection DotPure


lemma pure_mult1:
  assumes "pure A"
  shows "Mult p A, Δ ⊢ A"
  using assms entails_def logic.pure_def logic_axioms by fastforce

lemma pure_mult2:
  assumes "pure A"
  shows "A, Δ ⊢ Mult p A"
    using assms entailsI pure_def sat_mult
    by metis

lemma DotPure: 
  assumes "pure A"
  shows "Mult p A, Δ ≡ A"
  by (simp add: assms equivalent_def pure_mult1 pure_mult2)

lemma WildPure: 
  assumes "pure A"
  shows "Wildcard A, Δ ≡ A"
proof (rule equivalentI)
  show "⋀σ s. σ, s, Δ ⊨ Wildcard A ⟹ σ, s, Δ ⊨ A"
    using assms pure_def sat.simps(12) by blast
  show "⋀σ s. σ, s, Δ ⊨ A ⟹ σ, s, Δ ⊨ Wildcard A"
    by (metis one_neutral sat.simps(12))
qed


subsection DotFull

lemma mult_one_same1:
  "Mult one A, Δ ⊢ A"
  by (simp add: entails_def one_neutral)


lemma mult_one_same2:
  "A, Δ ⊢ Mult one A"
  by (simp add: entailsI one_neutral)

lemma DotFull:
  "Mult one A, Δ ≡ A"
  using equivalent_def mult_one_same1 mult_one_same2 by blast




subsection DotExists


lemma dot_exists1:
  "Mult p (Exists x A), Δ ⊢ Exists x (Mult p A)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult p (Exists x A)"
  then show "σ, s, Δ ⊨ Exists x (Mult p A)"
    by auto
qed

lemma dot_exists2:
  "Exists x (Mult p A), Δ ⊢ Mult p (Exists x A)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Exists x (Mult p A)"
  then show "σ, s, Δ ⊨ Mult p (Exists x A)" by auto
qed

lemma DotExists:
  "Mult p (Exists x A), Δ ≡ Exists x (Mult p A)"
  by (simp add: dot_exists1 dot_exists2 equivalent_def)


lemma WildExists:
  "Wildcard (Exists x A), Δ ≡ Exists x (Wildcard A)"
proof (rule equivalentI)
  show "⋀σ s. σ, s, Δ ⊨ Wildcard (Exists x A) ⟹ σ, s, Δ ⊨ Exists x (Wildcard A)"
    by auto
  show "⋀σ s. σ, s, Δ ⊨ Exists x (Wildcard A) ⟹ σ, s, Δ ⊨ Wildcard (Exists x A)"
    by auto
qed

subsection DotForall

lemma dot_forall1:
  "Mult p (Forall x A), Δ ⊢ Forall x (Mult p A)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Mult p (Forall x A)"
  then show "σ, s, Δ ⊨ Forall x (Mult p A)"
    by auto
qed

lemma dot_forall2:
  "Forall x (Mult p A), Δ ⊢ Mult p (Forall x A)"
proof (rule entailsI)
  fix σ s Δ
  assume "σ, s, Δ ⊨ Forall x (Mult p A)"
  obtain a where "σ = p ⊙ a"
    using sat.simps(1) sat_mult by blast
  have "a, s, Δ ⊨ Forall x A"
  proof (rule sat_forall)
    fix v show "a, s(x := v), Δ ⊨ A"
      using ‹σ = p ⊙ a› ‹σ, s, Δ ⊨ Forall x (Mult p A)› can_divide by auto
  qed
  then show "σ, s, Δ ⊨ Mult p (Forall x A)"
    using ‹σ = p ⊙ a› by auto
qed

lemma DotForall:
  "Mult p (Forall x A), Δ ≡ Forall x (Mult p A)"
  by (simp add: dot_forall1 dot_forall2 equivalent_def)

lemma WildForall:
  "Wildcard (Forall x A), Δ ⊢ Forall x (Wildcard A)"
  by (metis (no_types, lifting) entailsI sat.simps(12) sat.simps(9))

subsection Split

lemma split:
  "Mult (sadd a b) A, Δ ⊢ Star (Mult a A) (Mult b A)"
proof (rule entailsI)
  fix σ s
  assume "σ, s, Δ ⊨ Mult (sadd a b) A"
  then show "σ, s, Δ ⊨ Star (Mult a A) (Mult b A)"
    using distrib_mult by fastforce
qed

end

end