Theory SC_Depth

theory SC_Depth
imports SC
begin
  
text‹
Many textbook arguments about SC use the depth of the derivation tree as basis for inductions.
We had originally thought that this is mandatory for the proof of contraction,
but found out it is not.
It remains unclear to us whether there is any proof on SC that requires an argument using depth.
›
text‹
We keep our formalization of SC with depth for didactic reasons:
we think that arguments about depth do not need much meta-explanation,
but structural induction and rule induction usually need extra explanation
for students unfamiliar with Isabelle/HOL.
They are also a lot harder to execute.
We dare the reader to write down (a few of) the cases for, e.g. ‹AndL_inv'›, by hand.
›

(* Warning: This theory may have name collisions with SC.thy… *)

inductive SCc :: "'a formula multiset ⇒ 'a formula multiset ⇒ nat ⇒ bool" (‹((_ ⇒/ _) ↓ _)› [53,53] 53) where
BotL: "⊥ ∈# Γ ⟹ Γ⇒Δ ↓ Suc n" |
Ax: "Atom k ∈# Γ ⟹ Atom k ∈# Δ ⟹ Γ⇒Δ ↓ Suc n" |
NotL: "Γ ⇒ F,Δ ↓ n ⟹ Not F, Γ ⇒ Δ ↓ Suc n" |
NotR: "F,Γ ⇒ Δ ↓ n ⟹ Γ ⇒ Not F, Δ ↓ Suc n" |
AndL: "F,G,Γ ⇒ Δ ↓ n ⟹ And F G, Γ ⇒ Δ ↓ Suc n" |
AndR: "⟦ Γ ⇒ F,Δ ↓ n; Γ ⇒ G,Δ ↓ n ⟧ ⟹ Γ ⇒ And F G, Δ ↓ Suc n" |
OrL: "⟦ F,Γ ⇒ Δ ↓ n; G,Γ ⇒ Δ ↓ n ⟧ ⟹ Or F G, Γ ⇒ Δ ↓ Suc n" |
OrR: "Γ ⇒ F,G,Δ ↓ n ⟹ Γ ⇒ Or F G, Δ ↓ Suc n" |
ImpL: "⟦ Γ ⇒ F,Δ ↓ n; G,Γ ⇒ Δ ↓ n ⟧ ⟹ Imp F G, Γ ⇒ Δ ↓ Suc n" |
ImpR: "F,Γ ⇒ G,Δ ↓ n ⟹ Γ ⇒ Imp F G, Δ ↓ Suc n"

lemma
  shows BotL_canonical'[intro!]: "⊥,Γ⇒Δ ↓ Suc n"
    and Ax_canonical'[intro!]: "Atom k,Γ ⇒ Atom k,Δ ↓ Suc n"
  by (meson SCc.intros union_single_eq_member)+
    
lemma deeper: "Γ ⇒ Δ ↓ n ⟹ Γ ⇒ Δ ↓ n + m"
  by(induction rule: SCc.induct; insert SCc.intros; auto) 
lemma deeper_suc: "Γ ⇒ Δ ↓ n ⟹ Γ ⇒ Δ ↓ Suc n"
  (* this version is actually required more often. It can be declared as an elim!, but I want to make its usage explicit *)
  thm deeper[unfolded Suc_eq_plus1[symmetric]]
  by(drule deeper[where m=1]) simp
    
text‹The equivalence is obvious.›
theorem SC_SCp_eq:
  fixes Γ Δ :: "'a formula multiset"
  shows "(∃n. Γ ⇒ Δ ↓ n) ⟷ Γ ⇒ Δ" (is "?c ⟷ ?p")
proof
  assume ?c
  then obtain n where "Γ ⇒ Δ ↓ n" ..
  thus ?p by(induction rule: SCc.induct; simp add: SCp.intros)
next
  have deeper_max: "Γ ⇒ Δ ↓ max m n" "Γ ⇒ Δ ↓ max n m" if "Γ ⇒ Δ ↓ n" for n m and Γ Δ :: "'a formula multiset"
  proof -
    have "n ≤ m ⟹ ∃k. m = n + k" by presburger
    with that[THEN deeper] that
    show "Γ ⇒ Δ ↓ max n m" unfolding max_def by clarsimp
    thus "Γ ⇒ Δ ↓ max m n" by (simp add: max.commute)
  qed
  assume ?p thus ?c by(induction rule: SCp.induct)
    (insert SCc.intros[where 'a='a] deeper_max; metis)+
qed

(* it makes a difference whether we say Ax is 0 or any: with Ax ↓ 0 we could not prove the deepening rules.
   Also, it is important to allow only atoms in Ax, otherwise the inv-rules are not depth preserving.
  Making Ax/BotL start from ≥1 saves proving the base-cases twice
 *)
lemma no_0_SC[dest!]: "Γ ⇒ Δ ↓ 0 ⟹ False"
  by(cases rule: SCc.cases[of Γ Δ 0]) assumption
    

