Theory Proof

theory Proof
  imports ILL
begin

subsection‹Deep Embedding of Deductions›

text‹
  To directly manipulate ILL deductions themselves we deeply embed them as a datatype.
  This datatype has a constructor to represent each introduction rule of @{const sequent}, with the
  ILL propositions and further deductions those rules use as arguments.
  Additionally, it has a constructor to represent premises (sequents assumed to be valid) which
  allow us to represent contingent deductions.

  The datatype is parameterised by two type variables:
  ▪ @{typ 'a} represents the propositional variables for the contained ILL propositions, and
  ▪ @{typ 'l} represents labels we associate with premises.
›
datatype ('a, 'l) ill_deduct =
    Premise "'a ill_prop list" "'a ill_prop" 'l
  | Identity "'a ill_prop"
  | Exchange "'a ill_prop list" "'a ill_prop" "'a ill_prop" "'a ill_prop list" "'a ill_prop"
      "('a, 'l) ill_deduct"
  | Cut "'a ill_prop list" "'a ill_prop" "'a ill_prop list" "'a ill_prop list" "'a ill_prop"
      "('a, 'l) ill_deduct" "('a, 'l) ill_deduct"
  | TimesL "'a ill_prop list" "'a ill_prop" "'a ill_prop" "'a ill_prop list" "'a ill_prop"
      "('a, 'l) ill_deduct"
  | TimesR "'a ill_prop list" "'a ill_prop" "'a ill_prop list" "'a ill_prop" "('a, 'l) ill_deduct"
      "('a, 'l) ill_deduct"
  | OneL "'a ill_prop list" "'a ill_prop list" "'a ill_prop" "('a, 'l) ill_deduct"
  | OneR
  | LimpL "'a ill_prop list" "'a ill_prop" "'a ill_prop list" "'a ill_prop" "'a ill_prop list"
      "'a ill_prop" "('a, 'l) ill_deduct" "('a, 'l) ill_deduct"
  | LimpR "'a ill_prop list" "'a ill_prop" "'a ill_prop list" "'a ill_prop" "('a, 'l) ill_deduct"
  | WithL1 "'a ill_prop list" "'a ill_prop" "'a ill_prop" "'a ill_prop list" "'a ill_prop"
      "('a, 'l) ill_deduct"
  | WithL2 "'a ill_prop list" "'a ill_prop" "'a ill_prop" "'a ill_prop list" "'a ill_prop"
      "('a, 'l) ill_deduct"
  | WithR "'a ill_prop list" "'a ill_prop" "'a ill_prop" "('a, 'l) ill_deduct" "('a, 'l) ill_deduct"
  | TopR "'a ill_prop list"
  | PlusL "'a ill_prop list" "'a ill_prop" "'a ill_prop" "'a ill_prop list" "'a ill_prop"
      "('a, 'l) ill_deduct" "('a, 'l) ill_deduct"
  | PlusR1 "'a ill_prop list" "'a ill_prop" "'a ill_prop" "('a, 'l) ill_deduct"
  | PlusR2 "'a ill_prop list" "'a ill_prop" "'a ill_prop" "('a, 'l) ill_deduct"
  | ZeroL "'a ill_prop list" "'a ill_prop list" "'a ill_prop"
  | Weaken "'a ill_prop list" "'a ill_prop list" "'a ill_prop" "'a ill_prop" "('a, 'l) ill_deduct"
  | Contract "'a ill_prop list" "'a ill_prop" "'a ill_prop list" "'a ill_prop" "('a, 'l) ill_deduct"
  | Derelict "'a ill_prop list" "'a ill_prop" "'a ill_prop list" "'a ill_prop" "('a, 'l) ill_deduct"
  | Promote "'a ill_prop list" "'a ill_prop" "('a, 'l) ill_deduct"
(* Above definition takes long and jEdit is slowed down as long as it is shown *)

subsubsection‹Semantics›

text‹
  With every deduction we associate the antecedents and consequent of its conclusion sequent
›
primrec antecedents :: "('a, 'l) ill_deduct ⇒ 'a ill_prop list"
  where
    "antecedents (Premise G c l) = G"
  | "antecedents (Identity a) = [a]"
  | "antecedents (Exchange G a b D c P) = G @ [b] @ [a] @ D"
  | "antecedents (Cut G b D E c P Q) = D @ G @ E"
  | "antecedents (TimesL G a b D c P) = G @ [a ⊗ b] @ D"
  | "antecedents (TimesR G a D b P Q) = G @ D"
  | "antecedents (OneL G D c P) = G @ [𝟭] @ D"
  | "antecedents (OneR) = []"
  | "antecedents (LimpL G a D b E c P Q) = G @ D @ [a ⊳ b] @ E"
  | "antecedents (LimpR G a D b P) = G @ D"
  | "antecedents (WithL1 G a b D c P) = G @ [a & b] @ D"
  | "antecedents (WithL2 G a b D c P) = G @ [a & b] @ D"
  | "antecedents (WithR G a b P Q) = G"
  | "antecedents (TopR G) = G"
  | "antecedents (PlusL G a b D c P Q) = G @ [a ⊕ b] @ D"
  | "antecedents (PlusR1 G a b P) = G"
  | "antecedents (PlusR2 G a b P) = G"
  | "antecedents (ZeroL G D c) = G @ [𝟬] @ D"
  | "antecedents (Weaken G D b a P) = G @ [!a] @ D"
  | "antecedents (Contract G a D b P) = G @ [!a] @ D"
  | "antecedents (Derelict G a D b P) = G @ [!a] @ D"
  | "antecedents (Promote G a P) = map Exp G"

primrec consequent :: "('a, 'l) ill_deduct ⇒ 'a ill_prop"
  where
    "consequent (Premise G c l) = c"
  | "consequent (Identity a) = a"
  | "consequent (Exchange G a b D c P) = c"
  | "consequent (Cut G b D E c P Q) = c"
  | "consequent (TimesL G a b D c P) = c"
  | "consequent (TimesR G a D b P Q) = a ⊗ b"
  | "consequent (OneL G D c P) = c"
  | "consequent (OneR) = 𝟭"
  | "consequent (LimpL G a D b E c P Q) = c"
  | "consequent (LimpR G a D b P) = a ⊳ b"
  | "consequent (WithL1 G a b D c P) = c"
  | "consequent (WithL2 G a b D c P) = c"
  | "consequent (WithR G a b P Q) = a & b"
  | "consequent (TopR G) = ⊤"
  | "consequent (PlusL G a b D c P Q) = c"
  | "consequent (PlusR1 G a b P) = a ⊕ b"
  | "consequent (PlusR2 G a b P) = a ⊕ b"
  | "consequent (ZeroL G D c) = c"
  | "consequent (Weaken G D b a P) = b"
  | "consequent (Contract G a D b P) = b"
  | "consequent (Derelict G a D b P) = b"
  | "consequent (Promote G a P) = !a"

text‹
  We define a sequent datatype for presenting deduction tree conclusions, deeply embedding (possibly
  invalid) sequents themselves.

  Note: these are not used everywhere, separate antecedents and consequent tend to work better for
  proof automation.
  For instance, the full conclusion cannot be derived where only facts about antecedents are known.
›
datatype 'a ill_sequent = Sequent "'a ill_prop list" "'a ill_prop"

text‹Validity of deeply embedded sequents is defined by the shallow @{const sequent} relation›
primrec ill_sequent_valid :: "'a ill_sequent ⇒ bool"
  where "ill_sequent_valid (Sequent a c) = a ⊢ c"

text‹
  We set up a notation bundle to have infix @{text ⊢} for stand for the sequent datatype and not
  the relation
›
bundle deep_sequent
begin
no_notation sequent (infix "⊢" 60)
notation Sequent (infix "⊢" 60)
end

context
  includes deep_sequent
begin

text‹With deeply embedded sequents we can define the conclusion of every deduction›
primrec ill_conclusion :: "('a, 'l) ill_deduct ⇒ 'a ill_sequent"
  where
    "ill_conclusion (Premise G c l) = G ⊢ c"
  | "ill_conclusion (Identity a) = [a] ⊢ a"
  | "ill_conclusion (Exchange G a b D c P) = G @ [b] @ [a] @ D ⊢ c"
  | "ill_conclusion (Cut G b D E c P Q) = D @ G @ E ⊢ c"
  | "ill_conclusion (TimesL G a b D c P) = G @ [a ⊗ b] @ D ⊢ c"
  | "ill_conclusion (TimesR G a D b P Q) = G @ D ⊢ a ⊗ b"
  | "ill_conclusion (OneL G D c P) = G @ [𝟭] @ D ⊢ c"
  | "ill_conclusion (OneR) = [] ⊢ 𝟭"
  | "ill_conclusion (LimpL G a D b E c P Q) = G @ D @ [a ⊳ b] @ E ⊢ c"
  | "ill_conclusion (LimpR G a D b P) = G @ D ⊢ a ⊳ b"
  | "ill_conclusion (WithL1 G a b D c P) = G @ [a & b] @ D ⊢ c"
  | "ill_conclusion (WithL2 G a b D c P) = G @ [a & b] @ D ⊢ c"
  | "ill_conclusion (WithR G a b P Q) = G ⊢ a & b"
  | "ill_conclusion (TopR G) = G ⊢ ⊤"
  | "ill_conclusion (PlusL G a b D c P Q) = G @ [a ⊕ b] @ D ⊢ c"
  | "ill_conclusion (PlusR1 G a b P) = G ⊢ a ⊕ b"
  | "ill_conclusion (PlusR2 G a b P) = G ⊢ a ⊕ b"
  | "ill_conclusion (ZeroL G D c) = G @ [𝟬] @ D ⊢ c"
  | "ill_conclusion (Weaken G D b a P) = G @ [!a] @ D ⊢ b"
  | "ill_conclusion (Contract G a D b P) = G @ [!a] @ D ⊢ b"
  | "ill_conclusion (Derelict G a D b P) = G @ [!a] @ D ⊢ b"
  | "ill_conclusion (Promote G a P) = map Exp G ⊢ !a"

text‹This conclusion is the same as what @{const antecedents} and @{const consequent} express› 
lemma ill_conclusionI [intro!]:
  assumes "antecedents P = G"
      and "consequent P = c"
    shows "ill_conclusion P = G ⊢ c"
  using assms by (induction P) simp_all

lemma ill_conclusionE [elim!]:
  assumes "ill_conclusion P = G ⊢ c"
  obtains "antecedents P = G"
      and "consequent P = c"
  using assms by (induction P) simp_all

lemma ill_conclusion_alt:
  "(ill_conclusion P = G ⊢ c) = (antecedents P = G ∧ consequent P = c)"
  by blast

lemma ill_conclusion_antecedents: "ill_conclusion P = G ⊢ c ⟹ antecedents P = G"
  and ill_conclusion_consequent: "ill_conclusion P = G ⊢ c ⟹ consequent P = c"
  by blast+

text‹
  Every deduction is well-formed if all deductions it relies on are well-formed and have the form
  required by the corresponding @{const sequent} rule.
›
primrec ill_deduct_wf :: "('a, 'l) ill_deduct ⇒ bool"
  where
    "ill_deduct_wf (Premise G c l) = True"
  | "ill_deduct_wf (Identity a) = True"
  | "ill_deduct_wf (Exchange G a b D c P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ [a] @ [b] @ D ⊢ c)"
  | "ill_deduct_wf (Cut G b D E c P Q) =
      ( ill_deduct_wf P ∧ ill_conclusion P = G ⊢ b ∧
        ill_deduct_wf Q ∧ ill_conclusion Q = D @ [b] @ E ⊢ c)"
  | "ill_deduct_wf (TimesL G a b D c P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ [a] @ [b] @ D ⊢ c)"
  | "ill_deduct_wf (TimesR G a D b P Q) =
      ( ill_deduct_wf P ∧ ill_conclusion P = G ⊢ a ∧
        ill_deduct_wf Q ∧ ill_conclusion Q = D ⊢ b)"
  | "ill_deduct_wf (OneL G D c P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ D ⊢ c)"
  | "ill_deduct_wf (OneR) = True"
  | "ill_deduct_wf (LimpL G a D b E c P Q) =
      ( ill_deduct_wf P ∧ ill_conclusion P = G ⊢ a ∧
        ill_deduct_wf Q ∧ ill_conclusion Q = D @ [b] @ E ⊢ c)"
  | "ill_deduct_wf (LimpR G a D b P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ [a] @ D ⊢ b)"
  | "ill_deduct_wf (WithL1 G a b D c P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ [a] @ D ⊢ c)"
  | "ill_deduct_wf (WithL2 G a b D c P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ [b] @ D ⊢ c)"
  | "ill_deduct_wf (WithR G a b P Q) =
      ( ill_deduct_wf P ∧ ill_conclusion P = G ⊢ a ∧
        ill_deduct_wf Q ∧ ill_conclusion Q = G ⊢ b)"
  | "ill_deduct_wf (TopR G) = True"
  | "ill_deduct_wf (PlusL G a b D c P Q) =
      ( ill_deduct_wf P ∧ ill_conclusion P = G @ [a] @ D ⊢ c ∧
        ill_deduct_wf Q ∧ ill_conclusion Q = G @ [b] @ D ⊢ c)"
  | "ill_deduct_wf (PlusR1 G a b P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G ⊢ a)"
  | "ill_deduct_wf (PlusR2 G a b P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G ⊢ b)"
  | "ill_deduct_wf (ZeroL G D c) = True"
  | "ill_deduct_wf (Weaken G D b a P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ D ⊢ b)"
  | "ill_deduct_wf (Contract G a D b P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ [!a] @ [!a] @ D ⊢ b)"
  | "ill_deduct_wf (Derelict G a D b P) =
      (ill_deduct_wf P ∧ ill_conclusion P = G @ [a] @ D ⊢ b)"
  | "ill_deduct_wf (Promote G a P) =
      (ill_deduct_wf P ∧ ill_conclusion P = map Exp G ⊢ a)"

text‹
  In some proofs phasing well-formedness in terms of @{const antecedents} and @{const consequent} is
  more useful.
›
lemmas ill_deduct_wf_alt = ill_deduct_wf.simps[unfolded ill_conclusion_alt]

end

text‹
  Premises of a deduction can be gathered recursively.
  Because every element of the result is an instance of @{const Premise}, we represent them with the
  relevant three parameters (antecedents, consequent, label).
›
primrec ill_deduct_premises
    :: "('a, 'l) ill_deduct ⇒ ('a ill_prop list × 'a ill_prop × 'l) list"
  where
    "ill_deduct_premises (Premise G c l) = [(G, c, l)]"
  | "ill_deduct_premises (Identity a) = []"
  | "ill_deduct_premises (Exchange G a b D c P) = ill_deduct_premises P"
  | "ill_deduct_premises (Cut G b D E c P Q) =
      (ill_deduct_premises P @ ill_deduct_premises Q)"
  | "ill_deduct_premises (TimesL G a b D c P) = ill_deduct_premises P"
  | "ill_deduct_premises (TimesR G a D b P Q) =
      (ill_deduct_premises P @ ill_deduct_premises Q)"
  | "ill_deduct_premises (OneL G D c P) = ill_deduct_premises P"
  | "ill_deduct_premises (OneR) = []"
  | "ill_deduct_premises (LimpL G a D b E c P Q) =
      (ill_deduct_premises P @ ill_deduct_premises Q)"
  | "ill_deduct_premises (LimpR G a D b P) = ill_deduct_premises P"
  | "ill_deduct_premises (WithL1 G a b D c P) = ill_deduct_premises P"
  | "ill_deduct_premises (WithL2 G a b D c P) = ill_deduct_premises P"
  | "ill_deduct_premises (WithR G a b P Q) =
      (ill_deduct_premises P @ ill_deduct_premises Q)"
  | "ill_deduct_premises (TopR G) = []"
  | "ill_deduct_premises (PlusL G a b D c P Q) =
      (ill_deduct_premises P @ ill_deduct_premises Q)"
  | "ill_deduct_premises (PlusR1 G a b P) = ill_deduct_premises P"
  | "ill_deduct_premises (PlusR2 G a b P) = ill_deduct_premises P"
  | "ill_deduct_premises (ZeroL G D c) = []"
  | "ill_deduct_premises (Weaken G D b a P) = ill_deduct_premises P"
  | "ill_deduct_premises (Contract G a D b P) = ill_deduct_premises P"
  | "ill_deduct_premises (Derelict G a D b P) = ill_deduct_premises P"
  | "ill_deduct_premises (Promote G a P) = ill_deduct_premises P"

subsubsection‹Soundness›

text‹
  Deeply embedded deductions are sound with respect to @{const sequent} in the sense that the
  conclusion of any well-formed deduction is a valid sequent if all of its premises are assumed to
  be valid sequents.
  This is proven easily, because our definitions stem from the @{const sequent} relation.
›
lemma ill_deduct_sound:
  assumes "ill_deduct_wf P"
      and "⋀a c l. (a, c, l) ∈ set (ill_deduct_premises P) ⟹ ill_sequent_valid (Sequent a c)"
    shows "ill_sequent_valid (ill_conclusion P)"
  using assms
proof (induct P)
  case (Premise G c l) then show ?case by simp next
  case (Identity x) then show ?case by simp next
  case (Exchange x1a x2 x3 x4 x5 x6) then show ?case using exchange by simp blast next
  case (Cut x1a x2 x3 x4 x5 x6 x7) then show ?case using cut by simp blast next
  case (TimesL x1a x2 x3 x4 x5 x6) then show ?case using timesL by simp blast next
  case (TimesR x1a x2 x3 x4 x5 x6) then show ?case using timesR by simp blast next
  case (OneL x1a x1b x2 x3) then show ?case using oneL by simp blast next
  case OneR then show ?case using oneR by simp next
  case (LimpL x1a x2 x3 x4 x5 x6 x7) then show ?case using limpL by simp blast next
  case (LimpR x1a x2 x3 x4 x5) then show ?case using limpR by simp blast next
  case (WithL1 x1a x2 x3 x4 x5 x6) then show ?case using withL1 by simp blast next
  case (WithL2 x1a x2 x3 x4 x5 x6) then show ?case using withL2 by simp blast next
  case (WithR x1a x2 x3 x4 x5) then show ?case using withR by simp blast next
  case (TopR x) then show ?case using topR by simp blast next
  case (PlusL x1a x2 x3 x4 x5 x6 x7) then show ?case using plusL by simp blast next
  case (PlusR1 x1a x2 x3 x4) then show ?case using plusR1 by simp blast next
  case (PlusR2 x1a x2 x3 x4) then show ?case using plusR2 by simp blast next
  case (ZeroL x1a x2 x3) then show ?case using zeroL by simp blast next
  case (Weaken x1a x2 x3 x4 x5) then show ?case using weaken by simp blast next
  case (Contract x1a x2 x3 x4 x5) then show ?case using contract by simp blast next
  case (Derelict x1a x2 x3 x4 x5) then show ?case using derelict by simp blast next
  case (Promote x1a x2 x3) then show ?case using promote by simp blast
qed

subsubsection‹Completeness›

text‹
  Deeply embedded deductions are complete with respect to @{const sequent} in the sense that for
  any valid sequent there exists a well-formed deduction with no premises that has it as its
  conclusion.
  This is proven easily, because the deduction nodes map directly onto the rules of the
  @{const sequent} relation.
›
lemma ill_deduct_complete:
  assumes "G ⊢ c"
    shows "∃P. ill_conclusion P = Sequent G c ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
  using assms
proof (induction rule: sequent.induct)
  case (identity a)
  then show ?case
    using ill_conclusion.simps(2) by fastforce
next
  case (exchange G a b D c)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [a] @ [b] @ D) c ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (Exchange G a b D c P)" and "ill_deduct_premises (Exchange G a b D c P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(3))
next
  case (cut G b D E c)
  then obtain P Q :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent G b ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
      and "ill_conclusion Q = Sequent (D @ [b] @ E) c ∧ ill_deduct_wf Q ∧ ill_deduct_premises Q = []"
    by blast
  then have "ill_deduct_wf (Cut G b D E c P Q)" and "ill_deduct_premises (Cut G b D E c P Q) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(4))
next
  case (timesL G a b D c)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [a] @ [b] @ D) c ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (TimesL G a b D c P)" and "ill_deduct_premises (TimesL G a b D c P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(5))
