section‹Intuitionistic Linear Logic›

theory ILL
  imports
    Main
    "HOL-Combinatorics.Permutations"
begin

text‹
 Note that in this theory we often use procedural proofs rather than structured ones.
 We find these to be more informative about how the basic rules of the logic are used when
 compared to collecting all the rules in one call of an automated method.
 ›

subsection‹Deep Embedding of Propositions›

text‹
 We formalise ILL propositions as a datatype, parameterised by the type of propositional variables.
 The propositions are:
 ▪ Propositional variables
 ▪ Times of two terms, with unit @{text 1}
 ▪ With of two terms, with unit @{text ⊤}
 ▪ Plus of two terms, with unit @{text 0}
 ▪ Linear implication, with no unit
 ▪ Exponential of a term
 ›
datatype 'a ill_prop =
    Prop 'a
  | Times "'a ill_prop" "'a ill_prop" (infixr "⊗" 90) | One ("1")
  | With "'a ill_prop" "'a ill_prop" (infixr "&" 90) | Top ("⊤")
  | Plus "'a ill_prop" "'a ill_prop" (infixr "⊕" 90) | Zero ("0")
  | LImp "'a ill_prop" "'a ill_prop" (infixr "⊳" 90)
    ― ‹Note that Isabelle font does not include $\multimap$, so we use @{text ⊳} instead›
  | Exp "'a ill_prop" ("!" 1000)

(* Note: With syntax causes ambiguity, do the following to counteract it:
no_notation HOL.conj (infixr "&" 35)
 *)

subsection‹Shallow Embedding of Deductions›

text‹
 See Bierman~cite‹"bierman-1994"› or Kalvala and de~Paiva~cite‹"kalvala_depaiva-1995"› for an
 overview of valid sequents in ILL.

 We first formalise ILL deductions as a relation between a list of propositions (anteceents) and a
 single proposition (consequent).
 This constitutes a shallow embedding of deductions (with a deep embedding to follow).

 In using a list, as opposed to a multiset, we make the exchange rule explicit.
 Furthermore, we take as primitive a rule exchanging two propositions and later derive both the
 corresponding rule for lists of propositions as well as for multisets.

 The specific formulation of rules we use here includes lists in more positions than is
 traditionally done when presenting ILL.
 This is inspired by the recommendations of Kalvala and de~Paiva, intended to improve pattern
 matching and automation.
 ›
inductive sequent :: "'a ill_prop list → 'a ill_prop → bool" (infix "⊨" 60)
  where
  identity: "[a] ⊨ a"
| exchange: "[G @ [a] @ [b] @ D ⊨ c] ==> G @ [b] @ [a] @ D ⊨ c"
| cut:      "[G ⊨ b; D @ [b] @ E ⊨ c] ==> D @ G @ E ⊨ c"
| timesL:   "G @ [a] @ [b] @ D ⊨ c ==> G @ [a ⊗ b] @ D ⊨ c"
| timesR:   "[G ⊨ a; D ⊨ b] ==> G @ D ⊨ a ⊗ b"
| oneL:     "G @ D ⊨ c ==> G @ [1] @ D ⊨ c"
| oneR:     "[] ⊨ 1"
| limpL:    "[G ⊨ a; D @ [b] @ E ⊨ c] ==> G @ D @ [a ⊳ b] @ E ⊨ c"
| limpR:    "G @ [a] @ D ⊨ b ==> G @ D ⊨ a ⊳ b"
| withL1:   "G @ [a] @ D ⊨ c ==> G @ [a & b] @ D ⊨ c"
| withL2:   "G @ [b] @ D ⊨ c ==> G @ [a & b] @ D ⊨ c"
| withR:    "[G ⊨ a; G ⊨ b] ==> G ⊨ a & b"
| topR:     "G ⊨ ⊤"
| plusL:    "[G @ [a] @ D ⊨ c; G @ [b] @ D ⊨ c] ==> G @ [a ⊕ b] @ D ⊨ c"
| plusR1:   "G ⊨ a ==> G ⊨ a ⊕ b"
| plusR2:   "G ⊨ b ==> G ⊨ a ⊕ b"
| zeroL:    "G @ [0] @ D ⊨ c"
| weaken:   "G @ D ⊨ b ==> G @ [!a] @ D ⊨ b"
| contract: "G @ [!a] @ [!a] @ D ⊨ b ==> G @ [!a] @ D ⊨ b"
| derelict: "G @ [a] @ D ⊨ b ==> G @ [!a] @ D ⊨ b"
| promote:  "map Exp G ⊨ a ==> map Exp G ⊨ !a"

