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 ‹Grounding Data›

locale standard_lifting_data = 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

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)}›

(* lem:derived-consequence-relation *)
sublocale herbrand: consequence_relation Bot_F "(⊨𝒢)"
proof unfold_locales
  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

end

subsection ‹Tiebreaker Grounding Data›

locale tiebreaker_lifting_data =
  empty_ord?: standard_lifting_data 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


text ‹Only preservation of contradiction entailment is needed to obtain a
  calculus for an independently chosen consequence relation.›

lemma calculus_with_entailment:
  assumes cons: "consequence_relation Bot_F entails_F"
    and bot_iff: "⋀B N. B ∈ Bot_F ⟹
      (entails_F N {B} ⟷ entails_G (𝒢_Fset N) (𝒢_F B))"
  shows "calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢"
proof -
  interpret chosen: consequence_relation Bot_F entails_F by (rule cons)
  show ?thesis
  proof
    fix B N N' ι
    show "Red_I_𝒢 N ⊆ Inf_F" unfolding Red_I_𝒢_def by blast
    show "B ∈ Bot_F ⟹ entails_F N {B} ⟹ entails_F (N - Red_F_𝒢 N) {B}"
      using Red_F_Bot_F bot_iff by simp
    show "N ⊆ N' ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 N'" by (rule Red_F_of_subset_F)
    show "N ⊆ N' ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 N'" by (rule Red_I_of_subset_F)
    show "N' ⊆ Red_F_𝒢 N ⟹ Red_F_𝒢 N ⊆ Red_F_𝒢 (N - N')"
      by (rule Red_F_of_Red_F_subset_F)
    show "N' ⊆ Red_F_𝒢 N ⟹ Red_I_𝒢 N ⊆ Red_I_𝒢 (N - N')"
      by (rule Red_I_of_Red_F_subset_F)
    show "ι ∈ Inf_F ⟹ concl_of ι ∈ N ⟹ ι ∈ Red_I_𝒢 N"
      by (rule Red_I_of_Inf_to_N_F)
  qed
qed

end


subsection ‹Standard Lifting with Independent Entailment›

locale standard_lifting_with_entailment =
  standard_lifting_data Inf_F Bot_G Inf_G entails_G Red_I_G Red_F_G Bot_F 𝒢_F 𝒢_I +
  consequence_relation Bot_F entails_F
  for Bot_F :: "'f set" and Inf_F Bot_G Inf_G entails_G Red_I_G Red_F_G 𝒢_F 𝒢_I
    and entails_F :: "'f set ⇒ 'f set ⇒ bool" +
  assumes entails_F_bot_iff:
      "B ∈ Bot_F ⟹ (entails_F N {B} ⟷ entails_G (𝒢_Fset N) (𝒢_F B))"
begin

notation entails_G (infix ‹⊨G› 50)

interpretation empt_ord: tiebreaker_lifting_data Bot_F Inf_F Bot_G entails_G Inf_G
  Red_I_G Red_F_G 𝒢_F 𝒢_I "λg C C'. False"
  by unfold_locales (auto simp: wfp_def transp_def)

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_F Red_I_𝒢 Red_F_𝒢
  using empt_ord.calculus_with_entailment[OF consequence_relation_axioms entails_F_bot_iff]
    red_f_equiv by simp

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)"

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_with_entailment:
  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_F Red_I_𝒢 Red_F_𝒢"
proof
  fix B N
  assume
    b_in: "B ∈ Bot_F" and
    sat_n: "saturated N" and
    n_entails_bot: "entails_F N {B}"
  have ground_n_entails: "𝒢_Fset N ⊨G 𝒢_F B"
    using entails_F_bot_iff[OF b_in] 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

corollary dyn_ref_comp_with_entailment:
  assumes "statically_complete_calculus Bot_G Inf_G entails_G Red_I_G Red_F_G"
    and "⋀N. calc.saturated N ⟹ ground_Inf_overapproximated N"
  shows "dynamically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢"
proof -
  interpret chosen: statically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢
    by (rule stat_ref_comp_with_entailment[OF assms])
  show ?thesis by (rule chosen.dynamically_complete_calculus_axioms)
qed

end


subsection ‹Tiebreaker Lifting with Independent Entailment›