next
  case (timesR G a D b)
  then obtain P Q :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent G a ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
      and "ill_conclusion Q = Sequent D b ∧ ill_deduct_wf Q ∧ ill_deduct_premises Q = []"
    by blast
  then have "ill_deduct_wf (TimesR G a D b P Q)" and "ill_deduct_premises (TimesR G a D b P Q) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(6))
next
  case (oneL G D c)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ D) c ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (OneL G D c P)" and "ill_deduct_premises (OneL G D c P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(7))
next
  case oneR
  then show ?case
    using ill_conclusion.simps(8) by fastforce
next
  case (limpL G a D b E c)
  then obtain P Q :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent G a ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
      and "ill_conclusion Q = Sequent (D @ [b] @ E) c ∧ ill_deduct_wf Q ∧ ill_deduct_premises Q = []"
    by blast
  then have "ill_deduct_wf (LimpL G a D b E c P Q)" and "ill_deduct_premises (LimpL G a D b E c P Q) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(9))
next
  case (limpR G a D b)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [a] @ D) b ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (LimpR G a D b P)" and "ill_deduct_premises (LimpR G a D b P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(10))
next
  case (withL1 G a D c b)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [a] @ D) c ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (WithL1 G a b D c P)" and "ill_deduct_premises (WithL1 G a b D c P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(11))
