Theory WandProperties

section ‹Properties of Magic Wands›

theory WandProperties
  imports Distributivity
begin

context logic
begin

lemma modus_ponens:
  "Star P (Wand P Q), Δ ⊢ Q"
proof (rule entailsI)
  fix σ s
  assume "σ, s, Δ ⊨ Star P (Wand P Q)"
  show "σ, s, Δ ⊨ Q"
    using ‹σ, s, Δ ⊨ Star P (Wand P Q)› commutative by force
qed

lemma transitivity:
  "Star (Wand A B) (Wand B C), Δ ⊢ Wand A C"
proof (rule entailsI)
  fix σ s
  assume asm0: "σ, s, Δ ⊨ Star (Wand A B) (Wand B C)"
  then obtain ab bc where "Some σ = ab ⊕ bc" "ab, s, Δ ⊨ Wand A B" "bc, s, Δ ⊨ Wand B C"
    by auto
  show "σ, s, Δ ⊨ Wand A C"
  proof (rule sat_wand)
    fix a σ'
    assume asm1: "a, s, Δ ⊨ A ∧ Some σ' = σ ⊕ a"
    then obtain aab where "Some aab = ab ⊕ a"
      by (metis ‹Some σ = ab ⊕ bc› asso3 commutative compatible_def option.exhaust_sel)
    then have "Some σ' = aab ⊕ bc"
      by (metis ‹Some σ = ab ⊕ bc› asm1 asso1 commutative)
    moreover have "aab, s, Δ ⊨ B"
      using ‹Some aab = ab ⊕ a› ‹ab, s, Δ ⊨ Wand A B› asm1 by auto
    ultimately show "σ', s, Δ ⊨ C"
      using ‹bc, s, Δ ⊨ Wand B C› commutative by auto
  qed
qed

lemma currying1:
  "Wand (Star A B) C, Δ ⊢ Wand A (Wand B C)"
proof (rule entailsI)
  fix σ s
  assume asm0: "σ, s, Δ ⊨ Wand (Star A B) C"
  show "σ, s, Δ ⊨ Wand A (Wand B C)"
  proof (rule sat_wand)
    fix a σ'
    assume asm1: "a, s, Δ ⊨ A ∧ Some σ' = σ ⊕ a"
    show "σ', s, Δ ⊨ Wand B C"
    proof (rule sat_wand)
      fix b σ''
      assume asm2: "b, s, Δ ⊨ B ∧ Some σ'' = σ' ⊕ b"
      then obtain ab where "Some ab = a ⊕ b"
        by (metis asm1 asso2 compatible_def option.collapse)
      then have "ab, s, Δ ⊨ Star A B"
        using asm1 asm2 by auto
      moreover have "Some σ'' = σ ⊕ ab"
        by (metis ‹Some ab = a ⊕ b› asm1 asm2 asso1)
      ultimately show "σ'', s, Δ ⊨ C"
        using asm0 sat.simps(3) by blast
    qed
  qed
qed

lemma currying2:
  "Wand A (Wand B C), Δ ⊢ Wand (Star A B) C"
proof (rule entailsI)
  fix σ s
  assume asm0: "σ, s, Δ ⊨ Wand A (Wand B C)"
  show "σ, s, Δ ⊨ Wand (Star A B) C"
  proof (rule sat_wand)
    fix ab σ'
    assume asm1: "ab, s, Δ ⊨ Star A B ∧ Some σ' = σ ⊕ ab"
    then obtain a b where "Some ab = a ⊕ b" "a, s, Δ ⊨ A" "b, s, Δ ⊨ B"
      by auto
    then obtain bc where "Some bc = σ ⊕ a"
      by (metis asm1 asso3 compatible_def option.exhaust_sel)
    then have "bc, s, Δ ⊨ Wand B C"
      using ‹a, s, Δ ⊨ A› asm0 by auto
    moreover have "Some σ' = bc ⊕ b"
      by (metis ‹Some ab = a ⊕ b› ‹Some bc = σ ⊕ a› asm1 asso1)
    ultimately show "σ', s, Δ ⊨ C"
      using ‹b, s, Δ ⊨ B› sat.simps(3) by blast
  qed
qed

lemma distribution:
  "Star (Wand A B) C, Δ ⊢ Wand A (Star B C)"
proof (rule entailsI)
  fix σ s
  assume asm0: "σ, s, Δ ⊨ Star (Wand A B) C"
  then obtain ab c where "Some σ = ab ⊕ c" "ab, s, Δ ⊨ Wand A B" "c, s, Δ ⊨ C"
    by auto
  show "σ, s, Δ ⊨ Wand A (Star B C)"
  proof (rule sat_wand)
    fix a σ'
    assume asm1: "a, s, Δ ⊨ A ∧ Some σ' = σ ⊕ a"
    then obtain b where "Some b = ab ⊕ a"
      by (metis ‹Some σ = ab ⊕ c› asso3 commutative compatible_def option.exhaust_sel)
    then have "b, s, Δ ⊨ B"
      using ‹ab, s, Δ ⊨ Wand A B› asm1 by force
    moreover have "Some σ' = b ⊕ c"
      by (metis ‹Some σ = ab ⊕ c› ‹Some b = ab ⊕ a› asm1 asso1 commutative)
    ultimately show "σ', s, Δ ⊨ Star B C"
      using ‹c, s, Δ ⊨ C› sat.simps(2) by blast
  qed
qed

lemma adjunct1:
  assumes "A, Δ ⊢ Wand B C"
  shows "Star A B, Δ ⊢ C"
proof (rule entailsI)
  fix σ s
  assume "σ, s, Δ ⊨ Star A B"
  then show "σ, s, Δ ⊨ C"
    using assms entails_def by force
qed

lemma adjunct2:
  assumes "Star A B, Δ ⊢ C"
  shows "A, Δ ⊢ Wand B C"
proof (rule entailsI)
  fix σ s
  assume "σ, s, Δ ⊨ A"
  then show "σ, s, Δ ⊨ Wand B C"
    by (meson assms entails_def sat.simps(2) sat_wand)
qed


end

end