locale tiebreaker_lifting_with_entailment =
  tiebreaker_lifting_data Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G 𝒢_F 𝒢_I Prec_F_g +
  consequence_relation Bot_F entails_F
  for Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G 𝒢_F 𝒢_I Prec_F_g entails_F +
  assumes entails_F_bot_iff:
      "B ∈ Bot_F ⟹ (entails_F N {B} ⟷ entails_G (𝒢_Fset N) (𝒢_F B))"
begin

sublocale calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢
  by (rule calculus_with_entailment[OF consequence_relation_axioms entails_F_bot_iff])

sublocale empty_ord_general: standard_lifting_with_entailment Bot_F Inf_F Bot_G Inf_G
  entails_G Red_I_G Red_F_G 𝒢_F 𝒢_I entails_F
  by unfold_locales (use consequence_relation_axioms entails_F_bot_iff in auto)

lemma static_empty_order_equiv_static:
  "statically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢 =
    statically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 empty_ord.Red_F_𝒢"
  unfolding statically_complete_calculus_def
  by (simp add: calculus_axioms empty_ord_general.calc.calculus_axioms)

theorem stat_ref_comp_with_entailment:
  assumes "statically_complete_calculus Bot_G Inf_G entails_G Red_I_G Red_F_G"
    and "⋀N. saturated N ⟹ empty_ord_general.ground_Inf_overapproximated N"
  shows "statically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢"
  using empty_ord_general.stat_ref_comp_with_entailment[OF assms]
    static_empty_order_equiv_static by blast

corollary dyn_ref_comp_with_entailment:
  assumes "statically_complete_calculus Bot_G Inf_G entails_G Red_I_G Red_F_G"
    and "⋀N. saturated N ⟹ empty_ord_general.ground_Inf_overapproximated N"
  shows "dynamically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢"
proof -
  interpret chosen: statically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢
    by (rule stat_ref_comp_with_entailment[OF assms])
  show ?thesis by (rule chosen.dynamically_complete_calculus_axioms)
qed

end

subsection ‹Intersection Lifting with Independent Entailment›

locale lifting_intersection_data = 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_data 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_data 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
  moreover have "calculus Bot_F Inf_F (entails_𝒢_q q) wf_lift.Red_I_𝒢 wf_lift.Red_F_𝒢"
    by (rule wf_lift.calculus_with_entailment[OF wf_lift.herbrand.consequence_relation_axioms]) simp
  ultimately show ?thesis 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_data 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
  moreover have "calculus Bot_F Inf_F (entails_𝒢_q q) wf_lift.Red_I_𝒢 wf_lift.empty_ord.Red_F_𝒢"
  proof -
    interpret standard: standard_lifting_with_entailment Bot_F Inf_F Bot_G "Inf_G_q q"
      "entails_q q" "Red_I_q q" "Red_F_q q" "𝒢_F_q q" "𝒢_I_q q" "entails_𝒢_q q"
      by unfold_locales simp
    show ?thesis by (rule standard.calc.calculus_axioms)
  qed
  ultimately show ?thesis by simp
qed

sublocale herbrand: 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_data 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 (rule lift.herbrand.consequence_relation_axioms)
qed

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

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

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

lemmas lifted_entails_def = herbrand.entails_def
lemmas Red_I_𝒢_def = herbrand.Red_I_def
lemmas Red_F_𝒢_def = herbrand.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: ground.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: "herbrand.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 herbrand.all_red_crit calculus.saturated_def herbrand.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:
  "herbrand.saturated N ⟹ q ∈ Q ⟹ ground_Inf_overapproximated q N ⟹ ground_saturated q N"
  using sat_inf_imp_ground_red_fam_inter by auto

