diff options
Diffstat (limited to 'spartan/core/focus.ML')
| -rw-r--r-- | spartan/core/focus.ML | 96 |
1 files changed, 64 insertions, 32 deletions
diff --git a/spartan/core/focus.ML b/spartan/core/focus.ML index 1d8de78..2ad4c8a 100644 --- a/spartan/core/focus.ML +++ b/spartan/core/focus.ML @@ -1,14 +1,51 @@ (* Title: focus.ML - Author: Makarius Wenzel, Joshua Chen + Author: Joshua Chen -A modified version of the Isar `subgoal` command -that keeps schematic variables in the goal state. +Focus on head subgoal, with optional variable renaming. -Modified from code originally written by Makarius Wenzel. +Modified from code contained in ~~/Pure/Isar/subgoal.ML. *) local +fun reverse_prems imp = + let val (prems, concl) = (Drule.strip_imp_prems imp, Drule.strip_imp_concl imp) + in fold (curry mk_implies) prems concl end + +fun gen_focus ctxt i bindings raw_st = + let + val st = raw_st + |> Thm.solve_constraints + |> Thm.transfer' ctxt + |> Raw_Simplifier.norm_hhf_protect ctxt + + val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt + + val ((params, goal), ctxt2) = + Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1 + + val (asms, concl) = + (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) + + fun intern_var_assms asm (asms, concl) = + if Lib.no_vars (Thm.term_of asm) + then (asm :: asms, concl) + else (asms, Drule.mk_implies (asm, concl)) + + val (asms', concl') = fold intern_var_assms asms ([], concl) + |> apfst rev |> apsnd reverse_prems + + val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of (asms')) ctxt2 + val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst) + val schematics = (schematic_types, schematic_terms) + val asms' = map (Thm.instantiate_cterm schematics) asms' + val concl' = Thm.instantiate_cterm schematics concl' + val (prems, context) = Assumption.add_assumes asms' ctxt3 + in + ({context = context, params = params, prems = prems, + asms = asms', concl = concl', schematics = schematics}, Goal.init concl') + end + fun param_bindings ctxt (param_suffix, raw_param_specs) st = let val _ = if Thm.no_prems st then error "No subgoals!" else () @@ -24,8 +61,8 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st = error ("Excessive subgoal parameter specification" ^ Position.here_list (map snd (drop n raw_param_specs))) - val param_specs = - raw_param_specs |> map + val param_specs = raw_param_specs + |> map (fn (NONE, _) => NONE | (SOME x, pos) => let @@ -39,7 +76,7 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st = | bindings _ ys = map Binding.name ys in bindings param_specs subgoal_params end -fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state = +fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state = let val _ = Proof.assert_backward state @@ -47,17 +84,13 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s |> Proof.map_context (Proof_Context.set_mode Proof_Context.mode_schematic) |> Proof.refine_insert [] - val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1 - + val {context = ctxt, facts, goal = st} = Proof.raw_goal state1 val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding - val (prems_binding, do_prems) = - (case raw_prems_binding of - SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true) - | NONE => (Binding.empty_atts, false)) - val (subgoal_focus, _) = - (if do_prems then Subgoal.focus_prems else Subgoal.focus_params) ctxt - 1 (SOME (param_bindings ctxt param_specs st)) st + val subgoal_focus = #1 + (gen_focus ctxt 1 (SOME (param_bindings ctxt param_specs st)) st) + + val prems = #prems subgoal_focus fun after_qed (ctxt'', [[result]]) = Proof.end_block #> (fn state' => @@ -83,31 +116,29 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s |> Proof.begin_block |> Proof.map_context (fn _ => #context subgoal_focus - |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2) + |> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])] + |> #2) |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal" - NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2 - |> Proof.using_facts facts + NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] + |> #2 + |> Proof.using_facts (facts @ prems) |> pair subgoal_focus end val opt_fact_binding = - Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) + Scan.optional ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Args.colon) Binding.empty_atts -val for_params = - Scan.optional - (\<^keyword>\<open>vars\<close> |-- - Parse.!!! ((Scan.option Parse.dots >> is_some) -- - (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) - (false, []) +val for_params = Scan.optional + (\<^keyword>\<open>vars\<close> |-- + Parse.!!! ((Scan.option Parse.dots >> is_some) -- + (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) + (false, []) val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd -val parser = - opt_fact_binding - -- (Scan.option (\<^keyword>\<open>prems\<close> |-- Parse.!!! opt_fact_binding)) - -- for_params >> (fn ((a, b), c) => - Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd a b c)) +val parser = opt_fact_binding -- for_params >> (fn (fact, params) => + Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd fact params)) in @@ -117,9 +148,10 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>focus\<close> "focus on first subgoal within backward refinement, without instantiating schematic vars" parser -val _ = Outer_Syntax.command \<^command_keyword>\<open>\<guillemotright>\<close> "focus bullet" parser val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^item>\<close> "focus bullet" parser val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^enum>\<close> "focus bullet" parser +val _ = Outer_Syntax.command \<^command_keyword>\<open>\<circ>\<close> "focus bullet" parser +val _ = Outer_Syntax.command \<^command_keyword>\<open>\<diamondop>\<close> "focus bullet" parser val _ = Outer_Syntax.command \<^command_keyword>\<open>~\<close> "focus bullet" parser end |