src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
changeset 38618 5536897d04c2
parent 38613 4ca2cae2653f
child 38652 e063be321438
equal deleted inserted replaced
38617:f7b32911340b 38618:5536897d04c2
    77         do_conn bs AIff t1 t2
    77         do_conn bs AIff t1 t2
    78       | _ => (fn ts => do_term bs (Envir.eta_contract t)
    78       | _ => (fn ts => do_term bs (Envir.eta_contract t)
    79                        |>> AAtom ||> union (op =) ts)
    79                        |>> AAtom ||> union (op =) ts)
    80   in do_formula [] end
    80   in do_formula [] end
    81 
    81 
    82 fun presimplify_term thy =
    82 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
    83   Skip_Proof.make_thm thy
       
    84   #> Meson.presimplify
       
    85   #> prop_of
       
    86 
    83 
    87 fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
    84 fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
    88 fun conceal_bounds Ts t =
    85 fun conceal_bounds Ts t =
    89   subst_bounds (map (Free o apfst concealed_bound_name)
    86   subst_bounds (map (Free o apfst concealed_bound_name)
    90                     (0 upto length Ts - 1 ~~ Ts), t)
    87                     (0 upto length Ts - 1 ~~ Ts), t)
   190     FOLFormula {name = name, combformula = combformula, kind = kind,
   187     FOLFormula {name = name, combformula = combformula, kind = kind,
   191                 ctypes_sorts = ctypes_sorts}
   188                 ctypes_sorts = ctypes_sorts}
   192   end
   189   end
   193 
   190 
   194 fun make_axiom ctxt presimp (name, th) =
   191 fun make_axiom ctxt presimp (name, th) =
   195   (name, make_formula ctxt presimp name Axiom (prop_of th))
   192   case make_formula ctxt presimp name Axiom (prop_of th) of
       
   193     FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
       
   194     NONE
       
   195   | formula => SOME (name, formula)
   196 fun make_conjecture ctxt ts =
   196 fun make_conjecture ctxt ts =
   197   let val last = length ts - 1 in
   197   let val last = length ts - 1 in
   198     map2 (fn j => make_formula ctxt true (Int.toString j)
   198     map2 (fn j => make_formula ctxt true (Int.toString j)
   199                                (if j = last then Conjecture else Hypothesis))
   199                                (if j = last then Conjecture else Hypothesis))
   200          (0 upto last) ts
   200          (0 upto last) ts
   234      |> full_types ? append optional_typed_helpers
   234      |> full_types ? append optional_typed_helpers
   235      |> maps (fn (ss, ths) =>
   235      |> maps (fn (ss, ths) =>
   236                  if exists is_needed ss then map (`Thm.get_name_hint) ths
   236                  if exists is_needed ss then map (`Thm.get_name_hint) ths
   237                  else [])) @
   237                  else [])) @
   238     (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
   238     (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
   239     |> map (snd o make_axiom ctxt false)
   239     |> map_filter (Option.map snd o make_axiom ctxt false)
   240   end
   240   end
   241 
   241 
   242 fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
   242 fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
   243   let
   243   let
   244     val thy = ProofContext.theory_of ctxt
   244     val thy = ProofContext.theory_of ctxt
   259     val supers = tvar_classes_of_terms axiom_ts
   259     val supers = tvar_classes_of_terms axiom_ts
   260     val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
   260     val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
   261     (* TFrees in the conjecture; TVars in the axioms *)
   261     (* TFrees in the conjecture; TVars in the axioms *)
   262     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
   262     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
   263     val (axiom_names, axioms) =
   263     val (axiom_names, axioms) =
   264       ListPair.unzip (map (make_axiom ctxt true) axioms)
   264       ListPair.unzip (map_filter (make_axiom ctxt true) axioms)
   265     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
   265     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
   266     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   266     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   267     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   267     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   268   in
   268   in
   269     (Vector.fromList axiom_names,
   269     (Vector.fromList axiom_names,