author | wenzelm |
Sat, 13 Jun 2015 15:51:19 +0200 | |
changeset 60453 | ba9085f7433f |
parent 60452 | 3a0d57f1d6ef |
child 60454 | a4c6b278f3a7 |
permissions | -rw-r--r-- |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/obtain.ML |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
3 |
|
60452 | 4 |
Generalized existence and cases rules within Isar proof text. |
8094 | 5 |
*) |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
6 |
|
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
7 |
signature OBTAIN = |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
8 |
sig |
60444 | 9 |
val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list |
60448 | 10 |
val parse_clause: Proof.context -> term -> |
11 |
(binding * typ option * mixfix) list -> string list -> term |
|
12 |
val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list |
|
13 |
val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list |
|
14 |
val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state |
|
15 |
val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
16 |
val obtain: binding -> (binding * typ option * mixfix) list -> |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
17 |
(Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state |
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
18 |
val obtain_cmd: binding -> (binding * string option * mixfix) list -> |
30211 | 19 |
(Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
20308 | 20 |
val result: (Proof.context -> tactic) -> thm list -> Proof.context -> |
32199 | 21 |
((string * cterm) list * thm list) * Proof.context |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
22 |
val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
23 |
val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
24 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
25 |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
26 |
structure Obtain: OBTAIN = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
27 |
struct |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
28 |
|
60452 | 29 |
(** specification elements **) |
30 |
||
31 |
(* obtain_export *) |
|
18670 | 32 |
|
18870 | 33 |
(* |
18897 | 34 |
[x, A x] |
35 |
: |
|
36 |
B |
|
37 |
-------- |
|
38 |
B |
|
18870 | 39 |
*) |
21686 | 40 |
fun eliminate_term ctxt xs tm = |
41 |
let |
|
42 |
val vs = map (dest_Free o Thm.term_of) xs; |
|
43 |
val bads = Term.fold_aterms (fn t as Free v => |
|
44 |
if member (op =) vs v then insert (op aconv) t else I | _ => I) tm []; |
|
45 |
val _ = null bads orelse |
|
46 |
error ("Result contains obtained parameters: " ^ |
|
24920 | 47 |
space_implode " " (map (Syntax.string_of_term ctxt) bads)); |
21686 | 48 |
in tm end; |
49 |
||
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
50 |
fun eliminate ctxt rule xs As thm = |
9468 | 51 |
let |
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
52 |
val _ = eliminate_term ctxt xs (Thm.full_prop_of thm); |
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
53 |
val _ = Object_Logic.is_judgment ctxt (Thm.concl_of thm) orelse |
20308 | 54 |
error "Conclusion in obtained context must be object-logic judgment"; |
55 |
||
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
56 |
val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt; |
20308 | 57 |
val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm')); |
9468 | 58 |
in |
20308 | 59 |
((Drule.implies_elim_list thm' (map Thm.assume prems) |
60315 | 60 |
|> Drule.implies_intr_list (map (Drule.norm_hhf_cterm ctxt') As) |
20308 | 61 |
|> Drule.forall_intr_list xs) |
62 |
COMP rule) |
|
63 |
|> Drule.implies_intr_list prems |
|
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
64 |
|> singleton (Variable.export ctxt' ctxt) |
9468 | 65 |
end; |
66 |
||
21686 | 67 |
fun obtain_export ctxt rule xs _ As = |
68 |
(eliminate ctxt rule xs As, eliminate_term ctxt xs); |
|
69 |
||
9468 | 70 |
|
60448 | 71 |
(* result declaration *) |
72 |
||
60444 | 73 |
fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) = |
74 |
let |
|
75 |
val case_names = obtains |> map_index (fn (i, (b, _)) => |
|
76 |
if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b); |
|
77 |
in [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names] end; |
|
78 |
||
79 |
||
60448 | 80 |
(* obtain thesis *) |
81 |
||
82 |
fun obtain_thesis ctxt = |
|
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
83 |
let |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
84 |
val ([x], ctxt') = |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
85 |
Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] ctxt; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
86 |
val t = Object_Logic.fixed_judgment ctxt x; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
87 |
val v = dest_Free (Object_Logic.drop_judgment ctxt t); |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
88 |
in ((v, t), ctxt') end; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
89 |
|
60448 | 90 |
|
91 |
(* obtain clauses *) |
|
92 |
||
93 |
local |
|
94 |
||
95 |
fun prepare_clause parse_prop ctxt thesis vars raw_props = |
|
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
96 |
let |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
97 |
val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
98 |
val xs = map (Variable.check_name o #1) vars; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
99 |
|
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
100 |
val default_name = AList.lookup (op =) (xs' ~~ xs); |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
101 |
val default_type = Variable.default_type ctxt'; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
102 |
in |
60448 | 103 |
Logic.list_implies (map (parse_prop ctxt') raw_props, thesis) |
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
104 |
|> Element.close_form ctxt default_name default_type |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
105 |
end; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
106 |
|
60448 | 107 |
fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains = |
108 |
let |
|
109 |
val all_types = |
|
110 |
fold_map prep_var (maps (fn (_, (vs, _)) => vs) raw_obtains) |
|
111 |
(ctxt |> Context_Position.set_visible false) |
|
112 |
|> #1 |> map_filter (fn (_, opt_T, _) => opt_T); |
|
113 |
val types_ctxt = fold Variable.declare_typ all_types ctxt; |
|
114 |
||
115 |
val clauses = |
|
116 |
raw_obtains |> map (fn (_, (raw_vars, raw_props)) => |
|
117 |
let |
|
118 |
val (vars, vars_ctxt) = fold_map prep_var raw_vars types_ctxt; |
|
119 |
val clause = prepare_clause parse_prop vars_ctxt thesis vars raw_props; |
|
120 |
in clause end) |
|
121 |
|> Syntax.check_terms ctxt; |
|
122 |
in map fst raw_obtains ~~ clauses end; |
|
123 |
||
124 |
in |
|
125 |
||
126 |
val parse_clause = prepare_clause Syntax.parse_prop; |
|
127 |
||
128 |
val read_obtains = prepare_obtains Proof_Context.read_var Syntax.parse_prop; |
|
129 |
val cert_obtains = prepare_obtains Proof_Context.cert_var (K I); |
|
130 |
||
131 |
end; |
|
132 |
||
133 |
||
134 |
||
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
135 |
(** consider: generalized elimination and cases rule **) |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
136 |
|
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
137 |
(* |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
138 |
consider x where (a) "A x" | y (b) where "B x" | ... == |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
139 |
|
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
140 |
have thesis |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
141 |
if a [intro?]: "!!x. A x ==> thesis" |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
142 |
and b [intro?]: "!!x. B x ==> thesis" |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
143 |
and ... |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
144 |
for thesis |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
145 |
apply (insert that) |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
146 |
*) |
60448 | 147 |
|
148 |
local |
|
149 |
||
150 |
fun gen_consider prep_obtains raw_obtains int state = |
|
151 |
let |
|
152 |
val _ = Proof.assert_forward_or_chain state; |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
153 |
val ctxt = Proof.context_of state; |
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
154 |
|
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
155 |
val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt; |
60448 | 156 |
val obtains = prep_obtains thesis_ctxt thesis raw_obtains; |
157 |
in |
|
158 |
state |
|
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
159 |
|> Proof.have NONE (K I) |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
160 |
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
161 |
(map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains) |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
162 |
[((Binding.empty, obtains_attributes raw_obtains), [(thesis, [])])] int |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
163 |
|> (fn state' => state' |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
164 |
|> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt)) |
60448 | 165 |
end; |
166 |
||
167 |
in |
|
168 |
||
169 |
val consider = gen_consider cert_obtains; |
|
170 |
val consider_cmd = gen_consider read_obtains; |
|
171 |
||
172 |
end; |
|
173 |
||
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
174 |
|
60444 | 175 |
|
60452 | 176 |
(** obtain: augmented context based on generalized existence rule **) |
177 |
||
178 |
(* |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
179 |
obtain (a) x where "A x" <proof> == |
60452 | 180 |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
181 |
have thesis if a [intro?]: "!!x. A x ==> thesis" for thesis |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
182 |
apply (insert that) |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
183 |
<proof> |
60452 | 184 |
fix x assm <<obtain_export>> "A x" |
185 |
*) |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
186 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
187 |
local |
8094 | 188 |
|
60379 | 189 |
fun gen_obtain prep_att prep_var prep_propp |
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
190 |
that_binding raw_vars raw_asms int state = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
191 |
let |
9468 | 192 |
val _ = Proof.assert_forward_or_chain state; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
193 |
val ctxt = Proof.context_of state; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
194 |
|
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
195 |
(*vars*) |
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
196 |
val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt; |
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
197 |
val ((xs', vars), fix_ctxt) = thesis_ctxt |
60392 | 198 |
|> fold_map prep_var raw_vars |
199 |
|-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars); |
|
42494 | 200 |
val xs = map (Variable.check_name o #1) vars; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
201 |
|
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
202 |
(*asms*) |
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
203 |
val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms); |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
204 |
val props = flat propss; |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
205 |
val declare_asms = |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
206 |
fold Variable.declare_term props #> |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
207 |
fold Variable.bind_term binds; |
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
208 |
val asms = |
60392 | 209 |
map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~ |
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
210 |
map (map (rpair [])) propss; |
10464 | 211 |
|
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
212 |
(*params*) |
60407 | 213 |
val (params, params_ctxt) = |
214 |
declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free; |
|
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
215 |
val cparams = map (Thm.cterm_of params_ctxt) params; |
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
216 |
val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds; |
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
217 |
|
60401 | 218 |
val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
219 |
|
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
220 |
(*statements*) |
10582 | 221 |
val that_prop = |
45328 | 222 |
Logic.list_rename_params xs |
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset
|
223 |
(fold_rev Logic.all params (Logic.list_implies (props, thesis))); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
224 |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
225 |
fun after_qed (result_ctxt, results) state' = |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
226 |
let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
227 |
state' |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
228 |
|> Proof.fix vars |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
229 |
|> Proof.map_context declare_asms |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
230 |
|> Proof.assm (obtain_export params_ctxt rule cparams) asms |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
231 |
end; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
232 |
in |
8094 | 233 |
state |
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
234 |
|> Proof.have NONE after_qed |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
235 |
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
236 |
[((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])] |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
237 |
[(Thm.empty_binding, [(thesis, [])])] int |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
238 |
|> (fn state' => state' |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
239 |
|> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt)) |
60401 | 240 |
|> Proof.map_context (fold Variable.bind_term binds') |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
241 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
242 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
243 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
244 |
|
60388 | 245 |
val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.cert_propp; |
246 |
val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.read_propp; |
|
8094 | 247 |
|
248 |
end; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
249 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
250 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
251 |
|
20308 | 252 |
(** tactical result **) |
253 |
||
254 |
fun check_result ctxt thesis th = |
|
255 |
(case Thm.prems_of th of |
|
256 |
[prem] => |
|
257 |
if Thm.concl_of th aconv thesis andalso |
|
258 |
Logic.strip_assums_concl prem aconv thesis then th |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31794
diff
changeset
|
259 |
else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th) |
38875
c7a66b584147
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents:
36323
diff
changeset
|
260 |
| [] => error "Goal solved -- nothing guessed" |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31794
diff
changeset
|
261 |
| _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th)); |
20308 | 262 |
|
263 |
fun result tac facts ctxt = |
|
264 |
let |
|
60448 | 265 |
val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt; |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
266 |
val st = Goal.init (Thm.cterm_of ctxt thesis); |
20308 | 267 |
val rule = |
59616 | 268 |
(case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of |
20308 | 269 |
NONE => raise THM ("Obtain.result: tactic failed", 0, facts) |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
270 |
| SOME th => |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
271 |
check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th))); |
20308 | 272 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
273 |
val closed_rule = Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) rule; |
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30763
diff
changeset
|
274 |
val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; |
59616 | 275 |
val obtain_rule = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
276 |
Thm.forall_elim (Thm.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule'; |
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
wenzelm
parents:
42494
diff
changeset
|
277 |
val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt'; |
20308 | 278 |
val (prems, ctxt'') = |
32199 | 279 |
Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params)) |
20308 | 280 |
(Drule.strip_imp_prems stmt) fix_ctxt; |
281 |
in ((params, prems), ctxt'') end; |
|
282 |
||
283 |
||
284 |
||
60452 | 285 |
(** guess: obtain based on tactical result **) |
286 |
||
287 |
(* |
|
288 |
<chain_facts> |
|
289 |
guess x <proof body> <proof end> == |
|
290 |
||
291 |
{ |
|
292 |
fix thesis |
|
293 |
<chain_facts> have "PROP ?guess" |
|
294 |
apply magic -- {* turns goal into "thesis ==> #thesis" *} |
|
295 |
<proof body> |
|
296 |
apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into |
|
297 |
"#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} |
|
298 |
<proof end> |
|
299 |
} |
|
300 |
fix x assm <<obtain_export>> "A x" |
|
301 |
*) |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
302 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
303 |
local |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
304 |
|
20308 | 305 |
fun unify_params vars thesis_var raw_rule ctxt = |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
306 |
let |
42360 | 307 |
val thy = Proof_Context.theory_of ctxt; |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38875
diff
changeset
|
308 |
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); |
17891 | 309 |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31794
diff
changeset
|
310 |
fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
311 |
|
19978 | 312 |
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; |
19779 | 313 |
val rule = Thm.incr_indexes (maxidx + 1) raw_rule; |
314 |
||
33368 | 315 |
val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
316 |
val m = length vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
317 |
val n = length params; |
19779 | 318 |
val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
319 |
|
19779 | 320 |
fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) |
321 |
handle Type.TUNIFY => |
|
322 |
err ("Failed to unify variable " ^ |
|
323 |
string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ |
|
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
47815
diff
changeset
|
324 |
string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule; |
33957 | 325 |
val (tyenv, _) = fold unify (map #1 vars ~~ take m params) |
19779 | 326 |
(Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
327 |
val norm_type = Envir.norm_type tyenv; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
328 |
|
19978 | 329 |
val xs = map (apsnd norm_type o fst) vars; |
33957 | 330 |
val ys = map (apsnd norm_type) (drop m params); |
20085
c5d60752587f
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20004
diff
changeset
|
331 |
val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; |
59623 | 332 |
val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys'); |
19779 | 333 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
334 |
val instT = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
335 |
fold (Term.add_tvarsT o #2) params [] |
59623 | 336 |
|> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T))); |
20308 | 337 |
val closed_rule = rule |
59623 | 338 |
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) |
20308 | 339 |
|> Thm.instantiate (instT, []); |
17891 | 340 |
|
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30763
diff
changeset
|
341 |
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; |
19978 | 342 |
val vars' = |
343 |
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ |
|
344 |
(map snd vars @ replicate (length ys) NoSyn); |
|
59623 | 345 |
val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule'; |
19978 | 346 |
in ((vars', rule''), ctxt') end; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
347 |
|
28080
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
348 |
fun inferred_type (binding, _, mx) ctxt = |
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
349 |
let |
42494 | 350 |
val x = Variable.check_name binding; |
60407 | 351 |
val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt |
19779 | 352 |
in ((x, T, mx), ctxt') end; |
353 |
||
20004
e6d3f2b031e6
guess: proper context for polymorphic parameters;
wenzelm
parents:
19978
diff
changeset
|
354 |
fun polymorphic ctxt vars = |
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19844
diff
changeset
|
355 |
let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) |
19779 | 356 |
in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; |
18693 | 357 |
|
60379 | 358 |
fun gen_guess prep_var raw_vars int state = |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
359 |
let |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
360 |
val _ = Proof.assert_forward_or_chain state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
361 |
val ctxt = Proof.context_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
362 |
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
363 |
|
60448 | 364 |
val (thesis_var, thesis) = #1 (obtain_thesis ctxt); |
60379 | 365 |
val vars = ctxt |
366 |
|> fold_map prep_var raw_vars |-> fold_map inferred_type |
|
367 |
|> fst |> polymorphic ctxt; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
368 |
|
19978 | 369 |
fun guess_context raw_rule state' = |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
370 |
let |
19978 | 371 |
val ((parms, rule), ctxt') = |
20308 | 372 |
unify_params vars thesis_var raw_rule (Proof.context_of state'); |
42501
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset
|
373 |
val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt'; |
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset
|
374 |
val ps = xs ~~ map (#2 o #1) parms; |
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset
|
375 |
val ts = map Free ps; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
376 |
val asms = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
377 |
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46215
diff
changeset
|
378 |
|> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), [])); |
19779 | 379 |
val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
380 |
in |
19978 | 381 |
state' |
382 |
|> Proof.map_context (K ctxt') |
|
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
383 |
|> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
384 |
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
385 |
(obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts)) |
59616 | 386 |
[(Thm.empty_binding, asms)]) |
60401 | 387 |
|> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts) |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
388 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
389 |
|
19779 | 390 |
val goal = Var (("guess", 0), propT); |
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset
|
391 |
val pos = Position.thread_data (); |
19779 | 392 |
fun print_result ctxt' (k, [(s, [_, th])]) = |
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset
|
393 |
Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
394 |
val before_qed = |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
395 |
Method.primitive_text (fn ctxt => |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
396 |
Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
397 |
(fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))); |
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
398 |
fun after_qed (result_ctxt, results) state' = |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
399 |
let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
400 |
in |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
401 |
state' |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
402 |
|> Proof.end_block |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
403 |
|> guess_context (check_result ctxt thesis res) |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
404 |
end; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
405 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
406 |
state |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
407 |
|> Proof.enter_forward |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
408 |
|> Proof.begin_block |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
409 |
|> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
410 |
|> Proof.chain_facts chain_facts |
60406 | 411 |
|> Proof.internal_goal print_result Proof_Context.mode_schematic "guess" |
60414 | 412 |
(SOME before_qed) after_qed [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])] |
59616 | 413 |
|> Proof.refine (Method.primitive_text (fn _ => fn _ => |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
414 |
Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
415 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
416 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
417 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
418 |
|
60379 | 419 |
val guess = gen_guess Proof_Context.cert_var; |
420 |
val guess_cmd = gen_guess Proof_Context.read_var; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
421 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
422 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
423 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
424 |
end; |