<commit_before>(*  Title:      HOL/Tools/SMT/z3_proof_tools.ML
    Author:     <NAME>, <NAME>

Helper functions required for Z3 proof reconstruction.
*)

signature Z3_PROOF_TOOLS =
sig
  (*modifying terms*)
  val as_meta_eq: cterm -> cterm

  (*theorem nets*)
  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
  val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
    cterm -> 'a option
  val net_instance: thm Net.net -> cterm -> thm option

  (*proof combinators*)
  val under_assumption: (thm -> thm) -> cterm -> thm
  val with_conv: conv -> (cterm -> thm) -> cterm -> thm
  val discharge: thm -> thm -> thm
  val varify: string list -> thm -> thm
  val unfold_eqs: Proof.context -> thm list -> conv
  val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
  val by_tac: (int -> tactic) -> cterm -> thm
  val make_hyp_def: thm -> Proof.context -> thm * Proof.context
  val by_abstraction: bool * bool -> Proof.context -> thm list ->
    (Proof.context -> cterm -> thm) -> cterm -> thm

  (*a faster COMP*)
  type compose_data
  val precompose: (cterm -> cterm list) -> thm -> compose_data
  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
  val compose: compose_data -> thm -> thm

  (*unfolding of 'distinct'*)
  val unfold_distinct_conv: conv

  (*simpset*)
  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
  val make_simpset: Proof.context -> thm list -> simpset
end

structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
struct



(* modifying terms *)

fun as_meta_eq ct =
  uncurry SMT_Utils.mk_cequals (Thm.dest_binop (SMT_Utils.dest_cprop ct))



(* theorem nets *)

fun thm_net_of f xthms =
  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
  in fold insert xthms Net.empty end

fun maybe_instantiate ct thm =
  try Thm.first_order_match (Thm.cprop_of thm, ct)
  |> Option.map (fn inst => Thm.instantiate inst thm)

fun net_instance' f net ct =
  let
    val xthms = Net.match_term net (Thm.term_of ct)
    fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
    fun first_of' f ct =
      let val thm = Thm.trivial ct
      in get_first (f (try (fn rule => rule COMP thm))) xthms end
  in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
val net_instance = net_instance' I


<commit_msg>use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)<commit_after>(*  Title:      HOL/Tools/SMT/z3_proof_tools.ML
    Author:     <NAME>, <NAME>

Helper functions required for Z3 proof reconstruction.
*)

signature Z3_PROOF_TOOLS =
sig
  (*modifying terms*)
  val as_meta_eq: cterm -> cterm

  (*theorem nets*)
  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
  val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
    cterm -> 'a option
  val net_instance: thm Net.net -> cterm -> thm option

  (*proof combinators*)
  val under_assumption: (thm -> thm) -> cterm -> thm
  val with_conv: conv -> (cterm -> thm) -> cterm -> thm
  val discharge: thm -> thm -> thm
  val varify: string list -> thm -> thm
  val unfold_eqs: Proof.context -> thm list -> conv
  val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
  val by_tac: (int -> tactic) -> cterm -> thm
  val make_hyp_def: thm -> Proof.context -> thm * Proof.context
  val by_abstraction: bool * bool -> Proof.context -> thm list ->
    (Proof.context -> cterm -> thm) -> cterm -> thm

  (*a faster COMP*)
  type compose_data
  val precompose: (cterm -> cterm list) -> thm -> compose_data
  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
  val compose: compose_data -> thm -> thm

  (*unfolding of 'distinct'*)
  val unfold_distinct_conv: conv

  (*simpset*)
  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
  val make_simpset: Proof.context -> thm list -> simpset
end

structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
struct



(* modifying terms *)

fun as_meta_eq ct =
  uncurry SMT_Utils.mk_cequals (Thm.dest_binop (SMT_Utils.dest_cprop ct))



(* theorem nets *)

fun thm_net_of f xthms =
  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
  in fold insert xthms Net.empty end

fun maybe_instantiate ct thm =
  try Thm.first_order_match (Thm.cprop_of thm, ct)
  |> Option.map (fn inst => Thm.instantiate inst thm)

local
  fun instances_from_net match f net ct =
    let
      val lookup = if match then Net.match_term else Net.unify_term
      val xthms = lookup net (Thm.term_of ct)
      fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
      fun first_of' f ct =
        let val thm = Thm.trivial ct
        in get_first (f (try (fn rule => rule COMP thm))) xthms end
    in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
in

fun net_instance' f = instances_from_net false f

val net_instance = instances_from_net true I

end



{'fraction_non_alphanumeric': 0.11810707840385001, 'fraction_numerical': 0.00240625626629236, 'mean_word_length': 3.1670843776106934, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 123, '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': '4608113', 'n_tokens_mistral': 1897, 'n_tokens_neox': 1797, 'n_words': 577}