Theory First_Order_Clause.Selection_Function_Select_Max

theory Selection_Function_Select_Max
  imports
    Maximal_Literal
    Selection_Function
begin

text‹Example Selection Function›

context maximal_literal
begin

abbreviation select_max where
  "select_max C ≡
    if ∃l∈#C. is_maximal l C ∧ is_neg l
    then {#SOME l. is_maximal l C ∧ is_neg l#}
    else {#}"

sublocale select_max: selection_function select_max
proof unfold_locales
  fix C

  {
    assume "∃l∈# C. is_maximal l C ∧ is_neg l" 

    then have "∃l. is_maximal l C ∧ is_neg l"
      by blast
  
    then have "(SOME l. is_maximal l C ∧ is_neg l) ∈# C"
      by (rule someI2_ex) (simp add: maximal_in_clause)
  }

  then show "select_max C ⊆# C"
    by auto
next
  fix C l

  {
    assume "∃l∈#C. is_maximal l C ∧ is_neg l" 

    then have "∃l. is_maximal l C ∧ is_neg l"
      by blast
  
    then have "is_neg (SOME l. is_maximal l C ∧ is_neg l)"
      by (rule someI2_ex) simp
  }

  then show "l ∈# select_max C ⟹ is_neg l"
    by (smt (verit, ccfv_threshold) ex_in_conv set_mset_add_mset_insert set_mset_eq_empty_iff 
        singletonD)
qed

end

end