next
  case (withL2 G b D c a)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [b] @ D) c ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (WithL2 G a b D c P)" and "ill_deduct_premises (WithL2 G a b D c P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(12))
next
  case (withR G a b)
  then obtain P Q :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent G a ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
      and "ill_conclusion Q = Sequent G b ∧ ill_deduct_wf Q ∧ ill_deduct_premises Q = []"
    by blast
  then have "ill_deduct_wf (WithR G a b P Q)" and "ill_deduct_premises (WithR G a b P Q) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(13))
next
  case (topR G)
  then show ?case
    using ill_conclusion.simps(14) by fastforce
next
  case (plusL G a D c b)
  then obtain P Q :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [a] @ D) c ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
      and "ill_conclusion Q = Sequent (G @ [b] @ D) c ∧ ill_deduct_wf Q ∧ ill_deduct_premises Q = []"
    by blast
  then have "ill_deduct_wf (PlusL G a b D c P Q)" and "ill_deduct_premises (PlusL G a b D c P Q) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(15))
next
  case (plusR1 G a b)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent G a ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (PlusR1 G a b P)" and "ill_deduct_premises (PlusR1 G a b P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(16))
next
  case (plusR2 G b a)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent G b ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (PlusR2 G a b P)" and "ill_deduct_premises (PlusR2 G a b P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(17))
next
  case (zeroL G D c)
  then show ?case
    using ill_conclusion.simps(18) by fastforce
next
  case (weaken G D b a)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ D) b ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (Weaken G D b a P)" and "ill_deduct_premises (Weaken G D b a P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(19))
next
  case (contract G a D b)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [! a] @ [! a] @ D) b ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (Contract G a D b P)" and "ill_deduct_premises (Contract G a D b P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(20))
next
  case (derelict G a D b)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (G @ [a] @ D) b ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (Derelict G a D b P)" and "ill_deduct_premises (Derelict G a D b P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(21))
next
  case (promote G a)
  then obtain P :: "('a, 'b) ill_deduct"
    where "ill_conclusion P = Sequent (map Exp G) a ∧ ill_deduct_wf P ∧ ill_deduct_premises P = []"
    by blast
  then have "ill_deduct_wf (Promote G a P)" and "ill_deduct_premises (Promote G a P) = []"
    by simp_all
  then show ?case
    by (meson ill_conclusion.simps(22))
qed

subsubsection‹Derived Deductions›

text‹
  We define a number of useful deduction patterns as (potentially recursive) functions.
  In each case we verify the well-formedness, conclusion and premises.
›

text‹Swap order in a times proposition: @{prop "[a ⊗ b] ⊢ b ⊗ a"}:›
fun ill_deduct_swap :: "'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_swap a b =
    TimesL [] a b [] (b ⊗ a)
    ( Exchange [] b a [] (b ⊗ a)
      ( TimesR [b] b [a] a (Identity b) (Identity a)))"

lemma ill_deduct_swap [simp]:
  "ill_deduct_wf (ill_deduct_swap a b)"
  "ill_conclusion (ill_deduct_swap a b) = Sequent [a ⊗ b] (b ⊗ a)"
  "ill_deduct_premises (ill_deduct_swap a b) = []"
  by simp_all

text‹Simplified cut rule: @{prop "⟦G ⊢ b; [b] ⊢ c⟧ ⟹ G ⊢ c"}:›
fun ill_deduct_simple_cut :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_simple_cut P Q = Cut (antecedents P) (consequent P) [] [] (consequent Q) P Q"

lemma ill_deduct_simple_cut [simp]:
  "⟦[consequent P] = antecedents Q; ill_deduct_wf P; ill_deduct_wf Q⟧ ⟹
    ill_deduct_wf (ill_deduct_simple_cut P Q)"
  "[consequent P] = antecedents Q ⟹
    ill_conclusion (ill_deduct_simple_cut P Q) = Sequent (antecedents P) (consequent Q)"
  "ill_deduct_premises (ill_deduct_simple_cut P Q) = ill_deduct_premises P @ ill_deduct_premises Q"
  by simp_all blast

text‹Combine two deductions with times: @{prop "⟦[a] ⊢ b; [c] ⊢ d⟧ ⟹ [a ⊗ c] ⊢ b ⊗ d"}:›
fun ill_deduct_tensor :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_tensor p q =
    TimesL [] (hd (antecedents p)) (hd (antecedents q)) [] (consequent p ⊗ consequent q)
      (TimesR (antecedents p) (consequent p) (antecedents q) (consequent q) p q)"

lemma ill_deduct_tensor [simp]:
  "⟦antecedents P = [a]; antecedents Q = [c]; ill_deduct_wf P; ill_deduct_wf Q⟧ ⟹
    ill_deduct_wf (ill_deduct_tensor P Q)"
  "⟦antecedents P = [a]; antecedents Q = [c]⟧ ⟹
    ill_conclusion (ill_deduct_tensor P Q) = Sequent [a ⊗ c] (consequent P ⊗ consequent Q)"
  "ill_deduct_premises (ill_deduct_tensor P Q) = ill_deduct_premises P @ ill_deduct_premises Q"
  by simp_all blast

text‹Associate times proposition to right: @{prop "[(a ⊗ b) ⊗ c] ⊢ a ⊗ (b ⊗ c)"}:›
fun ill_deduct_assoc :: "'a ill_prop ⇒ 'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_assoc a b c =
    TimesL [] (a ⊗ b) c [] (a ⊗ (b ⊗ c))
    ( Exchange [] c (a ⊗ b) [] (a ⊗ (b ⊗ c))
      ( TimesL [c] a b [] (a ⊗ (b ⊗ c))
        ( Exchange [] a c [b] (a ⊗ (b ⊗ c))
          ( TimesR [a] a [c, b] (b ⊗ c)
            ( Identity a)
            ( Exchange [] b c [] (b ⊗ c)
              ( TimesR [b] b [c] c
                ( Identity b)
                ( Identity c)))))))"