lemma inR1': "Γ ⇒ G, H, Δ ↓ n ⟹ Γ ⇒ H, G, Δ ↓ n" by(simp add: add_mset_commute)
lemma inL1': "G, H, Γ ⇒ Δ ↓ n ⟹ H, G, Γ ⇒ Δ ↓ n" by(simp add: add_mset_commute)
lemma inR2': "Γ ⇒ F, G, H, Δ ↓ n ⟹ Γ ⇒ G, H, F, Δ ↓ n" by(simp add: add_mset_commute)
lemma inL2': "F, G, H, Γ ⇒ Δ ↓ n ⟹ G, H, F, Γ ⇒ Δ ↓ n" by(simp add: add_mset_commute)
lemma inR3': "Γ ⇒ F, G, H, Δ ↓ n ⟹ Γ ⇒ H, F, G, Δ ↓ n" by(simp add: add_mset_commute)
lemma inR4': "Γ ⇒ F, G, H, I, Δ ↓ n ⟹ Γ ⇒ H, I, F, G, Δ ↓ n" by(simp add: add_mset_commute)
lemma inL3': "F, G, H, Γ ⇒ Δ ↓ n ⟹ H, F, G, Γ ⇒ Δ ↓ n" by(simp add: add_mset_commute)
lemma inL4': "F, G, H, I, Γ ⇒ Δ ↓ n ⟹ H, I, F, G, Γ ⇒ Δ ↓ n" by(simp add: add_mset_commute)
lemmas SC_swap_applies[intro,elim!] = inL1' inL2' inL3' inL4' inR1' inR2' inR3' inR4'
  (* these are here because they can be used for more careful reasoning with intro *)

