Theory Lifting_to_Non_Ground_Calculi

(*  Title:       Lifting to Non-Ground Calculi
 *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)

section ‹Lifting to Non-ground Calculi›

text ‹The section 3.1 to 3.3 of the report are covered by the current section.
  Various forms of lifting are proven correct. These allow to obtain the dynamic
  refutational completeness of a non-ground calculus from the static refutational
  completeness of its ground counterpart.›

theory Lifting_to_Non_Ground_Calculi
  imports
    Intersection_Calculus
    Calculus_Variations
begin


subsection ‹Standard Lifting›

locale standard_lifting = inference_system Inf_F +
  ground: calculus Bot_G Inf_G entails_G Red_I_G Red_F_G
  for
    Inf_F :: ‹'f inference set› and
    Bot_G :: ‹'g set› and
    Inf_G ::  ‹'g inference set› and
    entails_G ::  ‹'g set ⇒ 'g set ⇒ bool› (infix ‹⊨G› 50) and
    Red_I_G :: ‹'g set ⇒ 'g inference set› and
    Red_F_G :: ‹'g set ⇒ 'g set›
  + fixes
    Bot_F :: ‹'f set› and
    𝒢_F :: ‹'f ⇒ 'g set› and
    𝒢_I :: ‹'f inference ⇒ 'g inference set option›
  assumes
    Bot_F_not_empty: "Bot_F ≠ {}" and
    Bot_map_not_empty: ‹B ∈ Bot_F ⟹ 𝒢_F B ≠ {}› and
    Bot_map: ‹B ∈ Bot_F ⟹ 𝒢_F B ⊆ Bot_G› and
    Bot_cond: ‹𝒢_F C ∩ Bot_G ≠ {} ⟶ C ∈ Bot_F› and
    inf_map: ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Red_I_G (𝒢_F (concl_of ι))›
begin

