Theory LSC

subsection‹Transforming SC proofs into proofs of CNFs›
theory LSC
imports CNF_Formulas SC_Cut
begin

text‹Left handed SC with NNF transformation:›
inductive LSC (‹(_ ⇒⇩n)› [53]) where
― ‹logic:›
Ax: "❙¬(Atom k),Atom k,Γ ⇒⇩n" |
BotL: "⊥,Γ ⇒⇩n" |
AndL: "F,G,Γ ⇒⇩n ⟹ F❙∧G,Γ ⇒⇩n" |               
OrL: "F,Γ ⇒⇩n ⟹ G,Γ ⇒⇩n ⟹ F❙∨G,Γ ⇒⇩n" |
― ‹nnf rules:›
NotOrNNF: "❙¬F,❙¬G,Γ ⇒⇩n ⟹ ❙¬(F❙∨G),Γ ⇒⇩n" |
NotAndNNF: "❙¬F,Γ ⇒⇩n ⟹ ❙¬G,Γ ⇒⇩n ⟹ ❙¬(F❙∧G),Γ ⇒⇩n" |
ImpNNF: "❙¬F,Γ ⇒⇩n ⟹ G,Γ ⇒⇩n ⟹ F❙→G,Γ ⇒⇩n" |
NotImpNNF: "F,❙¬G,Γ ⇒⇩n ⟹ ❙¬(F❙→G),Γ ⇒⇩n" |
NotNotNNF: "F,Γ ⇒⇩n ⟹ ❙¬(❙¬F),Γ ⇒⇩n"
lemmas LSC.intros[intro!]
text‹You can prove that derivability in @{const SCp} is invariant to @{const nnf},
and then transform @{const SCp} to @{const LSC} while assuming NNF.
However, the transformation introduces the trouble of handling the right side of @{const SCp}.
The idea behind this is that handling the transformation is easier when not requiring NNF.›

text‹One downside of the whole approach is that we often need everything to be in NNF. To shorten:›
abbreviation "is_nnf_mset Γ ≡ ∀x ∈ set_mset Γ. is_nnf x"

lemma "Γ ⇒ {#} ⟹ is_nnf_mset Γ ⟹ Γ ⇒⇩n"
proof(induction Γ "{#}::'a formula multiset " rule: SCp.induct)
  case (BotL Γ)
  then obtain Γ' where "Γ = ⊥,Γ'" by(meson multi_member_split)
  thus ?case by auto
