Theory MiniSC

subsection‹SC and Implication-only formulas›
theory MiniSC
imports MiniFormulas SC
begin

abbreviation "is_mini_mset Γ ≡ ∀F ∈ set_mset Γ. is_mini_formula F"
lemma to_mini_mset_is: "is_mini_mset (image_mset to_mini_formula Γ)" by simp

lemma SC_full_to_mini:
  defines "tms ≡ image_mset to_mini_formula"
  assumes asm: "Γ ⇒ Δ"
  shows "tms Γ ⇒ tms Δ"
proof -
  have tmsi[simp]: "tms (F,S) = to_mini_formula F, tms S" for F S unfolding tms_def by simp
  from asm show ?thesis
  proof(induction Γ Δ rule: SCp.induct)
    case (BotL Γ)
    hence "⊥ ∈# tms Γ" unfolding tms_def by force
    thus ?case using SCp.BotL by blast
  next
    case (Ax k Γ Δ)
    hence "Atom k ∈# tms Γ" "Atom k ∈# tms Δ" unfolding tms_def using image_iff by fastforce+
    thus ?case using SCp.Ax[of k] by blast
  next
    case (NotR F Γ Δ) thus ?case 
      unfolding tmsi to_mini_formula.simps
      using weakenR SCp.ImpR by blast
  next
    case (NotL Γ F Δ) from this(2) show ?case
      by(auto intro!: SCp.ImpL)
  next
    case ImpR thus ?case using SCp.ImpR by simp
  next
    case ImpL thus ?case using SCp.ImpL by simp
  next
    case AndR from AndR(3,4) show ?case 
      using weakenR by(auto intro!: SCp.ImpR SCp.ImpL)
  next
    case AndL from AndL(2) show ?case 
      using weakenR[where 'a='a] by(fastforce intro!: SCp.ImpR SCp.ImpL)
  next
    case OrR from OrR(2) show ?case
      using weakenR by(fastforce intro!: SCp.ImpR SCp.ImpL)
  next
    case (OrL F Γ Δ G)
    note SCp.ImpL
    moreover {
      have "to_mini_formula F, tms Γ ⇒ tms Δ" using  OrL(3)[unfolded tmsi] .
      with weakenR have "to_mini_formula F, tms Γ ⇒ ⊥, tms Δ" by blast (* sooo close. *)
      with SCp.ImpR have "tms Γ ⇒ to_mini_formula F ❙→ ⊥, tms Δ" . }
    moreover have "to_mini_formula G, tms Γ ⇒ tms Δ" using ‹tms (G, Γ) ⇒ tms Δ› unfolding tmsi .
    ultimately have "(to_mini_formula F ❙→ ⊥) ❙→ to_mini_formula G, tms Γ ⇒ tms Δ" .
    thus ?case unfolding tmsi to_mini_formula.simps .
  qed
qed
  
lemma SC_mini_to_full:
  defines "tms ≡ image_mset to_mini_formula"
  assumes asm: "tms Γ ⇒ tms Δ"
  shows "Γ ⇒ Δ"