lemma "Atom C ❙→ Atom D ❙→ Atom E,
       Atom k ❙→ Atom C ❙∧ Atom D, 
       Atom k, {#} 
⇒ {# Atom E #} ↓ Suc (Suc (Suc (Suc (Suc 0))))"
  by(auto intro!: SCc.intros(3-) intro: SCc.intros(1,2))

lemma Bot_delR': "Γ ⇒ Δ ↓ n ⟹ Γ ⇒ Δ-{#⊥#} ↓ n"
proof(induction rule: SCc.induct) 
  case BotL thus ?case by(rule SCc.BotL; simp) (* SC.BotL refers to SC.SCp.BotL. Even more interestingly, there used to be a SCc.SC.BotL (which was not reffered to). I'll just leave this here and see how long till someone breaks it. *)
next case (Ax k) thus ?case by(intro SCc.Ax[of k]; simp; metis diff_single_trivial formula.distinct(1) insert_DiffM lem1)
next case NotL thus ?case using SCc.NotL by (metis add_mset_remove_trivial diff_single_trivial diff_union_swap insert_DiffM)
next case NotR thus ?case using SCc.NotR by (metis diff_union_swap formula.distinct(11))
next case AndR thus ?case using SCc.AndR by (metis diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(13))
next case OrR thus ?case using SCc.OrR by (metis diff_single_trivial diff_union_swap2 formula.distinct(15) insert_iff set_mset_add_mset_insert)
next case ImpL thus ?case using SCc.ImpL by (metis diff_single_trivial diff_union_swap2)
next case ImpR thus ?case using SCc.ImpR by (metis diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(17))
qed (simp_all add: SCc.intros)
  
lemma NotL_inv': "Not F, Γ ⇒ Δ ↓ n ⟹ Γ ⇒ F,Δ  ↓ n"
proof(induction "Not F, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (NotL Γ' G Δ n) thus ?case by(cases "Not F = Not G")
    (auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc)
qed (auto intro!: SCc.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)

lemma AndL_inv': "And F G, Γ ⇒ Δ ↓ n ⟹ F,G,Γ ⇒ Δ ↓ n"
proof(induction "And F G, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (AndL F' G' Γ' Δ) thus ?case 
    by(cases "And F G = And F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       metis add_mset_commute)
qed (auto intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2 inL2')

lemma OrL_inv': 
  assumes "Or F G, Γ ⇒ Δ ↓ n"
  shows "F,Γ ⇒ Δ ↓ n ∧ G,Γ ⇒ Δ ↓ n"
proof(insert assms, induction "Or F G, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (OrL F' Γ' Δ n G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma ImpL_inv': 
  assumes "Imp F G, Γ ⇒ Δ ↓ n"
  shows "Γ ⇒ F,Δ ↓ n ∧ G,Γ ⇒ Δ ↓ n"
proof(insert assms, induction "Imp F G, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (ImpL Γ' F' Δ n G') thus ?case 
    by(cases "Or F G = Or F' G'"; (* oops, I didn't pay attention and used the wrong constructor… doesn't matter! *)
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+
  
lemma ImpR_inv':
  assumes "Γ ⇒ Imp F G,Δ ↓ n"
  shows "F,Γ ⇒ G,Δ ↓ n"
proof(insert assms, induction Γ "Imp F G, Δ" n arbitrary: Δ rule: SCc.induct)
  case (ImpR  F' Γ G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma AndR_inv':
shows "Γ ⇒ And F G, Δ ↓ n ⟹ Γ ⇒ F, Δ ↓ n ∧ Γ ⇒ G, Δ ↓ n"
proof(induction Γ "And F G, Δ" n arbitrary: Δ rule: SCc.induct)
  case (AndR  Γ F' Δ' n G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma OrR_inv': "Γ ⇒ Or F G, Δ ↓ n ⟹ Γ ⇒ F,G,Δ ↓ n"
proof(induction Γ "Or F G, Δ" n arbitrary: Δ rule: SCc.induct)
  case (OrR  Γ F' G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       metis add_mset_commute)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma NotR_inv': "Γ ⇒ Not F, Δ ↓ n ⟹ F,Γ ⇒ Δ ↓ n"
proof(induction Γ "Not F, Δ" n arbitrary: Δ rule: SCc.induct)
  case (NotR  G Γ Δ') thus ?case 
    by(cases "Not F = Not G"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       metis add_mset_commute)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma weakenL': "Γ ⇒ Δ ↓ n ⟹ F,Γ ⇒ Δ  ↓ n"
  by(induction rule: SCc.induct) 
    (auto intro!: SCc.intros(3-) intro: SCc.intros(1,2))

lemma weakenR': "Γ ⇒ Δ  ↓ n ⟹ Γ ⇒ F,Δ  ↓ n"
  by(induction rule: SCc.induct)
    (auto intro!: SCc.intros(3-) intro: SCc.intros(1,2))

lemma contract':
  "(F,F,Γ ⇒ Δ ↓ n ⟶ F,Γ ⇒ Δ ↓ n) ∧ (Γ ⇒ F,F,Δ ↓ n ⟶ Γ ⇒ F,Δ ↓ n)"
proof(induction n arbitrary: F Γ Δ)
  case (Suc n)
  hence IH: "F, F, Γ ⇒ Δ ↓ n ⟹ F, Γ ⇒ Δ ↓ n" "Γ ⇒ F, F, Δ ↓ n ⟹ Γ ⇒ F, Δ ↓ n" for F :: "'a formula" and Γ Δ by blast+
  show ?case proof(intro conjI allI impI, goal_cases)
    case 1
    let ?ffs = "λΓ. Γ - {# F #} - {# F #}"
    from 1 show ?case proof(insert 1; cases rule: SCc.cases[of "F,F,Γ" Δ "Suc n"])
      case (NotL  Γ' G)
      show ?thesis
      proof(cases)
        assume e: "F = ❙¬G"
        with NotL have Γ': "Γ' = ❙¬G, Γ" by simp
        from NotL_inv' NotL(2) have "Γ ⇒ G, G, Δ ↓ n" unfolding Γ' .
        with IH(2) have "Γ ⇒ G, Δ ↓ n" .
        with SCc.NotL show ?thesis unfolding e .
      next
        assume e: "F ≠ ❙¬G"
        have ?thesis
          using NotL(2) IH(1)[of F "?ffs Γ'" "G, Δ"] SCc.NotL[of "F, Γ' - {# F #} - {# F #}" G Δ n]
          using e NotL(1) by (metis (no_types, lifting) insert_DiffM lem2)
        from e NotL(1) have Γ: "Γ = ❙¬ G, ?ffs Γ'" by (meson lem1)
        with NotL(1) have Γ': "F,F,?ffs Γ' = Γ'" by simp
        show ?thesis using NotL(2) IH(1)[of F "?ffs Γ'" "G, Δ"] SCc.NotL[of "F, ?ffs Γ'" G Δ n] ‹F, Γ ⇒ Δ ↓ Suc n› by blast
      qed
    next
      case (AndL G H Γ') show ?thesis proof cases
        assume e: "F = And G H"
        with AndL(1) have Γ': "Γ' = And G H, Γ" by simp
        have "G ❙∧ H, G, H, Γ ⇒ Δ ↓ n" using AndL(2) unfolding Γ' by auto
        hence "G, H, G, H, Γ ⇒ Δ ↓ n" by(rule AndL_inv')
        hence "G, H, Γ ⇒ Δ ↓ n" using IH(1) by (metis inL1' inL3')
        thus "F, Γ ⇒ Δ ↓ Suc n" using e SCc.AndL by simp
      next
        assume ne: "F ≠ And G H"
        with AndL(1) have Γ: "Γ = And G H, ?ffs Γ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "F, F, G, H, ?ffs Γ' ⇒ Δ ↓ n" using AndL(2) using Γ inL4' local.AndL(1) by auto
        hence "G, H, F, ?ffs Γ' ⇒ Δ ↓ n" using IH(1) inL2 by blast
        thus ?thesis using SCc.AndL unfolding Γ using inL1 by blast
      qed
    next
      case (OrL G Γ' H) show ?thesis proof cases
        assume e: "F = Or G H"
        with OrL(1) have Γ': "Γ' = Or G H, Γ" by simp
        have "Or G H, G, Γ ⇒ Δ ↓ n" "Or G H, H, Γ ⇒ Δ ↓ n" using OrL(2,3) unfolding Γ' by simp_all
        hence "G, G, Γ ⇒ Δ ↓ n" "H, H, Γ ⇒ Δ ↓ n" using OrL_inv' by blast+
        hence "G, Γ ⇒ Δ ↓ n" "H, Γ ⇒ Δ ↓ n" using IH(1) by presburger+
        thus "F, Γ ⇒ Δ ↓ Suc n" unfolding e using SCc.OrL by blast
      next
        assume ne: "F ≠ Or G H"
        with OrL(1) have Γ: "Γ = Or G H, ?ffs Γ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "F, F, G, ?ffs Γ' ⇒ Δ ↓ n" "F, F, H,?ffs Γ' ⇒ Δ ↓ n" using OrL Γ by auto
        hence "G, F, ?ffs Γ' ⇒ Δ ↓ n" "H, F, ?ffs Γ' ⇒ Δ ↓ n" using IH(1) by(metis add_mset_commute)+
        thus ?thesis using SCc.OrL unfolding Γ by auto
      qed
    next
      case (ImpL Γ' G H) show ?thesis proof cases
        assume e: "F = Imp G H"
        with ImpL(1) have Γ': "Γ' = Imp G H, Γ" by simp
        have "H, Γ ⇒ Δ ↓ n" "Γ ⇒ G,Δ ↓ n" using IH ImpL_inv' ImpL(2,3) unfolding Γ'
          by (metis add_mset_commute)+
        thus ?thesis unfolding e using SCc.ImpL[where 'a='a] by simp
      next
        assume ne: "F ≠ Imp G H"
        with ImpL(1) have Γ: "Γ = Imp G H, ?ffs Γ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "F, F, ?ffs Γ' ⇒ G, Δ ↓ n" "F, F, H, ?ffs Γ' ⇒ Δ ↓ n" using ImpL Γ by auto
        thus ?thesis using SCc.ImpL IH unfolding Γ by (metis inL1')
      qed
    next
      case ImpR thus ?thesis by (simp add: IH(1) SCc.intros(10) add_mset_commute)
    next
      case (NotR G Δ') thus ?thesis using IH(1) by (simp add: SCc.NotR add_mset_commute)
    qed (auto intro: IH SCc.intros(1,2) intro!: SCc.intros(3-10))
  next
    case 2
    let ?ffs = "λΓ. Γ - {# F #} - {# F #}"
    have not_principal[dest]:
      "⟦F ≠ f G H; F, F, Δ = f G H, Δ'⟧ ⟹ Δ = f G H, ?ffs Δ' ∧ F, F, ?ffs Δ' = Δ'" for f G H Δ' proof(intro conjI, goal_cases)
        case 2
        from 2 have "F ∈# Δ'" by(blast dest: lem1[THEN iffD1])
        then obtain Δ'' where Δ': "Δ' = F,Δ''"  by (metis insert_DiffM)
        with 2(2) have "F, Δ = f G H, Δ''" by(simp add: add_mset_commute)
        hence "F ∈# Δ''" using 2(1) by(blast dest: lem1[THEN iffD1])
        then obtain Δ''' where Δ'': "Δ'' = F,Δ'''" by (metis insert_DiffM)
        show ?case unfolding Δ' Δ'' by simp
        case 1 show ?case using 1(2) unfolding Δ' Δ'' by(simp add: add_mset_commute)
      qed
    have principal[dest]: "F, F, Δ = f G H, Δ' ⟹ F = f G H ⟹ Δ' = f G H, Δ" for f G H Δ' by simp
    from 2 show ?case proof(cases rule: SCc.cases[of Γ "F,F,Δ" "Suc n"])
      case (ImpR G H Δ') thus ?thesis proof cases
        assume e[simp]: "F = Imp G H"
        with ImpR(1) have Δ'[simp]: "Δ' = Imp G H, Δ" by simp
        have "G, Γ ⇒ Imp G H, H, Δ ↓ n" using ImpR(2) by simp
        hence "G, G, Γ ⇒ H, H, Δ ↓ n" by(rule ImpR_inv')
        hence "G, Γ ⇒ H, Δ ↓ n" using IH by fast
        thus "Γ ⇒ F, Δ ↓ Suc n" using SCc.ImpR by simp
      next
        assume a: "F ≠ Imp G H"
        with ImpR(1) have Δ: "Δ = Imp G H, ?ffs Δ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "G,Γ ⇒ F, F, H, ?ffs Δ' ↓ n" using ImpR Δ by fastforce
        thus ?thesis using SCc.ImpR IH unfolding Δ by (metis inR1')
      qed
    next
      case (AndR G Δ' H) thus ?thesis proof(cases "F = And G H")
        case True thus ?thesis using AndR by(auto intro!: SCc.intros(3-) dest!: AndR_inv' intro: IH)
      next
        case False 
        hence e: "Δ = And G H, ?ffs Δ'" using AndR(1) using diff_diff_add lem2 by blast
        hence "G ❙∧ H, F, F, ?ffs Δ' = G ❙∧ H, Δ'" using AndR(1) by simp
        hence "Γ ⇒ F, F, G, ?ffs Δ' ↓ n" "Γ ⇒ F, F, H, ?ffs Δ' ↓ n" using AndR(2,3) using add_left_imp_eq inR2 by fastforce+
        hence "Γ ⇒ G, F, ?ffs Δ' ↓ n" "Γ ⇒ H, F, ?ffs Δ' ↓ n" using IH(2) by blast+
        thus ?thesis unfolding e by(intro SCc.AndR[THEN inR1'])
      qed
    next
    case (OrR G H Δ') thus ?thesis proof cases
      assume a: "F = Or G H" 
      hence Δ': "Δ' = G ❙∨ H, Δ" using OrR(1) by(intro principal)
      hence "Γ ⇒ G, H, G, H, Δ ↓ n" using inR3'[THEN OrR_inv'] OrR(2) by auto
      hence "Γ ⇒ H, G, Δ ↓ n" using IH(2)[of Γ G "H,H,Δ"] IH(2)[of Γ H "G,Δ"]
        unfolding add_ac(3)[of "{#H#}" "{#G#}"] using inR2  by blast
      hence "Γ ⇒ G, H, Δ ↓ n" by(elim SC_swap_applies)
    thus ?thesis unfolding a by (simp add: SCc.OrR)
    next
      assume a: "F ≠ Or G H"
      with not_principal have np: "Δ = G ❙∨ H, ?ffs Δ' ∧ F, F, ?ffs Δ' = Δ'" using OrR(1) .
      with OrR(2) have "Γ ⇒ G, H, F, ?ffs Δ' ↓ n" using IH(2) by (metis inR2' inR4')
      hence "Γ ⇒ F, G ❙∨ H, ?ffs Δ' ↓ Suc n" by(intro SCc.OrR[THEN inR1'])
      thus ?thesis using np by simp
    qed
    next
      case (NotR G Δ') thus ?thesis proof(cases "F = Not G") 
        case True 
        with principal NotR(1) have "Δ' = ❙¬ G, Δ" .
        with NotR_inv' NotR(2) have "G, G, Γ ⇒ Δ ↓ n" by blast
        with IH(1) have "G, Γ ⇒ Δ ↓ n" .
        thus "Γ ⇒ F, Δ ↓ Suc n" unfolding True by(intro SCc.NotR)
      next
        case False 
        with not_principal have np: "Δ = ❙¬ G, Δ' - (F, {#F#}) ∧ F, F, Δ' - (F, {#F#}) = Δ'" using NotR(1) by auto
        hence "G, Γ ⇒ F, F, ?ffs Δ' ↓ n" using NotR(2) by simp
        hence "G, Γ ⇒ F, ?ffs Δ' ↓ n" by(elim IH(2))
        thus ?thesis using np SCc.NotR inR1 by auto
      qed
    next
      case BotL thus ?thesis by(elim SCc.BotL)
    next
      case (Ax k) thus ?thesis by(intro SCc.Ax[where k=k]) simp_all
    next
      case NotL thus ?thesis by (simp add: SCc.NotL Suc.IH add_mset_commute)
    next
      case AndL thus ?thesis using SCc.AndL Suc.IH by blast
    next
      case OrL thus ?thesis using SCc.OrL Suc.IH by blast
    next
      case ImpL thus ?thesis by (metis SCc.ImpL Suc.IH add_mset_commute)
    qed
  qed
qed blast

(* depth for cut? *)
lemma Cut_Atom_depth: "Atom k,Γ ⇒ Δ ↓ n ⟹ Γ ⇒ Atom k,Δ ↓ m ⟹ Γ ⇒ Δ ↓ n + m"
proof(induction "Atom k,Γ" "Δ" n arbitrary: Γ m rule: SCc.induct)
  case (BotL Δ)
  hence "⊥ ∈# Γ" by simp
  thus ?case using SCc.BotL  by auto
next
  case (Ax l Δ)
  show ?case proof cases
    assume "l = k"
    with ‹Atom l ∈# Δ› obtain Δ' where "Δ = Atom k, Δ'" by (meson multi_member_split)
    with ‹Γ ⇒ Atom k, Δ ↓ m› have "Γ ⇒ Δ ↓ m" using contract' by blast
    thus ?thesis by (metis add.commute deeper)
  next
    assume "l ≠ k"
    with ‹Atom l ∈# Atom k, Γ› have "Atom l ∈# Γ" by simp
    with ‹Atom l ∈# Δ› show ?thesis using SCc.Ax[of l] by simp
  qed
next
  case (NotL Γ F Δ)
  obtain Γ' where Γ: "Γ = Not F, Γ'" by (meson NotL.hyps(3) add_eq_conv_ex formula.simps(9))
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.NotL)
    apply(intro NotL.hyps (* IH *))
     subgoal using NotL Γ by (simp add: lem2)
    subgoal using Γ NotL.prems NotL_inv' by blast
  done
next
  case (NotR F Δ)
  then show ?case by(auto intro!: SCc.NotR dest!: NotR_inv')
next
  case (AndL F G Γ Δ)
  obtain Γ' where Γ: "Γ = And F G, Γ'" by (metis AndL.hyps(3) add_eq_conv_diff formula.distinct(5))
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.AndL)
    apply(intro AndL.hyps (* IH *))
     subgoal using AndL Γ by (simp add: lem2)
    subgoal using Γ AndL.prems AndL_inv' by blast
  done
next
  case (AndR F Δ G)
  then show ?case
    using AndR_inv' SCc.AndR by (metis add_Suc inR1')
next
  case (OrL F Γ' Δ n G)
  obtain Γ'' where Γ: "Γ = Or F G, Γ''" by (meson OrL.hyps(5) add_eq_conv_ex formula.simps(13))
  have ihm: "F, Γ' = Atom k, F, Γ''" "G, Γ' = Atom k, G, Γ''" using OrL Γ  by (simp_all add: lem2)
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.OrL OrL.hyps(2)[OF ihm(1)] OrL.hyps(4)[OF ihm(2)])
     subgoal using Γ OrL.prems OrL_inv' by blast
    subgoal using Γ OrL.prems OrL_inv' by blast
  done
next
  case (OrR F G Δ)
  then show ?case by(auto intro!: SCc.intros(3-) dest!: OrR_inv')
next
  case (ImpL Γ' F Δ n G)
  obtain Γ'' where Γ: "Γ = Imp F G, Γ''" by (metis ImpL.hyps(5) add_eq_conv_ex formula.simps)
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.ImpL ImpL.hyps(2) ImpL.hyps(4))
       subgoal using ImpL Γ by (simp add: lem2)
      subgoal using Γ ImpL.prems by(auto dest!: ImpL_inv')
     subgoal using ImpL Γ by (simp add: lem2)
    subgoal using Γ ImpL.prems ImpL_inv' by blast
  done
next
  case (ImpR F G Δ)
  then show ?case by (auto dest!: ImpR_inv' intro!: SCc.ImpR)
qed
primrec cut_bound :: "nat ⇒ nat ⇒ 'a formula ⇒ nat" where
  "cut_bound n m (Atom _) = m + n" |
  "cut_bound n m Bot = n" |
  "cut_bound n m (Not F) = cut_bound m n F" |
  "cut_bound n m (And F G) = cut_bound n (cut_bound n m F) G" |
  "cut_bound n m (Or F G) = cut_bound (cut_bound n m F) m G" |
  "cut_bound n m (Imp F G) = cut_bound (cut_bound m n F) m G"
theorem cut_bound: "Γ ⇒ F,Δ ↓ n ⟹ F,Γ ⇒ Δ  ↓ m ⟹ Γ ⇒ Δ ↓ cut_bound n m F"
proof(induction F arbitrary: Γ Δ n m)
  case (Atom k) thus ?case using Cut_Atom_depth by simp fast
next
  case Bot thus ?case using Bot_delR' by fastforce 
next
  case Not from Not.prems show ?case by(auto dest!: NotL_inv' NotR_inv' intro!: Not.IH elim!: weakenL)
next
  case (And F G) from And.prems show ?case by(auto dest!: AndL_inv' AndR_inv' intro!: And.IH elim!: weakenR' weakenL')
next
  case (Or F G) from Or.prems show ?case by(auto dest: OrL_inv' OrR_inv' intro!: Or.IH elim!:  weakenR' weakenL')
next
  case (Imp F G)
  from ImpR_inv' ‹Γ ⇒ F ❙→ G, Δ ↓ n› have R: "F, Γ ⇒ G, Δ ↓ n" by blast
  from ImpL_inv' ‹F ❙→ G, Γ ⇒ Δ ↓ m› have L: "Γ ⇒ F, Δ ↓ m" "G, Γ ⇒ Δ ↓ m" by blast+
  from L(1) have "Γ ⇒ F, G, Δ ↓ m" using weakenR' by blast
  from Imp.IH(1)[OF this R] have "Γ ⇒ G, Δ ↓ cut_bound m n F" .
  from Imp.IH(2)[OF this L(2)] have "Γ ⇒ Δ ↓ cut_bound (cut_bound m n F) m G" .
  thus "Γ ⇒ Δ ↓ cut_bound n m (F ❙→ G)" by simp
qed
  
context begin
private primrec cut_bound' :: "nat ⇒ 'a formula ⇒ nat" where
  "cut_bound' n (Atom _) = 2*n" |
  "cut_bound' n Bot = n" |
  "cut_bound' n (Not F) = cut_bound' n F" |
  "cut_bound' n (And F G) = cut_bound' (cut_bound' n F) G" |
  "cut_bound' n (Or F G) = cut_bound' (cut_bound' n F) G" |
  "cut_bound' n (Imp F G) = cut_bound' (cut_bound' n F) G"
  
private lemma cut_bound'_mono: "a ≤ b ⟹ cut_bound' a F ≤ cut_bound' b F"
  by(induction F arbitrary: a b; simp)
    
private lemma cut_bound_mono: "a ≤ c ⟹ b ≤ d ⟹ cut_bound a b F ≤ cut_bound c d F"
  by(induction F arbitrary: a b c d; simp)
    
private lemma cut_bound_max: "max n (cut_bound' (max n m) F) = cut_bound' (max n m) F"
  by(induction F arbitrary: n m; simp; metis)
private lemma cut_bound_max': "max n (cut_bound' n F) = cut_bound' n F"
  by(induction F arbitrary: n ; simp; metis max.assoc)
    
private lemma cut_bound_': "cut_bound n m F ≤ cut_bound' (max n m) F"
proof(induction F arbitrary: n m)
  case (Not F)
  then show ?case by simp (metis max.commute)
next
  case (And F1 F2)
  from And.IH(1) have 1: "cut_bound n (cut_bound n m F1) F2 ≤ cut_bound n (cut_bound' (max n m) F1) F2" 
    by(rule cut_bound_mono[OF order.refl])
  also from And.IH(2) have "… ≤ cut_bound' (max n (cut_bound' (max n m) F1)) F2" by simp
  also have "… = cut_bound' (cut_bound' (max n m) F1) F2" by (simp add: cut_bound_max)
  finally show ?case by simp
next
  case (Or F1 F2)
  from Or.IH(1) have 1: "cut_bound (cut_bound n m F1) m F2 ≤ cut_bound (cut_bound' (max n m) F1) m F2" 
    by(rule cut_bound_mono[OF _ order.refl])
  also from Or.IH(2)[of "cut_bound' (max n m) F1"] have "… ≤ cut_bound' (max (cut_bound' (max n m) F1) m) F2" by simp
  also have "… = cut_bound' (cut_bound' (max n m) F1) F2" by (simp add: cut_bound_max max.commute)
  finally show ?case by simp
next
  case (Imp F1 F2)
  from Imp.IH(1) have 1: "cut_bound (cut_bound m n F1) m F2 ≤ cut_bound (cut_bound' (max m n) F1) m F2" 
    by(rule cut_bound_mono[OF _ order.refl])
  also from Imp.IH(2)[of "cut_bound' (max m n) F1"] have "… ≤ cut_bound' (max (cut_bound' (max m n) F1) m) F2" by simp
  also have "… = cut_bound' (cut_bound' (max n m) F1) F2" by (simp add: cut_bound_max max.commute)
  finally show ?case by simp
qed simp_all
    
primrec depth :: "'a formula ⇒ nat" where
  "depth (Atom _) = 0" |
  "depth Bot = 0" |
  "depth (Not F) = Suc (depth F)" |
  "depth (And F G) = Suc (max (depth F) (depth G))" |
  "depth (Or F G) = Suc (max (depth F) (depth G))" |
  "depth (Imp F G) = Suc (max (depth F) (depth G))"
  
private primrec (* primrec works, but fun would give me a nicer induction rule *) cbnd where
  "cbnd k 0 = 2*k" |
  "cbnd k (Suc n) = cbnd (cbnd k n) n"
  
private lemma cbnd_grow: "(k :: nat) ≤ cbnd k d"
  by(induction d arbitrary: k; simp) (insert le_trans, blast)
    
private lemma cbnd_mono: assumes "b ≤ d" shows "cbnd (a::nat) b ≤ cbnd a d"
proof -
  have "cbnd (a::nat) b ≤ cbnd a (b + d)" for b d
    by(induction d arbitrary: a b; simp) (insert le_trans cbnd_grow, blast)
  thus ?thesis using assms using le_Suc_ex by blast
qed

private lemma cut_bound'_cbnd: "cut_bound' n F ≤ cbnd n (depth F)"
proof(induction F arbitrary: n)
next
  case (Not F)
  then show ?case using cbnd_grow dual_order.trans by fastforce
next
  case (And F1 F2)
  let ?md = "max (depth F1) (depth F2)"
  have "cut_bound' (cut_bound' n F1) F2 ≤ cut_bound' (cbnd n (depth F1)) F2" by (simp add: And.IH(1) cut_bound'_mono)
  also have "... ≤ cut_bound' (cbnd n ?md) F2" by (simp add: cbnd_mono cut_bound'_mono)
  also have "... ≤ cbnd (cbnd n ?md) (depth F2)" using And.IH(2) by blast
  also have "... ≤ cbnd (cbnd n ?md) ?md" by (simp add: cbnd_mono)
  finally show ?case by simp
next
  case (Imp F1 F2)
  case (Or F1 F2)
  text‹analogous› (*<*)
  let ?md = "max (depth F1) (depth F2)"
  have "cut_bound' (cut_bound' n F1) F2 ≤ cut_bound' (cbnd n (depth F1)) F2" by (simp add: Or.IH(1) cut_bound'_mono)
  also have "... ≤ cut_bound' (cbnd n ?md) F2" by (simp add: cbnd_mono cut_bound'_mono)
  also have "... ≤ cbnd (cbnd n ?md) (depth F2)" using Or.IH(2) by blast
  also have "... ≤ cbnd (cbnd n ?md) ?md" by (simp add: cbnd_mono)
  finally show ?case by simp
next
  case (Imp F1 F2)
  let ?md = "max (depth F1) (depth F2)"
  have "cut_bound' (cut_bound' n F1) F2 ≤ cut_bound' (cbnd n (depth F1)) F2" by (simp add: Imp.IH(1) cut_bound'_mono)
  also have "... ≤ cut_bound' (cbnd n ?md) F2" by (simp add: cbnd_mono cut_bound'_mono)
  also have "... ≤ cbnd (cbnd n ?md) (depth F2)" using Imp.IH(2) by blast
  also have "... ≤ cbnd (cbnd n ?md) ?md" by (simp add: cbnd_mono)
  finally show ?case by simp
(*>*)
qed simp_all

value "map (cbnd (0::int)) [0,1,2,3,4]"
value "map (cbnd (1::int)) [0,1,2,3,4]" (* int, because that's easier to read… *)
value "map (cbnd (2::int)) [0,1,2,3,4]"
value "map (cbnd (3::int)) [0,1,2,3,4]"
value [nbe] "map (int ∘ (λn. n div 3) ∘ cut_bound 3 3 ∘ (λn. ((λF. And F F) ^^ n) (Atom 0))) [0,1,2,3,4,5,6,7]"
value [nbe] "map (int ∘ (λn. n div 3) ∘ cut_bound' 3 ∘ (λn. ((λF. And F F) ^^ n) (Atom 0))) [0,1,2,3,4]"
(* TODO: hm *)
value [nbe] "map (int ∘ (λn. n div 3) ∘ cut_bound 3 3 ∘ (λn. ((λF. Imp (Or F F) (And F F)) ^^ n) (Atom 0))) [0,1,2]"
value [nbe] "map (int ∘ (λn. n div 3) ∘ cut_bound' 3 ∘ (λn. ((λF. Imp (Or F F) (And F F)) ^^ n) (Atom 0))) [0,1,2]"
(* Hmhm *)
value [nbe] "(λF. And (Or F F) (Or F F)) ^^ 2"

lemma "n + ((n + m) * 2 ^ (size F - Suc 0) + 
      (n + (n + m + (n + m) * 2 ^ (size F - Suc 0))) * 2 ^ (size G - Suc 0))
    ≤ (n + (m :: nat)) * 2 ^ (size F + size G)"
  oops
    (* so the proof below won't work. *)
lemma "cut_bound (n :: nat) m F ≤ (n + m) * (2 ^ (size F - 1) + 1)"
proof(induction F arbitrary: n m)
next
  case (Not F)
  show ?case unfolding cut_bound.simps by(rule le_trans[OF Not]) (simp add: add.commute)
next
  have "1 ≤ size F" for F :: "'a formula" by(cases F; simp)
  case (And F G)
  from And(2) have "cut_bound n (cut_bound n m F) G ≤ (n + (cut_bound n m F)) * (2 ^ (size G - 1) + 1)" by simp
  also from And(1) have "… ≤ (n + (n + m) * (2 ^ (size F - 1) + 1)) * (2 ^ (size G - 1) + 1)" 
    by (meson add_le_cancel_left mult_le_mono1)
  also have "… ≤ (n + m) * (2 ^ (size (F ❙∧ G) - 1) + 1)"
    apply simp
    oops
      
(* Oh! Look: *)
private lemma cbnd_comm: "cbnd (l * k::nat) n = l * cbnd (k::nat) n"
  by(induction n arbitrary: k; simp)

private lemma cbnd_closed: "cbnd (k::nat) n = k * 2 ^ (2 ^ n)"
  by(induction n arbitrary: k;simp add: semiring_normalization_rules(26))
    
theorem cut': assumes "Γ ⇒ F,Δ ↓ n" "F,Γ ⇒ Δ ↓ n" shows "Γ ⇒ Δ ↓ n * 2 ^ (2 ^ depth F)"
proof -
  from cut_bound[OF assms] have c: "Γ ⇒ Δ ↓ cut_bound n n F" .
  have d: "cut_bound n n F ≤ max n n * 2 ^ (2 ^ depth F)" 
    using cut_bound_' cut_bound'_cbnd cbnd_closed by (metis order_trans)
  show ?thesis using c d le_Suc_ex deeper unfolding max.idem by metis
qed
  
end

end