Theory ND_FiniteAssms

theory ND_FiniteAssms
imports ND
begin

lemma ND_finite_assms: "Γ ⊢ F ⟹ ∃Γ'. Γ' ⊆ Γ ∧ finite Γ' ∧ (Γ' ⊢ F)"
proof(induction rule: ND.induct)
  case (Ax F Γ) thus ?case by(intro exI[of _ "{F}"]) (simp add: ND.Ax)
next
  case (AndI Γ F G)
  from AndI.IH obtain Γ1 Γ2
    where "Γ1 ⊆ Γ ∧ finite Γ1 ∧ (Γ1 ⊢ F)"
      and "Γ2 ⊆ Γ ∧ finite Γ2 ∧ (Γ2 ⊢ G)"
    by blast
  then show ?case by(intro exI[where x="Γ1∪Γ2"]) (force elim: Weaken intro!: ND.AndI)
next
  case (CC F Γ)
  from CC.IH obtain Γ' where Γ': "Γ' ⊆ ❙¬ F ▹ Γ ∧ finite Γ' ∧ (Γ' ⊢ ⊥)" ..
  thus ?case proof(cases "Not F ∈ Γ'") text‹case distinction: Did we actually use @{term "❙¬F"}?›
    case False hence "Γ' ⊆ Γ" using Γ' by blast
    with Γ' show ?thesis using BotE by(intro exI[where x="Γ'"]) fast
  next
    case True
    then obtain Γ'' where "Γ' = ❙¬ F▹Γ''" "❙¬ F ∉ Γ''" by (meson Set.set_insert)
    hence "Γ'' ⊆ Γ" "finite Γ''" "❙¬ F▹Γ'' ⊢ ⊥" using Γ' by auto
    thus ?thesis using ND.CC by auto
  qed
next
  case AndE1 thus ?case by(blast dest: ND.AndE1) next
  case AndE2 thus ?case by(blast dest: ND.AndE2)
next
  case OrI1 thus ?case by(blast dest: ND.OrI1) next
  case OrI2 thus ?case by(blast dest: ND.OrI2)
next
  case (OrE Γ F G H)
  from OrE.IH obtain Γ1 Γ2 Γ3
    where IH:
      "Γ1 ⊆ Γ ∧ finite Γ1 ∧ (Γ1 ⊢ F ❙∨ G)"
      "Γ2 ⊆ F ▹ Γ ∧ finite Γ2 ∧ (Γ2 ⊢ H)"
      "Γ3 ⊆ G ▹ Γ ∧ finite Γ3 ∧ (Γ3 ⊢ H)"
    by blast
  let ?w = "Γ1 ∪ (Γ2 - {F}) ∪ (Γ3 - {G})"
  from IH have "?w ⊢ F ❙∨ G" using Weaken[OF _ sup_ge1] by metis moreover
  from IH have "F▹?w ⊢ H" "G▹?w ⊢ H" using Weaken by (metis Un_commute Un_insert_right Un_upper1 Weaken insert_Diff_single)+ ultimately
  have "?w ⊢ H" using ND.OrE by blast
  thus ?case using IH by(intro exI[where x="?w"]) auto
  text‹Clever evasion of the case distinction made for CC.›
next
  case (ImpI F Γ G)
  from ImpI.IH obtain Γ' where "Γ' ⊆ F ▹ Γ ∧ finite Γ' ∧ (Γ' ⊢ G)" ..
  thus ?case by (intro exI[where x="Γ' - {F}"]) (force elim: Weaken intro!: ND.ImpI)
next
  case (ImpE Γ F G)
  from ImpE.IH obtain Γ1 Γ2 where
      "Γ1 ⊆ Γ ∧ finite Γ1 ∧ (Γ1 ⊢ F ❙→ G)"
      "Γ2 ⊆ Γ ∧ finite Γ2 ∧ (Γ2 ⊢ F)"
    by blast
  then show ?case by(intro exI[where x="Γ1 ∪ Γ2"]) (force elim: Weaken intro: ND.ImpE[where F=F])
next
  case (NotE Γ F)
  from NotE.IH obtain Γ1 Γ2 where
      "Γ1 ⊆ Γ ∧ finite Γ1 ∧ (Γ1 ⊢ ❙¬ F)"
      "Γ2 ⊆ Γ ∧ finite Γ2 ∧ (Γ2 ⊢ F)"
    by blast
  then show ?case by(intro exI[where x="Γ1 ∪ Γ2"]) (force elim: Weaken intro: ND.NotE[where F=F])
next
  case (NotI F Γ)
  from NotI.IH obtain Γ' where "Γ' ⊆ F ▹ Γ ∧ finite Γ' ∧ (Γ' ⊢ ⊥)" ..
  thus ?case by(intro exI[where x="Γ' - {F}"]) (force elim: Weaken intro: ND.NotI[where F=F])
qed

text‹We thought that a lemma like this would be necessary for the ND completeness by SC completeness proof
  (this lemma shows that if we made an ND proof, we can always limit ourselves to a finite set of assumptions --
   and thus put all the assumptions into one formula).
That is not the case, since in the completeness proof,
we assume a valid entailment and have to show (the existence of) a derivation.
The author hopes that his misunderstanding can help the reader's understanding.›
corollary ND_no_assms: 
  assumes "Γ ⊢ F"
  obtains Γ' where "set Γ' ⊆ Γ ∧ ({} ⊢ ❙⋀Γ' ❙→ F)"
proof(goal_cases)
  case 1
  from ND_finite_assms[OF assms] obtain Γ' where "Γ'⊆Γ" "finite Γ'" "Γ' ⊢ F" by blast
  from ‹finite Γ'› obtain G where Γ'[simp]: "Γ' = set G"  using finite_list by blast
  with ‹Γ'⊆Γ› have "set G ⊆ Γ" by clarify
  moreover from ‹Γ' ⊢ F› have "{} ⊢ ❙⋀ G ❙→ F" unfolding Γ' AssmBigAnd .
  ultimately show ?case by(intro 1[where Γ'=G] conjI)
qed

end