proof -
  have tmsi[simp]: "tms (F,S) = to_mini_formula F, tms S" for F S unfolding tms_def by simp
  note ImpL_inv ImpR_inv[dest]
  have no: "f ≠ (λF G. Not F)" "f ≠ Or" "f ≠ And" if "f F G, S' = tms S" for f F G S S'
    by (metis that is_mini_formula.simps(4-6) msed_map_invR tms_def to_mini_is_mini union_commute)+
  note dr = no(1)[where f="λF G. Not F", simplified, dest!]
            no(2)[where f=Or, simplified, dest!] 
            no(3)[where f=And, simplified, dest!]
  have whai(* we have an implication *): "
    (∃S2 H J. S = H ❙→ J, S2 ∧ F = to_mini_formula H ∧ G = to_mini_formula J) ∨
    (∃S2 H J. S = H ❙∨ J, S2 ∧ F = (to_mini_formula H ❙→ ⊥) ∧ G = to_mini_formula J) ∨
    (∃S2 H J. S = H ❙∧ J, S2 ∧ F =  to_mini_formula H ❙→ to_mini_formula J ❙→ ⊥ ∧ G = ⊥) ∨
    (∃S2 H. S = ❙¬ H, S2 ∧ F = to_mini_formula H ∧ G = ⊥)
  " if "F ❙→ G, S1 = tms S" for F G S1 S proof - (* ohno… *)
    note that[unfolded tms_def]
    then obtain S2 pim where S2: "S1 = image_mset to_mini_formula S2"
                        and   S: "S = pim, S2"
                        and pim: "F ❙→ G = to_mini_formula pim"
      by (metis msed_map_invR union_commute)
    show ?thesis using pim unfolding S by(cases pim; simp; blast)
  qed
  from asm show ?thesis
  proof(induction "tms Γ"  "tms Δ" arbitrary: Γ Δ rule: SCp.induct)
    have *: "to_mini_formula F = ⊥ ⟹ F = ⊥" for F by(cases F; simp)
    case BotL thus ?case unfolding tms_def using * SCp.BotL by (metis image_iff multiset.set_map)
  next
    have *: "Atom k = to_mini_formula F ⟹ F = Atom k" for F k by(cases F; simp)
    case (Ax _ k) thus ?case
      unfolding tms_def unfolding in_image_mset Set.image_iff
      apply(elim bexE)
      apply(drule *)+
      apply(intro SCp.Ax)
    by simp_all
  next
    case (ImpL Γ' F G)
    note whai[OF ImpL(5)]
    thus ?case proof(elim disjE exE conjE)
      fix S2 H J
      assume *: "Γ = H ❙→ J, S2" "F = to_mini_formula H" "G = to_mini_formula J"
      hence "Γ' = tms S2" "F, tms Δ = tms (H,Δ)" "G, Γ' = tms (J, S2)" "tms Δ = tms Δ" using ImpL.hyps(5) add_left_imp_eq by auto
      from ImpL(2)[OF this(1,2)] ImpL(4)[OF this(3-)]
      show ?thesis using SCp.ImpL by(simp add: *)
    next
      fix S2 H J
      assume *: "Γ = H ❙∨ J, S2" "F = to_mini_formula H ❙→ ⊥" "G = to_mini_formula J"
      hence "Γ' = tms S2" "F, tms Δ = tms (H ❙→ ⊥,Δ)" "G, Γ' = tms (J, S2)" "tms Δ = tms Δ" using ImpL.hyps(5) add_left_imp_eq by auto
      from ImpL(2)[OF this(1,2)] ImpL(4)[OF this(3-)]
      show ?thesis using Bot_delR by(force intro!: SCp.OrL dest!: ImpR_inv simp: *)
    next
      fix S2 H J
      assume *: "Γ = H ❙∧ J, S2" "F = to_mini_formula H ❙→ to_mini_formula J ❙→ ⊥" "G = ⊥"
      hence "Γ' = tms S2" "F, tms Δ = tms (H ❙→ J ❙→ ⊥,Δ)" "G, Γ' = tms (⊥, S2)" "tms Δ = tms Δ" using ImpL.hyps(5) add_left_imp_eq by auto
      from ImpL(2)[OF this(1,2)]
      show ?thesis using Bot_delR SCp.AndL ImpR_inv * by (metis add_mset_remove_trivial inL1)
    next
      fix S2 H
      assume *: "Γ = ❙¬ H, S2" "F = to_mini_formula H" "G = ⊥"
      hence "Γ' = tms S2" "F, tms Δ = tms (H,Δ)" "G, Γ' = tms (⊥, S2)" "tms Δ = tms Δ" using ImpL.hyps(5) add_left_imp_eq by auto
      from ImpL(2)[OF this(1,2)]
      show ?thesis by(force intro!: SCp.NotL dest!: ImpR_inv simp: *)
    qed
  next
    case (ImpR F G Δ')
    note whai[OF ImpR(3)]
    thus ?case proof(elim disjE  exE conjE)
      fix S2 H J
      assume "Δ = H ❙→ J, S2" "F = to_mini_formula H" "G = to_mini_formula J"
      thus ?thesis using ImpR.hyps(2,3) by (auto intro!: SCp.ImpR)
    next
      fix S2 H J
      assume *: "Δ = H ❙∨ J, S2" "F = to_mini_formula H ❙→ ⊥" "G = to_mini_formula J"
      hence "Δ' = tms S2" "F, tms Δ = tms (H ❙→ ⊥,Δ)" "G, Δ' = tms (J, S2)" "tms Δ = tms Δ" using ImpR.hyps(3) add_left_imp_eq by auto
      thus ?thesis using SCp.OrR[where 'a='a] * ImpR.hyps(2) by (simp add: NotL_inv)
    next
      have botoff: "Γ ⇒ H, ⊥, S2 ⟹ Γ ⇒ H, S2" for Γ H S2 using Bot_delR by fastforce
      fix S2 H J
      assume *: "Δ = H ❙∧ J, S2" "F = to_mini_formula H ❙→ to_mini_formula J ❙→ ⊥" "G = ⊥"
      hence "F, tms Γ = tms (H ❙→ J ❙→ ⊥, Γ)" " G, Δ' = tms (⊥, S2)"
        using ImpR.hyps(3) by(auto) (* hm, not optimal that we need mini_mini… *)
      from ImpR(2)[OF this] show ?thesis by(auto simp add: * intro!: SCp.intros(3-) dest!: ImpL_inv botoff)
    next  
      (* verbose version *)
      fix S2 H
      assume "Δ = ❙¬ H, S2" "F = to_mini_formula H" "G = ⊥"
      then obtain S2 H where *: "Δ = ❙¬ H, S2" "F = to_mini_formula H ∧ G = ⊥" by blast
      hence "F, tms Γ = tms (H, Γ)" "G, Δ' = tms (⊥, S2)" using ImpR(3) by simp_all
      with ImpR(2) have "H, Γ ⇒ ⊥, S2" .
      hence "Γ ⇒ ❙¬ H, S2" using SCp.NotR Bot_delR by fastforce
      thus "Γ ⇒ Δ" by(simp add: *)
    qed
  qed auto
qed

theorem MiniSC_eq: "image_mset to_mini_formula Γ ⇒ image_mset to_mini_formula Δ ⟷ Γ ⇒ Δ"
  using SC_mini_to_full SC_full_to_mini by blast

end