abbreviation 𝒢_Fset :: ‹'f set ⇒ 'g set› where
  ‹𝒢_Fset N ≡ ⋃ (𝒢_F ` N)›

lemma 𝒢_subset: ‹N1 ⊆ N2 ⟹ 𝒢_Fset N1 ⊆ 𝒢_Fset N2› by auto

abbreviation entails_𝒢  :: ‹'f set ⇒ 'f set ⇒ bool› (infix ‹⊨𝒢› 50) where
  ‹N1 ⊨𝒢 N2 ≡ 𝒢_Fset N1 ⊨G 𝒢_Fset N2›

lemma subs_Bot_G_entails:
  assumes
    not_empty: ‹sB ≠ {}› and
    in_bot: ‹sB ⊆ Bot_G›
  shows ‹sB ⊨G N›
proof -
  have ‹∃B. B ∈ sB› using not_empty by auto
  then obtain B where B_in: ‹B ∈ sB› by auto
  then have r_trans: ‹{B} ⊨G N› using ground.bot_entails_all in_bot by auto
  have l_trans: ‹sB ⊨G {B}› using B_in ground.subset_entailed by auto
  then show ?thesis using r_trans ground.entails_trans[of sB "{B}"] by auto
qed

(* lem:derived-consequence-relation *)
sublocale consequence_relation Bot_F entails_𝒢
proof
  show "Bot_F ≠ {}" using Bot_F_not_empty .
next
  show ‹B∈Bot_F ⟹ {B} ⊨𝒢 N› for B N
  proof -
    assume ‹B ∈ Bot_F›
    then show ‹{B} ⊨𝒢 N›
      using Bot_map ground.bot_entails_all[of _ "𝒢_Fset N"] subs_Bot_G_entails Bot_map_not_empty
      by auto
  qed
next
  fix N1 N2 :: ‹'f set›
  assume
    ‹N2 ⊆ N1›
  then show ‹N1 ⊨𝒢 N2› using 𝒢_subset ground.subset_entailed by auto
next
  fix N1 N2
  assume
    N1_entails_C: ‹∀C ∈ N2. N1 ⊨𝒢 {C}›
  show ‹N1 ⊨𝒢 N2› using ground.all_formulas_entailed N1_entails_C
    by (simp add: ground.entail_unions)
next
  fix N1 N2 N3
  assume
    ‹N1 ⊨𝒢 N2› and ‹N2 ⊨𝒢 N3›
  then show ‹N1 ⊨𝒢 N3› using ground.entails_trans by blast
qed

definition Red_I_𝒢 :: "'f set ⇒ 'f inference set" where
  ‹Red_I_𝒢 N = {ι ∈ Inf_F. (𝒢_I ι ≠ None ∧ the (𝒢_I ι) ⊆ Red_I_G (𝒢_Fset N))
  ∨ (𝒢_I ι = None ∧ 𝒢_F (concl_of ι) ⊆ 𝒢_Fset N ∪ Red_F_G (𝒢_Fset N))}›

definition Red_F_𝒢 :: "'f set ⇒ 'f set" where
  ‹Red_F_𝒢 N = {C. ∀D ∈ 𝒢_F C. D ∈ Red_F_G (𝒢_Fset N)}›
end

subsection ‹Strong Standard Lifting›

(* rmk:strong-standard-lifting *)
locale strong_standard_lifting = inference_system Inf_F +
  ground: calculus Bot_G Inf_G entails_G Red_I_G Red_F_G
  for
    Inf_F :: ‹'f inference set› and
    Bot_G :: ‹'g set› and
    Inf_G ::  ‹'g inference set› and
    entails_G ::  ‹'g set  ⇒ 'g set  ⇒ bool› (infix ‹⊨G› 50) and
    Red_I_G :: ‹'g set ⇒ 'g inference set› and
    Red_F_G :: ‹'g set ⇒ 'g set›
  + fixes
    Bot_F :: ‹'f set› and
    𝒢_F :: ‹'f ⇒ 'g set› and
    𝒢_I :: ‹'f inference ⇒ 'g inference set option›
  assumes
    Bot_F_not_empty: "Bot_F ≠ {}" and
    Bot_map_not_empty: ‹B ∈ Bot_F ⟹ 𝒢_F B ≠ {}› and
    Bot_map: ‹B ∈ Bot_F ⟹ 𝒢_F B ⊆ Bot_G› and
    Bot_cond: ‹𝒢_F C ∩ Bot_G ≠ {} ⟶ C ∈ Bot_F› and
    strong_inf_map: ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ concl_of ` (the (𝒢_I ι)) ⊆ (𝒢_F (concl_of ι))› and
    inf_map_in_Inf: ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Inf_G›
begin

sublocale standard_lifting Inf_F Bot_G Inf_G "(⊨G)" Red_I_G Red_F_G Bot_F 𝒢_F 𝒢_I
proof
  show "Bot_F ≠ {}" using Bot_F_not_empty .
next
  fix B
  assume b_in: "B ∈ Bot_F"
  show "𝒢_F B ≠ {}" using Bot_map_not_empty[OF b_in] .
next
  fix B
  assume b_in: "B ∈ Bot_F"
  show "𝒢_F B ⊆ Bot_G" using Bot_map[OF b_in] .
next
  show "⋀C. 𝒢_F C ∩ Bot_G ≠ {} ⟶ C ∈ Bot_F" using Bot_cond .
next
  fix ι
  assume i_in: "ι ∈ Inf_F" and
    some_g: "𝒢_I ι ≠ None"
  show "the (𝒢_I ι) ⊆ Red_I_G (𝒢_F (concl_of ι))"
  proof
    fix ιG
    assume ig_in1: "ιG ∈ the (𝒢_I ι)"
    then have ig_in2: "ιG ∈ Inf_G" using inf_map_in_Inf[OF i_in some_g] by blast
    show "ιG ∈ Red_I_G (𝒢_F (concl_of ι))"
      using strong_inf_map[OF i_in some_g] ground.Red_I_of_Inf_to_N[OF ig_in2]
        ig_in1 by blast
  qed
qed

end
  

subsection ‹Lifting with a Family of Tiebreaker Orderings›

locale tiebreaker_lifting =
  empty_ord?: standard_lifting Inf_F Bot_G Inf_G entails_G Red_I_G Red_F_G Bot_F 𝒢_F 𝒢_I
  for
    Bot_F :: ‹'f set› and
    Inf_F :: ‹'f inference set› and
    Bot_G :: ‹'g set› and
    entails_G :: ‹'g set ⇒ 'g set ⇒ bool› (infix ‹⊨G› 50) and
    Inf_G :: ‹'g inference set› and
    Red_I_G :: ‹'g set ⇒ 'g inference set› and
    Red_F_G :: ‹'g set ⇒ 'g set› and
    𝒢_F :: "'f ⇒ 'g set" and
    𝒢_I :: "'f inference ⇒ 'g inference set option"
  + fixes
    Prec_F_g :: ‹'g ⇒ 'f ⇒ 'f ⇒ bool›
  assumes
    all_wf: "wfp (Prec_F_g g)" "transp (Prec_F_g g)"
begin

definition Red_F_𝒢 :: "'f set ⇒ 'f set" where
  ‹Red_F_𝒢 N = {C. ∀D ∈ 𝒢_F C. D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E ∈ N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)}›

lemma Prec_trans:
  assumes
    ‹Prec_F_g D A B› and
    ‹Prec_F_g D B C›
  shows
    ‹Prec_F_g D A C›
  using assms all_wf 
  unfolding transp_on_def
  by blast

lemma prop_nested_in_set: "D ∈ P C ⟹ C ∈ {C. ∀D ∈ P C. A D ∨ B C D} ⟹ A D ∨ B C D"
  by blast