(* lem:intersect-saturation-indep-of-sqsubset *)
lemma sat_eq_sat_empty_order: "herbrand.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 herbrand.entails herbrand.Red_I herbrand.Red_F =
  statically_complete_calculus Bot_F Inf_F herbrand.entails herbrand.Red_I Red_F_𝒢_empty"
  unfolding statically_complete_calculus_def
  by (simp add: empty_ord.calculus_axioms herbrand.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
    herbrand.entails herbrand.Red_I Red_F_𝒢_empty =
  dynamically_complete_calculus Bot_F Inf_F herbrand.entails herbrand.Red_I herbrand.Red_F"
  using herbrand.dyn_equiv_stat static_empty_ord_inter_equiv_static_inter
  by blast

end


locale lifting_intersection_with_entailment =
  lifting_intersection_data Inf_F Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q Bot_F
    𝒢_F_q 𝒢_I_q Prec_F_g +
  consequence_relation Bot_F entails_F
  for Bot_F :: "'f set" and Inf_F Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q
    𝒢_F_q 𝒢_I_q Prec_F_g
    and entails_F :: "'f set ⇒ 'f set ⇒ bool" +
  assumes entails_F_bot_iff:
      "B ∈ Bot_F ⟹ (entails_F N {B} ⟷
        (∀q ∈ Q. entails_q q (𝒢_Fset_q q N) (𝒢_F_q q B)))"
begin

lemma entails_F_bot_iff_lifted:
  "B ∈ Bot_F ⟹ (entails_F N {B} ⟷ herbrand.entails N {B})"
  using entails_F_bot_iff unfolding lifted_entails_def by simp

sublocale chosen: calculus Bot_F Inf_F entails_F herbrand.Red_I herbrand.Red_F
  by (rule herbrand.calculus_with_equivalent_entailment[OF consequence_relation_axioms entails_F_bot_iff_lifted])

sublocale chosen_empty_ord: calculus Bot_F Inf_F entails_F herbrand.Red_I Red_F_𝒢_empty
  by (rule empty_ord.calculus_with_equivalent_entailment[OF consequence_relation_axioms entails_F_bot_iff_lifted])

(* thm:intersect-finf-complete *)
lemma stat_ref_comp_empty_with_entailment:
  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. chosen.saturated N ⟹ ∃q ∈ Q. ground_Inf_overapproximated q N"
  shows
    "statically_complete_calculus Bot_F Inf_F entails_F Red_I_𝒢 Red_F_𝒢_empty"
    using chosen_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: "chosen.saturated N" and
    entails_bot: "entails_F 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 herbrand.all_red_crit[rule_format, OF q_in] .
  have n_q_sat: "q_calc.saturated N"
    using q_in herbrand.sat_int_to_sat_q sat_n by simp
  interpret q_data: tiebreaker_lifting_data 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 blast
  interpret lifted_q_calc: standard_lifting_with_entailment Bot_F Inf_F Bot_G "Inf_G_q q"
    "entails_q q" "Red_I_q q" "Red_F_q q" "𝒢_F_q q" "𝒢_I_q q" "entails_𝒢_q q"
    by unfold_locales simp
  have n_lift_sat: "lifted_q_calc.calc.saturated N"
    using n_q_sat unfolding Red_I_𝒢_q_def q_data.Red_I_𝒢_def
      lifted_q_calc.calc.saturated_def q_calc.saturated_def by auto
  have ground_sat_n: "q_data.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 entails_F_bot_iff[OF b_in] 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 q_data.Bot_map_not_empty[OF b_in] by blast
  then have "BG ∈ Bot_G" using q_data.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 q_data.ground.entail_set_all_formulas[of "𝒢_Fset_q q N" "𝒢_Fset_q q {B}"]
    by simp
  then show "∃B'∈ Bot_F. B' ∈ N" using q_data.Bot_cond by blast
qed

theorem stat_ref_comp_with_entailment:
  assumes ground_complete:
      "∀q ∈ Q. statically_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q) (Red_F_q q)"
    and coverage: "⋀N. chosen.saturated N ⟹ ∃q ∈ Q. ground_Inf_overapproximated q N"
  shows "statically_complete_calculus Bot_F Inf_F entails_F herbrand.Red_I herbrand.Red_F"
    and "statically_complete_calculus Bot_F Inf_F entails_F herbrand.Red_I Red_F_𝒢_empty"
proof -
  show "statically_complete_calculus Bot_F Inf_F entails_F herbrand.Red_I Red_F_𝒢_empty"
    by (rule stat_ref_comp_empty_with_entailment[OF ground_complete coverage])
  then show "statically_complete_calculus Bot_F Inf_F entails_F herbrand.Red_I herbrand.Red_F"
    unfolding statically_complete_calculus_def
    by (simp add: chosen.calculus_axioms chosen_empty_ord.calculus_axioms)