lemma ill_deduct_assoc [simp]:
  "ill_deduct_wf (ill_deduct_assoc a b c)"
  "ill_conclusion (ill_deduct_assoc a b c) = Sequent [(a ⊗ b) ⊗ c] (a ⊗ (b ⊗ c))"
  "ill_deduct_premises (ill_deduct_assoc a b c) = []"
  by simp_all

text‹Associate times proposition to left: @{prop "[a ⊗ (b ⊗ c)] ⊢ (a ⊗ b) ⊗ c"}:›
fun ill_deduct_assoc' :: "'a ill_prop ⇒ 'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_assoc' a b c =
    TimesL [] a (b ⊗ c) [] ((a ⊗ b) ⊗ c)
    ( TimesL [a] b c [] ((a ⊗ b) ⊗ c)
      ( TimesR [a, b] (a ⊗ b) [c] c
        ( TimesR [a] a [b] b
          ( Identity a)
          ( Identity b))
        ( Identity c)))"


lemma ill_deduct_assoc' [simp]:
  "ill_deduct_wf (ill_deduct_assoc' a b c)"
  "ill_conclusion (ill_deduct_assoc' a b c) = Sequent [a ⊗ (b ⊗ c)] ((a ⊗ b) ⊗ c)"
  "ill_deduct_premises (ill_deduct_assoc' a b c) = []"
  by simp_all

text‹Eliminate times unit a proposition: @{prop "[a ⊗ 𝟭] ⊢ a"}:›
fun ill_deduct_unit :: "'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_unit a = TimesL [] a (𝟭) [] a (OneL [a] [] a (Identity a))"

lemma ill_deduct_unit [simp]:
  "ill_deduct_wf (ill_deduct_unit a)"
  "ill_conclusion (ill_deduct_unit a) = Sequent [a ⊗ 𝟭] a"
  "ill_deduct_premises (ill_deduct_unit a) = []"
  by simp_all

text‹Introduce times unit into a proposition @{prop "[a] ⊢ a ⊗ 𝟭"}:›
fun ill_deduct_unit' :: "'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_unit' a = TimesR [a] a [] (𝟭) (Identity a) OneR"

lemma ill_deduct_unit' [simp]:
  "ill_deduct_wf (ill_deduct_unit' a)"
  "ill_conclusion (ill_deduct_unit' a) = Sequent [a] (a ⊗ 𝟭)"
  "ill_deduct_premises (ill_deduct_unit' a) = []"
  by simp_all

text‹Simplified weakening: @{prop "[!a] ⊢ 𝟭"}:›
fun ill_deduct_simple_weaken :: "'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_simple_weaken a = Weaken [] [] (𝟭) a OneR"

lemma ill_deduct_simple_weaken [simp]:
  "ill_deduct_wf (ill_deduct_simple_weaken a)"
  "ill_conclusion (ill_deduct_simple_weaken a) = Sequent [!a] 𝟭"
  "ill_deduct_premises (ill_deduct_simple_weaken a) = []"
  by simp_all

text‹Simplified dereliction: @{prop "[!a] ⊢ a"}:›
fun ill_deduct_dereliction :: "'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_dereliction a = Derelict [] a [] a (Identity a)"

lemma ill_deduct_dereliction [simp]:
  "ill_deduct_wf (ill_deduct_dereliction a)"
  "ill_conclusion (ill_deduct_dereliction a) = Sequent [!a] a"
  "ill_deduct_premises (ill_deduct_dereliction a) = []"
  by simp_all

text‹Duplicate exponentiated proposition: @{prop "[!a] ⊢ !a ⊗ !a"}:›
fun ill_deduct_duplicate :: "'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_duplicate a =
    Contract [] a [] (!a ⊗ !a) (TimesR [!a] (!a) [!a] (!a) (Identity (!a)) (Identity (!a)))"

lemma ill_deduct_duplicate [simp]:
  "ill_deduct_wf (ill_deduct_duplicate a)"
  "ill_conclusion (ill_deduct_duplicate a) = Sequent [!a] (!a ⊗ !a)"
  "ill_deduct_premises (ill_deduct_duplicate a) = []"
  by simp_all

text‹Simplified plus elimination: @{prop "⟦[a] ⊢ c; [b] ⊢ c⟧ ⟹ [a ⊕ b] ⊢ c"}:›
fun ill_deduct_simple_plusL :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_simple_plusL p q =
    PlusL [] (hd (antecedents p)) (hd (antecedents q)) [] (consequent p) p q"

lemma ill_deduct_simple_plusL [simp]:
  "⟦ antecedents P = [a]; antecedents Q = [b]; ill_deduct_wf P
   ; ill_deduct_wf Q; consequent P = consequent Q⟧ ⟹
    ill_deduct_wf (ill_deduct_simple_plusL P Q)"
  "⟦antecedents P = [a]; antecedents Q = [b]⟧ ⟹
    ill_conclusion (ill_deduct_simple_plusL P Q) = Sequent [a ⊕ b] (consequent P)"
  " ill_deduct_premises (ill_deduct_simple_plusL P Q)
  = ill_deduct_premises P @ ill_deduct_premises Q"
  by simp_all blast

text‹Simplified left plus introduction: @{prop "[a] ⊢ a ⊕ b"}:›
fun ill_deduct_plusR1 :: "'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_plusR1 a b = PlusR1 [a] a b (Identity a)"

lemma ill_deduct_plusR1 [simp]:
  "ill_deduct_wf (ill_deduct_plusR1 a b)"
  "ill_conclusion (ill_deduct_plusR1 a b) = Sequent [a] (a ⊕ b)"
  "ill_deduct_premises (ill_deduct_plusR1 a b) = []"
  by simp_all

text‹Simplified right plus introduction: @{prop "[b] ⊢ a ⊕ b"}:›
fun ill_deduct_plusR2 :: "'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_plusR2 a b = PlusR2 [b] a b (Identity b)"

lemma ill_deduct_plusR2 [simp]:
  "ill_deduct_wf (ill_deduct_plusR2 a b)"
  "ill_conclusion (ill_deduct_plusR2 a b) = Sequent [b] (a ⊕ b)"
  "ill_deduct_premises (ill_deduct_plusR2 a b) = []"
  by simp_all

text‹Simplified linear implication introduction: @{prop "[a] ⊢ b ⟹ [𝟭] ⊢ a ⊳ b"}:›
fun ill_deduct_simple_limpR :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_simple_limpR p =
    LimpR [] (hd (antecedents p)) [𝟭] (consequent p)
    ( OneL [hd (antecedents p)] [] (consequent p) p)"

lemma ill_deduct_simple_limpR [simp]:
  "⟦antecedents P = [a]; consequent P = b; ill_deduct_wf P⟧ ⟹
    ill_deduct_wf (ill_deduct_simple_limpR P)"
  "⟦antecedents P = [a]; consequent P = b⟧ ⟹
    ill_conclusion (ill_deduct_simple_limpR P) = Sequent [𝟭] (a ⊳ b)"
  " ill_deduct_premises (ill_deduct_simple_limpR P)
  = ill_deduct_premises P"
  by simp_all blast

text‹Simplified introduction of exponentiated impliciation: @{prop "[a] ⊢ b ⟹ [𝟭] ⊢ !(a ⊳ b)"}:›
fun ill_deduct_simple_limpR_exp :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_simple_limpR_exp p =
    OneL [] [] (!((hd (antecedents p)) ⊳ (consequent p)))
    ( Promote [] ((hd (antecedents p)) ⊳ (consequent p))
      ( ill_deduct_simple_cut
        OneR
        ( ill_deduct_simple_limpR p)))"

lemma ill_deduct_simple_limpR_exp [simp]:
  "⟦antecedents P = [a]; consequent P = b; ill_deduct_wf P⟧ ⟹
    ill_deduct_wf (ill_deduct_simple_limpR_exp P)"
  "⟦antecedents P = [a]; consequent P = b⟧ ⟹
    ill_conclusion (ill_deduct_simple_limpR_exp P) = Sequent [𝟭] (!(a ⊳ b))"
  "ill_deduct_premises (ill_deduct_simple_limpR_exp P) = ill_deduct_premises P"
  by simp_all blast

text‹Linear implication elimination with times: @{prop "[a ⊗ a ⊳ b] ⊢ b"}:›
fun ill_deduct_limp_eval :: "'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_limp_eval a b =
    TimesL [] a (a ⊳ b) [] b (LimpL [a] a [] b [] b (Identity a) (Identity b))"

lemma ill_deduct_limp_eval [simp]:
  "ill_deduct_wf (ill_deduct_limp_eval a b)"
  "ill_conclusion (ill_deduct_limp_eval a b) = Sequent [a ⊗ a ⊳ b] b"
  "ill_deduct_premises (ill_deduct_limp_eval a b) = []"
  by simp_all