lemmas [simp] = sequent.identity

subsection‹Proposition Equivalence›

text‹Two propositions are equivalent when each can be derived from the other›
definition ill_eq :: "'a ill_prop → 'a ill_prop → bool" (infix "⊣⊨" 60)
  where "a ⊣⊨ b = ([a] ⊨ b ∧ [b] ⊨ a)"

text‹We show that this is an equivalence relation›
lemma ill_eq_refl [simp]:
  "a ⊣⊨ a"
  by (simp add: ill_eq_def)

lemma ill_eq_sym [sym]:
  "a ⊣⊨ b ==> b ⊣⊨ a"
  by (smt ill_eq_def)

lemma ill_eq_tran [trans]:
  "[a ⊣⊨ b; b ⊣⊨ c] ==> a ⊣⊨ c"
  using cut[of _ _ Nil Nil] by (simp add: ill_eq_def) blast

lemma "equivp ill_eq"
  by (metis equivpI ill_eq_refl ill_eq_sym ill_eq_tran reflp_def sympI transp_def)

lemma ill_eqI [intro]:
  "[a] ⊨ b ==> [b] ⊨ a ==> a ⊣⊨ b"
  using ill_eq_def by blast

lemma ill_eqE [elim]:
  "a ⊣⊨ b ==> ([a] ⊨ b ==> [b] ⊨ a ==> R) ==> R"
  by (simp add: ill_eq_def)

lemma ill_eq_lr: "a ⊣⊨ b ==> [a] ⊨ b"
  and ill_eq_rl: "a ⊣⊨ b ==> [b] ⊨ a"
  by (simp_all add: ill_eq_def)

subsection‹Useful Rules›

text‹
 We can derive a number of useful rules from the defining ones, especially their specific
 instantiations.

 Particularly useful is an instantiation of the Cut rule that makes it transitive, allowing us to
 use equational reasoning (@{command also} and @{command finally}) to build derivations using
 single propositions
 ›
lemma simple_cut [trans]:
  "[G ⊨ b; [b] ⊨ c] ==> G ⊨ c"
  using cut[of _ _ Nil Nil] by simp

lemma
  shows sequent_Nil_left: "[] @ G ⊨ c ==> G ⊨ c"
    and sequent_Nil_right: "G @ [] ⊨ c ==> G ⊨ c"
  by simp_all

lemma simple_exchange:
  "[[a, b] ⊨ c] ==> [b, a] ⊨ c "
  using exchange[of Nil _ _ Nil] by simp

lemma simple_timesL:
  "[[a] @ [b] ⊨ c] ==> [a ⊗ b] ⊨ c"
  using timesL[of Nil] by simp

lemma simple_withL1: "[[a] ⊨ c] ==> [a & b] ⊨ c"
  and simple_withL2: "[[b] ⊨ c] ==> [a & b] ⊨ c"
  using withL1[of Nil] withL2[of Nil] by simp_all

lemma simple_plusL:
  "[[a] ⊨ c; [b] ⊨ c] ==> [a ⊕ b] ⊨ c"
  using plusL[of Nil] by simp

lemma simple_weaken:
  "[!a] ⊨ 1"
  using weaken[of Nil] oneR by simp

lemma simple_derelict:
  "[[a] ⊨ b] ==> [!a] ⊨ b"
  using derelict[of Nil] by simp

lemmas simple_promote = promote[of "[_]", unfolded list.map]

lemma promote_and_derelict:
  assumes "G ⊨ c"
  shows "map Exp G ⊨ !c"
proof -
  have ind: "map Exp (take n G) @ drop n G ⊨ c" if n: "n ≤ length G" for n
    using n
  proof (induct n)
    case 0
    then show ?case using assms by simp
  next
    case (Suc m)
    moreover have "nth G m # drop (Suc m) G = drop m G"
      using Suc Cons_nth_drop_Suc Suc_le_lessD by blast
    moreover have "map Exp (take m G) @ [! (nth G m)] = map Exp (take (Suc m) G)"
      by (simp add: Suc Suc_le_lessD take_Suc_conv_app_nth)
    ultimately show ?case
      using derelict[of "map Exp (take m G)" "nth G m" "drop (Suc m) G" c]
      by simp (metis append.assoc append_Cons append_Nil)
  qed

  have "map Exp G ⊨ c"
    using ind[of "length G"] by simp
  then show ?thesis
    by (rule promote)
qed

lemmas dereliction = simple_derelict[OF identity]

lemma simple_contract:
  "[[!a] @ [!a] ⊨ b] ==> [!a] ⊨ b"
  using contract[of Nil] by simp