next
  case (Ax A Γ) hence False by simp thus ?case ..
  (* this case makes you think that there's something wrong with this proof *)
next
  case (AndL Γ F G) 
  hence IH: "Γ, F, G ⇒⇩n" by force
  thus ?case by auto
next
  case (NotL) thus ?case
  (* this demonstrates it *)
oops

lemma LSC_to_SC:
  shows "Γ ⇒⇩n ⟹ Γ ⇒ {#}"
proof(induction rule: LSC.induct)
qed (auto dest!: NotL_inv intro!: SCp.intros(3-) intro: extended_Ax)

lemma SC_to_LSC:
  assumes "Γ ⇒ Δ"
  shows "Γ + (image_mset Not Δ) ⇒⇩n"
proof -
  have GO[simp]: 
    "NO_MATCH {# B #} F ⟹ (F,S) + T = F, (S+T)" 
    "NO_MATCH {# B #} S ⟹ S + (F,T) = F, (S+T)"
    "NO_MATCH (❙¬H) F ⟹ F,❙¬G,S = ❙¬G,F,S"
    for B S F G H T by simp_all
  from assms show ?thesis
  proof(induction rule: SCp.induct)
    case (BotL Γ)
    then obtain Γ' where "Γ = ⊥,Γ'" by(meson multi_member_split)
    thus ?case by auto
  next
    case (Ax k Γ Δ)
    then obtain Γ' Δ' where "Γ = Atom k, Γ'" "Δ = Atom k, Δ'" by(meson multi_member_split)
    thus ?case using LSC.Ax by simp
  qed auto
qed

corollary SC_LSC: "Γ ⇒ {#} ⟷ Γ ⇒⇩n" using SC_to_LSC LSC_to_SC by fastforce

text‹The nice thing: The NNF-Transformation is even easier to show on the one-sided variant.›
(* part of that is because it is written down in a way that is easier to tackle for the solvers *)
lemma LSC_NNF: "Γ ⇒⇩n ⟹ image_mset nnf Γ ⇒⇩n"
proof(induction rule: LSC.induct) 
  (* auto solved all, but I want to know what's going on. *)
  case (NotOrNNF F G Γ)
  from NotOrNNF.IH have "nnf (❙¬ F), nnf (❙¬ G), image_mset nnf Γ ⇒⇩n" by simp
  with LSC.AndL have "nnf (❙¬ F) ❙∧ nnf (❙¬ G), image_mset nnf Γ ⇒⇩n" .
  thus ?case by simp
next
  case (AndL F G Γ)
  from AndL.IH have "nnf F, nnf G, image_mset nnf Γ ⇒⇩n" by simp
  with LSC.AndL[where 'a='a] have "nnf F ❙∧ nnf G, image_mset nnf Γ ⇒⇩n" by simp
  thus ?case by simp
next  
qed (auto, metis add_mset_commute)

lemma LSC_NNF_back: "image_mset nnf Γ ⇒⇩n ⟹ Γ ⇒⇩n"
proof(induction "image_mset nnf Γ" rule: LSC.induct) 
oops
(* should be possible, but I don't need it. *)

text‹If we got rid of the rules for NNF, we could call it Gentzen-Schütte-calculus. But it turned out that not doing that works quite fine.›
 
text‹If you stare at left-handed Sequent calcului for too long, and they start staring back:
Try imagining that there is a @{term ⊥} on the right hand side.
Also, bear in mind that provability of @{term "Γ ⇒⇩n"} and satisfiability of @{term "Γ"} are opposites here.›

lemma LHCut:
  assumes "F,Γ ⇒⇩n" "❙¬F, Γ ⇒⇩n"
  shows "Γ ⇒⇩n"
using assms
unfolding SC_LSC[symmetric]
using NotL_inv cut by blast

lemma 
 shows LSC_AndL_inv: "F❙∧G,Γ ⇒⇩n ⟹ F,G,Γ ⇒⇩n"
 and   LSC_OrL_inv: "F❙∨G,Γ ⇒⇩n ⟹ F,Γ ⇒⇩n ∧ G,Γ ⇒⇩n"
 using SC_LSC AndL_inv OrL_inv by blast+
lemmas LSC_invs = LSC_AndL_inv LSC_OrL_inv
(* these are actually suitable as dest rules. But the proofs are usually slow, so I'd rather not. *)

(* direct proof is easy here and it saves us the hassle of the nnf-assumption *)
lemma LSC_weaken_set: "Γ ⇒⇩n ⟹ Γ + Θ ⇒⇩n"
  by(induction rule: LSC.induct) (auto simp: add.assoc)
lemma LSC_weaken: "Γ ⇒⇩n ⟹ F,Γ ⇒⇩n"
  using LSC_weaken_set by (metis add_mset_add_single)

lemma LSC_Contract:
  assumes sfp: "F, F, Γ ⇒⇩n"
  shows "F, Γ ⇒⇩n"
  using SC_LSC contractL sfp by blast

lemma cnf:
  shows 
    "F ❙∨ (G ❙∧ H), Γ ⇒⇩n ⟷ (F ❙∨ G) ❙∧ (F ❙∨ H), Γ ⇒⇩n" (is "?l1 ⟷ ?r1")
    "(G ❙∧ H) ❙∨ F, Γ ⇒⇩n ⟷ (G ❙∨ F) ❙∧ (H ❙∨ F), Γ ⇒⇩n" (is "?l2 ⟷ ?r2")
proof -
  have GO(* get out *)[simp]:   
    "F,G,S ⇒⇩n ⟹ G,F,S ⇒⇩n"
    for F G :: "'a formula" and S by (simp add: add_mset_commute)
  have ?r1 if ?l1 proof -
    from ‹?l1›[THEN LSC_invs(2)] have f: "F, Γ ⇒⇩n" "G ❙∧ H, Γ ⇒⇩n" by simp_all
    from this(2)[THEN LSC_invs(1)] have gh: "G, H, Γ ⇒⇩n" by simp
    show ?r1 using f gh by(auto dest!: LSC_invs simp: LSC_weaken)
  qed
  moreover have ?r2 if ?l2 proof -
    from ‹?l2› have f: "F, Γ ⇒⇩n" "G, H, Γ ⇒⇩n" by(auto dest!: LSC_invs)
    thus ?r2  by(auto dest!: LSC_invs simp: LSC_weaken)
  qed
  moreover have ?l1 if ?r1 proof -
    from ‹?r1›[THEN LSC_invs(1)] have *: "F ❙∨ G, F ❙∨ H, Γ ⇒⇩n" by simp
    hence "F, Γ ⇒⇩n" "G, H, Γ ⇒⇩n" by (auto elim!: LSC_Contract dest!: LSC_invs)
    thus ?l1 by(intro LSC.intros)
  qed
  moreover have ?l2 if ?r2 proof -
    from ‹?r2›[THEN LSC_invs(1)] have *: "G ❙∨ F, H ❙∨ F, Γ ⇒⇩n" by simp
    hence "F, Γ ⇒⇩n" "G, H, Γ ⇒⇩n" by(auto elim!: LSC_Contract dest!: LSC_invs)
    thus ?l2 by(intro LSC.intros)
  qed
  ultimately show "?l1 ⟷ ?r1" "?l2 ⟷ ?r2" by argo+
qed

text‹
  Interestingly, the DNF congruences are a lot easier to show, requiring neither weakening nor contraction.
  The reasons are to be sought in the asymmetries between the rules for @{const And} and @{const Or}.
›
lemma dnf:
  shows 
    "F ❙∧ (G ❙∨ H), Γ ⇒⇩n ⟷ (F ❙∧ G) ❙∨ (F ❙∧ H), Γ ⇒⇩n" (is "?t1")
    "(G ❙∨ H) ❙∧ F, Γ ⇒⇩n ⟷ (G ❙∧ F) ❙∨ (H ❙∧ F), Γ ⇒⇩n" (is "?t2")
proof -
    have GO(* get out *)[simp]:
    "F,G,S ⇒⇩n ⟹ G,F,S ⇒⇩n"
    for F G H I J S by(simp_all add: add_mset_commute)
    show ?t1 ?t2 by(auto dest!: LSC_invs)
qed

lemma LSC_sim_Resolution1:
  assumes R: "S ❙∨ T, Γ ⇒⇩n"
  shows "Atom k ❙∨ S, (❙¬(Atom k)) ❙∨ T, Γ ⇒⇩n"
proof -
  from R have r: "T, Γ ⇒⇩n" "S, Γ ⇒⇩n" by(auto dest: LSC_invs)
  show ?thesis proof(rule LHCut[where F="Atom k"])
    have 2: "T, Atom k, Atom k ❙∨ S, Γ ⇒⇩n" using LSC_weaken r(1) by auto
    hence " ❙¬ (Atom k) ❙∨ T, Atom k, Atom k ❙∨ S, Γ ⇒⇩n" by auto
    thus "Atom k, Atom k ❙∨ S, ❙¬ (Atom k) ❙∨ T, Γ ⇒⇩n" 
      by(auto dest!: LSC_invs) (metis add_mset_commute)
  next text‹analogously›(*<*)
    have 2: "S, ❙¬(Atom k), ❙¬(Atom k) ❙∨ T, Γ ⇒⇩n" using LSC_weaken r(2) by auto
    hence "Atom k ❙∨ S, ❙¬ (Atom k), ❙¬ (Atom k) ❙∨ T, Γ ⇒⇩n" using LSC_weaken
      by(auto dest!: LSC_invs) blast
    from this (*>*)
    show "❙¬ (Atom k), Atom k ❙∨ S, ❙¬ (Atom k) ❙∨ T, Γ ⇒⇩n" by simp
  qed
qed

lemma
  LSC_need_it_once_have_many:
  assumes el: "A ∈ set F"
  assumes once: "form_of_lit A ❙∨ disj_of_clause (removeAll A F),Γ ⇒⇩n"
  shows "disj_of_clause F,Γ ⇒⇩n"
using assms
proof(induction F)
  case Nil hence False by simp thus ?case ..
next (* there might be a smarter way to prove this by splitting F into two lists… but nah. *)
  case (Cons f F) 
  thus ?case proof(cases "A = f")
    case True
    with Cons.prems have ihm: "form_of_lit A ❙∨ disj_of_clause (removeAll A F), Γ ⇒⇩n" by simp
    with True have split: "form_of_lit f, Γ ⇒⇩n" "disj_of_clause (removeAll A F), Γ ⇒⇩n" 
      by (auto dest!: LSC_invs(2))
    from Cons.IH[OF _ ihm] have "A ∈ set F ⟹ disj_of_clause F, Γ ⇒⇩n" .
    with split(2) have "disj_of_clause F, Γ ⇒⇩n" by(cases "A ∈ set F") simp_all
    with split(1) show ?thesis by auto
  next
    case False
    with Cons.prems(2) have prem: "form_of_lit A, Γ ⇒⇩n" "form_of_lit f, Γ ⇒⇩n" "disj_of_clause (removeAll A F), Γ ⇒⇩n" 
       by (auto dest!: LSC_invs(2))
    hence d: "form_of_lit A ❙∨ disj_of_clause (removeAll A F), Γ ⇒⇩n" by blast
    from False Cons.prems have el: "A ∈ set F"  by simp
    from Cons.IH[OF el d] have "disj_of_clause F, Γ ⇒⇩n" .
    with prem(2) show ?thesis by auto
 qed
qed

(* LSC_sim_Resolution1 is the naive summer child that requires everything to be in the right order. Here comes the real fun *)
lemma LSC_Sim_resolution_la:
  fixes k :: 'a
  assumes R: "disj_of_clause (removeAll (k⇧+) F @ removeAll (k¯) G), Γ ⇒⇩n"
  assumes el: "k⇧+ ∈ set F" "k¯ ∈ set G"
  shows "disj_of_clause F, disj_of_clause G, Γ ⇒⇩n"
proof -
  have LSC_or_assoc: "(F ❙∨ G) ❙∨ H, Γ ⇒⇩n ⟷ F ❙∨ (G ❙∨ H), Γ ⇒⇩n" if "is_nnf F" "is_nnf G" "is_nnf H" for F G H
    using that by(auto dest!: LSC_invs(2))
  have dd: "disj_of_clause (F @ G), Γ ⇒⇩n ⟹ disj_of_clause F ❙∨ disj_of_clause G, Γ ⇒⇩n" for F G
    by(induction F) (auto dest!: LSC_invs(2) simp add: LSC_or_assoc)
  from LSC_sim_Resolution1[OF dd[OF R]]
  have unord: "Atom k ❙∨ disj_of_clause (removeAll (k⇧+) F), ❙¬ (Atom k) ❙∨ disj_of_clause (removeAll (k¯) G), Γ ⇒⇩n" .
  show ?thesis
    using LSC_need_it_once_have_many[OF el(1)] LSC_need_it_once_have_many[OF el(2)] unord
    by(simp add: add_mset_commute del: sc_insertion_ordering)
qed

lemma two_list_induct[case_names Nil Cons]: "P [] [] ⟹ (⋀a S T. P S T ⟹ P (a # S) T &&& P S (a # T)) ⟹ P S T"
  apply(induction S)
   apply(induction T)
    apply(simp_all)
done

lemma distrib1: "⟦F, Γ ⇒⇩n; image_mset disj_of_clause (mset G) + Γ ⇒⇩n⟧
    ⟹ mset (map (λd. F ❙∨ disj_of_clause d) G) + Γ ⇒⇩n"
(* surprisingly, the proof having a ❙∧ instead of the ❙∨ looks very similar. Yes, I mistook the two at some point… and downstream, where this is used, I only had to do a few text replacements. makes you really wonder whether what you're proving is meaningful. *)
proof(induction G arbitrary: Γ)
  have GO(* get out *)[simp]:
   "NO_MATCH ({#I❙∨J#}) H ⟹ H+{#F❙∨G#}+S = F❙∨G,H+S"
   for F G H S I J by(simp_all add: add_mset_commute)
  case (Cons g G)
  from ‹F, Γ ⇒⇩n› have 1: "F, disj_of_clause g, Γ ⇒⇩n" by (metis LSC_weaken add_mset_commute)
  from ‹image_mset disj_of_clause (mset (g # G)) + Γ ⇒⇩n› 
  have 2: "image_mset disj_of_clause (mset G) + (disj_of_clause g, Γ) ⇒⇩n" by(simp add: add_mset_commute)
  from Cons.IH[OF 1 2] have IH: "disj_of_clause g, mset (map (λd. F ❙∨ disj_of_clause d) G) + Γ ⇒⇩n" 
    by(simp add: add_mset_commute)
  from ‹F, Γ ⇒⇩n› have 3: "F, mset (map (λd. F ❙∨ disj_of_clause d) G) + Γ ⇒⇩n"
    using LSC_weaken_set by (metis add.assoc add.commute add_mset_add_single)
  from IH 3 show ?case by auto
qed simp

lemma mset_concat_map_cons:
  "mset (concat (map (λc. F c # G c) S)) = mset (map F S) + mset (concat (map G S))"
by(induction S; simp add: add_mset_commute)

lemma distrib: "
  image_mset disj_of_clause (mset F) + Γ ⇒⇩n ⟹ 
  image_mset disj_of_clause (mset G) + Γ ⇒⇩n ⟹
  mset [disj_of_clause c ❙∨ disj_of_clause d. c ← F, d ← G] + Γ ⇒⇩n"
proof(induction F G arbitrary: Γ rule: two_list_induct)
  case (Cons a F G)
  case 1
  from ‹image_mset disj_of_clause (mset (a # F)) + Γ ⇒⇩n›
  have a: "disj_of_clause a, image_mset disj_of_clause (mset F) + Γ ⇒⇩n" by(simp add: add_mset_commute)
  from ‹image_mset disj_of_clause (mset G) + Γ ⇒⇩n›
  have b: "image_mset disj_of_clause (mset G) + (image_mset disj_of_clause (mset F) + Γ) ⇒⇩n"
   and c: "image_mset disj_of_clause (mset G) + (mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) G) + Γ) ⇒⇩n"
    using LSC_weaken_set by (metis add.commute union_assoc)+
  from distrib1[OF a b]
  have "image_mset disj_of_clause (mset F) + (mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) G) + Γ) ⇒⇩n" 
    by (simp add: union_lcomm)
  from Cons[OF this c]
  have "mset (concat (map (λc. map (λd. disj_of_clause c ❙∨ disj_of_clause d) G) F)) +
  (mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) G) + Γ) ⇒⇩n" .
  thus ?case by(simp add: add.commute union_assoc)
next
  case (Cons a F G) case 2 text‹Just the whole thing again, with slightly more mset magic and swapping things around.›
  from ‹image_mset disj_of_clause (mset (a # G)) + Γ ⇒⇩n›
  have a: "disj_of_clause a, image_mset disj_of_clause (mset G) + Γ ⇒⇩n" by(simp add: add_mset_commute)
  from ‹image_mset disj_of_clause (mset F) + Γ ⇒⇩n›
  have b: "image_mset disj_of_clause (mset F) + (image_mset disj_of_clause (mset G) + Γ) ⇒⇩n"
   and c: "image_mset disj_of_clause (mset F) + (mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) F) + Γ) ⇒⇩n"
    using LSC_weaken_set by (metis add.commute union_assoc)+
  have list_commute: "(mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) F) + Γ) ⇒⇩n =
  (mset (map (λd. disj_of_clause d ❙∨ disj_of_clause a) F) + Γ) ⇒⇩n" for Γ
  proof(induction F arbitrary: Γ) (* meh, I should have only prooved one direction, would have been easier *)
    case (Cons f F) 
    have "mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) (f # F)) + Γ ⇒⇩n =
      disj_of_clause a ❙∨ disj_of_clause f, mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) F) + Γ ⇒⇩n" by(simp add: add_mset_commute)
    also have "… = disj_of_clause f ❙∨ disj_of_clause a, mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) F) + Γ ⇒⇩n"
      by(auto dest!: LSC_invs)
    also have "… = mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) F) + (disj_of_clause f ❙∨ disj_of_clause a, Γ) ⇒⇩n" by (simp add: add_mset_commute)
    also have "… = mset (map (λd. disj_of_clause d ❙∨ disj_of_clause a) F) + (disj_of_clause f ❙∨ disj_of_clause a, Γ) ⇒⇩n" using Cons.IH
      by (metis disj_of_clause_is_nnf insert_iff is_nnf.simps(3) set_mset_add_mset_insert)
      (* this was the step that shows why I'm doing this *)
    finally show ?case by simp
  qed simp
  from distrib1[OF a b]
  have "image_mset disj_of_clause (mset G) + (mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) F) + Γ) ⇒⇩n"
    by(auto simp add: add.left_commute)
  from Cons[OF c this ]
  have "mset (concat (map (λc. map (λd. disj_of_clause c ❙∨ disj_of_clause d) G) F)) +
  (mset (map (λd. disj_of_clause a ❙∨ disj_of_clause d) F) + Γ) ⇒⇩n" .
  thus ?case using list_commute by (simp add: mset_concat_map_cons add.assoc add.left_commute)
qed simp

lemma LSC_BigAndL: "mset F + Γ ⇒⇩n ⟹ ❙⋀F, Γ ⇒⇩n"
  by(induction F arbitrary: Γ; simp add: LSC_weaken) (metis LSC.AndL add_mset_commute union_mset_add_mset_right)
lemma LSC_Top_unused: "⟦Γ ⇒⇩n; is_nnf_mset Γ⟧ ⟹ Γ - {#❙¬ ⊥#} ⇒⇩n"
proof(induction rule: LSC.induct)
  case Ax thus ?case by (metis LSC.Ax add.commute diff_union_swap formula.distinct(1,3) formula.inject(2))
next
 case BotL thus ?case by (metis LSC.BotL add.commute diff_union_swap formula.distinct(11))
next
  case (AndL F G Γ)
  hence "(F, G, Γ) - {#❙¬ ⊥#} ⇒⇩n" by simp_all
  hence "F ❙∧ G, Γ - {#❙¬ ⊥#} ⇒⇩n"
    by (metis AndL.hyps LSC.AndL diff_single_trivial diff_union_swap2)
  thus ?case by (metis add.commute diff_union_swap formula.distinct(19))
next
  case (OrL F Γ G)
  hence "(F, Γ) - {#❙¬ ⊥#} ⇒⇩n" "(G, Γ) - {#❙¬ ⊥#} ⇒⇩n" by simp_all
  hence "F ❙∨ G, Γ - {#❙¬ ⊥#} ⇒⇩n" by (metis LSC.OrL OrL.hyps(1) OrL.hyps(2) diff_single_trivial diff_union_swap2)
  thus ?case by (metis diff_union_swap formula.distinct(21))
qed auto

lemma LSC_BigAndL_inv: "❙⋀F, Γ ⇒⇩n ⟹ ∀f ∈ set F. is_nnf f ⟹ is_nnf_mset Γ ⟹ mset F + Γ ⇒⇩n"
proof(induction F arbitrary: Γ)
  case Nil
  then show ?case using LSC_Top_unused by fastforce
next
  case (Cons a F)
  hence "❙⋀F, a, Γ ⇒⇩n" by(auto dest: LSC_invs simp: add_mset_commute)
  with Cons have "mset F + (a, Γ) ⇒⇩n" by fastforce
  then show ?case by simp
qed

lemma LSC_reassociate_Ands: "{#disj_of_clause c ❙∨ disj_of_clause d. (c, d) ∈# C#} + Γ ⇒⇩n ⟹
   is_nnf_mset Γ ⟹
  {#disj_of_clause (c @ d). (c, d) ∈# C#} + Γ ⇒⇩n"
proof(induction C arbitrary: Γ)
  case (add x C)
  obtain a b where [simp]: "x = (a, b)" by(cases x)
  from add.prems have a: "(disj_of_clause a ❙∨ disj_of_clause b), {#disj_of_clause c ❙∨ disj_of_clause d. (c, d) ∈# C#} + Γ ⇒⇩n" by(simp add: add_mset_commute)
  hence "(disj_of_clause (a@b)), {#disj_of_clause c ❙∨ disj_of_clause d. (c, d) ∈# C#} + Γ ⇒⇩n" proof -
    have pn: "is_nnf_mset ({#disj_of_clause c ❙∨ disj_of_clause d. (c, d) ∈# C#} + Γ)"
      using ‹is_nnf_mset Γ› by auto
    have "disj_of_clause a ❙∨ disj_of_clause b, Γ ⇒⇩n ⟹ is_nnf_mset Γ ⟹ disj_of_clause (a @ b), Γ ⇒⇩n" for Γ
      by(induction a) (auto dest!: LSC_invs)
    from this[OF _ pn] a show ?thesis .
  qed
  hence "{#disj_of_clause c ❙∨ disj_of_clause d. (c, d) ∈# C#} + ((disj_of_clause (a@b)),Γ) ⇒⇩n" by(simp add: add_mset_commute)
  with add.IH have "{#disj_of_clause (c @ d). (c, d) ∈# C#} + (disj_of_clause (a @ b), Γ) ⇒⇩n"
    using ‹is_nnf_mset Γ› by fastforce
  thus ?case by(simp add: add_mset_commute)
qed simp

lemma LSC_cnf: "Γ ⇒⇩n ⟹ is_nnf_mset Γ ⟹ image_mset cnf_form_of Γ ⇒⇩n"
proof(induction "Γ" rule: LSC.induct)
  have [simp]: "NO_MATCH (And I J) F ⟹ NO_MATCH (❙¬⊥) F ⟹ F,❙¬⊥,Γ = ❙¬⊥,F,Γ" for F I J Γ by simp
  have [intro!]: "Γ ⇒⇩n ⟹ ❙¬⊥, Γ ⇒⇩n" for Γ by (simp add: LSC_weaken)
  case Ax thus ?case by(auto simp: cnf_form_of_defs)
next
  case BotL show ?case by(auto simp: cnf_form_of_defs)
next
  have GO[simp]:
    "NO_MATCH ({#❙⋀I#}) F ⟹ F + (❙⋀G, S) = ❙⋀G, (F + S)" 
    for F G H S I J a b by(simp_all add: add_mset_commute)
  case (AndL F G Γ) thus ?case
  by(auto dest!: LSC_BigAndL_inv intro!: LSC_BigAndL simp add: cnf_form_of_defs) (simp add: add_ac)
next
  case (OrL F Γ G)
  have 2: "image_mset disj_of_clause (mset (concat (map (λf. map ((@) f) (cnf_lists G)) (cnf_lists F)))) + Γ ⇒⇩n"
    if pig: "is_nnf_mset Γ" and a:
      "mset (concat (map (λc. map (λd. disj_of_clause c ❙∨ disj_of_clause d) (cnf_lists G)) (cnf_lists F))) + Γ ⇒⇩n"
    (* just some nasty modification of the conjunction *) for Γ
  proof - 
    note cms[simp] = mset_map[symmetric] map_concat comp_def
    from a have "image_mset (λ(c,d). disj_of_clause c ❙∨ disj_of_clause d) (
      mset (concat (map (λc. map (λd. (c,d)) (cnf_lists G)) (cnf_lists F)))) + Γ ⇒⇩n" by simp
    hence "image_mset (λ(c,d). disj_of_clause (c@d)) (
      mset (concat (map (λc. map (λd. (c,d)) (cnf_lists G)) (cnf_lists F)))) + Γ ⇒⇩n" 
      using LSC_reassociate_Ands pig by blast
    thus ?thesis by simp
  qed
  have 1: "⟦❙⋀ (map disj_of_clause (cnf_lists F)), Γ ⇒⇩n; ❙⋀ (map disj_of_clause (cnf_lists G)), Γ ⇒⇩n⟧
    ⟹ is_nnf_mset Γ
    ⟹ ❙⋀ (map disj_of_clause (concat (map (λf. map ((@) f) (cnf_lists G)) (cnf_lists F)))), Γ ⇒⇩n" 
    (* the actual disjunction is happening here *)
      for Γ using distrib[where 'a='a] 2 by(auto dest!: LSC_BigAndL_inv intro!: LSC_BigAndL)
  from OrL show ?case
    by(auto elim!: 1 simp add: cnf_form_of_def form_of_cnf_def)
qed auto

end