Theory Provenance_Labels

(*  Title:      Provenance_Labels.thy
    Author:     Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz, 2026
    Maintainer: Arthur Freitas Ramos

    Provenance-label instance: labels are sets of natural-number
    assumption indices. Records a sound over-approximation of assumption
    dependencies and the headline provenance-completeness theorem
    equating ordinary derivability with the existence of a
    provenance-labelled derivation whose filtered sub-context still
    derives the conclusion.
*)

theory Provenance_Labels
  imports Label_Algebra
begin

text ‹
This theory instantiates labels by sets of natural-number assumption indices.
Application and pairing combine provenance by union, implication introduction
removes the discharged assumption label, and disjunction elimination records
the analysed disjunction together with the branch dependencies that survive
discharge.
›

type_synonym prov = "nat set"

interpretation provenance: label_structure
  where app = "λ(S::prov) T. S ∪ T"
    and lam = "λ(S::prov) T. T - S"
    and pair = "λ(S::prov) T. S ∪ T"
    and fst_l = "λ(S::prov). S"
    and snd_l = "λ(S::prov). S"
    and abort = "λ(S::prov). S"
    and inl = "λ(S::prov). S"
    and inr = "λ(S::prov). S"
    and cases = "λ(S::prov) (M::prov) (N::prov) (P::prov) (Q::prov).
      S ∪ (N - M) ∪ (Q - P)"
  .

definition provenance_erase_label :: "prov ⇒ unit" where
  "provenance_erase_label S = ()"

definition provenance_lift_label :: "(prov, 'a) lfm list ⇒ 'a fm ⇒ prov" where
  "provenance_lift_label Γ A =
    (SOME S. provenance.lderives Γ (S, A))"

interpretation provenance: label_algebra
  where app = "λ(S::prov) T. S ∪ T"
    and lam = "λ(S::prov) T. T - S"
    and pair = "λ(S::prov) T. S ∪ T"
    and fst_l = "λ(S::prov). S"
    and snd_l = "λ(S::prov). S"
    and abort = "λ(S::prov). S"
    and inl = "λ(S::prov). S"
    and inr = "λ(S::prov). S"
    and cases = "λ(S::prov) (M::prov) (N::prov) (P::prov) (Q::prov).
      S ∪ (N - M) ∪ (Q - P)"
    and lderives = provenance.lderives
    and erase_label = provenance_erase_label
    and lift_label = provenance_lift_label
proof
  fix S :: prov
  show "provenance_erase_label S = ()"
    by (simp add: provenance_erase_label_def)
next
  fix Γ :: "(prov, 'a) lfm list" and x :: "(prov, 'a) lfm"
  assume "provenance.lderives Γ x"
  then show "erase_ctx Γ ⊢ erase_lfm x"
    by (rule provenance.erasure_sound)
next
  fix Γ :: "(prov, 'a) lfm list" and A :: "'a fm"
  assume ordinary: "erase_ctx Γ ⊢ A"
  have "∃S. provenance.lderives Γ (S, A)"
    by (rule provenance.lifting_general[OF ordinary])
  then show "provenance.lderives Γ (provenance_lift_label Γ A, A)"
    unfolding provenance_lift_label_def by (rule someI_ex)
qed

fun indexed :: "nat ⇒ 'a fm list ⇒ (prov × 'a fm) list" where
  "indexed n [] = []"
| "indexed n (A # Γ) = ({n}, A) # indexed (Suc n) Γ"

definition ctx_prov :: "(prov, 'a) lfm list ⇒ prov" where
  "ctx_prov Γ = ⋃(fst ` set Γ)"

lemma ctx_prov_Cons [simp]:
  "ctx_prov ((M, A) # Γ) = M ∪ ctx_prov Γ"
  unfolding ctx_prov_def
  by auto

lemma erase_ctx_indexed [simp]:
  "erase_ctx (indexed n Γ) = Γ"
  by (induction Γ arbitrary: n) auto