lemma duplicate:
  "[!a] ⊨ !a ⊗ !a"
  using identity simple_contract timesR by blast

lemma unary_promote:
  "[[!g] ⊨ a] ==> [!g] ⊨ !a"
  by (metis (mono_tags, opaque_lifting) promote list.simps(8) list.simps(9))

lemma tensor:
  "[[a] ⊨ b; [c] ⊨ d] ==> [a ⊗ c] ⊨ b ⊗ d"
  using simple_timesL timesR by blast

lemma ill_eq_tensor:
  "a ⊣⊨ b ==> x ⊣⊨ y ==> a ⊗ x ⊣⊨ b ⊗ y"
  by (simp add: ill_eq_def tensor)

lemma times_assoc:
  "[(a ⊗ b) ⊗ c] ⊨ a ⊗ (b ⊗ c)"
proof -
  have "[a] @ [b] @ [c] ⊨ a ⊗ (b ⊗ c)"
    by (rule timesR[OF identity timesR, OF identity identity])
  then have "[a ⊗ b] @ [c] ⊨ a ⊗ (b ⊗ c)"
    by (metis timesL append_self_conv2)
  then show ?thesis
    by (simp add: simple_timesL)
qed

lemma times_assoc':
  "[a ⊗ (b ⊗ c)] ⊨ (a ⊗ b) ⊗ c"
proof -
  have "([a] @ [b]) @ [c] ⊨ (a ⊗ b) ⊗ c"
    by (rule timesR[OF timesR identity, OF identity identity])
  then have "[a] @ [b] @ [c] ⊨ (a ⊗ b) ⊗ c"
    by simp
  then show ?thesis
    using timesL[of "[a]" b c Nil] by (simp add: simple_timesL)
qed

lemma simple_limpR:
  "[a] ⊨ b ==> [1] ⊨ a ⊳ b"
  using limpR[of Nil _ "[1]"] oneL[of "[a]" Nil b] by simp

lemma simple_limpR_exp:
  "[a] ⊨ b ==> [1] ⊨ !(a ⊳ b)"
proof -
  assume "[a] ⊨ b"
  then have "[] ⊨ a ⊳ b"
    by (rule simple_cut[of Nil 1 "a ⊳ b", OF oneR simple_limpR])
  then have "[] ⊨ !(a ⊳ b)"
    using promote[of Nil "a ⊳ b"] by simp
  then show ?thesis
    using oneL[of Nil] by simp
qed

lemma limp_eval:
  "[a ⊗ a ⊳ b] ⊨ b"
  using limpL[of "[a]" a Nil] simple_timesL[of a] by simp

lemma timesR_intro:
  "[G ⊨ a; D ⊨ b; G @ D = X] ==> X ⊨ a ⊗ b"
  using timesR by metis

lemma explimp_eval:
  "[a ⊗ !(a ⊳ b)] ⊨ b ⊗ !(a ⊳ b)"
  apply (rule simple_timesL)
  apply (subst (2) append_Nil2[symmetric], subst append_assoc)
  apply (rule contract)
  apply (subst append_Nil2, subst append_assoc[symmetric])
  apply (rule timesR)

   apply (subst (2) append_Nil2[symmetric], subst append_assoc)
   apply (rule derelict)
   apply (subst (2) append_Nil[symmetric], subst append_assoc)
   apply (rule limpL)
    apply (rule identity)
   apply (subst append_Nil2, subst append_Nil)
   apply (rule identity)

  apply (rule identity)
  done

lemma plus_progress:
  "[[a] ⊨ b; [c] ⊨ d] ==> [a ⊕ c] ⊨ b ⊕ d"
  using plusR1 plusR2 simple_plusL by blast

text‹
 The following set of rules are based on Proposition~1 of Bierman~cite‹"bierman-1994"›.
 Where there is a direct correspondence, we include a comment indicating the specific item in the
 proposition.
 ›

lemma swap: ― ‹Item 1›
  "[a ⊗ b] ⊨ b ⊗ a"
proof -
  have "[b] @ [a] ⊨ b ⊗ a"
    by (rule timesR[OF identity identity])
  then have "[a] @ [b] ⊨ b ⊗ a"
    using simple_exchange by force
  then show ?thesis
    using simple_timesL by simp
qed

lemma unit: ― ‹Item 2›
  "[a ⊗ 1] ⊨ a"
  using oneL[of "[a]"] by (simp add: simple_timesL)

lemma unit': ― ‹Item 2›
  "[a] ⊨ a ⊗ 1"
  using timesR[of "[a]" a Nil 1] oneR by simp

