Theory SC_Depth_Limit

theory SC_Depth_Limit
imports SC_Sema SC_Depth
begin
  
lemma SC_completeness: "⊨ Γ ⇒ Δ ⟹ Γ ⇒ Δ ↓ sequent_cost Γ Δ"
proof(induction "sequent_cost Γ Δ" arbitrary: Γ Δ)
  case 0 hence False by(simp add: sequent_cost_def) thus ?case by clarify
next
  case (Suc n)
  from Suc(3) show ?case
    using SCc.cases[OF Suc.hyps(1)]
oops
text‹Making this proof of completeness go through should be possible,
  but finding the right way to split the cases could get verbose.
The variant with the search procedure is a lot more elegant.›
  

lemma sc_sim_depth:
  assumes "sc Γ A Δ B = {}"
  shows "image_mset Atom (mset A) + mset Γ ⇒ image_mset Atom (mset B) + mset Δ ↓ sum_list (map size (Γ@Δ)) + (if set A ∩ set B = {} then 0 else 1)"
proof -
  have [simp]: "image_mset Atom (mset A) ⇒ image_mset Atom (mset B) ↓ Suc 0" (is ?k) if "set A ∩ set B ≠ {}" for A B 
  proof -
    from that obtain a where "a ∈ set A" "a ∈ set B" by blast
    thus ?k by(force simp: in_image_mset intro: SCc.Ax[where k=a])
  qed
  note SCc.intros(3-)[intro]
  have [elim!]: "Γ ⇒ Δ ↓ n ⟹ n ≤ m ⟹ Γ ⇒ Δ ↓ m" for Γ Δ n m using dec_induct by(fastforce elim!: deeper_suc) (* sledgehammer is flippin' using induction. *)
  from assms show ?thesis
    by(induction Γ A Δ B rule: sc.induct)
      (auto
      simp add: list_sequent_cost_def add.assoc deeper_suc weakenR'
      split: if_splits option.splits)
qed

corollary sc_depth_complete:
  assumes s: "⊨ Γ ⇒ Δ"
  shows "Γ ⇒ Δ ↓ sum_mset (image_mset size (Γ+Δ))"
proof -
  obtain Γ' Δ' where p: "Γ = mset Γ'" "Δ = mset Δ'" by (metis ex_mset)
  with s have sl: "⊨ mset Γ' ⇒ mset Δ'" by simp
  let ?d = "sum_mset (image_mset size (Γ+Δ))"
  have d: "?d = sum_list (map size (Γ'@Δ'))"
    unfolding p by (metis mset_append mset_map sum_mset_sum_list)
  have "mset Γ' ⇒ mset Δ' ↓ ?d"
  proof cases
    assume "sc Γ' [] Δ' [] = {}"
    from sc_sim_depth[OF this] show "mset Γ' ⇒ mset Δ' ↓ ?d" unfolding d by auto
  next
    assume "sc Γ' [] Δ' [] ≠ {}"
    with SC_counterexample have "¬ ⊨ mset Γ' ⇒ mset Δ'" by fastforce
    moreover note s[unfolded p]
    ultimately have False ..
    thus "mset Γ' ⇒ mset Δ' ↓ ?d" ..
  qed
  thus ?thesis unfolding p .
qed

end