src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
changeset 38613 4ca2cae2653f
parent 38610 5266689abbc1
child 38618 5536897d04c2
equal deleted inserted replaced
38612:fa7e19c6be74 38613:4ca2cae2653f
   141                      |> reveal_bounds Ts
   141                      |> reveal_bounds Ts
   142         val ([t], ctxt') = Variable.import_terms true [t] ctxt
   142         val ([t], ctxt') = Variable.import_terms true [t] ctxt
   143       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   143       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   144       handle THM _ =>
   144       handle THM _ =>
   145              (* A type variable of sort "{}" will make abstraction fail. *)
   145              (* A type variable of sort "{}" will make abstraction fail. *)
   146              case kind of
   146              if kind = Conjecture then HOLogic.false_const
   147                Axiom => HOLogic.true_const
   147              else HOLogic.true_const
   148              | Conjecture => HOLogic.false_const
       
   149   end
   148   end
   150 
   149 
   151 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   150 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   152    same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   151    same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   153 fun freeze_term t =
   152 fun freeze_term t =
   173         HOLogic.eq_const T $ t1 $ t2
   172         HOLogic.eq_const T $ t1 $ t2
   174       | aux _ = raise Fail "aux"
   173       | aux _ = raise Fail "aux"
   175   in perhaps (try aux) end
   174   in perhaps (try aux) end
   176 
   175 
   177 (* making axiom and conjecture formulas *)
   176 (* making axiom and conjecture formulas *)
   178 fun make_formula ctxt presimp (name, kind, t) =
   177 fun make_formula ctxt presimp name kind t =
   179   let
   178   let
   180     val thy = ProofContext.theory_of ctxt
   179     val thy = ProofContext.theory_of ctxt
   181     val t = t |> Envir.beta_eta_contract
   180     val t = t |> Envir.beta_eta_contract
   182               |> atomize_term
   181               |> atomize_term
   183     val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
   182     val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
   184               |> extensionalize_term
   183               |> extensionalize_term
   185               |> presimp ? presimplify_term thy
   184               |> presimp ? presimplify_term thy
   186               |> perhaps (try (HOLogic.dest_Trueprop))
   185               |> perhaps (try (HOLogic.dest_Trueprop))
   187               |> introduce_combinators_in_term ctxt kind
   186               |> introduce_combinators_in_term ctxt kind
   188               |> kind = Conjecture ? freeze_term
   187               |> kind <> Axiom ? freeze_term
   189     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   188     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   190   in
   189   in
   191     FOLFormula {name = name, combformula = combformula, kind = kind,
   190     FOLFormula {name = name, combformula = combformula, kind = kind,
   192                 ctypes_sorts = ctypes_sorts}
   191                 ctypes_sorts = ctypes_sorts}
   193   end
   192   end
   194 
   193 
   195 fun make_axiom ctxt presimp (name, th) =
   194 fun make_axiom ctxt presimp (name, th) =
   196   (name, make_formula ctxt presimp (name, Axiom, prop_of th))
   195   (name, make_formula ctxt presimp name Axiom (prop_of th))
   197 fun make_conjectures ctxt ts =
   196 fun make_conjecture ctxt ts =
   198   map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
   197   let val last = length ts - 1 in
   199        (0 upto length ts - 1) ts
   198     map2 (fn j => make_formula ctxt true (Int.toString j)
       
   199                                (if j = last then Conjecture else Hypothesis))
       
   200          (0 upto last) ts
       
   201   end
   200 
   202 
   201 (** Helper facts **)
   203 (** Helper facts **)
   202 
   204 
   203 fun count_combterm (CombConst ((s, _), _, _)) =
   205 fun count_combterm (CombConst ((s, _), _, _)) =
   204     Symtab.map_entry s (Integer.add 1)
   206     Symtab.map_entry s (Integer.add 1)
   234                  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
   235                  else [])) @
   237                  else [])) @
   236     (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)
   237     |> map (snd o make_axiom ctxt false)
   239     |> map (snd o make_axiom ctxt false)
   238   end
   240   end
   239 
       
   240 fun meta_not t = @{const "==>"} $ t $ @{prop False}
       
   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
   245     val axiom_ts = map (prop_of o snd) axioms
   245     val axiom_ts = map (prop_of o snd) axioms
   257     val is_FO = Meson.is_fol_term thy goal_t
   257     val is_FO = Meson.is_fol_term thy goal_t
   258     val subs = tfree_classes_of_terms [goal_t]
   258     val subs = tfree_classes_of_terms [goal_t]
   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 = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
   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 (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'
   357 
   357 
   358 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   358 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   359   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   359   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   360 
   360 
   361 fun problem_line_for_free_type lit =
   361 fun problem_line_for_free_type lit =
   362   Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
   362   Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
   363 fun problem_lines_for_free_types conjectures =
   363 fun problem_lines_for_free_types conjectures =
   364   let
   364   let
   365     val litss = map free_type_literals_for_conjecture conjectures
   365     val litss = map free_type_literals_for_conjecture conjectures
   366     val lits = fold (union (op =)) litss []
   366     val lits = fold (union (op =)) litss []
   367   in map problem_line_for_free_type lits end
   367   in map problem_line_for_free_type lits end