Theory First_Order_Select

theory First_Order_Select
  imports 
    Selection_Function
    First_Order_Clause
    First_Order_Type_System
begin

type_synonym ('f, 'v, 'ty) typed_clause = "('f, 'v) atom clause × ('v, 'ty) var_types"

type_synonym 'f ground_select = "'f ground_atom clause ⇒ 'f ground_atom clause"
type_synonym ('f, 'v) select = "('f, 'v) atom clause ⇒ ('f, 'v) atom clause"

definition is_select_grounding :: "('f, 'v) select ⇒ 'f ground_select ⇒ bool" where 
  "⋀select select⇩G.
        is_select_grounding select select⇩G = (∀clause⇩G. ∃clause γ.
        clause.is_ground (clause ⋅ γ)  ∧ 
        clause⇩G = clause.to_ground (clause ⋅ γ) ∧ 
        select⇩G clause⇩G = clause.to_ground ((select clause) ⋅ γ))"

lemma infinite_lists_per_length: "infinite {l :: ('a :: infinite) list. length (tl l) = y}"
proof(induction y)
  case 0

  show ?case
  proof
    assume a: "finite {l :: 'a list. length (tl l) = 0}"

    define f where "⋀x:: 'a . f x ≡ [x]"


    have "⋀x y. f x = f y ⟹ x = y"
      unfolding f_def
      by (metis nth_Cons_0)

    moreover have "⋀x. length (f x) ≤ Suc 0"
      unfolding f_def
      by simp

    moreover have "⋀x. length x = Suc 0 ⟹ x ∈ range f"
      unfolding f_def
      by (smt (z3) One_nat_def Suc_length_conv Suc_pred' diff_Suc_1 diff_is_0_eq' 
          length_0_conv nat.simps(3) not_gr0 rangeI)

    moreover have "⋀x. ⟦x ∉ range f; length x ≤ Suc 0⟧ ⟹ x = []"
      using calculation(3) le_Suc_eq by auto

    moreover have "⋀xa. f xa = [] ⟹ False"
      unfolding f_def
      by simp

    ultimately have tt: "bij_betw f UNIV  ({l. length (tl l) = 0} - {[]})"
      unfolding bij_betw_def inj_def
      by auto presburger

    then have "infinite ({l :: 'a list. length (tl l) = 0} - {[]})"
      using bij_betw_finite infinite_UNIV by blast

    then have "infinite {l :: 'a list. length (tl l) = 0}"
      by simp

    with a show False
      by blast
  qed
next
  case (Suc y)


  have 1: "{l :: 'a list. length (tl l) = y} = 
    (if y = 0 then insert [] {l. length l = 1} else {l.  length l = Suc y})"
    by (auto simp: le_Suc_eq)

  have 2: "⋀x. length x = Suc y ⟹ x ∈ tl ` {l. length l - Suc 0 = Suc y}"
    by (metis (mono_tags, lifting) One_nat_def imageI length_tl list.sel(3) mem_Collect_eq)

  show ?case 
  proof
    assume "finite {l  :: 'a list. length (tl l) = Suc y}"

    then have "finite (tl ` {l :: 'a list. length (tl l) = Suc y})"
      by blast

    moreover have "tl ` {l :: 'a list. length (tl l) = Suc y} = {l :: 'a list. length l  = Suc y}"
      using 2
      by auto

    ultimately show False
      using Suc 1  
      by (smt (verit, ccfv_SIG) Collect_cong One_nat_def finite_insert)
  qed
qed

lemma infinite_prods': "{p :: 'a × 'a . fst p = y} = {y} × UNIV"
  by auto
 

lemma infinite_prods: "infinite {p :: (('a :: infinite) × 'a). fst p = y}"
  unfolding infinite_prods'
  using finite_cartesian_productD2 infinite_UNIV by blast

lemma nat_version': "∃f :: nat ⇒ nat. ∀y :: nat. infinite {x. f x = y}"
proof-
  obtain g :: "nat ⇒ nat × nat" where bij_g: "bij g"
    using bij_prod_decode by blast

  define f :: "nat ⇒ nat" where 
    "⋀x. f x ≡ fst (g x)"

  have "⋀y. infinite {x. f x = y}"
  proof-
    fix y
    have x: "{x. fst (g x) = y} =  inv g ` {p. fst p = y}"
      by (smt (verit, ccfv_SIG) Collect_cong bij_g bij_image_Collect_eq bij_imp_bij_inv inv_inv_eq)

    show "infinite {x. f x = y}"
      unfolding f_def x
      using infinite_prods
      by (metis bij_betw_def bij_g finite_imageI image_f_inv_f)
  qed

  then show ?thesis
    by blast    
qed

lemma not_nat_version': "∃f :: ('a :: infinite) ⇒ 'a. ∀y. infinite {x. f x = y}"
proof-
  obtain g :: "'a ⇒ 'a × 'a" where bij_g: "bij g"
    using Times_same_infinite_bij_betw_types bij_betw_inv infinite_UNIV by blast

  define f :: "'a ⇒ 'a" where 
    "⋀x. f x ≡ fst (g x)"

  have "⋀y. infinite {x. f x = y}"
  proof-
    fix y
    have x: "{x. fst (g x) = y} =  inv g ` {p. fst p = y}"
      by (smt (verit, ccfv_SIG) Collect_cong bij_g bij_image_Collect_eq bij_imp_bij_inv inv_inv_eq)

    show "infinite {x. f x = y}"
      unfolding f_def x
      using infinite_prods 
      by (metis bij_g bij_is_surj finite_imageI image_f_inv_f)
  qed

  then show ?thesis
    by blast    