text‹Exponential implication elimination with times: @{prop "[a ⊗ !(a ⊳ b)] ⊢ b ⊗ !(a ⊳ b)"}:›
fun ill_deduct_explimp_eval :: "'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_explimp_eval a b =
    TimesL [] a (!(a ⊳ b)) [] (b ⊗ !(a ⊳ b)) (
    Contract [a] (a ⊳ b) [] (b ⊗ !(a ⊳ b)) (
    TimesR [a, !(a ⊳ b)] b [!(a ⊳ b)] (!(a ⊳ b))
    ( Derelict [a] (a ⊳ b) [] b (
      LimpL [a] a [] b [] b
      ( Identity a)
      ( Identity b)))
    ( Identity (!(a ⊳ b)))))"

lemma ill_deduct_explimp_eval [simp]:
  "ill_deduct_wf (ill_deduct_explimp_eval a b)"
  "ill_conclusion (ill_deduct_explimp_eval a b) = Sequent [a ⊗ !(a ⊳ b)] (b ⊗ !(a ⊳ b))"
  "ill_deduct_premises (ill_deduct_explimp_eval a b) = []"
  by simp_all

text‹Distributing times over plus: @{prop "[a ⊗ (b ⊕ c)] ⊢ (a ⊗ b) ⊕ (a ⊗ c)"}:›
fun ill_deduct_distrib_plus :: "'a ill_prop ⇒ 'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_distrib_plus a b c =
  TimesL [] a (b ⊕ c) [] ((a ⊗ b) ⊕ (a ⊗ c))
  ( PlusL [a] b c [] ((a ⊗ b) ⊕ (a ⊗ c))
    ( PlusR1 [a, b] (a ⊗ b) (a ⊗ c)
      ( TimesR [a] a [b] b
        ( Identity a)
        ( Identity b)))
    ( PlusR2 [a, c] (a ⊗ b) (a ⊗ c)
      ( TimesR [a] a [c] c
        ( Identity a)
        ( Identity c))))"

lemma ill_deduct_distrib_plus [simp]:
  "ill_deduct_wf (ill_deduct_distrib_plus a b c)"
  "ill_conclusion (ill_deduct_distrib_plus a b c) = Sequent [a ⊗ (b ⊕ c)] ((a ⊗ b) ⊕ (a ⊗ c))"
  "ill_deduct_premises (ill_deduct_distrib_plus a b c) = []"
  by simp_all

text‹Distributing times out of plus: @{prop "[(a ⊗ b) ⊕ (a ⊗ c)] ⊢ a ⊗ (b ⊕ c)"}:›
fun ill_deduct_distrib_plus' :: "'a ill_prop ⇒ 'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_distrib_plus' a b c =
  PlusL [] (a ⊗ b) (a ⊗ c) [] (a ⊗ (b ⊕ c))
  ( ill_deduct_tensor
    ( Identity a)
    ( ill_deduct_plusR1 b c))
  ( ill_deduct_tensor
    ( Identity a)
    ( ill_deduct_plusR2 b c))"

lemma ill_deduct_distrib_plus' [simp]:
  "ill_deduct_wf (ill_deduct_distrib_plus' a b c)"
  "ill_conclusion (ill_deduct_distrib_plus' a b c) = Sequent [(a ⊗ b) ⊕ (a ⊗ c)] (a ⊗ (b ⊕ c))"
  "ill_deduct_premises (ill_deduct_distrib_plus' a b c) = []"
  by simp_all

text‹Combining two deductions with plus: @{prop "⟦[a] ⊢ b; [c] ⊢ d⟧ ⟹ [a ⊕ c] ⊢ b ⊕ d"}:›
fun ill_deduct_plus_progress :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_plus_progress p q =
    ill_deduct_simple_plusL
    ( ill_deduct_simple_cut p (ill_deduct_plusR1 (consequent p) (consequent q)))
    ( ill_deduct_simple_cut q (ill_deduct_plusR2 (consequent p) (consequent q)))"

lemma ill_deduct_plus_progress [simp]:
  "⟦antecedents P = [a]; antecedents Q = [c]; ill_deduct_wf P; ill_deduct_wf Q⟧ ⟹
    ill_deduct_wf (ill_deduct_plus_progress P Q)"
  "⟦antecedents P = [a]; antecedents Q = [c]⟧ ⟹
    ill_conclusion (ill_deduct_plus_progress P Q) = Sequent [a ⊕ c] (consequent P ⊕ consequent Q)"
  " ill_deduct_premises (ill_deduct_plus_progress P Q)
  = ill_deduct_premises P @ ill_deduct_premises Q"
  by simp_all blast

text‹Simplified with introduction: @{prop "⟦[a] ⊢ b; [a] ⊢ c⟧ ⟹ [a] ⊢ b & c"}:›
fun ill_deduct_with :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_with p q = WithR [hd (antecedents p)] (consequent p) (consequent q) p q"

lemma ill_deduct_with [simp]:
  "⟦ antecedents P = [a]; antecedents Q = [a]; consequent P = b
   ; consequent Q = c; ill_deduct_wf P; ill_deduct_wf Q⟧ ⟹
    ill_deduct_wf (ill_deduct_with P Q)"
  "⟦antecedents P = [a]; antecedents Q = [a]; consequent P = b; consequent Q = c⟧ ⟹
    ill_conclusion (ill_deduct_with P Q) = Sequent [a] (consequent P & consequent Q)"
  "ill_deduct_premises (ill_deduct_with P Q) = ill_deduct_premises P @ ill_deduct_premises Q"
  by simp_all blast

text‹Simplified with left projection: @{prop "[a & b] ⊢ a"}:›
fun ill_deduct_projectL :: "'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_projectL a b = WithL1 [] a b [] a (Identity a)"

lemma ill_deduct_projectL [simp]:
  "ill_deduct_wf (ill_deduct_projectL a b)"
  "ill_conclusion (ill_deduct_projectL a b) = Sequent [a & b] a"
  "ill_deduct_premises (ill_deduct_projectL a b) = []"
  by simp_all

text‹Simplified with right projection: @{prop "[a & b] ⊢ b"}:›
fun ill_deduct_projectR :: "'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_projectR a b = WithL2 [] a b [] b (Identity b)"

lemma ill_deduct_projectR [simp]:
  "ill_deduct_wf (ill_deduct_projectR a b)"
  "ill_conclusion (ill_deduct_projectR a b) = Sequent [a & b] b"
  "ill_deduct_premises (ill_deduct_projectR a b) = []"
  by simp_all

text‹Distributing times over with: @{prop "[a ⊗ (b & c)] ⊢ (a ⊗ b) & (a ⊗ c)"}:›
fun ill_deduct_distrib_with :: "'a ill_prop ⇒ 'a ill_prop ⇒ 'a ill_prop ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_distrib_with a b c =
  WithR [a ⊗ (b & c)] (a ⊗ b) (a ⊗ c)
  ( ill_deduct_tensor
    ( Identity a)
    ( ill_deduct_projectL b c))
  ( ill_deduct_tensor
    ( Identity a)
    ( ill_deduct_projectR b c))"

lemma ill_deduct_distrib_with [simp]:
  "ill_deduct_wf (ill_deduct_distrib_with a b c)"
  "ill_conclusion (ill_deduct_distrib_with a b c) = Sequent [a ⊗ (b & c)] ((a ⊗ b) & (a ⊗ c))"
  "ill_deduct_premises (ill_deduct_distrib_with a b c) = []"
  by simp_all

text‹Weakening a list of propositions: @{prop "G @ D ⊢ b ⟹ G @ (map Exp xs) @ D ⊢ b"}:›
fun ill_deduct_weaken_list
    :: "'a ill_prop list ⇒ 'a ill_prop list ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct
    ⇒ ('a, 'l) ill_deduct"
  where
    "ill_deduct_weaken_list G D [] P = P"
  | "ill_deduct_weaken_list G D (x#xs) P =
      Weaken G (map Exp xs @ D) (consequent P) x (ill_deduct_weaken_list G D xs P)"

lemma ill_deduct_weaken_list [simp]:
  "⟦antecedents P = G @ D; ill_deduct_wf P⟧ ⟹ ill_deduct_wf (ill_deduct_weaken_list G D xs P)"
  "antecedents P = G @ D ∨ xs ≠ [] ⟹
    antecedents (ill_deduct_weaken_list G D xs P) = G @ (map Exp xs) @ D"
  "consequent (ill_deduct_weaken_list G D xs P) = consequent P"
  "ill_deduct_premises (ill_deduct_weaken_list G D xs P) = ill_deduct_premises P"
proof -
  have [simp]: "antecedents (ill_deduct_weaken_list G D xs P) = G @ (map Exp xs) @ D"
    if "antecedents P = G @ D ∨ xs ≠ []"
    for G D :: "'c ill_prop list" and xs :: "'c ill_prop list" and P :: "('c, 'd) ill_deduct"
    using that by (induct xs) simp_all
  then show "antecedents P = G @ D ∨ xs ≠ [] ⟹
    antecedents (ill_deduct_weaken_list G D xs P) = G @ (map Exp xs) @ D" .

  have [simp]: "consequent (ill_deduct_weaken_list G D xs P) = consequent P"
    for G D :: "'c ill_prop list" and xs and P :: "('c, 'd) ill_deduct"
    by (induct xs) simp_all
  then show "consequent (ill_deduct_weaken_list G D xs P) = consequent P" .

  show "⟦antecedents P = G @ D; ill_deduct_wf P⟧ ⟹ ill_deduct_wf (ill_deduct_weaken_list G D xs P)"
    by (induct xs) (simp_all add: ill_conclusion_alt)

  show "ill_deduct_premises (ill_deduct_weaken_list G D xs P) = ill_deduct_premises P"
    by (induct xs) simp_all