lemma with_swap: ― ‹Item 3›
  "[a & b] ⊨ b & a"
  using withL2[of Nil b] withL1[of Nil a] by (simp add: withR)

lemma with_top: ― ‹Item 4›
  "a ⊣⊨ a & ⊤"
proof
  show "[a & ⊤] ⊨ a"
    by (simp add: simple_withL1)
next
  show "[a] ⊨ a & ⊤"
    by (rule withR[OF identity topR])
qed

lemma plus_swap: ― ‹Item 5›
  "[a ⊕ b] ⊨ b ⊕ a"
  using plusL[of Nil a] by (simp add: plusR1 plusR2)

lemma plus_zero: ― ‹Item 6›
  "a ⊣⊨ a ⊕ 0"
proof
  show "[a ⊕ 0] ⊨ a"
    using plusL[of Nil a] zeroL[of Nil _ a] by simp
next
  show "[a] ⊨ a ⊕ 0"
    by (simp add: plusR1)
qed

lemma with_distrib: ― ‹Item 7›
  "[a ⊗ (b & c)] ⊨ (a ⊗ b) & (a ⊗ c)"
  by (intro withR tensor identity simple_withL1 simple_withL2)

lemma plus_distrib: ― ‹Item 8›
  "[a ⊗ (b ⊕ c)] ⊨ (a ⊗ b) ⊕ (a ⊗ c)"
  using timesR[OF identity identity] plusL[of "[a]" b Nil _ c]
  by (metis append_Cons append_Nil plusR1 plusR2 simple_timesL)

lemma plus_distrib': ― ‹Item 9›
  "[(a ⊗ b) ⊕ (a ⊗ c)] ⊨ a ⊗ (b ⊕ c)"
  by (simp add: simple_plusL tensor plusR1 plusR2)

lemma times_exp: ― ‹Item 10›
  "[!a ⊗ !b] ⊨ !(a ⊗ b)"
proof -
  have "[a, b] ⊨ a ⊗ b"
    using timesR[of "[a]"] by simp
  then have "[!a, !b] ⊨ a ⊗ b"
    by (metis derelict append_Cons append_Nil)
  then have "[!a, !b] ⊨ !(a ⊗ b)"
    by (metis (mono_tags, opaque_lifting) promote list.simps(8) list.simps(9))
  then show ?thesis
    by (simp add: simple_timesL)
qed

lemma one_exp: ― ‹Item 10›
  "1 ⊣⊨ !(1)"
  by (meson ill_eq_def simple_cut simple_limpR_exp simple_weaken unary_promote)

lemma ― ‹Item 11›
  "[!a] ⊨ 1 & a & (!a ⊗ !a)"
  by (metis identity withR simple_weaken simple_derelict simple_contract timesR)

lemma ― ‹Item 12›
  "!a ⊗ !b ⊣⊨ !(a & b)"
proof
  show "[!a ⊗ !b] ⊨ !(a & b)"
  proof -
    have "[!a, !b] ⊨ a & b"
    proof (rule withR)
      show "[! a, ! b] ⊨ a"
        using weaken[of "[!a]"] dereliction[of a] by simp
    next
      show "[! a, ! b] ⊨ b"
        using weaken[of "[!b]"] dereliction[of b] simple_exchange[of "!b" "!a"] by simp
    qed
    then show ?thesis
      using promote simple_timesL
      by (metis (mono_tags, opaque_lifting) append_Cons append_Nil list.simps(8) list.simps(9))
  qed
next
  show "[!(a & b)] ⊨ !a ⊗ !b"
  proof (rule simple_contract, rule timesR)
    show "[! (a & b)] ⊨ ! a"
      by (simp add: unary_promote simple_derelict simple_withL1)
  next
    show "[! (a & b)] ⊨ ! b"
      by (simp add: unary_promote simple_derelict simple_withL2)
  qed
qed

lemma ― ‹Item 13›
  "1 ⊣⊨ !(⊤)"
proof
  show "[1] ⊨ !(⊤)"
    using simple_cut simple_limpR_exp topR unary_promote by blast
next
  show "[!(⊤)] ⊨ 1"
    by (rule simple_weaken)
qed

subsection‹Compacting Lists of Propositions›

text‹
 Compacting transforms a list of propositions into a single proposition using the @{const Times}
 operator, taking care to not expand the size when given a list with only one element.
 This operation allows us to link the meta-level antecedent concatenation with the object-level
 @{const Times} operator, turning a list of antecedents into a single proposition with the same
 power in proofs.
 ›