qed

lemma not_nat_version'': 
  assumes "|UNIV :: 'b set| ≤o |UNIV :: ('a :: infinite) set|"
  shows "∃f :: 'a ⇒ 'b. ∀y. infinite {x. f x = y}"
proof-
  obtain g :: "'a ⇒ 'a × 'a" where bij_g: "bij g"
    using Times_same_infinite_bij_betw_types bij_betw_inv infinite_UNIV by blast

  define f :: "'a ⇒ 'a" where 
    "⋀x. f x ≡ fst (g x)"

  have inf: "⋀y. infinite {x. f x = y}"
  proof-
    fix y
    have x: "{x. fst (g x) = y} =  inv g ` {p. fst p = y}"
      by (smt (verit, ccfv_SIG) Collect_cong bij_g bij_image_Collect_eq bij_imp_bij_inv inv_inv_eq)

    show "infinite {x. f x = y}"
      unfolding f_def x
      using infinite_prods
      by (metis bij_g bij_is_surj finite_imageI image_f_inv_f)
  qed

  obtain f' ::  "'a ⇒ 'b" where "surj f'"
    using assms
    by (metis card_of_ordLeq2 empty_not_UNIV)

  then have "⋀y. infinite {x. f' (f x) = y}"
    using inf
    by (smt (verit, ccfv_SIG) Collect_mono finite_subset surjD)

  then show ?thesis
    by meson
qed



lemma nat_version: "∃f :: nat ⇒ nat. ∀y :: nat. infinite {x. f x = y}"
proof-
  obtain g :: "nat ⇒ nat list" where bij_g: "bij g"
    using bij_list_decode by blast

  define f :: "nat ⇒ nat" where 
    "⋀x. f x ≡ length (tl (g x))"

  have "⋀y. infinite {x. f x = y}"
  proof-
    fix y
    have "{x. length (tl (g x)) = y} = inv g ` {l. length (tl l) = y}"
      by (smt (verit, ccfv_SIG) Collect_cong bij_betw_def bij_g bij_image_Collect_eq image_inv_f_f 
          inv_inv_eq surj_imp_inj_inv)

    then show "infinite {x. f x = y}"
      unfolding f_def
      using infinite_lists_per_length
      by (metis bij_g bij_is_surj finite_imageI image_f_inv_f)
  qed

  then show ?thesis
    by blast    
qed