qed

text‹Exponentiating a deduction: @{prop "G ⊢ b ⟹ map Exp G ⊢ ! b"}›
fun ill_deduct_exp_helper :: "nat ⇒ ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  ― ‹Helper function to apply @{const Derelict} to first @{text n} antecedents›
  where
    "ill_deduct_exp_helper 0 P = P"
  | "ill_deduct_exp_helper (Suc n) P =
      Derelict
        (map Exp (take n (antecedents P)))
        (nth (antecedents P) n)
        (drop (Suc n) (antecedents P))
        (consequent P)
        (ill_deduct_exp_helper n P)"

lemma ill_deduct_exp_helper:
  "n ≤ length (antecedents P) ⟹
      antecedents (ill_deduct_exp_helper n P)
    = map Exp (take n (antecedents P)) @ drop n (antecedents P)"
  "consequent (ill_deduct_exp_helper n P) = consequent P"
  "n ≤ length (antecedents P) ⟹ ill_deduct_wf (ill_deduct_exp_helper n P) = ill_deduct_wf P"
  "ill_deduct_premises (ill_deduct_exp_helper n P) = ill_deduct_premises P"
proof -
  have [simp]:
    " antecedents (ill_deduct_exp_helper n P)
    = map Exp (take n (antecedents P)) @ drop n (antecedents P)"
    if "n ≤ length (antecedents P)" for n
    using that by (induct n) (simp_all add: take_Suc_conv_app_nth)
  then show "n ≤ length (antecedents P) ⟹
      antecedents (ill_deduct_exp_helper n P)
    = map Exp (take n (antecedents P)) @ drop n (antecedents P)" .

  have [simp]: "consequent (ill_deduct_exp_helper n P) = consequent P" for n
    by (induct n) simp_all
  then show "consequent (ill_deduct_exp_helper n P) = consequent P" .

  show "n ≤ length (antecedents P) ⟹ ill_deduct_wf (ill_deduct_exp_helper n P) = ill_deduct_wf P"
    by (induct n) (simp_all add: ill_conclusion_alt Cons_nth_drop_Suc)

  show "ill_deduct_premises (ill_deduct_exp_helper n P) = ill_deduct_premises P"
    by (induct n) simp_all
qed

fun ill_deduct_exp :: "('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_exp P =
    Promote (antecedents P) (consequent P) (ill_deduct_exp_helper (length (antecedents P)) P)"

lemma ill_deduct_exp [simp]:
  "ill_conclusion (ill_deduct_exp P) = Sequent (map Exp (antecedents P)) (!(consequent P))"
  "ill_deduct_wf (ill_deduct_exp P) = ill_deduct_wf P"
  "ill_deduct_premises (ill_deduct_exp P) = ill_deduct_premises P"
  by (simp_all add: ill_conclusion_alt ill_deduct_exp_helper)

subsubsection‹Compacting Equivalences›

text‹Compacting cons equivalence: @{prop "a ⊗ compact b ⊣⊢ compact (a # b)"}:›
primrec ill_deduct_times_to_compact_cons :: "'a ill_prop ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct"
  ― ‹@{prop "[a ⊗ compact b] ⊢ compact (a # b)"}›
  where
    "ill_deduct_times_to_compact_cons a [] = ill_deduct_unit a"
  | "ill_deduct_times_to_compact_cons a (b#bs) = Identity (a ⊗ compact (b#bs))"