qed

corollary dyn_ref_comp_with_entailment:
  assumes "∀q ∈ Q. statically_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q) (Red_F_q q)"
    and "⋀N. chosen.saturated N ⟹ ∃q ∈ Q. ground_Inf_overapproximated q N"
  shows "dynamically_complete_calculus Bot_F Inf_F entails_F herbrand.Red_I herbrand.Red_F"
proof -
  interpret chosen: statically_complete_calculus Bot_F Inf_F entails_F herbrand.Red_I herbrand.Red_F
    by (rule stat_ref_comp_with_entailment(1)[OF assms])
  show ?thesis by (rule chosen.dynamically_complete_calculus_axioms)
qed

end


subsection ‹Herbrand Lifting Interfaces›

text ‹The remaining locales specialize the general construction to Herbrand
  entailment and preserve the original interfaces.›

locale standard_lifting =
  standard_lifting_data Inf_F Bot_G Inf_G entails_G Red_I_G Red_F_G Bot_F 𝒢_F 𝒢_I
  for Inf_F :: "'f inference set" and Bot_G Inf_G entails_G Red_I_G Red_F_G Bot_F 𝒢_F 𝒢_I
begin

sublocale standard_lifting_with_entailment Bot_F Inf_F Bot_G Inf_G entails_G
  Red_I_G Red_F_G 𝒢_F 𝒢_I "(⊨𝒢)"
  by unfold_locales simp

lemmas stat_ref_comp_to_non_ground = stat_ref_comp_with_entailment

end

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 and Bot_G :: "'g set"
    and entails_G Inf_G Red_I_G Red_F_G 𝒢_F 𝒢_I +
  fixes Prec_F_g :: "'g ⇒ 'f ⇒ 'f ⇒ bool"
  assumes all_wf: "wfp (Prec_F_g g)" "transp (Prec_F_g g)"
begin

sublocale tiebreaker_lifting_with_entailment Bot_F Inf_F Bot_G entails_G Inf_G
  Red_I_G Red_F_G 𝒢_F 𝒢_I Prec_F_g "(⊨𝒢)"
  by unfold_locales (use all_wf in auto)

end

lemma tiebreaker_lifting_iff_data:
  "tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G 𝒢_F 𝒢_I Prec_F_g =
    tiebreaker_lifting_data Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G 𝒢_F 𝒢_I Prec_F_g"
  unfolding tiebreaker_lifting_def tiebreaker_lifting_data_def standard_lifting_def
    standard_lifting_data_def standard_lifting_data_axioms_def
    tiebreaker_lifting_axioms_def tiebreaker_lifting_data_axioms_def
  by blast

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 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 (⊨𝒢) Red_I_𝒢 Red_F_𝒢 =
      statically_complete_calculus Bot_F Inf_F (⊨𝒢) 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 (⊨𝒢) Red_I_𝒢 empty_ord.Red_F_𝒢 =
      dynamically_complete_calculus Bot_F Inf_F (⊨𝒢) Red_I_𝒢 Red_F_𝒢"
  using dyn_equiv_stat static_empty_order_equiv_static
  by blast
   
end

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"
    and 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

interpretation lifting_intersection_data Inf_F Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q
  Bot_F 𝒢_F_q 𝒢_I_q Prec_F_g
  by unfold_locales (use standard_lifting_family in ‹auto simp: tiebreaker_lifting_iff_data›)

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

lemmas entails_𝒢_def = lifted_entails_def

sublocale consequence_relation_family Bot_F Q entails_𝒢_q
  by (rule herbrand.consequence_relation_family_axioms)

sublocale intersection_calculus Bot_F Inf_F Q entails_𝒢_q Red_I_𝒢_q Red_F_𝒢_q
  by (rule herbrand.intersection_calculus_axioms)

sublocale lifting_intersection_with_entailment Bot_F Inf_F Bot_G Q Inf_G_q
  entails_q Red_I_q Red_F_q 𝒢_F_q 𝒢_I_q Prec_F_g entails_𝒢
  by unfold_locales (simp add: entails_𝒢_def)

lemmas stat_ref_comp_to_non_ground_fam_inter = stat_ref_comp_empty_with_entailment

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

end