definition all_types where 
  "all_types 𝒱 ≡ ∀ty. infinite {x. 𝒱 x = ty}"


lemma all_types_nat: "∃𝒱 :: nat ⇒ nat. all_types 𝒱"
  unfolding all_types_def
  using nat_version
  by blast

lemma all_types: "∃𝒱 :: ('v :: {infinite, countable} ⇒ 'ty :: countable). all_types 𝒱"
proof-
  obtain 𝒱_nat :: "nat ⇒ nat" where 𝒱_nat: "all_types 𝒱_nat"
    using all_types_nat
    by blast

  obtain v_to_nat :: "'v ⇒ nat" where v_to_nat: "bij v_to_nat"
    using countableI_type infinite_UNIV to_nat_on_infinite by blast

  obtain nat_to_ty :: "nat ⇒ 'ty" and N where nat_to_ty: "bij_betw nat_to_ty N UNIV"
    using countableE_bij
    by (metis countableI_type)

  define 𝒱 where "⋀x. 𝒱 x ≡ nat_to_ty (𝒱_nat (v_to_nat x))"

  have 1: "⋀ty. {x. 𝒱_nat (v_to_nat x) = ty} = inv v_to_nat ` {x. 𝒱_nat x = ty}"
    by (smt (verit, best) Collect_cong bij_image_Collect_eq bij_imp_bij_inv inv_inv_eq v_to_nat)

  have 2: "⋀ty. infinite {x. 𝒱_nat (v_to_nat x) = ty}"
    unfolding 1
    using 𝒱_nat 
    unfolding all_types_def
    by (metis bij_betw_def finite_imageI image_f_inv_f v_to_nat)


  have "⋀ty. infinite {x. 𝒱 x = ty}"
    using 𝒱_nat
    unfolding 𝒱_def all_types_def
    by (smt (verit) "2" Collect_mono UNIV_I bij_betw_iff_bijections finite_subset nat_to_ty)
  
  then show "∃𝒱 :: 'v :: {infinite, countable} ⇒ 'ty :: countable. all_types 𝒱"
    unfolding all_types_def
    by fast
qed

lemma all_types': 
  assumes "|UNIV :: 'ty set| ≤o |UNIV :: ('v :: infinite) set|"
  shows "∃𝒱 :: ('v :: infinite ⇒ 'ty). all_types 𝒱"
  using not_nat_version''[OF assms]
  unfolding all_types_def
  by argo

definition clause_groundings :: "('f, 'ty) fun_types ⇒ ('f, 'v, 'ty) typed_clause ⇒ 'f ground_atom clause set"  where
  "clause_groundings ℱ clause = { clause.to_ground (fst clause ⋅ γ) | γ. 
    term_subst.is_ground_subst γ ∧ 
    welltyped⇩c ℱ (snd clause) (fst clause) ∧ 
    welltyped⇩σ_on (clause.vars (fst clause))  ℱ (snd clause) γ ∧ 
    all_types (snd clause)
  }"

