1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
(* Title: focus.ML
Author: Joshua Chen
Focus on head subgoal, with optional variable renaming.
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 ()
val subgoal = #1 (Logic.dest_implies (Thm.prop_of st))
val subgoal_params =
map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
|> Term.variant_frees subgoal |> map #1
val n = length subgoal_params
val m = length raw_param_specs
val _ =
m <= n orelse
error ("Excessive subgoal parameter specification" ^
Position.here_list (map snd (drop n raw_param_specs)))
val param_specs = raw_param_specs
|> map
(fn (NONE, _) => NONE
| (SOME x, pos) =>
let
val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
val _ = Variable.check_name b
in SOME b end)
|> param_suffix ? append (replicate (n - m) NONE)
fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys
| bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys
| bindings _ ys = map Binding.name ys
in bindings param_specs subgoal_params end
fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state =
let
val _ = Proof.assert_backward state
val state1 = state
|> Proof.map_context (Proof_Context.set_mode Proof_Context.mode_schematic)
|> Proof.refine_insert []
val {context = ctxt, facts, goal = st} = Proof.raw_goal state1
val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding
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' =>
let
val ctxt' = Proof.context_of state'
val results' =
Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result)
in
state'
|> Proof.refine_primitive (fn _ => fn _ =>
Subgoal.retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
(Goal.protect 0 result) st
|> Seq.hd)
|> Proof.map_context
(#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
end)
#> Proof.reset_facts
#> Proof.enter_backward
in
state1
|> Proof.enter_forward
|> Proof.using_facts []
|> Proof.begin_block
|> Proof.map_context (fn _ =>
#context subgoal_focus
|> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])]
|> snd
|> Context_Facts.register_facts prems)
|> 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 @ prems)
|> pair subgoal_focus
end
val opt_fact_binding =
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 schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd
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
(** Outer syntax commands **)
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>\<^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
|
