Theory Conditionals

subsection ‹Decomposing Conditionals›

theory Conditionals
imports
  Complex_Main
  "../Case_Labeling"
  "HOL-Eisbach.Eisbach"
begin

context begin
  interpretation Labeling_Syntax .

  lemma DC_conj:
    assumes "C⟨inp,ct,outp': a⟩" "C⟨outp',ct,outp: b⟩"
    shows "C⟨inp,ct,outp: a ∧ b⟩"
    using assms unfolding LABEL_simps by auto

  lemma DC_if:
    fixes ct defines "ct' ≡ λpos name. (name, pos,[]) # ct"
    assumes "H⟨ct' inp ''then'': a⟩ ⟹ C⟨Suc inp,ct' inp ''then'', outp': b⟩"
    assumes "H⟨ct' outp' ''else'': ¬a⟩ ⟹ C⟨Suc outp',ct' outp' ''else'', outp: c⟩"
    shows "C⟨inp,ct,outp: if a then b else c⟩"
    using assms(2-) unfolding LABEL_simps by auto

  lemma DC_final:
    assumes "V⟨(''g'',inp,[]), ct: a⟩"
    shows "C⟨inp,ct,Suc inp: a⟩"
    using assms unfolding LABEL_simps by auto

end

method vcg_dc = (intro DC_conj DC_if; rule DC_final)

lemma
  assumes a: "a"
    and d: "b ⟹ c ⟹ d"
    and d': "b ⟹ c ⟹ d'"
    and e: "b ⟹ ¬c ⟹ e"
    and f: "¬b ⟹ f"
  shows "a ∧ (if b then (if c then d ∧ d' else e) else f)"
  apply (rule Initial_Label)
  apply vcg_dc
proof casify
  case g show ?case by (fact a)
next
  case "then" note b = ‹b›
  { case "then" note c = ‹c›
    { case g show ?case using b c by (fact d)
    next
      case ga show ?case using b c by (fact d')
    }
  next
    case else
    { case g show ?case using "then" else by (fact e) }
  }
next
  case "else"
  { case g show ?case using else by (fact f) }
qed



subsection ‹Protecting similar subgoals›

text ‹
  The proof below fails if the @{verbatim disambig_subgoals} option is omitted: all three
  subgoals have the same conclusion and can be discharged without using their assumptions.
  If the case @{verbatim g} is solved first, it discharges instead the subgoal @{prop "a ⟹ b"},
  making the case @{command then} fail afterwards.

  The @{verbatim disambig_subgoals} options prevents this by inserting vacuous assumptions.
›

lemma
  assumes b
  shows "(if a then b else b) ∧ b"
  apply (rule Initial_Label)
  apply vcg_dc
proof (casify (disambig_subgoals))
  case g show ?case by (fact ‹b›)
next
  case "then" case g show ?case by (fact ‹b›)
next
  case "else" case g show ?case by (fact ‹b›)
qed



subsection ‹Unnamed Cases›

lemma
  assumes "a ⟹ b" "¬a ⟹ c" "d"
  shows "(if a then b else c) ∧ d"
  apply (rule Initial_Label)
  apply vcg_dc
  apply (simp_all only: LABEL_simps)[2]
proof (casify (disambig_subgoals))
  case unnamed from ‹a› show ?case by fact
next
  case unnameda from ‹¬a› show ?case by fact
next
  case g show ?case by fact
qed

end