(* lem:wolog-C'-nonredundant *)
lemma Red_F_𝒢_equiv_def:
  ‹Red_F_𝒢 N = {C. ∀Di ∈ 𝒢_F C. Di ∈ Red_F_G (𝒢_Fset N) ∨
    (∃E ∈ (N - Red_F_𝒢 N). Prec_F_g Di E C ∧ Di ∈ 𝒢_F E)}›
proof (rule; clarsimp)
  fix C D
  assume
    C_in: ‹C ∈ Red_F_𝒢 N› and
    D_in: ‹D ∈ 𝒢_F C› and
    not_sec_case: ‹∀E ∈ N - Red_F_𝒢 N. Prec_F_g D E C ⟶ D ∉ 𝒢_F E›
  have C_in_unfolded: "C ∈ {C. ∀Di ∈ 𝒢_F C. Di ∈ Red_F_G (𝒢_Fset N) ∨
    (∃E∈N. Prec_F_g Di E C ∧ Di ∈ 𝒢_F E)}"
    using C_in unfolding Red_F_𝒢_def .
  have neg_not_sec_case: ‹¬ (∃E∈N - Red_F_𝒢 N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
    using not_sec_case by clarsimp
  have unfol_C_D: ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
    using prop_nested_in_set[of D 𝒢_F C "λx. x ∈ Red_F_G (⋃ (𝒢_F ` N))"
      "λx y. ∃E ∈ N. Prec_F_g y E x ∧ y ∈ 𝒢_F E", OF D_in C_in_unfolded] by blast
  show ‹D ∈ Red_F_G (𝒢_Fset N)›
  proof (rule ccontr)
    assume contrad: ‹D ∉ Red_F_G (𝒢_Fset N)›
    have non_empty: ‹∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E› using contrad unfol_C_D by auto
    define B where ‹B = {E ∈ N. Prec_F_g D E C ∧ D ∈ 𝒢_F E}›
    then have B_non_empty: ‹B ≠ {}› using non_empty by auto

    obtain F :: 'f where F: "F ∈ B" "∀y. Prec_F_g D y F ⟶ y ∉ B" 
      using all_wf[of D]
      by (metis B_non_empty wfp_iff_ex_minimal)

    then have D_in_F: ‹D ∈ 𝒢_F F› 
      unfolding B_def using non_empty
      by blast
     
    have F_prec: ‹Prec_F_g D F C› using F unfolding B_def by auto
    have F_not_in: ‹F ∉ Red_F_𝒢 N›
    proof
      assume F_in: ‹F ∈ Red_F_𝒢 N›
      have unfol_F_D: ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃G∈N. Prec_F_g D G F ∧ D ∈ 𝒢_F G)›
        using F_in D_in_F unfolding Red_F_𝒢_def by auto
      then have ‹∃G∈N. Prec_F_g D G F ∧ D ∈ 𝒢_F G› using contrad D_in unfolding Red_F_𝒢_def by auto
      then obtain G where G_in: ‹G ∈ N› and G_prec: ‹Prec_F_g D G F› and G_map: ‹D ∈ 𝒢_F G› by auto
      have ‹Prec_F_g D G C› using G_prec F_prec Prec_trans by blast
      then have ‹G ∈ B› unfolding B_def using G_in G_map by auto
      then show ‹False› using F G_prec by auto
    qed
    have ‹F ∈ N› using F B_def by blast 
    then have ‹F ∈ N - Red_F_𝒢 N› using F_not_in by auto
    then show ‹False›
      using D_in_F neg_not_sec_case F_prec by blast
  qed
next
  fix C
  assume only_if: ‹∀D∈𝒢_F C. D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E∈N - Red_F_𝒢 N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
  show ‹C ∈ Red_F_𝒢 N› unfolding Red_F_𝒢_def using only_if by auto
qed

(* lem:lifting-main-technical *)
lemma not_red_map_in_map_not_red: ‹𝒢_Fset N - Red_F_G (𝒢_Fset N) ⊆ 𝒢_Fset (N - Red_F_𝒢 N)›
proof
  fix D
  assume D_hyp: ‹D ∈ 𝒢_Fset N - Red_F_G (𝒢_Fset N)›


  have D_in: ‹D ∈ 𝒢_Fset N› using D_hyp by blast
  have  D_not_in: ‹D ∉ Red_F_G (𝒢_Fset N)› using D_hyp by blast
  have exist_C: ‹∃C. C ∈ N ∧ D ∈ 𝒢_F C› using D_in by auto
  define B where ‹B = {C ∈ N. D ∈ 𝒢_F C}›
  obtain C where C: "C ∈ B" "∀y. Prec_F_g D y C ⟶ y ∉ B" 
    by (metis (no_types, lifting) B_def all_wf(1) exist_C mem_Collect_eq wfp_eq_minimal)
  have C_in_N: ‹C ∈ N›
    using B_def C by auto
  have D_in_C: ‹D ∈ 𝒢_F C›
    using B_def C by auto
  have C_not_in: ‹C ∉ Red_F_𝒢 N›
  proof
    assume C_in: ‹C ∈ Red_F_𝒢 N›
    have ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
      using C_in D_in_C unfolding Red_F_𝒢_def by auto
    then show ‹False›
      proof
        assume ‹D ∈ Red_F_G (𝒢_Fset N)›
        then show ‹False› using D_not_in by simp
      next
        assume ‹∃E∈N. Prec_F_g D E C ∧ D ∈ 𝒢_F E›
        then show ‹False›
          using C B_def by auto
      qed
  qed
  show ‹D ∈ 𝒢_Fset (N - Red_F_𝒢 N)› using D_in_C C_not_in C_in_N by blast
qed
  
(* lem:nonredundant-entails-redundant *)
lemma Red_F_Bot_F: ‹B ∈ Bot_F ⟹ N ⊨𝒢 {B} ⟹ N - Red_F_𝒢 N ⊨𝒢 {B}›
proof -
  fix B N
  assume
    B_in: ‹B ∈ Bot_F› and
    N_entails: ‹N ⊨𝒢 {B}›
  then have to_bot: ‹𝒢_Fset N - Red_F_G (𝒢_Fset N) ⊨G 𝒢_F B›
    using ground.Red_F_Bot Bot_map
    by (metis SUP_upper ground.entail_set_all_formulas in_mono singletonI)
  have from_f: ‹𝒢_Fset (N - Red_F_𝒢 N) ⊨G 𝒢_Fset N - Red_F_G (𝒢_Fset N)›
    using ground.subset_entailed[OF not_red_map_in_map_not_red] by blast
  then have ‹𝒢_Fset (N - Red_F_𝒢 N) ⊨G 𝒢_F B› using to_bot ground.entails_trans by blast
  then show ‹N - Red_F_𝒢 N ⊨𝒢 {B}› using Bot_map by simp
