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

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

signature MESON_CLAUSIFY =
sig
  val new_skolem_var_prefix : string
  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 cluster_of_zapped_var_name : string -> (int * int) * bool
  val cnf_axiom :
    Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
  val meson_general_tac : Proof.context -> thm list -> int -> tactic
  val setup: theory -> theory
end;

structure Meson_Clausify : MESON_CLAUSIFY =
struct

(* the extra "?" helps prevent clashes *)
val new_skolem_var_prefix = "?SK"
val new_nonskolem_var_prefix = "?V"

(**** 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_old_skolem_term_wrapper 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 old_skolem_defs 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_old_skolem_term_wrapper
          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
        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
      | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
      | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
      | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
      | dec_sko _ rhss = rhss
  in  dec_sko (prop_of th) []  end;


(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)

val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}

(* Removes the lambdas from an equation of the form "t = (%x. u)".
   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)<commit_msg>renamed internal function<commit_after>(*  Title:      HOL/Tools/Sledgehammer/meson_clausify.ML
    Author:     <NAME>, Cambridge University Computer Laboratory and NICTA
    Author:     <NAME>, <NAME>

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

signature MESON_CLAUSIFY =
sig
  val new_skolem_var_prefix : string
  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 cluster_of_zapped_var_name : string -> (int * int) * bool
  val cnf_axiom :
    Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
  val meson_general_tac : Proof.context -> thm list -> int -> tactic
  val setup: theory -> theory
end;

structure Meson_Clausify : MESON_CLAUSIFY =
struct

(* the extra "?" helps prevent clashes *)
val new_skolem_var_prefix = "?SK"
val new_nonskolem_var_prefix = "?V"

(**** 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_old_skolem_term_wrapper t =
  let val T = fastype_of t in
    Const (@{const_name skolem}, T --> T) $ t
  end

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

(*Traverse a theorem, accumulating Skolem function definitions.*)
fun old_skolem_defs 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_in_abs_body body)
            |> mk_old_skolem_term_wrapper
          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
        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
      | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
      | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
      | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
      | dec_sko _ rhss = rhss
  in  dec_sko (prop_of th) []  end;


(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)

val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}

(* Removes the lambdas from an equation of the form "t = (%x. u)".
   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
{'fraction_non_alphanumeric': 0.11433399042523233, 'fraction_numerical': 0.000281610813855252, 'mean_word_length': 3.271196632591702, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 55, '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': '664993', 'n_tokens_mistral': 2550, 'n_tokens_neox': 2511, 'n_words': 754}