abbreviation select_subst_stability_on where
  "⋀select select⇩G. select_subst_stability_on ℱ select select⇩G premises ≡
    ∀premise⇩G ∈ ⋃ (clause_groundings ℱ ` premises). ∃(premise, 𝒱) ∈ premises. ∃γ. 
      premise ⋅ γ = clause.from_ground premise⇩G ∧ 
      select⇩G (clause.to_ground (premise ⋅ γ)) = clause.to_ground ((select premise) ⋅ γ) ∧
      welltyped⇩c ℱ 𝒱 premise ∧ welltyped⇩σ_on (clause.vars premise) ℱ 𝒱 γ ∧ 
      term_subst.is_ground_subst γ  ∧ 
      all_types 𝒱"

lemma obtain_subst_stable_on_select_grounding:
  fixes select :: "('f, 'v) select"
  obtains select⇩G where 
    "select_subst_stability_on ℱ select select⇩G premises"
    "is_select_grounding select select⇩G"
proof-
  let ?premise_groundings = "⋃(clause_groundings ℱ ` premises)"

  have select⇩G_exists_for_premises: 
    "∀premise⇩G ∈ ?premise_groundings. ∃select⇩G γ. ∃(premise, 𝒱) ∈ premises.
          premise ⋅ γ = clause.from_ground premise⇩G 
        ∧ select⇩G premise⇩G = clause.to_ground ((select premise) ⋅ γ) 
        ∧ welltyped⇩c ℱ 𝒱 premise ∧ welltyped⇩σ_on (clause.vars premise) ℱ 𝒱 γ
        ∧ term_subst.is_ground_subst γ ∧ all_types 𝒱"
    unfolding clause_groundings_def
    using clause.is_ground_subst_is_ground
    by fastforce

  obtain select⇩G_on_premise_groundings where 
    select⇩G_on_premise_groundings: "∀premise⇩G ∈?premise_groundings. ∃(premise, 𝒱) ∈ premises. ∃γ.
        premise ⋅ γ = clause.from_ground premise⇩G 
      ∧ select⇩G_on_premise_groundings (clause.to_ground (premise ⋅ γ)) = 
          clause.to_ground ((select premise) ⋅ γ) 
      ∧ welltyped⇩c ℱ 𝒱 premise ∧ welltyped⇩σ_on (clause.vars premise) ℱ 𝒱 γ 
      ∧ term_subst.is_ground_subst γ ∧ all_types 𝒱"
    using Ball_Ex_comm(1)[OF select⇩G_exists_for_premises] 
      prod.case_eq_if clause.from_ground_inverse
    by fastforce

  define select⇩G where
    "⋀clause⇩G. select⇩G clause⇩G = (
        if clause⇩G  ∈ ?premise_groundings 
        then select⇩G_on_premise_groundings clause⇩G 
        else clause.to_ground (select (clause.from_ground clause⇩G))
    )"

  have grounding: "is_select_grounding select select⇩G"
  proof-
    have "⋀clause⇩G a b.
       ⟦∀y∈premises.
           ∀premise⇩G∈clause_groundings ℱ y.
              ∃x∈premises.
                 case x of
                 (premise, 𝒱) ⇒
                   ∃γ. premise ⋅ γ = clause.from_ground premise⇩G ∧
                       select⇩G_on_premise_groundings (clause.to_ground (premise ⋅ γ)) =
                       clause.to_ground (select premise ⋅ γ) ∧
                       welltyped⇩c ℱ 𝒱 premise ∧
                       welltyped⇩σ_on (clause.vars premise) ℱ 𝒱 γ ∧
                       term_subst.is_ground_subst γ ∧ all_types 𝒱;
        (a, b) ∈ premises; clause⇩G ∈ clause_groundings ℱ (a, b)⟧
       ⟹ ∃clause γ.
              clause.vars (clause ⋅ γ) = {} ∧
              clause⇩G = clause.to_ground (clause ⋅ γ) ∧
              select⇩G_on_premise_groundings clause⇩G = clause.to_ground (select clause ⋅ γ)"
      by force

    moreover have " ⋀clause⇩G.
       ⟦∀y∈premises.
           ∀premise⇩G∈clause_groundings ℱ y.
              ∃x∈premises.
                 case x of
                 (premise, 𝒱) ⇒
                   ∃γ. premise ⋅ γ = clause.from_ground premise⇩G ∧
                       select⇩G_on_premise_groundings (clause.to_ground (premise ⋅ γ)) =
                       clause.to_ground (select premise ⋅ γ) ∧
                       welltyped⇩c ℱ 𝒱 premise ∧
                       welltyped⇩σ_on (clause.vars premise) ℱ 𝒱 γ ∧
                       term_subst.is_ground_subst γ ∧ all_types 𝒱;
        ∀x∈premises. clause⇩G ∉ clause_groundings ℱ x⟧
       ⟹ ∃clause γ.
              clause.vars (clause ⋅ γ) = {} ∧
              clause⇩G = clause.to_ground (clause ⋅ γ) ∧
              clause.to_ground (select (clause.from_ground clause⇩G)) =
              clause.to_ground (select clause ⋅ γ)"
      by (metis (no_types, opaque_lifting) clause.comp_subst.left.action_neutral 
            clause.ground_is_ground clause.from_ground_inverse)

    ultimately show ?thesis
      unfolding is_select_grounding_def select⇩G_def
      using select⇩G_on_premise_groundings
      by auto
  qed
   
  show ?thesis
    using that[OF _ grounding] select⇩G_on_premise_groundings
    unfolding select⇩G_def 
    by fastforce
