src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 55273 e887c0743614
parent 55267 e68fd012bbf3
child 55274 b84867d6550b
equal deleted inserted replaced
55272:236114c5eb44 55273:e887c0743614
   131         val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
   131         val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
   132           atp_proof, goal) = try isar_params ()
   132           atp_proof, goal) = try isar_params ()
   133 
   133 
   134         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
   134         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
   135 
   135 
       
   136         val massage_meths = not try0_isar ? single o hd
       
   137 
   136         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
   138         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
   137         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
   139         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
   138         val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
   140         val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
   139 
   141 
   140         val do_preplay = preplay_timeout <> Time.zeroTime
   142         val do_preplay = preplay_timeout <> Time.zeroTime
   159         val lems =
   161         val lems =
   160           map_filter (get_role (curry (op =) Lemma)) atp_proof
   162           map_filter (get_role (curry (op =) Lemma)) atp_proof
   161           |> map (fn ((l, t), rule) =>
   163           |> map (fn ((l, t), rule) =>
   162             let
   164             let
   163               val (skos, meths) =
   165               val (skos, meths) =
   164                 if is_skolemize_rule rule then (skolems_of t, skolem_methods)
   166                 (if is_skolemize_rule rule then (skolems_of t, skolem_methods)
   165                 else if is_arith_rule rule then ([], arith_methods)
   167                  else if is_arith_rule rule then ([], arith_methods)
   166                 else ([], rewrite_methods)
   168                  else ([], rewrite_methods))
       
   169                 ||> massage_meths
   167             in
   170             in
   168               Prove ([], skos, l, t, [], (([], []), meths))
   171               Prove ([], skos, l, t, [], (([], []), meths))
   169             end)
   172             end)
   170 
   173 
   171         val bot = atp_proof |> List.last |> #1
   174         val bot = atp_proof |> List.last |> #1
   212 
   215 
   213         fun isar_steps outer predecessor accum [] =
   216         fun isar_steps outer predecessor accum [] =
   214             accum
   217             accum
   215             |> (if tainted = [] then
   218             |> (if tainted = [] then
   216                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
   219                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
   217                                ((the_list predecessor, []), metislike_methods)))
   220                                ((the_list predecessor, []), massage_meths metislike_methods)))
   218                 else
   221                 else
   219                   I)
   222                   I)
   220             |> rev
   223             |> rev
   221           | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
   224           | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
   222             let
   225             let
   228               fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
   231               fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
   229               fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
   232               fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
   230 
   233 
   231               val deps = fold add_fact_of_dependencies gamma no_facts
   234               val deps = fold add_fact_of_dependencies gamma no_facts
   232               val meths =
   235               val meths =
   233                 if skolem then skolem_methods
   236                 (if skolem then skolem_methods
   234                 else if is_arith_rule rule then arith_methods
   237                  else if is_arith_rule rule then arith_methods
   235                 else if is_datatype_rule rule then datatype_methods
   238                  else if is_datatype_rule rule then datatype_methods
   236                 else metislike_methods
   239                  else metislike_methods)
       
   240                 |> massage_meths
   237               val by = (deps, meths)
   241               val by = (deps, meths)
   238             in
   242             in
   239               if is_clause_tainted c then
   243               if is_clause_tainted c then
   240                 (case gamma of
   244                 (case gamma of
   241                   [g] =>
   245                   [g] =>
   257               val l = label_of_clause c
   261               val l = label_of_clause c
   258               val t = prop_of_clause c
   262               val t = prop_of_clause c
   259               val step =
   263               val step =
   260                 Prove (maybe_show outer c [], [], l, t,
   264                 Prove (maybe_show outer c [], [], l, t,
   261                   map isar_case (filter_out (null o snd) cases),
   265                   map isar_case (filter_out (null o snd) cases),
   262                   ((the_list predecessor, []), metislike_methods))
   266                   ((the_list predecessor, []), massage_meths metislike_methods))
   263             in
   267             in
   264               isar_steps outer (SOME l) (step :: accum) infs
   268               isar_steps outer (SOME l) (step :: accum) infs
   265             end
   269             end
   266         and isar_proof outer fix assms lems infs =
   270         and isar_proof outer fix assms lems infs =
   267           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
   271           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)