lemma ill_deduct_times_to_compact_cons [simp]:
  "ill_deduct_wf (ill_deduct_times_to_compact_cons a b)"
  " ill_conclusion (ill_deduct_times_to_compact_cons a b)
  = Sequent [a ⊗ compact b] (compact (a # b))"
  "ill_deduct_premises (ill_deduct_times_to_compact_cons a b) = []"
  by (cases b, simp_all)+

primrec ill_deduct_compact_cons_to_times :: "'a ill_prop ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct"
  ― ‹@{prop "[compact (a # b)] ⊢ a ⊗ compact b"}›
  where
    "ill_deduct_compact_cons_to_times a [] = ill_deduct_unit' a"
  | "ill_deduct_compact_cons_to_times a (b#bs) = Identity (a ⊗ compact (b#bs))"

lemma ill_deduct_compact_cons_to_times [simp]:
  "ill_deduct_wf (ill_deduct_compact_cons_to_times a b)"
  " ill_conclusion (ill_deduct_compact_cons_to_times a b)
  = Sequent [compact (a # b)] (a ⊗ compact b)"
  "ill_deduct_premises (ill_deduct_compact_cons_to_times a b) = []"
  by (cases b, simp, simp)+

text‹Compacting append equivalence: @{prop "compact a ⊗ compact b ⊣⊢ compact (a @ b)"}:›
primrec ill_deduct_times_to_compact_append
    :: "'a ill_prop list ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct"
  ― ‹@{prop "[compact a ⊗ compact b] ⊢ compact (a @ b)"}›
  where
    "ill_deduct_times_to_compact_append [] b =
      ill_deduct_simple_cut (ill_deduct_swap (𝟭) (compact b)) (ill_deduct_unit (compact b))"
  | "ill_deduct_times_to_compact_append (a#as) b =
      ill_deduct_simple_cut
      ( ill_deduct_simple_cut
        ( ill_deduct_simple_cut
          ( ill_deduct_tensor
            ( ill_deduct_compact_cons_to_times a as)
            ( Identity (compact b)))
          ( ill_deduct_assoc a (compact as) (compact b)))
        ( ill_deduct_tensor
          ( Identity a)
          ( ill_deduct_times_to_compact_append as b)))
      ( ill_deduct_times_to_compact_cons a (as @ b))"

lemma ill_deduct_times_to_compact_append [simp]:
  "ill_deduct_wf (ill_deduct_times_to_compact_append a b :: ('a, 'l) ill_deduct)"
  " ill_conclusion (ill_deduct_times_to_compact_append a b :: ('a, 'l) ill_deduct)
  = Sequent [compact a ⊗ compact b] (compact (a @ b))"
  "ill_deduct_premises (ill_deduct_times_to_compact_append a b) = []"
  by (induct a) (simp_all add: ill_conclusion_antecedents ill_conclusion_consequent)

primrec ill_deduct_compact_append_to_times
    :: "'a ill_prop list ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct"
  ― ‹@{prop "[compact (a @ b)] ⊢ compact a ⊗ compact b"}›
  where
    "ill_deduct_compact_append_to_times [] b =
      ill_deduct_simple_cut
        ( ill_deduct_unit' (compact b))
        ( ill_deduct_swap (compact b) (𝟭))"
  | "ill_deduct_compact_append_to_times (a#as) b =
      ill_deduct_simple_cut
      ( ill_deduct_compact_cons_to_times a (as @ b))
      ( ill_deduct_simple_cut
        ( ill_deduct_tensor
          ( Identity a)
          ( ill_deduct_compact_append_to_times as b))
        ( ill_deduct_simple_cut
          ( ill_deduct_assoc' a (compact as) (compact b))
          ( ill_deduct_tensor
            ( ill_deduct_times_to_compact_cons a as)
            ( Identity (compact b)))))"

lemma ill_deduct_compact_append_to_times [simp]:
  "ill_deduct_wf (ill_deduct_compact_append_to_times a b :: ('a, 'l) ill_deduct)"
  " ill_conclusion (ill_deduct_compact_append_to_times a b :: ('a, 'l) ill_deduct)
  = Sequent [compact (a @ b)] (compact a ⊗ compact b)"
  "ill_deduct_premises (ill_deduct_compact_append_to_times a b) = []"
  by (induct a) (simp_all add: ill_conclusion_antecedents ill_conclusion_consequent)

text‹
  Combine a list of deductions with times using @{const ill_deduct_tensor}, representing a
  generalised version of the following theorem of the shallow embedding: @{thm compact_sequent}
›
primrec ill_deduct_tensor_list :: "('a, 'l) ill_deduct list ⇒ ('a, 'l) ill_deduct"
  where
    "ill_deduct_tensor_list [] = Identity (𝟭)"
  | "ill_deduct_tensor_list (x#xs) =
      (if xs = [] then x else ill_deduct_tensor x (ill_deduct_tensor_list xs))"

lemma ill_deduct_tensor_list [simp]:
  fixes xs :: "('a, 'l) ill_deduct list"
  assumes "⋀x. x ∈ set xs ⟹ ∃a. antecedents x = [a]"
    shows " ill_conclusion (ill_deduct_tensor_list xs)
          = Sequent [compact (map (hd ∘ antecedents) xs)] (compact (map consequent xs))"
      and "(⋀x. x ∈ set xs ⟹ ill_deduct_wf x) ⟹ ill_deduct_wf (ill_deduct_tensor_list xs)"
      and "ill_deduct_premises (ill_deduct_tensor_list xs) = concat (map ill_deduct_premises xs)"
proof -
  have x [simp]:
    " ill_conclusion (ill_deduct_tensor_list xs)
    = Sequent [compact (map (hd ∘ antecedents) xs)] (compact (map consequent xs))"
    if "⋀x. x ∈ set xs ⟹ ∃a. antecedents x = [a]" for xs :: "('a, 'l) ill_deduct list"
    using that
  proof (induct xs)
    case Nil then show ?case by simp
  next
    case (Cons a xs)
    then show ?case
      using that by (simp add: ill_conclusion_antecedents ill_conclusion_consequent) fastforce
  qed
  then show
    " ill_conclusion (ill_deduct_tensor_list xs)
    = Sequent [compact (map (hd ∘ antecedents) xs)] (compact (map consequent xs))"
    using assms .

  show "(⋀x. x ∈ set xs ⟹ ill_deduct_wf x) ⟹ ill_deduct_wf (ill_deduct_tensor_list xs)"
    using assms
    by (induct xs) (fastforce simp add: ill_conclusion_antecedents ill_conclusion_consequent)+

  show "ill_deduct_premises (ill_deduct_tensor_list xs) = concat (map ill_deduct_premises xs)"
    using assms by (induct xs) simp_all
qed

subsubsection‹Premise Substitution›

text‹
  Premise substitution replaces certain premises in a deduction with other deductions.
  The target premises are specified with a predicate on the three arguments of the @{const Premise}
  constructor: antecedents, consequent and label.
  The replacement for each is specified as a function of those three arguments.
  In this way, the substitution can replace a whole class of premises in a single pass.
›
primrec ill_deduct_subst ::
  " ('a ill_prop list ⇒ 'a ill_prop ⇒ 'l ⇒ bool) ⇒
    ('a ill_prop list ⇒ 'a ill_prop ⇒ 'l ⇒ ('a, 'l) ill_deduct) ⇒
    ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where
    "ill_deduct_subst p f (Premise G c l) = (if p G c l then f G c l else Premise G c l)"
  | "ill_deduct_subst p f (Identity a) = Identity a"
  | "ill_deduct_subst p f (Exchange G a b D c P) = Exchange G a b D c (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (Cut G b D E c P Q) =
      Cut G b D E c (ill_deduct_subst p f P) (ill_deduct_subst p f Q)"
  | "ill_deduct_subst p f (TimesL G a b D c P) = TimesL G a b D c (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (TimesR G a D b P Q) =
      TimesR G a D b (ill_deduct_subst p f P) (ill_deduct_subst p f Q)"
  | "ill_deduct_subst p f (OneL G D c P) = OneL G D c (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (OneR) = OneR"
  | "ill_deduct_subst p f (LimpL G a D b E c P Q) =
      LimpL G a D b E c (ill_deduct_subst p f P) (ill_deduct_subst p f Q)"
  | "ill_deduct_subst p f (LimpR G a D b P) = LimpR G a D b (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (WithL1 G a b D c P) = WithL1 G a b D c (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (WithL2 G a b D c P) = WithL2 G a b D c (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (WithR G a b P Q) =
      WithR G a b (ill_deduct_subst p f P) (ill_deduct_subst p f Q)"
  | "ill_deduct_subst p f (TopR G) = TopR G"
  | "ill_deduct_subst p f (PlusL G a b D c P Q) =
      PlusL G a b D c (ill_deduct_subst p f P) (ill_deduct_subst p f Q)"
  | "ill_deduct_subst p f (PlusR1 G a b P) = PlusR1 G a b (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (PlusR2 G a b P) = PlusR2 G a b (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (ZeroL G D c) = ZeroL G D c"
  | "ill_deduct_subst p f (Weaken G D b a P) = Weaken G D b a (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (Contract G a D b P) = Contract G a D b (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (Derelict G a D b P) = Derelict G a D b (ill_deduct_subst p f P)"
  | "ill_deduct_subst p f (Promote G a P) = Promote G a (ill_deduct_subst p f P)"

text‹If the target premise is not present, then substitution does nothing›
lemma ill_deduct_subst_no_target:
  "(⋀G c l. (G, c, l) ∈ set (ill_deduct_premises x) ⟹ ¬ p G c l) ⟹ ill_deduct_subst p f x = x"
  by (induct x) simp_all

text‹If a deduction has no premise, then substitution does nothing›
lemma ill_deduct_subst_no_prems:
  "ill_deduct_premises x = [] ⟹ ill_deduct_subst p f x = x"
  using ill_deduct_subst_no_target empty_set emptyE by metis

text‹If we substitute the target, then the substitution does nothing›
lemma ill_deduct_subst_of_target [simp]:
  "f = Premise ⟹ ill_deduct_subst p f x = x"
  by (induct x) simp_all

text‹Substitution matching the target's antecedents preserves overall deduction antecedents›
lemma ill_deduct_subst_antecedents [simp]:
  assumes "(⋀G c l. p G c l ⟹ antecedents (f G c l) = G)"
    shows "antecedents (ill_deduct_subst p f x) = antecedents x"
  using assms by (induct x) simp_all

text‹Substitution matching the target's consequent preserves overall deduction consequent›
lemma ill_deduct_subst_consequent [simp]:
  assumes "⋀G c l. p G c l ⟹ consequent (f G c l) = c"
    shows "consequent (ill_deduct_subst p f x) = consequent x"
  by (induct x) (simp_all add: assms)

text‹
  Substitution matching target's antecedent, consequent and well-formedness preserves overall
  well-formedness
›
lemma ill_deduct_subst_wf [simp]:
  assumes "⋀G c l. p G c l ⟹ antecedents (f G c l) = G"
      and "⋀G c l. p G c l ⟹ consequent (f G c l) = c"
      and "⋀G c l. p G c l ⟹ ill_deduct_wf (f G c l)"
    shows "ill_deduct_wf x = ill_deduct_wf (ill_deduct_subst p f x)"
  using assms by (induct x) (simp_all add: ill_conclusion_alt)

text‹
  Premises after substitution are those that didn't satisfy the predicate and anything that was
  introduced by the function applied on satisfying premises' parameters.
›
lemma ill_deduct_subst_ill_deduct_premises:
  " ill_deduct_premises (ill_deduct_subst p f x)
  = concat (map (λ(G, c, l).
      if p G c l then ill_deduct_premises (f G c l) else [(G, c, l)])
    (ill_deduct_premises x))"
  by (induct x) (simp_all)

text‹This substitution commutes with many operations on deductions›
lemma
  assumes "⋀G c l. p G c l ⟹ antecedents (f G c l) = G"
      and "⋀G c l. p G c l ⟹ consequent (f G c l) = c"
    shows ill_deduct_subst_simple_cut [simp]:
      " ill_deduct_subst p f (ill_deduct_simple_cut X Y)
      = ill_deduct_simple_cut (ill_deduct_subst p f X) (ill_deduct_subst p f Y)"
      and ill_deduct_subst'_tensor [simp]:
      " ill_deduct_subst p f (ill_deduct_tensor X Y) =
        ill_deduct_tensor (ill_deduct_subst p f X) (ill_deduct_subst p f Y)"
      and ill_deduct_subst_simple_plusL [simp]:
      " ill_deduct_subst p f (ill_deduct_simple_plusL X Y) =
        ill_deduct_simple_plusL (ill_deduct_subst p f X) (ill_deduct_subst p f Y)"
      and ill_deduct_subst_with [simp]:
      " ill_deduct_subst p f (ill_deduct_with X Y) =
        ill_deduct_with (ill_deduct_subst p f X) (ill_deduct_subst p f Y)"
      and ill_deduct_subst_simple_limpR [simp]:
      " ill_deduct_subst p f (ill_deduct_simple_limpR X) =
        ill_deduct_simple_limpR (ill_deduct_subst p f X)"
      and ill_deduct_subst_simple_limpR_exp [simp]:
      " ill_deduct_subst p f (ill_deduct_simple_limpR_exp X) =
        ill_deduct_simple_limpR_exp (ill_deduct_subst p f X)"
  using assms by (simp_all add: ill_conclusion_alt)

subsubsection‹List-Based Exchange›

text‹
  To expand the applicability of the exchange rule to lists of propositions, we first need to
  establish that the well-formedness of a deduction is not affected by compacting a sublist of the
  antecedents of its conclusions.
  This corresponds to the following equality in the shallow embedding of deductions:
  @{thm compact_antecedents}.
›

text‹
  For one direction of the equality we need to use @{const TimesL} to recursively add one
  proposition at a time into the compacted part of the antecedents.
  Note that, just like @{const compact}, the recursion terminates in the singleton case.
›
primrec ill_deduct_compact_antecedents_split
    :: "nat ⇒ 'a ill_prop list ⇒ 'a ill_prop list ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct
    ⇒ ('a, 'l) ill_deduct"
  where
    "ill_deduct_compact_antecedents_split 0 X G Y P = OneL (X @ G) Y (consequent P) P"
  | "ill_deduct_compact_antecedents_split (Suc n) X G Y P = (if n = 0 then P else
      TimesL
        (X @ take (length G - (Suc n)) G)
        (hd (drop (length G - (Suc n)) G))
        (compact (drop (length G - n) G))
        Y
        (consequent P)
        (ill_deduct_compact_antecedents_split n X G Y P))"

lemma ill_deduct_compact_antecedents_split [simp]:
  assumes "n ≤ length G"
    shows "antecedents P = X @ G @ Y ⟹
            antecedents (ill_deduct_compact_antecedents_split n X G Y P)
          = X @ take (length G - n) G @ [compact (drop (length G - n) G)] @ Y"
      and "consequent (ill_deduct_compact_antecedents_split n X G Y P) = consequent P"
      and "⟦antecedents P = X @ G @ Y; ill_deduct_wf P⟧ ⟹
            ill_deduct_wf (ill_deduct_compact_antecedents_split n X G Y P)"
      and " ill_deduct_premises (ill_deduct_compact_antecedents_split n X G Y P)
          = ill_deduct_premises P"
proof -
  have [simp]:
    " antecedents (ill_deduct_compact_antecedents_split n X G Y P)
    = X @ take (length G - n) G @ [compact (drop (length G - n) G)] @ Y"
    if "antecedents P = X @ G @ Y" and "n ≤ length G" for n X G Y and P :: "('c, 'd) ill_deduct"
  proof -
    have tol_hd_tl: "⋀xs ys. ⟦ys = tl xs; ys ≠ []⟧ ⟹ hd xs ⊗ compact ys = compact xs"
      by (metis list.collapse compact.simps(1) tl_Nil)

    show ?thesis
      using that
    proof (induct n)
      case 0 then show ?case by simp
    next
      case m: (Suc m)
      then show ?case
      proof (cases m)
        case 0
        then have "drop (length G - 1) G = [last G]"
          using m
          by (metis Suc_le_lessD append_butlast_last_id append_eq_conv_conj length_butlast
                    length_greater_0_conv)
        then show ?thesis
          using m 0 by simp (metis append_take_drop_id)
      next
        case (Suc m')
        have "tl (drop (length G - Suc (Suc m')) G) = drop (length G - Suc m') G"
          using m.prems(2) by (metis Suc Suc_diff_Suc Suc_le_lessD drop_Suc tl_drop)
        then have
          " drop (length G - Suc (Suc m')) G
          = hd (drop (length G - Suc (Suc m')) G) # drop (length G - Suc m') G"
          using m.prems(2)
          by (metis Suc diff_diff_cancel diff_is_0_eq' drop_eq_Nil hd_Cons_tl nat.distinct(1))
        moreover have "drop (length G - Suc m') G ≠ []"
          using m.prems(2) by simp
        ultimately have
          " hd (drop (length G - Suc (Suc m')) G) ⊗ compact (drop (length G - Suc m') G)
          = compact (drop (length G - Suc (Suc m')) G)"
          by (metis compact.simps(1))
        then show ?thesis
          using Suc by simp
      qed
    qed
  qed
  then show "antecedents P = X @ G @ Y ⟹
      antecedents (ill_deduct_compact_antecedents_split n X G Y P)
    = X @ take (length G - n) G @ [compact (drop (length G - n) G)] @ Y"
    using assms by simp

  have [simp]: "consequent (ill_deduct_compact_antecedents_split n X G Y P) = consequent P"
    if "n ≤ length G" for n X G Y and P :: "('a, 'l) ill_deduct"
    by (induct n) simp_all
  then show "consequent (ill_deduct_compact_antecedents_split n X G Y P) = consequent P"
    using assms .

  show "⟦antecedents P = X @ G @ Y; ill_deduct_wf P⟧ ⟹
      ill_deduct_wf (ill_deduct_compact_antecedents_split n X G Y P)"
    using assms by (induct n) (simp_all add: Suc_diff_Suc take_hd_drop ill_conclusion_alt)
  show
    " ill_deduct_premises (ill_deduct_compact_antecedents_split n X G Y P)
    = ill_deduct_premises P"
    by (induct n) simp_all
qed

text‹Implication in the uncompacted-to-compacted direction›
fun ill_deduct_antecedents_to_times
    :: "'a ill_prop list ⇒ 'a ill_prop list ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct
    ⇒ ('a, 'l) ill_deduct"
  ― ‹@{prop "X @ G @ Y ⊢ c ⟹ X @ [compact G] @ Y ⊢ c"}›
  where "ill_deduct_antecedents_to_times X G Y P =
    ill_deduct_compact_antecedents_split (length G) X G Y P"

lemma ill_deduct_antecedents_to_times [simp]:
  "antecedents P = X @ G @ Y ⟹
    antecedents (ill_deduct_antecedents_to_times X G Y P) = X @ [compact G] @ Y"
  "consequent (ill_deduct_antecedents_to_times X G Y P) = consequent P"
  "⟦antecedents P = X @ G @ Y; ill_deduct_wf P⟧ ⟹
    ill_deduct_wf (ill_deduct_antecedents_to_times X G Y P)"
  "ill_deduct_premises (ill_deduct_antecedents_to_times X G Y P) = ill_deduct_premises P"
  by simp_all

text‹
  For the other direction we only need to derive the compacted propositions from the original list.
  This corresponds to the following valid sequent in the shallow embedding of deductions:
  @{thm identity_list}.
›
fun ill_deduct_identity_compact :: "'a ill_prop list ⇒ ('a, 'l) ill_deduct"
  where
    "ill_deduct_identity_compact [] = OneR"
  | "ill_deduct_identity_compact [x] = Identity x"
  | "ill_deduct_identity_compact (x#xs) =
      TimesR [x] x xs (compact xs) (Identity x) (ill_deduct_identity_compact xs)"

lemma ill_deduct_identity_compact [simp]:
  "ill_conclusion (ill_deduct_identity_compact G) = Sequent G (compact G)"
  "ill_deduct_wf (ill_deduct_identity_compact G)"
  "ill_deduct_premises (ill_deduct_identity_compact G) = []"
proof -
  have [simp]: "ill_conclusion (ill_deduct_identity_compact G) = Sequent G (compact G)"
    for G :: "'a ill_prop list"
    by (induct G rule: induct_list012) simp_all
  then show "ill_conclusion (ill_deduct_identity_compact G) = Sequent G (compact G)" .
  show "ill_deduct_wf (ill_deduct_identity_compact G)"
    by (induct G rule: induct_list012) (simp_all add: ill_conclusion_alt)
  show "ill_deduct_premises (ill_deduct_identity_compact G) = []"
    by (induct G rule: induct_list012) simp_all
qed

text‹Implication in the compacted-to-uncompacted direction›
fun ill_deduct_antecedents_from_times
    :: "'a ill_prop list ⇒ 'a ill_prop list ⇒ 'a ill_prop list ⇒ ('a, 'l) ill_deduct
    ⇒ ('a, 'l) ill_deduct"
  ― ‹@{prop "X @ [compact G] @ Y ⊢ c ⟹ X @ G @ Y ⊢ c"}›
  where "ill_deduct_antecedents_from_times X G Y P =
          Cut G (compact G) X Y (consequent P) (ill_deduct_identity_compact G) P"

lemma ill_deduct_antecedents_from_times [simp]:
  "ill_conclusion (ill_deduct_antecedents_from_times X G Y P) =
    Sequent (X @ G @ Y) (consequent P)"
  "⟦antecedents P = X @ [compact G] @ Y; ill_deduct_wf P⟧ ⟹
    ill_deduct_wf (ill_deduct_antecedents_from_times X G Y P)"
  " ill_deduct_premises (ill_deduct_antecedents_from_times X G Y P)
  = ill_deduct_premises P"
  by (simp_all add: ill_conclusion_alt)

text‹
  Finally, we establish the deep embedding of list-based exchange.
  This corresponds to the following theorem in the shallow embedding of deductions:
  @{thm exchange_list}.
›
fun ill_deduct_exchange_list
    :: "'a ill_prop list ⇒ 'a ill_prop list ⇒ 'a ill_prop list ⇒ 'a ill_prop list ⇒ 'a ill_prop
    ⇒ ('a, 'l) ill_deduct ⇒ ('a, 'l) ill_deduct"
  where "ill_deduct_exchange_list G A B D c P =
    ill_deduct_antecedents_from_times G B (A @ D)
    ( ill_deduct_antecedents_from_times (G @ [compact B]) A D
      ( Exchange G (compact A) (compact B) D c
        ( ill_deduct_antecedents_to_times (G @ [compact A]) B D
          ( ill_deduct_antecedents_to_times G A (B @ D) P))))"

lemma ill_deduct_exchange_list [simp]:
  "ill_conclusion (ill_deduct_exchange_list G A B D c P) = Sequent (G @ B @ A @ D) c"
  "⟦ill_deduct_wf P; antecedents P = G @ A @ B @ D; consequent P = c⟧ ⟹
    ill_deduct_wf (ill_deduct_exchange_list G A B D c P)"
  "ill_deduct_premises (ill_deduct_exchange_list G A B D c P) = ill_deduct_premises P"
  by (simp_all add: ill_conclusion_alt)

end