qed

locale first_order_select = select select
  for select :: "('f, 'v) atom clause ⇒ ('f, 'v) atom clause"
begin

abbreviation is_grounding :: "'f ground_select ⇒ bool" where
  "is_grounding select⇩G ≡ is_select_grounding select select⇩G"

definition select⇩G⇩s where
  "select⇩G⇩s = { ground_select. is_grounding ground_select }"

definition select⇩G_simple where
  "select⇩G_simple clause = clause.to_ground (select (clause.from_ground clause))"

lemma select⇩G_simple: "is_grounding select⇩G_simple"
  unfolding is_select_grounding_def select⇩G_simple_def
  by (metis clause.from_ground_inverse clause.ground_is_ground clause.subst_id_subst)

lemma select_from_ground_clause1: 
  assumes "clause.is_ground clause" 
  shows "clause.is_ground (select clause)"
  using select_subset sub_ground_clause assms
  by metis

lemma select_from_ground_clause2: 
  assumes "literal ∈# select (clause.from_ground clause)"  
  shows "literal.is_ground literal"
  using assms clause.sub_in_ground_is_ground select_subset
  by blast

lemma select_from_ground_clause3: 
  assumes "clause.is_ground clause" "literal⇩G ∈# clause.to_ground clause"
  shows "literal.from_ground literal⇩G ∈# clause"
  using assms 
  by (metis clause.to_ground_inverse clause.ground_sub_in_ground)

lemmas select_from_ground_clause =
  select_from_ground_clause1
  select_from_ground_clause2
  select_from_ground_clause3

lemma select_subst1:
  assumes "clause.is_ground (clause ⋅ γ)"  
  shows "clause.is_ground (select clause ⋅ γ)" 
  using assms
  by (metis image_mset_subseteq_mono select_subset sub_ground_clause clause.subst_def)

lemma select_subst2: 
  assumes "literal ∈# select clause ⋅ γ"  
  shows "is_neg literal"
  using assms subst_neg_stable select_negative_lits
  unfolding clause.subst_def
  by auto

lemmas select_subst = select_subst1 select_subst2

end

locale grounded_first_order_select = 
  first_order_select select for select +
fixes select⇩G 
assumes select⇩G: "is_select_grounding select select⇩G"
begin

abbreviation subst_stability_on where
  "subst_stability_on ℱ premises ≡ select_subst_stability_on ℱ select select⇩G premises"

lemma select⇩G_subset: "select⇩G clause ⊆# clause"
  using select⇩G 
  unfolding is_select_grounding_def
  by (metis select_subset clause.to_ground_def image_mset_subseteq_mono clause.subst_def)

lemma select⇩G_negative:
  assumes "literal⇩G ∈# select⇩G clause⇩G"
  shows "is_neg literal⇩G"
proof -
  obtain clause γ where 
    is_ground: "clause.is_ground (clause ⋅ γ)" and
    select⇩G: "select⇩G clause⇩G = clause.to_ground (select clause ⋅ γ)"
    using select⇩G
    unfolding is_select_grounding_def
    by blast

  show ?thesis
    using 
      select_from_ground_clause(3)[
        OF select_subst(1)[OF is_ground] assms[unfolded select⇩G], 
        THEN select_subst(2)
        ]
    unfolding literal.from_ground_def
    by simp
qed

sublocale ground: select select⇩G
  by unfold_locales (simp_all add: select⇩G_subset select⇩G_negative)

end

end