function compact :: "'a ill_prop list → 'a ill_prop"
  where
    "xs ≠ [] ==> compact (x # xs) = x ⊗ compact xs"
  | "xs = [] ==> compact (x # xs) = x"
  | "compact [] = 1"
  by (metis list.exhaust) simp_all
termination by (relation "measure length", auto)

text‹For code generation we use an if statement›
lemma compact_code [code]:
  "compact [] = 1"
  "compact (x # xs) = (if xs = [] then x else x ⊗ compact xs)"
  by simp_all

text‹
 Two lists of propositions that compact to the same result must be equal if they do not include any
 @{const Times} or @{const One} elements.
 We show first that they must be equally long and then that they must be equal.
 ›
lemma compact_eq_length:
  assumes "∧a. a ∈ set xs ==> a ≠ 1"
      and "∧a. a ∈ set ys ==> a ≠ 1"
      and "∧a u v. a ∈ set xs ==> a ≠ u ⊗ v"
      and "∧a u v. a ∈ set ys ==> a ≠ u ⊗ v"
      and "compact xs = compact ys"
    shows "length xs = length ys"
  using assms
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case
    by simp (metis ill_prop.simps(24) list.set_intros(1) compact.elims compact.simps(2))
next
  case xs: (Cons a xs)
  then show ?case
  proof (cases ys)
    case Nil
    then have False
      using xs by simp (metis compact.simps(1,2) ill_prop.distinct(17))
    then show ?thesis
      by metis
  next
    case (Cons a list)
    then show ?thesis
      using xs by simp (metis ill_prop.inject(2) compact.simps(1,2))
  qed
qed

lemma compact_eq:
  assumes "∧a. a ∈ set xs ==> a ≠ 1"
      and "∧a. a ∈ set ys ==> a ≠ 1"
      and "∧a u v. a ∈ set xs ==> a ≠ u ⊗ v"
      and "∧a u v. a ∈ set ys ==> a ≠ u ⊗ v"
      and "compact xs = compact ys"
    shows "xs = ys"
proof -
  have "length xs = length ys"
    using assms by (rule compact_eq_length)
  then show ?thesis
    using assms
  proof (induct xs arbitrary: ys)
    case Nil
    then show ?case by simp
  next
    case xs: (Cons a xs)
    then show ?case
    proof (cases ys)
      case Nil
      then show ?thesis using xs by simp
    next
      case (Cons a list)
      then show ?thesis
        using xs by simp (metis ill_prop.inject(2) compact.simps(1,2))
    qed
  qed
qed

text‹Compacting to @{const ILL.One} means the list of propositions was either empty or just that›
lemma compact_eq_oneE:
  assumes "compact xs = 1"
  obtains "xs = []" | "xs = [1]"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp (metis compact.simps(1,2) ill_prop.distinct(17))
qed

text‹
 Compacting to @{const ILL.Times} means the list of propositions was either just that or started
 with the left-hand proposition and the rest compacts to the right-hand proposition
 ›
lemma compact_eq_timesE:
  assumes "compact xs = x ⊗ y"
  obtains "xs = [x ⊗ y]" | ys where "xs = x # ys" and "compact ys = y"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp (metis compact.simps(1,2) ill_prop.inject(2))
qed

text‹
 Compacting to anything but @{const ILL.One} or @{const ILL.Times} means the list was just that
 ›
lemma compact_eq_otherD:
  assumes "compact xs = a"
      and "∧x y. a ≠ x ⊗ y"
      and "a ≠ 1"
    shows "xs = [a]"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp (metis compact_code(2))
qed

text‹For any list of propositions, we can derive its compacted form from it›
lemma identity_list:
  "G ⊨ (compact G)"
proof (induction G rule: induct_list012)
     case 1 then show ?case by (simp add: oneR)
next case (2 a) then show ?case by simp
next case (3 a b G) then show ?case using timesR[OF identity] by simp
qed

text‹For any valid sequent, we can compact any sublist of its antecedents without invalidating it›
lemma compact_split_antecedents:
  assumes "X @ G @ Y ⊨ c"
    shows "n ≤ length G ==> X @ take (length G - n) G @ [compact (drop (length G - n) G)] @ Y ⊨ c"
proof (induct n)
  case 0
  then show ?case
    using oneL[of "X @ G"] assms by simp
next
  case (Suc n)
  then obtain as x bs where G: "G = as @ [x] @ bs" and bs: "length bs = n"
    by (metis Suc_length_conv append_Cons append_Nil append_take_drop_id diff_diff_cancel
              length_drop)

  have "X @ take (length G - n) G @ [compact (drop (length G - n) G)] @ Y ⊨ c"
    using Suc by simp
  then show ?case
    using timesL[of "X @ as" x "compact bs" Y c, simplified] G Suc.prems assms bs
    using Suc_diff_le Suc_leD Suc_le_D append.assoc append_Cons append_Nil append_eq_append_conv
          append_take_drop_id butlast_snoc diff_Suc_Suc diff_diff_cancel diff_less length_drop
          take_hd_drop compact.simps(1) compact.simps(2) zero_less_Suc
    by (smt (verit, ccfv_threshold))