lemma finite_ctx_prov_indexed [simp]:
  "finite (ctx_prov (indexed n Γ))"
  by (induction Γ arbitrary: n) (auto simp: ctx_prov_def)

definition filter_indexed_by :: "nat set ⇒ 'a fm list ⇒ 'a fm list" where
  "filter_indexed_by S Γ =
     map snd (filter (λ(i, A). i ∈ S) (zip [0..<length Γ] Γ))"

lemma filter_indexed_by_mono:
  assumes "S ⊆ T"
  shows "set (filter_indexed_by S Γ) ⊆ set (filter_indexed_by T Γ)"
  using assms
  unfolding filter_indexed_by_def
  by auto

lemma filter_indexed_by_subset_ctx:
  shows "set (filter_indexed_by S Γ) ⊆ set Γ"
  unfolding filter_indexed_by_def
  by (auto simp: in_set_zip)

lemma filter_indexed_by_empty [simp]:
  "filter_indexed_by {} Γ = []"
  unfolding filter_indexed_by_def
  by auto

lemma filter_indexed_by_union:
  "set (filter_indexed_by (S ∪ T) Γ) =
    set (filter_indexed_by S Γ) ∪ set (filter_indexed_by T Γ)"
  unfolding filter_indexed_by_def
  by auto

definition filter_labeled_by :: "prov ⇒ (prov × 'a fm) list ⇒ 'a fm list" where
  "filter_labeled_by S Γ =
     map snd (filter (λ(M, A). M ∩ S ≠ {}) Γ)"

definition nonempty_prov_ctx :: "(prov × 'a fm) list ⇒ bool" where
  "nonempty_prov_ctx Γ ⟷ (∀x ∈ set Γ. fst x ≠ {})"

lemma nonempty_prov_ctx_Cons [simp]:
  "nonempty_prov_ctx ((S, A) # Γ) ⟷ S ≠ {} ∧ nonempty_prov_ctx Γ"
  unfolding nonempty_prov_ctx_def
  by auto

lemma nonempty_prov_ctx_indexed [simp]:
  "nonempty_prov_ctx (indexed n Γ)"
  by (induction Γ arbitrary: n) (auto simp: nonempty_prov_ctx_def)

lemma filter_labeled_by_mono:
  assumes "S ⊆ T"
  shows "set (filter_labeled_by S Γ) ⊆ set (filter_labeled_by T Γ)"
  using assms
  unfolding filter_labeled_by_def
  by auto

lemma filter_labeled_by_union_left:
  "set (filter_labeled_by S Γ) ⊆ set (filter_labeled_by (S ∪ T) Γ)"
  by (rule filter_labeled_by_mono) auto

lemma filter_labeled_by_union_right:
  "set (filter_labeled_by T Γ) ⊆ set (filter_labeled_by (S ∪ T) Γ)"
  by (rule filter_labeled_by_mono) auto

lemma ctx_prov_contains_label:
  assumes "(M, A) ∈ set Γ"
  shows "M ⊆ ctx_prov Γ"
  using assms
  unfolding ctx_prov_def
  by auto

lemma filter_labeled_by_minus_fresh:
  assumes "M ∩ ctx_prov Γ = {}"
  shows "set (filter_labeled_by N Γ) ⊆ set (filter_labeled_by (N - M) Γ)"
proof
  fix A
  assume "A ∈ set (filter_labeled_by N Γ)"
  then obtain y where y_in: "y ∈ set Γ"
    and y_used: "(case y of (L, B) ⇒ L ∩ N ≠ {})"
    and y_snd: "snd y = A"
    unfolding filter_labeled_by_def
    by auto
  obtain L B where y: "y = (L, B)"
    by (cases y)
  have in_ctx: "(L, A) ∈ set Γ"
    using y y_in y_snd by auto
  have used: "L ∩ N ≠ {}"
    using y y_used by simp
  have "L ∩ M = {}"
    using assms ctx_prov_contains_label[OF in_ctx] by auto
  with used have "L ∩ (N - M) ≠ {}"
    by auto
  with in_ctx have "(L, A) ∈
      set (filter (λ(K, B). K ∩ (N - M) ≠ {}) Γ)"
    by auto
  then show "A ∈ set (filter_labeled_by (N - M) Γ)"
    unfolding filter_labeled_by_def by force