qed

(* lem:redundancy-monotonic-addition 1/2 *)
lemma Red_F_of_subset_F: ‹N ⊆ N' ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 N'›
  using ground.Red_F_of_subset unfolding Red_F_𝒢_def by clarsimp (meson 𝒢_subset subsetD)

(* lem:redundancy-monotonic-addition 2/2 *)
lemma Red_I_of_subset_F: ‹N ⊆ N' ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 N'›
  using Collect_mono 𝒢_subset subset_iff ground.Red_I_of_subset unfolding Red_I_𝒢_def
  by (smt (verit, del_insts) UnCI UnE ground.Red_F_of_subset subsetD)

(* lem:redundancy-monotonic-deletion-forms *)
lemma Red_F_of_Red_F_subset_F: ‹N' ⊆ Red_F_𝒢 N ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 (N - N')›
proof
  fix N N' C
  assume
    N'_in_Red_F_N: ‹N' ⊆ Red_F_𝒢 N› and
    C_in_red_F_N: ‹C ∈ Red_F_𝒢 N›
  have lem8: ‹∀D ∈ 𝒢_F C. D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E ∈ (N - Red_F_𝒢 N). Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
    using Red_F_𝒢_equiv_def C_in_red_F_N by blast
  show ‹C ∈ Red_F_𝒢 (N - N')› unfolding Red_F_𝒢_def
  proof (rule,rule)
    fix D
    assume ‹D ∈ 𝒢_F C›
    then have ‹D ∈ Red_F_G (𝒢_Fset N) ∨ (∃E ∈ (N - Red_F_𝒢 N). Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
      using lem8 by auto
    then show ‹D ∈ Red_F_G (𝒢_Fset (N - N')) ∨ (∃E∈N - N'. Prec_F_g D E C ∧ D ∈ 𝒢_F E)›
    proof
      assume ‹D ∈ Red_F_G (𝒢_Fset N)›
      then have ‹D ∈ Red_F_G (𝒢_Fset N - Red_F_G (𝒢_Fset N))›
        using ground.Red_F_of_Red_F_subset[of "Red_F_G (𝒢_Fset N)" "𝒢_Fset N"] by auto
      then have ‹D ∈ Red_F_G (𝒢_Fset (N - Red_F_𝒢 N))›
        using ground.Red_F_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
      then have ‹D ∈ Red_F_G (𝒢_Fset (N - N'))›
        using N'_in_Red_F_N 𝒢_subset[of "N - Red_F_𝒢 N" "N - N'"]
        by (meson Diff_mono ground.Red_F_of_subset subset_iff)
      then show ?thesis by blast
    next
      assume ‹∃E∈N - Red_F_𝒢 N. Prec_F_g D E C ∧ D ∈ 𝒢_F E›
      then obtain E where
        E_in: ‹E∈N - Red_F_𝒢 N› and
        E_prec_C: ‹Prec_F_g D E C› and
        D_in: ‹D ∈ 𝒢_F E›
        by auto
      have ‹E ∈ N - N'› using E_in N'_in_Red_F_N by blast
      then show ?thesis using E_prec_C D_in by blast
    qed
  qed
qed

(* lem:redundancy-monotonic-deletion-infs *)
lemma Red_I_of_Red_F_subset_F: ‹N' ⊆ Red_F_𝒢 N ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 (N - N') ›
proof
  fix N N' ι
  assume
    N'_in_Red_F_N: ‹N' ⊆ Red_F_𝒢 N› and
    i_in_Red_I_N: ‹ι ∈ Red_I_𝒢 N›
  have i_in: ‹ι ∈ Inf_F› using i_in_Red_I_N unfolding Red_I_𝒢_def by blast
  {
    assume not_none: "𝒢_I ι ≠ None"
    have ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset N)›
      using not_none i_in_Red_I_N unfolding Red_I_𝒢_def by auto
    then have ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset N - Red_F_G (𝒢_Fset N))›
      using not_none ground.Red_I_of_Red_F_subset by blast
    then have ip_in_Red_I_G: ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset (N - Red_F_𝒢 N))›
      using not_none ground.Red_I_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
    then have not_none_in: ‹∀ι' ∈ the (𝒢_I ι). ι' ∈ Red_I_G (𝒢_Fset (N - N'))›
      using not_none N'_in_Red_F_N
      by (meson Diff_mono ground.Red_I_of_subset 𝒢_subset subset_iff subset_refl)
    then have "the (𝒢_I ι) ⊆ Red_I_G (𝒢_Fset (N - N'))" by blast
  }
  moreover {
    assume none: "𝒢_I ι = None"
    have ground_concl_subs: "𝒢_F (concl_of ι) ⊆ (𝒢_Fset N ∪ Red_F_G (𝒢_Fset N))"
      using none i_in_Red_I_N unfolding Red_I_𝒢_def by blast
    then have d_in_imp12: "D ∈ 𝒢_F (concl_of ι) ⟹ D ∈ 𝒢_Fset N - Red_F_G (𝒢_Fset N) ∨ D ∈ Red_F_G (𝒢_Fset N)"
      by blast
    have d_in_imp1: "D ∈ 𝒢_Fset N - Red_F_G (𝒢_Fset N) ⟹ D ∈ 𝒢_Fset (N - N')"
      using not_red_map_in_map_not_red N'_in_Red_F_N by blast
    have d_in_imp_d_in: "D ∈ Red_F_G (𝒢_Fset N) ⟹ D ∈ Red_F_G (𝒢_Fset N - Red_F_G (𝒢_Fset N))"
      using ground.Red_F_of_Red_F_subset[of "Red_F_G (𝒢_Fset N)" "𝒢_Fset N"] by blast
    have g_subs1: "𝒢_Fset N - Red_F_G (𝒢_Fset N) ⊆ 𝒢_Fset (N - Red_F_𝒢 N)"
      using not_red_map_in_map_not_red unfolding Red_F_𝒢_def by auto
    have g_subs2: "𝒢_Fset (N - Red_F_𝒢 N) ⊆ 𝒢_Fset (N - N')"
      using N'_in_Red_F_N by blast
    have d_in_imp2: "D ∈ Red_F_G (𝒢_Fset N) ⟹ D ∈ Red_F_G (𝒢_Fset (N - N'))"
      using ground.Red_F_of_subset ground.Red_F_of_subset[OF g_subs1]
        ground.Red_F_of_subset[OF g_subs2] d_in_imp_d_in by blast
    have "𝒢_F (concl_of ι) ⊆ (𝒢_Fset (N - N') ∪ Red_F_G (𝒢_Fset (N - N')))"
      using d_in_imp12 d_in_imp1 d_in_imp2
      by (smt (verit, ccfv_SIG) Un_Diff_cancel2 calculus.Red_F_of_subset g_subs1 g_subs2
          ground.Red_F_of_Red_F_subset ground.reduced_calc_is_calc ground_concl_subs order_eq_refl
          order_trans sup_mono)
  }
  ultimately show ‹ι ∈ Red_I_𝒢 (N - N')› using i_in unfolding Red_I_𝒢_def by auto
qed

(* lem:concl-contained-implies-red-inf *)
lemma Red_I_of_Inf_to_N_F:
  assumes
    i_in: ‹ι ∈ Inf_F› and
    concl_i_in: ‹concl_of ι ∈ N›
  shows
    ‹ι ∈ Red_I_𝒢 N ›
proof -
  have ‹ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Red_I_G (𝒢_F (concl_of ι))› using inf_map by simp
  moreover have ‹Red_I_G (𝒢_F (concl_of ι)) ⊆ Red_I_G (𝒢_Fset N)›
    using concl_i_in ground.Red_I_of_subset by blast
  moreover have "ι ∈ Inf_F ⟹ 𝒢_I ι = None ⟹ concl_of ι ∈ N ⟹ 𝒢_F (concl_of ι) ⊆ 𝒢_Fset N"
    by blast
  ultimately show ?thesis using i_in concl_i_in unfolding Red_I_𝒢_def by auto
qed

(* thm:FRedsqsubset-is-red-crit and also thm:lifted-red-crit if ordering empty *)
sublocale calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢
proof
  fix B N N' ι
  show ‹Red_I_𝒢 N ⊆ Inf_F› unfolding Red_I_𝒢_def by blast
  show ‹B ∈ Bot_F ⟹ N ⊨𝒢 {B} ⟹ N - Red_F_𝒢 N ⊨𝒢 {B}› using Red_F_Bot_F by simp
  show ‹N ⊆ N' ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 N'› using Red_F_of_subset_F by simp
  show ‹N ⊆ N' ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 N'› using Red_I_of_subset_F by simp
  show ‹N' ⊆ Red_F_𝒢 N ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 (N - N')› using Red_F_of_Red_F_subset_F by simp
  show ‹N' ⊆ Red_F_𝒢 N ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 (N - N')› using Red_I_of_Red_F_subset_F by simp
  show ‹ι ∈ Inf_F ⟹ concl_of ι ∈ N ⟹ ι ∈ Red_I_𝒢 N› using Red_I_of_Inf_to_N_F by simp
qed

end

lemma standard_empty_tiebreaker_equiv: "standard_lifting Inf_F Bot_G Inf_G entails_G Red_I_G
  Red_F_G Bot_F 𝒢_F 𝒢_I = tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G
  Red_F_G 𝒢_F 𝒢_I (λg C C'. False)"
proof -
  have "tiebreaker_lifting_axioms (λg C C'. False)"
    unfolding tiebreaker_lifting_axioms_def 
    by auto

  then show ?thesis
    unfolding standard_lifting_def tiebreaker_lifting_def by blast
qed

context standard_lifting
begin

  interpretation empt_ord: tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G
    Red_F_G 𝒢_F 𝒢_I "λg C C'. False"
    using standard_empty_tiebreaker_equiv using standard_lifting_axioms by blast

  lemma red_f_equiv: "empt_ord.Red_F_𝒢 = Red_F_𝒢"
    unfolding Red_F_𝒢_def empt_ord.Red_F_𝒢_def by simp

  sublocale calc?: calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢
    using empt_ord.calculus_axioms red_f_equiv by fastforce

  lemma grounded_inf_in_ground_inf: "ι ∈ Inf_F ⟹ 𝒢_I ι ≠ None ⟹ the (𝒢_I ι) ⊆ Inf_G"
    using inf_map ground.Red_I_to_Inf by blast

  abbreviation ground_Inf_overapproximated :: "'f set ⇒ bool" where
    "ground_Inf_overapproximated N ≡ ground.Inf_from (𝒢_Fset N)
      ⊆ {ι. ∃ι'∈ Inf_from N. 𝒢_I ι' ≠ None ∧ ι ∈ the (𝒢_I ι')} ∪ Red_I_G (𝒢_Fset N)"

(* abbreviation "saturated ≡ calc.saturated" *)

  lemma sat_inf_imp_ground_red:
    assumes
      "saturated N" and
      "ι' ∈ Inf_from N" and
      "𝒢_I ι' ≠ None ∧ ι ∈ the (𝒢_I ι')"
    shows "ι ∈ Red_I_G (𝒢_Fset N)"
      using assms Red_I_𝒢_def unfolding saturated_def by auto

(* lem:sat-wrt-finf *)
  lemma sat_imp_ground_sat:
    "saturated N ⟹ ground_Inf_overapproximated N ⟹ ground.saturated (𝒢_Fset N)"
    unfolding ground.saturated_def using sat_inf_imp_ground_red by auto

(* thm:finf-complete *)
  theorem stat_ref_comp_to_non_ground:
    assumes
      stat_ref_G: "statically_complete_calculus Bot_G Inf_G entails_G Red_I_G Red_F_G" and
      sat_n_imp: "⋀N. saturated N ⟹ ground_Inf_overapproximated N"
    shows
      "statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢"
  proof
    fix B N
    assume
      b_in: "B ∈ Bot_F" and
      sat_n: "saturated N" and
      n_entails_bot: "N ⊨𝒢 {B}"
    have ground_n_entails: "𝒢_Fset N ⊨G 𝒢_F B"
      using n_entails_bot by simp
    then obtain BG where bg_in1: "BG ∈ 𝒢_F B"
      using Bot_map_not_empty[OF b_in] by blast
    then have bg_in: "BG ∈ Bot_G"
      using Bot_map[OF b_in] by blast
    have ground_n_entails_bot: "𝒢_Fset N ⊨G {BG}"
      using ground_n_entails bg_in1 ground.entail_set_all_formulas by blast
    have "ground.Inf_from (𝒢_Fset N) ⊆
      {ι. ∃ι'∈ Inf_from N. 𝒢_I ι' ≠ None ∧ ι ∈ the (𝒢_I ι')} ∪ Red_I_G (𝒢_Fset N)"
      using sat_n_imp[OF sat_n] .
    have "ground.saturated (𝒢_Fset N)"
      using sat_imp_ground_sat[OF sat_n sat_n_imp[OF sat_n]] .
    then have "∃BG'∈Bot_G. BG' ∈ (𝒢_Fset N)"
      using stat_ref_G ground.calculus_axioms bg_in ground_n_entails_bot
      unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
      by blast
    then show "∃B'∈ Bot_F. B' ∈ N"
      using bg_in Bot_cond Bot_map_not_empty Bot_cond
      by blast
  qed
    
end

context tiebreaker_lifting 
begin

  (* lem:saturation-indep-of-sqsubset *)
  lemma saturated_empty_order_equiv_saturated:
    "saturated N = calc.saturated N"
    by (rule refl)
    
    (* lem:static-ref-compl-indep-of-sqsubset *)
  lemma static_empty_order_equiv_static:
    "statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢 =
      statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 empty_ord.Red_F_𝒢"
    unfolding statically_complete_calculus_def
    by (rule iffI) (standard,(standard)[],simp)+

    (* thm:FRedsqsubset-is-dyn-ref-compl *)
  theorem static_to_dynamic:
    "statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 empty_ord.Red_F_𝒢 =
      dynamically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢"
    using dyn_equiv_stat static_empty_order_equiv_static
    by blast
   
end

subsection ‹Lifting with a Family of Redundancy Criteria›

locale lifting_intersection = inference_system Inf_F +
  ground: inference_system_family Q Inf_G_q +
  ground: consequence_relation_family Bot_G Q entails_q
  for
    Inf_F :: "'f inference set" and
    Bot_G :: "'g set" and
    Q :: "'q set" and
    Inf_G_q :: ‹'q ⇒ 'g inference set› and
    entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool" and
    Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set" and
    Red_F_q :: "'q ⇒ 'g set ⇒ 'g set"
  + fixes
    Bot_F :: "'f set" and
    𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set" and
    𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option" and
    Prec_F_g :: "'g ⇒ 'f ⇒ 'f ⇒ bool"
  assumes
    standard_lifting_family:
      "∀q ∈ Q. tiebreaker_lifting Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q)
         (Red_F_q q) (𝒢_F_q q) (𝒢_I_q q) Prec_F_g"
begin

abbreviation 𝒢_Fset_q :: "'q ⇒ 'f set ⇒ 'g set" where
  "𝒢_Fset_q q N ≡ ⋃ (𝒢_F_q q ` N)"

definition Red_I_𝒢_q :: "'q ⇒ 'f set ⇒ 'f inference set" where
  "Red_I_𝒢_q q N = {ι ∈ Inf_F. (𝒢_I_q q ι ≠ None ∧ the (𝒢_I_q q ι) ⊆ Red_I_q q (𝒢_Fset_q q N))
   ∨ (𝒢_I_q q ι = None ∧ 𝒢_F_q q (concl_of ι) ⊆ (𝒢_Fset_q q N ∪ Red_F_q q (𝒢_Fset_q q N)))}"

definition Red_F_𝒢_empty_q :: "'q ⇒ 'f set ⇒ 'f set" where
  "Red_F_𝒢_empty_q q N = {C. ∀D ∈ 𝒢_F_q q C. D ∈ Red_F_q q (𝒢_Fset_q q N)}"

definition Red_F_𝒢_q :: "'q ⇒ 'f set ⇒ 'f set" where
  "Red_F_𝒢_q q N =
   {C. ∀D ∈ 𝒢_F_q q C. D ∈ Red_F_q q (𝒢_Fset_q q N) ∨ (∃E ∈ N. Prec_F_g D E C ∧ D ∈ 𝒢_F_q q E)}"

abbreviation entails_𝒢_q :: "'q ⇒ 'f set ⇒ 'f set ⇒ bool" where
  "entails_𝒢_q q N1 N2 ≡ entails_q q (𝒢_Fset_q q N1) (𝒢_Fset_q q N2)"

lemma red_crit_lifting_family:
  assumes q_in: "q ∈ Q"
  shows "calculus Bot_F Inf_F (entails_𝒢_q q) (Red_I_𝒢_q q) (Red_F_𝒢_q q)"
proof -
  interpret wf_lift:
    tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q"
      "Red_F_q q" "𝒢_F_q q" "𝒢_I_q q" Prec_F_g
    using standard_lifting_family q_in by metis
  have "Red_I_𝒢_q q = wf_lift.Red_I_𝒢"
    unfolding Red_I_𝒢_q_def wf_lift.Red_I_𝒢_def by blast
  moreover have "Red_F_𝒢_q q = wf_lift.Red_F_𝒢"
    unfolding Red_F_𝒢_q_def wf_lift.Red_F_𝒢_def by blast
  ultimately show ?thesis
    using wf_lift.calculus_axioms by simp
qed

lemma red_crit_lifting_family_empty_ord:
  assumes q_in: "q ∈ Q"
  shows "calculus Bot_F Inf_F (entails_𝒢_q q) (Red_I_𝒢_q q) (Red_F_𝒢_empty_q q)"
proof -
  interpret wf_lift:
    tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q"
      "Red_F_q q" "𝒢_F_q q" "𝒢_I_q q" Prec_F_g
    using standard_lifting_family q_in by metis
  have "Red_I_𝒢_q q = wf_lift.Red_I_𝒢"
    unfolding Red_I_𝒢_q_def wf_lift.Red_I_𝒢_def by blast
  moreover have "Red_F_𝒢_empty_q q = wf_lift.empty_ord.Red_F_𝒢"
    unfolding Red_F_𝒢_empty_q_def wf_lift.empty_ord.Red_F_𝒢_def by blast
  ultimately show ?thesis
    using wf_lift.calc.calculus_axioms by simp
qed

sublocale consequence_relation_family Bot_F Q entails_𝒢_q
proof (unfold_locales; (intro ballI)?)
  show "Q ≠ {}"
    by (rule ground.Q_nonempty)
next
  fix qi
  assume qi_in: "qi ∈ Q"

  interpret lift: tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q qi" "Inf_G_q qi"
    "Red_I_q qi" "Red_F_q qi" "𝒢_F_q qi" "𝒢_I_q qi" Prec_F_g
    using qi_in by (metis standard_lifting_family)

  show "consequence_relation Bot_F (entails_𝒢_q qi)"
    by unfold_locales
qed

sublocale intersection_calculus Bot_F Inf_F Q entails_𝒢_q Red_I_𝒢_q Red_F_𝒢_q
  by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family)

abbreviation entails_𝒢 :: "'f set ⇒ 'f set ⇒ bool" (infix ‹⊨∩𝒢› 50) where
  "(⊨∩𝒢) ≡ entails"

abbreviation Red_I_𝒢 :: "'f set ⇒ 'f inference set" where
  "Red_I_𝒢 ≡ Red_I"

abbreviation Red_F_𝒢 :: "'f set ⇒ 'f set" where
  "Red_F_𝒢 ≡ Red_F"

lemmas entails_𝒢_def = entails_def
lemmas Red_I_𝒢_def = Red_I_def
lemmas Red_F_𝒢_def = Red_F_def

sublocale empty_ord: intersection_calculus Bot_F Inf_F Q entails_𝒢_q Red_I_𝒢_q Red_F_𝒢_empty_q
  by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family_empty_ord)

abbreviation Red_F_𝒢_empty :: "'f set ⇒ 'f set" where
  "Red_F_𝒢_empty ≡ empty_ord.Red_F"

lemmas Red_F_𝒢_empty_def = empty_ord.Red_F_def

lemma sat_inf_imp_ground_red_fam_inter:
  assumes
    sat_n: "saturated N" and
    i'_in: "ι' ∈ Inf_from N" and
    q_in: "q ∈ Q" and
    grounding: "𝒢_I_q q ι' ≠ None ∧ ι ∈ the (𝒢_I_q q ι')"
  shows "ι ∈ Red_I_q q (𝒢_Fset_q q N)"
proof -
  have "ι' ∈ Red_I_𝒢_q q N"
    using sat_n i'_in q_in all_red_crit calculus.saturated_def sat_int_to_sat_q
    by blast
  then have "the (𝒢_I_q q ι') ⊆ Red_I_q q (𝒢_Fset_q q N)"
    by (simp add: Red_I_𝒢_q_def grounding)
  then show ?thesis
    using grounding by blast
qed

abbreviation ground_Inf_overapproximated :: "'q ⇒ 'f set ⇒ bool" where
  "ground_Inf_overapproximated q N ≡
   ground.Inf_from_q q (𝒢_Fset_q q N)
   ⊆ {ι. ∃ι'∈ Inf_from N. 𝒢_I_q q ι' ≠ None ∧ ι ∈ the (𝒢_I_q q ι')} ∪ Red_I_q q (𝒢_Fset_q q N)"

abbreviation ground_saturated :: "'q ⇒ 'f set ⇒ bool" where
  "ground_saturated q N ≡ ground.Inf_from_q q (𝒢_Fset_q q N) ⊆ Red_I_q q (𝒢_Fset_q q N)"

lemma sat_imp_ground_sat_fam_inter:
  "saturated N ⟹ q ∈ Q ⟹ ground_Inf_overapproximated q N ⟹ ground_saturated q N"
  using sat_inf_imp_ground_red_fam_inter by auto

(* thm:intersect-finf-complete *)
theorem stat_ref_comp_to_non_ground_fam_inter:
  assumes
    stat_ref_G:
      "∀q ∈ Q. statically_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q)
        (Red_F_q q)" and
    sat_n_imp: "⋀N. saturated N ⟹ ∃q ∈ Q. ground_Inf_overapproximated q N"
  shows
    "statically_complete_calculus Bot_F Inf_F entails_𝒢 Red_I_𝒢 Red_F_𝒢_empty"
    using empty_ord.calculus_axioms unfolding statically_complete_calculus_def
      statically_complete_calculus_axioms_def
proof (standard, clarify)
  fix B N
  assume
    b_in: "B ∈ Bot_F" and
    sat_n: "saturated N" and
    entails_bot: "N ⊨∩𝒢 {B}"
  then obtain q where
    q_in: "q ∈ Q" and
    inf_subs: "ground.Inf_from_q q (𝒢_Fset_q q N) ⊆
      {ι. ∃ι'∈ Inf_from N. 𝒢_I_q q ι' ≠ None ∧ ι ∈ the (𝒢_I_q q ι')}
      ∪ Red_I_q q (𝒢_Fset_q q N)"
    using sat_n_imp[of N] by blast
  interpret q_calc: calculus Bot_F Inf_F "entails_𝒢_q q" "Red_I_𝒢_q q" "Red_F_𝒢_q q"
    using all_red_crit[rule_format, OF q_in] .
  have n_q_sat: "q_calc.saturated N"
    using q_in sat_int_to_sat_q sat_n by simp
  interpret lifted_q_calc:
    tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q"
      "Red_F_q q" "𝒢_F_q q" "𝒢_I_q q"
    using q_in by (simp add: standard_lifting_family)
  have n_lift_sat: "lifted_q_calc.calc.saturated N"
    using n_q_sat unfolding Red_I_𝒢_q_def lifted_q_calc.Red_I_𝒢_def
      lifted_q_calc.saturated_def q_calc.saturated_def by auto
  have ground_sat_n: "lifted_q_calc.ground.saturated (𝒢_Fset_q q N)"
    by (rule lifted_q_calc.sat_imp_ground_sat[OF n_lift_sat])
      (use n_lift_sat inf_subs ground.Inf_from_q_def in auto)
  have ground_n_entails_bot: "entails_𝒢_q q N {B}"
    using q_in entails_bot unfolding entails_𝒢_def by simp
  interpret statically_complete_calculus Bot_G "Inf_G_q q" "entails_q q" "Red_I_q q"
    "Red_F_q q"
    using stat_ref_G[rule_format, OF q_in] .
  obtain BG where bg_in: "BG ∈ 𝒢_F_q q B"
    using lifted_q_calc.Bot_map_not_empty[OF b_in] by blast
  then have "BG ∈ Bot_G" using lifted_q_calc.Bot_map[OF b_in] by blast
  then have "∃BG'∈Bot_G. BG' ∈ 𝒢_Fset_q q N"
    using ground_sat_n ground_n_entails_bot statically_complete[of BG, OF _ ground_sat_n]
      bg_in lifted_q_calc.ground.entail_set_all_formulas[of "𝒢_Fset_q q N" "𝒢_Fset_q q {B}"]
    by simp
  then show "∃B'∈ Bot_F. B' ∈ N" using lifted_q_calc.Bot_cond by blast
qed

(* lem:intersect-saturation-indep-of-sqsubset *)
lemma sat_eq_sat_empty_order: "saturated N = empty_ord.saturated N"
  by (rule refl)

(* lem:intersect-static-ref-compl-indep-of-sqsubset *)
lemma static_empty_ord_inter_equiv_static_inter:
  "statically_complete_calculus Bot_F Inf_F entails Red_I Red_F =
  statically_complete_calculus Bot_F Inf_F entails Red_I Red_F_𝒢_empty"
  unfolding statically_complete_calculus_def
  by (simp add: empty_ord.calculus_axioms calculus_axioms)

(* thm:intersect-static-ref-compl-is-dyn-ref-compl-with-order *)
theorem stat_eq_dyn_ref_comp_fam_inter: "statically_complete_calculus Bot_F Inf_F
    entails Red_I Red_F_𝒢_empty =
  dynamically_complete_calculus Bot_F Inf_F entails Red_I Red_F"
  using dyn_equiv_stat static_empty_ord_inter_equiv_static_inter
  by blast

end

end