qed

text‹More generally, compacting a sublist of antecedents does not affect sequent validity›
lemma compact_antecedents:
  "(X @ [compact G] @ Y ⊨ c) = (X @ G @ Y ⊨ c)"
proof
  assume "X @ [compact G] @ Y ⊨ c"
  then show "X @ G @ Y ⊨ c"
    using identity_list cut by blast
next
  assume "X @ G @ Y ⊨ c"
  then show "X @ [compact G] @ Y ⊨ c"
    using compact_split_antecedents[where n = "length G"] by fastforce
qed

text‹Times with a single proposition can be absorbed into compacting up to proposition equivalence›
lemma times_equivalent_cons:
  "a ⊗ compact b ⊣⊨ compact (a # b)"
proof (cases b)
  case Nil then show ?thesis by (simp add: ill_eq_def unit unit')
next
  case (Cons a list) then show ?thesis by simp
qed

text‹Times of compacted lists is equivalent to compacting the appended lists›
lemma times_equivalent_append:
  "compact a ⊗ compact b ⊣⊨ compact (a @ b)"
proof (induct a)
  case Nil
  then show ?case
    using simple_cut[OF swap unit] simple_cut[OF unit' swap] ill_eqI by (simp, blast)
next
  case assm: (Cons a1 a2)
  have "compact (a1 # a2) ⊗ compact b ⊣⊨ (a1 ⊗ compact a2) ⊗ compact b"
    by (simp add: times_equivalent_cons ill_eq_sym ill_eq_tensor)
  also have "... ⊣⊨ a1 ⊗ (compact a2 ⊗ compact b)"
    by (simp add: times_assoc times_assoc' ill_eqI)
  also have "... ⊣⊨ a1 ⊗ compact (a2 @ b)"
    using ill_eq_tensor[OF _ assm] by simp
  finally show ?case
    by (simp add: ill_eq_tran times_equivalent_cons)
qed

text‹Any number of single-antecedent sequents can be compacted with the rule @{thm tensor}›
lemma compact_sequent:
  "∀x ∈ set xs. [f x] ⊨ g x ==> [compact (map f xs)] ⊨ compact (map g xs)"
proof (induct xs rule: induct_list012)
     case 1 then show ?case by simp
next case (2 x) then show ?case by simp
next case (3 x y zs) then show ?case by (simp add: tensor)
qed

text‹Any number of equivalences can be compacted together›
lemma compact_equivalent:
  "∀x ∈ set xs. f x ⊣⊨ g x ==> compact (map f xs) ⊣⊨ compact (map g xs)"
  by (simp add: ill_eqI[OF compact_sequent compact_sequent] ill_eq_lr ill_eq_rl)

subsection‹Multiset Exchange›

text‹
 Recall that our @{const sequent} definition uses explicit single-proposition exchange.
 We now derive a rule for exchanging lists of propositions and then a rule that uses multisets to
 disregard the antecedent order entirely.
 ›

text‹We can exchange lists of propositions by stepping through @{const compact}›
lemma exchange_list:
  "G @ A @ B @ D ⊨ c ==> G @ B @ A @ D ⊨ c"
proof -
  assume "G @ A @ B @ D ⊨ c"
  then have "G @ [compact A] @ B @ D ⊨ c"
    using compact_antecedents by force
  then have "G @ [compact A] @ [compact B] @ D ⊨ c"
    using compact_antecedents[where X = "G @ [compact A]" and G = B] by force
  then have "G @ [compact B] @ [compact A] @ D ⊨ c"
    using exchange by simp
  then have "G @ [compact B] @ A @ D ⊨ c"
    using compact_antecedents[where X = "G @ [compact B]" and G = A] by force
  then show ?thesis
    using compact_antecedents by force
qed

lemma simple_exchange_list:
  "[A @ B ⊨ c] ==> B @ A ⊨ c "
  using exchange_list[of Nil _ _ Nil] by simp

text‹By applying the list exchange rule multiple times, the lists do not need to be adjacent›
lemma exchange_separated:
  "G @ A @ X @ B @ D ⊨ c ==> G @ B @ X @ A @ D ⊨ c"
  by (metis append.assoc exchange_list)

text‹Single transposition in the antecedents does not invalidate a sequent›
lemma exchange_transpose:
  assumes "G ⊨ c"
      and "a ∈ {..<length G}"
      and "b ∈ {..<length G}"
    shows "permute_list (transpose a b) G ⊨ c"
proof -
  consider "a < b" | "a = b" | "b < a"
    using not_less_iff_gr_or_eq by blast
  moreover { fix x y
    assume x_in [simp]: "x ∈ {..<length G}"
       and y_in [simp]: "y ∈ {..<length G}"
       and xy [arith]: "x < y"

    have "G = take x G @ drop x G"
      by simp
    also have "... = take x G @ nth G x # drop (Suc x) G"
      by simp (metis x_in id_take_nth_drop lessThan_iff)
    also have "... = take x G @ nth G x # take (y - Suc x) (drop (Suc x) G) @ drop y G"
      by simp (metis Suc_leI add.commute append_take_drop_id drop_drop le_add_diff_inverse xy)
    also have
      "... = take x G @ nth G x # take (y - Suc x) (drop (Suc x) G) @ nth G y # drop (Suc y) G"
      by simp (metis Cons_nth_drop_Suc y_in lessThan_iff)
    finally have G:
      "G = take x G @ nth G x # take (y - Suc x) (drop (Suc x) G) @ nth G y # drop (Suc y) G" .

    have "take x G @ [nth G y] @ take (y - Suc x) (drop (Suc x) G) @ [nth G x] @ drop (Suc y) G ⊨ c"
      by (rule exchange_separated, simp add: G[symmetric] assms(1))
    moreover have
      " permute_list (transpose x y) G
      = take x G @ nth G y # take (y - Suc x) (drop (Suc x) G) @ nth G x # drop (Suc y) G"
      unfolding list_eq_iff_nth_eq drop_Suc
    proof safe
      show
        " length (permute_list (Transposition.transpose x y) G)
        = length (take x G @ nth G y # take (y - Suc x) (drop x (tl G)) @ nth G x # drop y (tl G))"
        using y_in by simp
    next
      fix i
      assume "i < length (permute_list (Transposition.transpose x y) G)"
      then show "nth (permute_list (Transposition.transpose x y) G) i =
            nth (take x G @ nth G y # take (y - Suc x) (drop x (tl G)) @ nth G x # drop y (tl G)) i"
        by (simp add: permute_list_def transpose_def nth_append min_diff nth_tl)
    qed
    ultimately have "permute_list (transpose x y) G ⊨ c"
      by simp
  }
  ultimately show ?thesis
    using assms by (metis permute_list_id transpose_commute transpose_same)
qed

text‹
 More generally, by transposition being involutive, a single antecedent transposition does not
 affect sequent validity
 ›
lemma exchange_permute_eq:
  assumes "a ∈ {..<length G}"
      and "b ∈ {..<length G}"
    shows "permute_list (transpose a b) G ⊨ c = G ⊨ c"
  using assms exchange_transpose transpose_comp_involutory
  by (metis length_permute_list permute_list_compose permute_list_id permutes_swap_id)

text‹
 Validity of a sequent is not affected by replacing any antecedent sublist with a list that
 represents the same multiset.
 This is because lists representing equal multisets are connected by a permutation, which is a
 sequence of transpositions and as such does not affect validity.
 ›
lemma exchange_mset:
  "mset A = mset B ==> G @ A @ D ⊨ c = G @ B @ D ⊨ c"
proof -
  { fix X Y :: "'a ill_prop list"
    assume "X ⊨ c" and "mset X = mset Y"
    then have "Y ⊨ c"
    proof (elim mset_eq_permutation)
      fix p
      have "finite {..<length Y}"
        by simp
      moreover assume *: "p permutes {..<length Y}"
      moreover assume "X ⊨ c" and "permute_list p Y = X"
      ultimately show "Y ⊨ c"
      proof (induct arbitrary: X rule: permutes_rev_induct)
        case id then show ?case by simp
      next
        case (swap a b p)
        then show ?case
          by (metis permute_list_compose permutes_swap_id length_permute_list exchange_permute_eq)
      qed
    qed
  } note base = this

  show "mset A = mset B ==> G @ A @ D ⊨ c = G @ B @ D ⊨ c"
    by (standard ; simp add: base)
qed

subsection‹Additional Lemmas›

text‹
 These rules are based on Figure~2 of Kalvala and de~Paiva~cite‹"kalvala_depaiva-1995"›, labelled
 by them as ``additional rules for proof search''.
 We present them out of order because we use some in the proofs of the others, but annotate them
 with the original labels as comments.
 ›

lemma ill_mp1: ― ‹@{text mp₁}›
  assumes "A @ [b] @ B @ C ⊨ c"
    shows "A @ [a] @ B @ [a ⊳ b] @ C ⊨ c"
proof -
  have "[a] @ [a ⊳ b] ⊨ b"
    using limpL[of "[a]" a Nil] by simp
  then have "A @ [a] @ [a ⊳ b] @ B @ C ⊨ c"
    using assms cut[of _ b A "B @ C" c] by force
  then show ?thesis
    using exchange_list[of "A @ [a]" "[a ⊳ b]"] by simp
qed

lemmas simple_mp1 = ill_mp1[of Nil _ Nil Nil, simplified, OF identity]

lemma ― ‹@{text raa₁}›
  "G @ [!b] @ D @ [!b ⊳ 0] @ E ⊨ a"
  using zeroL ill_mp1 by blast

lemma ill_mp2: ― ‹@{text mp₂}›
  assumes "A @ [b] @ B @ C ⊨ c"
    shows "A @ [a ⊳ b] @ B @ [a] @ C ⊨ c"
  using ill_mp1[OF assms] exchange_list by (metis append.assoc)

lemmas simple_mp2 = ill_mp2[of Nil _ Nil Nil, simplified, OF identity]

lemma ― ‹@{text raa₂}›
  "G @ [!b ⊳ 0] @ D @ [!b] @ P ⊨ A"
  using zeroL ill_mp2 by blast

lemma ― ‹@{text "⊗_&"}›
  assumes "G @ [(!a ⊳ 0) & (!b ⊳ 0)] @ D ⊨ c"
    shows "G @ [!(!(a ⊕ b) ⊳ 0)] @ D ⊨ c"
proof -
  note exp_injL = unary_promote[OF simple_derelict, OF plusR1[OF identity, of a b]]
   and exp_injR = unary_promote[OF simple_derelict, OF plusR2[OF identity, of b a]]
  have "[!(!(a ⊕ b) ⊳ 0)] ⊨ (!a ⊳ 0) & (!b ⊳ 0)"
    apply (rule withR ; rule simple_derelict , rule limpR[of Nil, simplified])
     apply (rule cut[OF exp_injL, of Nil, simplified], rule simple_mp1)
     apply (rule cut[OF exp_injR, of Nil, simplified], rule simple_mp1)
    done
  then show ?thesis
    using assms cut by blast
qed

lemma ― ‹@{text "&_lemma"}›
  assumes "G @ [!a, !b] @ D ⊨ c"
    shows "G @ [!(a & b)] @ D ⊨ c"
proof -
  have as: "[!(a & b)] ⊨ !a"
    apply (rule unary_promote)
    apply (rule simple_derelict)
    by (rule simple_withL1[OF identity])
  have bs: "[!(a & b)] ⊨ !b"
    apply (rule unary_promote)
    apply (rule simple_derelict)
    by (rule simple_withL2[OF identity])
  show ?thesis
    apply (rule contract)
    using cut[OF as, of G "[!b] @ D" c] cut[OF bs, of "G @ [!(a & b)]" D c] assms
    by simp
qed

lemma ― ‹$\multimap_L$@{text "_lemma"}›
  assumes "G @ D ⊨ a"
  shows "G @ [!(a ⊳ b)] @ D ⊨ b"
  apply (rule derelict)
  using exchange_list[of G D "[a ⊳ b]" Nil b, simplified]
        limpL[OF assms, of Nil b Nil b, simplified]
  by simp

lemma ― ‹$\multimap_R$@{text "_lemma"}›
  assumes "[a, !a] @ G ⊨ b"
  shows "G ⊨ !a ⊳ b"
  apply (rule limpR[of _ _ Nil, simplified])
  apply (rule exchange_list[of Nil "[!a]" _ Nil, simplified])
  apply (rule contract[of Nil, simplified])
  apply (rule derelict[of Nil, simplified])
  using assms by simp

lemma ― ‹@{text "a_not_a"}›
  assumes "G @ [!a ⊳ 0] @ D ⊨ b"
  shows "G @ [!a ⊳ (!a ⊳ 0)] @ D ⊨ b"
proof -
  have "[!a ⊳ (!a ⊳ 0)] ⊨ !a ⊳ 0"
    apply (rule limpR[of _ _ Nil, simplified])
    apply (rule contract[of _ _ Nil, simplified])
    apply simp
    apply (rule ill_mp2[of Nil _  Nil "[!a]", simplified])
    by (rule simple_mp2)
  then show ?thesis
    using cut[OF _ assms] by blast
qed

end