qed

lemma filter_labeled_by_cons_minus_subset:
  assumes "M ∩ ctx_prov Γ = {}"
  shows "set (filter_labeled_by N ((M, A) # Γ)) ⊆
    set (A # filter_labeled_by (N - M) Γ)"
proof -
  have "set (filter_labeled_by N ((M, A) # Γ)) ⊆
      insert A (set (filter_labeled_by N Γ))"
    unfolding filter_labeled_by_def
    by auto
  also have "… ⊆ set (A # filter_labeled_by (N - M) Γ)"
    using filter_labeled_by_minus_fresh[OF assms] by auto
  finally show ?thesis .
qed

lemma filter_labeled_by_cons_minus_mono_subset:
  assumes "M ∩ ctx_prov Γ = {}" and "N - M ⊆ U"
  shows "set (filter_labeled_by N ((M, A) # Γ)) ⊆
    set (A # filter_labeled_by U Γ)"
proof -
  have "set (filter_labeled_by N ((M, A) # Γ)) ⊆
      set (A # filter_labeled_by (N - M) Γ)"
    using assms(1) by (rule filter_labeled_by_cons_minus_subset)
  moreover have "set (filter_labeled_by (N - M) Γ) ⊆
      set (filter_labeled_by U Γ)"
    using assms(2) by (rule filter_labeled_by_mono)
  ultimately show ?thesis
    by auto
qed

lemma filter_labeled_by_indexed_upt:
  "filter_labeled_by S (indexed n Γ) =
    map snd (filter (λ(i, A). i ∈ S) (zip [n..<n + length Γ] Γ))"
proof (induction Γ arbitrary: n)
  case Nil
  then show ?case
    by (simp add: filter_labeled_by_def)
next
  case (Cons A Γ)
  have upt: "[n..<n + length (A # Γ)] =
      n # [Suc n..<Suc n + length Γ]"
  proof -
    have "[n..<n + length (A # Γ)] = n # [Suc n..<n + length (A # Γ)]"
      by (rule upt_conv_Cons) simp
    also have "… = n # [Suc n..<Suc n + length Γ]"
      by simp
    finally show ?thesis .
  qed
  show ?case
    using Cons.IH[of "Suc n"] upt
    by (auto simp: filter_labeled_by_def)
qed

lemma filter_labeled_by_indexed_0:
  "filter_labeled_by S (indexed 0 Γ) = filter_indexed_by S Γ"
  by (simp add: filter_labeled_by_indexed_upt filter_indexed_by_def)

inductive prov_safe :: "(prov × 'a fm) list ⇒ prov × 'a fm ⇒ bool"
  ("_ ⊢P _" [50, 50] 50)
where
  PAssm:
    "x ∈ set Γ ⟹ Γ ⊢P x"
| PBotE:
    "Γ ⊢P (S, Bot) ⟹ Γ ⊢P (S, A)"
| PImpI:
    "(M, A) # Γ ⊢P (N, B) ⟹
     M ∩ ctx_prov Γ = {} ⟹
     M ≠ {} ⟹
     Γ ⊢P (N - M, Imp A B)"
| PImpE:
    "Γ ⊢P (S, Imp A B) ⟹
     Γ ⊢P (T, A) ⟹
     Γ ⊢P (S ∪ T, B)"
| PConI:
    "Γ ⊢P (S, A) ⟹
     Γ ⊢P (T, B) ⟹
     Γ ⊢P (S ∪ T, Con A B)"
| PConE1:
    "Γ ⊢P (S, Con A B) ⟹ Γ ⊢P (S, A)"
| PConE2:
    "Γ ⊢P (S, Con A B) ⟹ Γ ⊢P (S, B)"
| PDisI1:
    "Γ ⊢P (S, A) ⟹ Γ ⊢P (S, Dis A B)"
| PDisI2:
    "Γ ⊢P (S, B) ⟹ Γ ⊢P (S, Dis A B)"
| PDisE:
    "Γ ⊢P (S, Dis A B) ⟹
     (M, A) # Γ ⊢P (N, C) ⟹
     (P, B) # Γ ⊢P (Q, C) ⟹
     M ∩ ctx_prov Γ = {} ⟹ M ≠ {} ⟹
     P ∩ ctx_prov Γ = {} ⟹ P ≠ {} ⟹
     M ∩ P = {} ⟹
     Γ ⊢P (S ∪ (N - M) ∪ (Q - P), C)"

lemma provenance_labels_in_context:
  assumes "provenance.lderives Γ x"
  shows "fst x ⊆ ctx_prov Γ"
  using assms
  by (induction rule: provenance.lderives.induct) (auto simp: ctx_prov_def)

lemma ctx_prov_indexed_bound:
  assumes "i ∈ ctx_prov (indexed n Γ)"
  shows "i < n + length Γ"
  using assms
proof (induction Γ arbitrary: n i)
  case Nil
  then show ?case
    by (simp add: ctx_prov_def)
next
  case (Cons A Γ)
  then consider "i = n" | "i ∈ ctx_prov (indexed (Suc n) Γ)"
    by (auto simp: ctx_prov_def)
  then show ?case
  proof cases
    case 1
    then show ?thesis
      by simp
  next
    case 2
    then have "i < Suc n + length Γ"
      by (rule Cons.IH)
    then show ?thesis
      by simp
  qed
qed

theorem provenance_overapproximates_dependencies:
  assumes "provenance.lderives (indexed 0 Γ0) (S, A)"
  shows "∀i. i ∈ S ⟶ i < length Γ0"
proof
  fix i
  show "i ∈ S ⟶ i < length Γ0"
  proof
    assume "i ∈ S"
    moreover have "S ⊆ ctx_prov (indexed 0 Γ0)"
      using provenance_labels_in_context[OF assms] by simp
    ultimately have "i ∈ ctx_prov (indexed 0 Γ0)"
      by auto
    then show "i < length Γ0"
      using ctx_prov_indexed_bound[of i 0 Γ0] by simp
  qed
qed

lemma prov_safe_implies_lderives:
  assumes "Γ ⊢P x"
  shows "provenance.lderives Γ x"
  using assms
  by (induction rule: prov_safe.induct)
    (auto intro: provenance.LAssm provenance.LBotE provenance.LImpI
      provenance.LImpE provenance.LConI provenance.LConE1 provenance.LConE2
      provenance.LDisI1 provenance.LDisI2 provenance.LDisE)

lemma provenance_drop_unused_general:
  assumes "Γ ⊢P x" and "nonempty_prov_ctx Γ"
  shows "filter_labeled_by (fst x) Γ ⊢ snd x"
  using assms
proof (induction rule: prov_safe.induct)
  case (PAssm x Γ)
  obtain M A where x: "x = (M, A)"
    by (cases x)
  then have in_ctx: "(M, A) ∈ set Γ"
    using PAssm by simp
  moreover have "M ≠ {}"
    using PAssm x
    unfolding nonempty_prov_ctx_def filter_labeled_by_def
    by auto
  then have "M ∩ M ≠ {}"
    by auto
  ultimately have "(M, A) ∈
      set (filter (λ(L, B). L ∩ M ≠ {}) Γ)"
    by auto
  then have "A ∈ set (filter_labeled_by M Γ)"
    unfolding filter_labeled_by_def by force
  then show ?case
    using x by (auto intro: derives.Assm)
next
  case (PBotE Γ S A)
  then show ?case
    by (auto intro: derives.BotE)
next
  case (PImpI M A Γ N B)
  have ne: "nonempty_prov_ctx ((M, A) # Γ)"
    using PImpI by simp
  have body: "filter_labeled_by N ((M, A) # Γ) ⊢ B"
    using PImpI.IH[OF ne] by simp
  have sub: "set (filter_labeled_by N ((M, A) # Γ)) ⊆
      set (A # filter_labeled_by (N - M) Γ)"
    using PImpI by (intro filter_labeled_by_cons_minus_subset) auto
  have "filter_labeled_by (N - M) Γ ⊢ Imp A B"
  proof (rule derives.ImpI)
    show "A # filter_labeled_by (N - M) Γ ⊢ B"
      by (rule weakening[OF body sub])
  qed
  then show ?case
    by simp
next
  case (PImpE Γ S A B T)
  have imp0: "filter_labeled_by S Γ ⊢ Imp A B"
    using PImpE.IH(1)[OF PImpE.prems] by simp
  have arg0: "filter_labeled_by T Γ ⊢ A"
    using PImpE.IH(2)[OF PImpE.prems] by simp
  have imp: "filter_labeled_by (S ∪ T) Γ ⊢ Imp A B"
    by (rule weakening[OF imp0 filter_labeled_by_union_left])
  have arg: "filter_labeled_by (S ∪ T) Γ ⊢ A"
    by (rule weakening[OF arg0 filter_labeled_by_union_right])
  have "filter_labeled_by (S ∪ T) Γ ⊢ B"
    by (rule derives.ImpE[OF imp arg])
  then show ?case
    by simp
next
  case (PConI Γ S A T B)
  have left0: "filter_labeled_by S Γ ⊢ A"
    using PConI.IH(1)[OF PConI.prems] by simp
  have right0: "filter_labeled_by T Γ ⊢ B"
    using PConI.IH(2)[OF PConI.prems] by simp
  have left: "filter_labeled_by (S ∪ T) Γ ⊢ A"
    by (rule weakening[OF left0 filter_labeled_by_union_left])
  have right: "filter_labeled_by (S ∪ T) Γ ⊢ B"
    by (rule weakening[OF right0 filter_labeled_by_union_right])
  have "filter_labeled_by (S ∪ T) Γ ⊢ Con A B"
    by (rule derives.ConI[OF left right])
  then show ?case
    by simp
next
  case (PConE1 Γ S A B)
  then show ?case
    by (auto intro: derives.ConE1)
next
  case (PConE2 Γ S A B)
  then show ?case
    by (auto intro: derives.ConE2)
next
  case (PDisI1 Γ S A B)
  then show ?case
    by (auto intro: derives.DisI1)
next
  case (PDisI2 Γ S B A)
  then show ?case
    by (auto intro: derives.DisI2)
next
  case (PDisE Γ S A B M N C P Q)
  let ?U = "S ∪ (N - M) ∪ (Q - P)"
  have ne_left: "nonempty_prov_ctx ((M, A) # Γ)"
    using PDisE by simp
  have ne_right: "nonempty_prov_ctx ((P, B) # Γ)"
    using PDisE by simp
  have disj0: "filter_labeled_by S Γ ⊢ Dis A B"
    using PDisE.IH(1)[OF PDisE.prems] by simp
  have left0: "filter_labeled_by N ((M, A) # Γ) ⊢ C"
    using PDisE.IH(2)[OF ne_left] by simp
  have right0: "filter_labeled_by Q ((P, B) # Γ) ⊢ C"
    using PDisE.IH(3)[OF ne_right] by simp
  have disj_sub: "set (filter_labeled_by S Γ) ⊆
      set (filter_labeled_by ?U Γ)"
    by (rule filter_labeled_by_mono) auto
  have disj: "filter_labeled_by ?U Γ ⊢ Dis A B"
    by (rule weakening[OF disj0 disj_sub])
  have left_sub: "set (filter_labeled_by N ((M, A) # Γ)) ⊆
      set (A # filter_labeled_by ?U Γ)"
    using PDisE
    by (intro filter_labeled_by_cons_minus_mono_subset) auto
  have left: "A # filter_labeled_by ?U Γ ⊢ C"
    by (rule weakening[OF left0 left_sub])
  have right_sub: "set (filter_labeled_by Q ((P, B) # Γ)) ⊆
      set (B # filter_labeled_by ?U Γ)"
    using PDisE
    by (intro filter_labeled_by_cons_minus_mono_subset) auto
  have right: "B # filter_labeled_by ?U Γ ⊢ C"
    by (rule weakening[OF right0 right_sub])
  have "filter_labeled_by ?U Γ ⊢ C"
    by (rule derives.DisE[OF disj left right])
  then show ?case
    by simp
qed

theorem provenance_drop_unused:
  assumes "indexed 0 Γ0 ⊢P (S, A)"
  shows "filter_indexed_by S Γ0 ⊢ A"
proof -
  have "filter_labeled_by S (indexed 0 Γ0) ⊢ A"
    using provenance_drop_unused_general[OF assms] by simp
  then show ?thesis
    by (simp add: filter_labeled_by_indexed_0)
qed

lemma fresh_nat:
  assumes "finite F"
  obtains i :: nat where "i ∉ F"
proof -
  have "∃i :: nat. i ∉ F"
    using assms ex_new_if_finite[OF infinite_UNIV_nat] by blast
  then show ?thesis
    using that by blast
qed

lemma fresh_nat2:
  assumes "finite F"
  obtains i j :: nat where "i ∉ F" and "j ∉ F" and "i ≠ j"
proof -
  obtain i where i: "i ∉ F"
    using assms by (rule fresh_nat)
  from assms have "finite (insert i F)"
    by simp
  then obtain j where j: "j ∉ insert i F"
    by (rule fresh_nat)
  from j have "j ∉ F" and "i ≠ j"
    by auto
  with i show ?thesis
    by (rule that)
qed

lemma ordinary_admits_safe_provenance_labeled:
  assumes "Δ ⊢ A"
    and "erase_ctx Γ = Δ"
    and "nonempty_prov_ctx Γ"
    and "finite (ctx_prov Γ)"
  shows "∃S. Γ ⊢P (S, A) ∧ S ⊆ ctx_prov Γ"
  using assms
proof (induction arbitrary: Γ rule: derives.induct)
  case (Assm A Δ)
  then have "A ∈ set (erase_ctx Γ)"
    by simp
  then obtain S where in_ctx: "(S, A) ∈ set Γ"
    by (rule erase_ctx_mem_label)
  have "Γ ⊢P (S, A)"
    using in_ctx by (rule prov_safe.PAssm)
  moreover have "S ⊆ ctx_prov Γ"
    using in_ctx by (rule ctx_prov_contains_label)
  ultimately show ?case
    by blast
next
  case (BotE Δ A)
  then obtain S where deriv: "Γ ⊢P (S, Bot)"
    and sub: "S ⊆ ctx_prov Γ"
    by blast
  have "Γ ⊢P (S, A)"
    by (rule prov_safe.PBotE[OF deriv])
  with sub show ?case
    by blast
next
  case (ImpI A Δ B)
  obtain i where fresh: "i ∉ ctx_prov Γ"
    using ImpI.prems(3) by (rule fresh_nat)
  let ?M = "{i}"
  have erase: "erase_ctx ((?M, A) # Γ) = A # Δ"
    using ImpI.prems(1) by simp
  have nonempty: "nonempty_prov_ctx ((?M, A) # Γ)"
    using ImpI.prems(2) by simp
  have finite: "finite (ctx_prov ((?M, A) # Γ))"
    using ImpI.prems(3) by simp
  obtain N where body: "(?M, A) # Γ ⊢P (N, B)"
    and sub_body: "N ⊆ ctx_prov ((?M, A) # Γ)"
    using ImpI.IH[OF erase nonempty finite] by blast
  have deriv: "Γ ⊢P (N - ?M, Imp A B)"
    by (rule prov_safe.PImpI[OF body]) (use fresh in auto)
  have "N - ?M ⊆ ctx_prov Γ"
    using sub_body fresh by auto
  with deriv show ?case
    by blast
next
  case (ImpE Δ A B)
  obtain S where imp: "Γ ⊢P (S, Imp A B)"
    and sub_imp: "S ⊆ ctx_prov Γ"
    using ImpE.IH(1)[OF ImpE.prems] by blast
  obtain T where arg: "Γ ⊢P (T, A)"
    and sub_arg: "T ⊆ ctx_prov Γ"
    using ImpE.IH(2)[OF ImpE.prems] by blast
  have "Γ ⊢P (S ∪ T, B)"
    by (rule prov_safe.PImpE[OF imp arg])
  moreover have "S ∪ T ⊆ ctx_prov Γ"
    using sub_imp sub_arg by auto
  ultimately show ?case
    by blast
next
  case (ConI Δ A B)
  obtain S where left: "Γ ⊢P (S, A)"
    and sub_left: "S ⊆ ctx_prov Γ"
    using ConI.IH(1)[OF ConI.prems] by blast
  obtain T where right: "Γ ⊢P (T, B)"
    and sub_right: "T ⊆ ctx_prov Γ"
    using ConI.IH(2)[OF ConI.prems] by blast
  have "Γ ⊢P (S ∪ T, Con A B)"
    by (rule prov_safe.PConI[OF left right])
  moreover have "S ∪ T ⊆ ctx_prov Γ"
    using sub_left sub_right by auto
  ultimately show ?case
    by blast
next
  case (ConE1 Δ A B)
  then obtain S where deriv: "Γ ⊢P (S, Con A B)"
    and sub: "S ⊆ ctx_prov Γ"
    by blast
  have "Γ ⊢P (S, A)"
    by (rule prov_safe.PConE1[OF deriv])
  with sub show ?case
    by blast
next
  case (ConE2 Δ A B)
  then obtain S where deriv: "Γ ⊢P (S, Con A B)"
    and sub: "S ⊆ ctx_prov Γ"
    by blast
  have "Γ ⊢P (S, B)"
    by (rule prov_safe.PConE2[OF deriv])
  with sub show ?case
    by blast
next
  case (DisI1 Δ A B)
  then obtain S where deriv: "Γ ⊢P (S, A)"
    and sub: "S ⊆ ctx_prov Γ"
    by blast
  have "Γ ⊢P (S, Dis A B)"
    by (rule prov_safe.PDisI1[OF deriv])
  with sub show ?case
    by blast
next
  case (DisI2 Δ B A)
  then obtain S where deriv: "Γ ⊢P (S, B)"
    and sub: "S ⊆ ctx_prov Γ"
    by blast
  have "Γ ⊢P (S, Dis A B)"
    by (rule prov_safe.PDisI2[OF deriv])
  with sub show ?case
    by blast
next
  case (DisE Δ A B C)
  obtain i j where fresh_i: "i ∉ ctx_prov Γ"
    and fresh_j: "j ∉ ctx_prov Γ"
    and neq: "i ≠ j"
    using DisE.prems(3) by (rule fresh_nat2)
  let ?M = "{i}"
  let ?P = "{j}"
  obtain S where disj: "Γ ⊢P (S, Dis A B)"
    and sub_disj: "S ⊆ ctx_prov Γ"
    using DisE.IH(1)[OF DisE.prems] by blast
  have erase_left: "erase_ctx ((?M, A) # Γ) = A # Δ"
    using DisE.prems(1) by simp
  have nonempty_left: "nonempty_prov_ctx ((?M, A) # Γ)"
    using DisE.prems(2) by simp
  have finite_left: "finite (ctx_prov ((?M, A) # Γ))"
    using DisE.prems(3) by simp
  obtain N where left: "(?M, A) # Γ ⊢P (N, C)"
    and sub_left: "N ⊆ ctx_prov ((?M, A) # Γ)"
    using DisE.IH(2)[OF erase_left nonempty_left finite_left] by blast
  have erase_right: "erase_ctx ((?P, B) # Γ) = B # Δ"
    using DisE.prems(1) by simp
  have nonempty_right: "nonempty_prov_ctx ((?P, B) # Γ)"
    using DisE.prems(2) by simp
  have finite_right: "finite (ctx_prov ((?P, B) # Γ))"
    using DisE.prems(3) by simp
  obtain Q where right: "(?P, B) # Γ ⊢P (Q, C)"
    and sub_right: "Q ⊆ ctx_prov ((?P, B) # Γ)"
    using DisE.IH(3)[OF erase_right nonempty_right finite_right] by blast
  have deriv: "Γ ⊢P (S ∪ (N - ?M) ∪ (Q - ?P), C)"
    by (rule prov_safe.PDisE[OF disj left right]) (use fresh_i fresh_j neq in auto)
  have "S ∪ (N - ?M) ∪ (Q - ?P) ⊆ ctx_prov Γ"
    using sub_disj sub_left sub_right fresh_i fresh_j by auto
  with deriv show ?case
    by blast
qed

theorem ordinary_admits_safe_provenance:
  assumes "Γ ⊢ A"
  shows "∃S. (indexed 0 Γ ⊢P (S, A))
            ∧ S ⊆ {0..<length Γ}
            ∧ set (filter_indexed_by S Γ) ⊆ set Γ"
proof -
  obtain S where deriv: "indexed 0 Γ ⊢P (S, A)"
    and sub_ctx: "S ⊆ ctx_prov (indexed 0 Γ)"
    using ordinary_admits_safe_provenance_labeled[OF assms, of "indexed 0 Γ"]
    by simp blast
  have sub_indices: "S ⊆ {0..<length Γ}"
  proof
    fix i
    assume "i ∈ S"
    then have "i ∈ ctx_prov (indexed 0 Γ)"
      using sub_ctx by auto
    then have "i < length Γ"
      using ctx_prov_indexed_bound[of i 0 Γ] by simp
    then show "i ∈ {0..<length Γ}"
      by simp
  qed
  have "set (filter_indexed_by S Γ) ⊆ set Γ"
    by (rule filter_indexed_by_subset_ctx)
  with deriv sub_indices show ?thesis
    by blast
qed

corollary ordinary_admits_tight_provenance:
  assumes "Γ ⊢ A"
  shows "∃S. (indexed 0 Γ ⊢P (S, A))
            ∧ S ⊆ {0..<length Γ}
            ∧ filter_indexed_by S Γ ⊢ A"
proof -
  obtain S where deriv: "indexed 0 Γ ⊢P (S, A)"
    and sub: "S ⊆ {0..<length Γ}"
    using ordinary_admits_safe_provenance[OF assms] by blast
  have "filter_indexed_by S Γ ⊢ A"
    by (rule provenance_drop_unused[OF deriv])
  with deriv sub show ?thesis
    by blast
qed

theorem provenance_completeness:
  shows "(Γ ⊢ A) ⟷
         (∃S. (indexed 0 Γ ⊢P (S, A)) ∧ filter_indexed_by S Γ ⊢ A)"
proof
  assume "Γ ⊢ A"
  then show "∃S. (indexed 0 Γ ⊢P (S, A)) ∧ filter_indexed_by S Γ ⊢ A"
    using ordinary_admits_tight_provenance by blast
next
  assume "∃S. (indexed 0 Γ ⊢P (S, A)) ∧ filter_indexed_by S Γ ⊢ A"
  then obtain S where deriv: "indexed 0 Γ ⊢P (S, A)"
    by blast
  have "filter_indexed_by S Γ ⊢ A"
    by (rule provenance_drop_unused[OF deriv])
  moreover have "set (filter_indexed_by S Γ) ⊆ set Γ"
    by (rule filter_indexed_by_subset_ctx)
  ultimately show "Γ ⊢ A"
    by (rule weakening)
qed

end