src/HOL/Tools/Metis/metis_tactic.ML
changeset 73932 fd21b4a93043
parent 70514 7a63b16c53c4
child 74051 bd575b1bd9bf
equal deleted inserted replaced
73866:66bff50bc5f1 73932:fd21b4a93043
   147 fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 =
   147 fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 =
   148   let
   148   let
   149     val thy = Proof_Context.theory_of ctxt
   149     val thy = Proof_Context.theory_of ctxt
   150 
   150 
   151     val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
   151     val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
   152     val do_lams =
   152     val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt
   153       (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? introduce_lam_wrappers ctxt
       
   154     val th_cls_pairs =
   153     val th_cls_pairs =
   155       map2 (fn j => fn th =>
   154       map2 (fn j => fn th =>
   156         (Thm.get_name_hint th,
   155         (Thm.get_name_hint th,
   157           th
   156           th
   158           |> Drule.eta_contraction_rule
   157           |> Drule.eta_contraction_rule
   278     HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
   277     HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
   279       CHANGED_PROP o metis_tac (these override_type_encs)
   278       CHANGED_PROP o metis_tac (these override_type_encs)
   280         (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
   279         (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
   281   end
   280   end
   282 
   281 
   283 val metis_lam_transs = [hide_lamsN, liftingN, combsN]
   282 val metis_lam_transs = [opaque_liftingN, liftingN, combsN]
   284 
   283 
   285 fun set_opt _ x NONE = SOME x
   284 fun set_opt _ x NONE = SOME x
   286   | set_opt get x (SOME x0) =
   285   | set_opt get x (SOME x0) =
   287     error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x))
   286     error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x))
   288 
   287 
   289 fun consider_opt s =
   288 fun consider_opt s =
   290   if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
   289   if s = "hide_lams" then
       
   290     error "\"hide_lams\" has been renamed \"opaque_lifting\""
       
   291   else if member (op =) metis_lam_transs s then
       
   292     apsnd (set_opt I s)
       
   293   else
       
   294     apfst (set_opt hd [s])
   291 
   295 
   292 val parse_metis_options =
   296 val parse_metis_options =
   293   Scan.optional
   297   Scan.optional
   294       (Args.parens (Args.name -- Scan.option (\<^keyword>\<open>,\<close> |-- Args.name))
   298       (Args.parens (Args.name -- Scan.option (\<^keyword>\<open>,\<close> |-- Args.name))
   295        >> (fn (s, s') =>
   299        >> (fn (s, s') =>