<commit_before>(*  Title:      HOL/Tools/Sledgehammer/clausifier.ML
    Author:     <NAME>, Cambridge University Computer Laboratory and NICTA
    Author:     <NAME>, <NAME>

Transformation of axiom rules (elim/intro/etc) into CNF forms.
*)

signature CLAUSIFIER =
sig
  val extensionalize_theorem : thm -> thm
  val introduce_combinators_in_cterm : cterm -> thm
  val introduce_combinators_in_theorem : thm -> thm
  val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
  val cnf_axiom : theory -> thm -> thm list
end;

structure Clausifier : CLAUSIFIER =
struct

(**** Transformation of Elimination Rules into First-Order Formulas****)

val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);

(* Converts an elim-rule into an equivalent theorem that does not have the
   predicate variable. Leaves other theorems unchanged. We simply instantiate
   the conclusion variable to False. (Cf. "transform_elim_term" in
   "Sledgehammer_Util".) *)
fun transform_elim_theorem th =
  case concl_of th of    (*conclusion variable*)
       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    | v as Var(_, @{typ prop}) =>
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    | _ => th

(*To enforce single-threading*)
exception Clausify_failure of theory;


(**** SKOLEMIZATION BY INFERENCE (lcp) ****)

fun mk_skolem t =
  let val T = fastype_of t in
    Const (@{const_name skolem}, T --> T) $ t
  end

fun beta_eta_under_lambdas (Abs (s, T, t')) =
    Abs (s, T, beta_eta_under_lambdas t')
  | beta_eta_under_lambdas t = Envir.beta_eta_contract t

(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skolem_funs th =
  let
    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
        (*Existential: declare a Skolem function, then insert into body and continue*)
        let
          val args = OldTerm.term_frees body
          (* Forms a lambda-abstraction over the formal parameters *)
          val rhs =
            list_abs_free (map dest_Free args,
                           HOLogic.choice_const T $ beta_eta_under_lambdas body)
            |> mk_skolem
          val comb = list_comb (rhs, args)
        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
        (*Universal quant: insert a free variable into body and continue*)
        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a<commit_msg>remove needless exception<commit_after>(*  Title:      HOL/Tools/Sledgehammer/clausifier.ML
    Author:     <NAME>, Cambridge University Computer Laboratory and NICTA
    Author:     <NAME>, <NAME>

Transformation of axiom rules (elim/intro/etc) into CNF forms.
*)

signature CLAUSIFIER =
sig
  val extensionalize_theorem : thm -> thm
  val introduce_combinators_in_cterm : cterm -> thm
  val introduce_combinators_in_theorem : thm -> thm
  val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
  val cnf_axiom : theory -> thm -> thm list
end;

structure Clausifier : CLAUSIFIER =
struct

(**** Transformation of Elimination Rules into First-Order Formulas****)

val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);

(* Converts an elim-rule into an equivalent theorem that does not have the
   predicate variable. Leaves other theorems unchanged. We simply instantiate
   the conclusion variable to False. (Cf. "transform_elim_term" in
   "Sledgehammer_Util".) *)
fun transform_elim_theorem th =
  case concl_of th of    (*conclusion variable*)
       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    | v as Var(_, @{typ prop}) =>
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    | _ => th


(**** SKOLEMIZATION BY INFERENCE (lcp) ****)

fun mk_skolem t =
  let val T = fastype_of t in
    Const (@{const_name skolem}, T --> T) $ t
  end

fun beta_eta_under_lambdas (Abs (s, T, t')) =
    Abs (s, T, beta_eta_under_lambdas t')
  | beta_eta_under_lambdas t = Envir.beta_eta_contract t

(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skolem_funs th =
  let
    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
        (*Existential: declare a Skolem function, then insert into body and continue*)
        let
          val args = OldTerm.term_frees body
          (* Forms a lambda-abstraction over the formal parameters *)
          val rhs =
            list_abs_free (map dest_Free args,
                           HOLogic.choice_const T $ beta_eta_under_lambdas body)
            |> mk_skolem
          val comb = list_comb (rhs, args)
        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
        (*Universal quant: insert a free variable into body and continue*)
        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
{'fraction_non_alphanumeric': 0.10784878142391095, 'fraction_numerical': 0.0, 'mean_word_length': 3.2168284789644015, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1998132', 'n_tokens_mistral': 1784, 'n_tokens_neox': 1742, 'n_words': 546}