author | wenzelm |
Tue, 11 May 2021 20:19:07 +0200 | |
changeset 73675 | 6c56f2ebe157 |
parent 70734 | 31364e70ff3e |
child 74230 | d637611b41bd |
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 |
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
9 |
val obtain_thesis: Proof.context -> ((string * typ) * term) * Proof.context |
60444 | 10 |
val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list |
63019 | 11 |
val obtains_attribs: ('typ, 'term) Element.obtain list -> Token.src list |
60448 | 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 |
|
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
14 |
val parse_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list |
60448 | 15 |
val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state |
16 |
val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
17 |
val obtain: binding -> (binding * typ option * mixfix) list -> |
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
18 |
(binding * typ option * mixfix) list -> (term * term list) list list -> |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
19 |
(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
|
20 |
val obtain_cmd: binding -> (binding * string option * mixfix) list -> |
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
21 |
(binding * string option * mixfix) list -> (string * string list) list list -> |
30211 | 22 |
(Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
20308 | 23 |
val result: (Proof.context -> tactic) -> thm list -> Proof.context -> |
32199 | 24 |
((string * cterm) list * thm list) * Proof.context |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
25 |
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
|
26 |
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
|
27 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
28 |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
29 |
structure Obtain: OBTAIN = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
30 |
struct |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
31 |
|
60452 | 32 |
(** specification elements **) |
33 |
||
34 |
(* obtain_export *) |
|
18670 | 35 |
|
18870 | 36 |
(* |
18897 | 37 |
[x, A x] |
38 |
: |
|
39 |
B |
|
40 |
-------- |
|
41 |
B |
|
18870 | 42 |
*) |
21686 | 43 |
fun eliminate_term ctxt xs tm = |
44 |
let |
|
45 |
val vs = map (dest_Free o Thm.term_of) xs; |
|
46 |
val bads = Term.fold_aterms (fn t as Free v => |
|
47 |
if member (op =) vs v then insert (op aconv) t else I | _ => I) tm []; |
|
48 |
val _ = null bads orelse |
|
49 |
error ("Result contains obtained parameters: " ^ |
|
24920 | 50 |
space_implode " " (map (Syntax.string_of_term ctxt) bads)); |
21686 | 51 |
in tm end; |
52 |
||
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
53 |
fun eliminate ctxt rule xs As thm = |
9468 | 54 |
let |
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
55 |
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
|
56 |
val _ = Object_Logic.is_judgment ctxt (Thm.concl_of thm) orelse |
20308 | 57 |
error "Conclusion in obtained context must be object-logic judgment"; |
58 |
||
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
59 |
val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt; |
60949 | 60 |
val prems = Drule.strip_imp_prems (Thm.cprop_of thm'); |
9468 | 61 |
in |
20308 | 62 |
((Drule.implies_elim_list thm' (map Thm.assume prems) |
60315 | 63 |
|> Drule.implies_intr_list (map (Drule.norm_hhf_cterm ctxt') As) |
20308 | 64 |
|> Drule.forall_intr_list xs) |
65 |
COMP rule) |
|
66 |
|> Drule.implies_intr_list prems |
|
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
67 |
|> singleton (Variable.export ctxt' ctxt) |
9468 | 68 |
end; |
69 |
||
21686 | 70 |
fun obtain_export ctxt rule xs _ As = |
71 |
(eliminate ctxt rule xs As, eliminate_term ctxt xs); |
|
72 |
||
9468 | 73 |
|
60448 | 74 |
(* result declaration *) |
75 |
||
63019 | 76 |
fun case_names (obtains: ('typ, 'term) Element.obtain list) = |
77 |
obtains |> map_index (fn (i, (b, _)) => |
|
78 |
if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b); |
|
79 |
||
80 |
fun obtains_attributes obtains = |
|
81 |
[Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names (case_names obtains)]; |
|
82 |
||
83 |
fun obtains_attribs obtains = |
|
84 |
[Attrib.consumes (~ (length obtains)), Attrib.case_names (case_names obtains)]; |
|
60444 | 85 |
|
86 |
||
60448 | 87 |
(* obtain thesis *) |
88 |
||
89 |
fun obtain_thesis ctxt = |
|
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
90 |
let |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
91 |
val ([x], ctxt') = |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
92 |
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
|
93 |
val t = Object_Logic.fixed_judgment ctxt x; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
94 |
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
|
95 |
in ((v, t), ctxt') end; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
96 |
|
60448 | 97 |
|
98 |
(* obtain clauses *) |
|
99 |
||
100 |
local |
|
101 |
||
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
102 |
val mk_all_external = Logic.all_constraint o Variable.default_type; |
60481 | 103 |
|
104 |
fun mk_all_internal ctxt (y, z) t = |
|
105 |
let |
|
106 |
val T = |
|
107 |
(case AList.lookup (op =) (Term.add_frees t []) z of |
|
108 |
SOME T => T |
|
109 |
| NONE => the_default dummyT (Variable.default_type ctxt z)); |
|
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
110 |
in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end; |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
111 |
|
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
112 |
fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props = |
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
113 |
let |
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
114 |
val ((xs', vars), ctxt') = ctxt |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
115 |
|> fold_map prep_var raw_vars |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
116 |
|-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars); |
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
117 |
val xs = map (Variable.check_name o #1) vars; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
118 |
in |
60448 | 119 |
Logic.list_implies (map (parse_prop ctxt') raw_props, thesis) |
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
120 |
|> fold_rev (mk_all ctxt') (xs ~~ xs') |
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
121 |
end; |
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
122 |
|
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
123 |
fun prepare_obtains prep_clause check_terms |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
124 |
ctxt thesis (raw_obtains: ('typ, 'term) Element.obtain list) = |
60448 | 125 |
let |
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
126 |
val clauses = raw_obtains |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
127 |
|> map (fn (_, (raw_vars, raw_props)) => prep_clause ctxt thesis raw_vars raw_props) |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
128 |
|> check_terms ctxt; |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
129 |
in map fst raw_obtains ~~ clauses end; |
60448 | 130 |
|
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
131 |
val parse_clause = prepare_clause Proof_Context.read_var Syntax.parse_prop mk_all_external; |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
132 |
val cert_clause = prepare_clause Proof_Context.cert_var (K I) mk_all_internal; |
60448 | 133 |
|
134 |
in |
|
135 |
||
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
136 |
val read_obtains = prepare_obtains parse_clause Syntax.check_terms; |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
137 |
val cert_obtains = prepare_obtains cert_clause (K I); |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60475
diff
changeset
|
138 |
val parse_obtains = prepare_obtains parse_clause (K I); |
60448 | 139 |
|
140 |
end; |
|
141 |
||
142 |
||
143 |
||
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
144 |
(** consider: generalized elimination and cases rule **) |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
145 |
|
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
146 |
(* |
67721 | 147 |
consider (a) x where "A x" | (b) y where "B y" | ... \<equiv> |
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
148 |
|
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
149 |
have thesis |
67721 | 150 |
if a [intro?]: "\<And>x. A x \<Longrightarrow> thesis" |
151 |
and b [intro?]: "\<And>y. B y \<Longrightarrow> thesis" |
|
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
152 |
and ... |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
153 |
for thesis |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
154 |
apply (insert that) |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
155 |
*) |
60448 | 156 |
|
157 |
local |
|
158 |
||
159 |
fun gen_consider prep_obtains raw_obtains int state = |
|
160 |
let |
|
161 |
val _ = Proof.assert_forward_or_chain state; |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
162 |
val ctxt = Proof.context_of state; |
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
163 |
|
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
164 |
val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt; |
60448 | 165 |
val obtains = prep_obtains thesis_ctxt thesis raw_obtains; |
60456 | 166 |
val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains; |
60448 | 167 |
in |
168 |
state |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60481
diff
changeset
|
169 |
|> Proof.have true NONE (K I) |
60451
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
170 |
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |
1f2b29f78439
clarified 'consider', using structured 'have' statement;
wenzelm
parents:
60448
diff
changeset
|
171 |
(map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains) |
60456 | 172 |
[((Binding.empty, atts), [(thesis, [])])] int |
60461 | 173 |
|-> Proof.refine_insert |
60448 | 174 |
end; |
175 |
||
176 |
in |
|
177 |
||
178 |
val consider = gen_consider cert_obtains; |
|
179 |
val consider_cmd = gen_consider read_obtains; |
|
180 |
||
181 |
end; |
|
182 |
||
60446
64f48e7f921f
support to parse obtain clause without type-checking yet;
wenzelm
parents:
60444
diff
changeset
|
183 |
|
60444 | 184 |
|
60452 | 185 |
(** obtain: augmented context based on generalized existence rule **) |
186 |
||
187 |
(* |
|
67721 | 188 |
obtain (a) x where "A x" <proof> \<equiv> |
60452 | 189 |
|
67721 | 190 |
have thesis if a [intro?]: "\<And>x. A x \<Longrightarrow> thesis" for thesis |
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
191 |
apply (insert that) |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
192 |
<proof> |
60452 | 193 |
fix x assm <<obtain_export>> "A x" |
194 |
*) |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
195 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
196 |
local |
8094 | 197 |
|
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
198 |
fun gen_obtain prep_stmt prep_att that_binding raw_decls raw_fixes raw_prems raw_concls int state = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
199 |
let |
9468 | 200 |
val _ = Proof.assert_forward_or_chain state; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
201 |
|
63037 | 202 |
val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state); |
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
203 |
|
70734 | 204 |
val ({vars, propss, binds, result_binds, ...}, params_ctxt) = |
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
205 |
prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt; |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
206 |
val (decls, fixes) = chop (length raw_decls) vars ||> map #2; |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
207 |
val (premss, conclss) = chop (length raw_prems) propss; |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
208 |
val propss' = (map o map) (Logic.close_prop fixes (flat premss)) conclss; |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
209 |
|
63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63037
diff
changeset
|
210 |
val that_prop = |
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
211 |
Logic.list_rename_params (map (#1 o #2) decls) |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
212 |
(fold_rev (Logic.all o #2 o #2) decls (Logic.list_implies (flat propss', thesis))); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
213 |
|
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
214 |
val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) decls; |
60387
76359ff1090f
more careful treatment of term bindings in 'obtain' proof body;
wenzelm
parents:
60383
diff
changeset
|
215 |
val asms = |
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
216 |
map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_concls ~~ |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
217 |
map (map (rpair [])) propss'; |
10464 | 218 |
|
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
219 |
fun after_qed (result_ctxt, results) state' = |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
220 |
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
|
221 |
state' |
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
222 |
|> Proof.fix (map #1 decls) |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63057
diff
changeset
|
223 |
|> Proof.map_context (fold (Variable.bind_term o apsnd (Logic.close_term fixes)) binds) |
61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61268
diff
changeset
|
224 |
|> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms |
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
225 |
end; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
226 |
in |
8094 | 227 |
state |
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60481
diff
changeset
|
228 |
|> Proof.have true NONE after_qed |
60453
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
229 |
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |
ba9085f7433f
clarified 'obtain', using structured 'have' statement;
wenzelm
parents:
60452
diff
changeset
|
230 |
[((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])] |
63352 | 231 |
[(Binding.empty_atts, [(thesis, [])])] int |
60461 | 232 |
|-> Proof.refine_insert |
70734 | 233 |
|> Proof.map_context (fold Variable.bind_term result_binds) |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
234 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
235 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
236 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
237 |
|
63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset
|
238 |
val obtain = gen_obtain Proof_Context.cert_stmt (K I); |
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset
|
239 |
val obtain_cmd = gen_obtain Proof_Context.read_stmt Attrib.attribute_cmd; |
8094 | 240 |
|
241 |
end; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
242 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
243 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
244 |
|
20308 | 245 |
(** tactical result **) |
246 |
||
247 |
fun check_result ctxt thesis th = |
|
248 |
(case Thm.prems_of th of |
|
249 |
[prem] => |
|
250 |
if Thm.concl_of th aconv thesis andalso |
|
251 |
Logic.strip_assums_concl prem aconv thesis then th |
|
61268 | 252 |
else error ("Guessed a different clause:\n" ^ Thm.string_of_thm ctxt th) |
38875
c7a66b584147
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents:
36323
diff
changeset
|
253 |
| [] => error "Goal solved -- nothing guessed" |
61268 | 254 |
| _ => error ("Guess split into several cases:\n" ^ Thm.string_of_thm ctxt th)); |
20308 | 255 |
|
256 |
fun result tac facts ctxt = |
|
257 |
let |
|
60448 | 258 |
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
|
259 |
val st = Goal.init (Thm.cterm_of ctxt thesis); |
20308 | 260 |
val rule = |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61654
diff
changeset
|
261 |
(case SINGLE (Method.insert_tac thesis_ctxt facts 1 THEN tac thesis_ctxt) st of |
20308 | 262 |
NONE => raise THM ("Obtain.result: tactic failed", 0, facts) |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
263 |
| SOME th => |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
264 |
check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th))); |
20308 | 265 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
266 |
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
|
267 |
val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; |
59616 | 268 |
val obtain_rule = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
269 |
Thm.forall_elim (Thm.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule'; |
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset
|
270 |
val ((params, stmt), fix_ctxt) = Variable.focus_cterm NONE (Thm.cprem_of obtain_rule 1) ctxt'; |
20308 | 271 |
val (prems, ctxt'') = |
32199 | 272 |
Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params)) |
20308 | 273 |
(Drule.strip_imp_prems stmt) fix_ctxt; |
274 |
in ((params, prems), ctxt'') end; |
|
275 |
||
276 |
||
277 |
||
60452 | 278 |
(** guess: obtain based on tactical result **) |
279 |
||
280 |
(* |
|
281 |
<chain_facts> |
|
67721 | 282 |
guess x <proof body> <proof end> \<equiv> |
60452 | 283 |
|
284 |
{ |
|
285 |
fix thesis |
|
286 |
<chain_facts> have "PROP ?guess" |
|
67721 | 287 |
apply magic \<comment> \<open>turn goal into \<open>thesis \<Longrightarrow> #thesis\<close>\<close> |
60452 | 288 |
<proof body> |
67721 | 289 |
apply_end magic \<comment> \<open>turn final \<open>(\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> #thesis\<close> into\<close> |
290 |
\<comment> \<open>\<open>#((\<And>x. A x \<Longrightarrow> thesis) \<Longrightarrow> thesis)\<close> which is a finished goal state\<close> |
|
60452 | 291 |
<proof end> |
292 |
} |
|
293 |
fix x assm <<obtain_export>> "A x" |
|
294 |
*) |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
295 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
296 |
local |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
297 |
|
20308 | 298 |
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
|
299 |
let |
42360 | 300 |
val thy = Proof_Context.theory_of ctxt; |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38875
diff
changeset
|
301 |
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); |
17891 | 302 |
|
61268 | 303 |
fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
304 |
|
19978 | 305 |
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; |
19779 | 306 |
val rule = Thm.incr_indexes (maxidx + 1) raw_rule; |
307 |
||
33368 | 308 |
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
|
309 |
val m = length vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
310 |
val n = length params; |
19779 | 311 |
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
|
312 |
|
19779 | 313 |
fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) |
314 |
handle Type.TUNIFY => |
|
315 |
err ("Failed to unify variable " ^ |
|
316 |
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
|
317 |
string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule; |
33957 | 318 |
val (tyenv, _) = fold unify (map #1 vars ~~ take m params) |
19779 | 319 |
(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
|
320 |
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
|
321 |
|
19978 | 322 |
val xs = map (apsnd norm_type o fst) vars; |
33957 | 323 |
val ys = map (apsnd norm_type) (drop m params); |
20085
c5d60752587f
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20004
diff
changeset
|
324 |
val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; |
59623 | 325 |
val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys'); |
19779 | 326 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
327 |
val instT = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
328 |
fold (Term.add_tvarsT o #2) params [] |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60555
diff
changeset
|
329 |
|> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v)))); |
20308 | 330 |
val closed_rule = rule |
59623 | 331 |
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) |
20308 | 332 |
|> Thm.instantiate (instT, []); |
17891 | 333 |
|
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30763
diff
changeset
|
334 |
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; |
19978 | 335 |
val vars' = |
336 |
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ |
|
337 |
(map snd vars @ replicate (length ys) NoSyn); |
|
59623 | 338 |
val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule'; |
19978 | 339 |
in ((vars', rule''), ctxt') end; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
340 |
|
28080
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
341 |
fun inferred_type (binding, _, mx) ctxt = |
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
342 |
let |
42494 | 343 |
val x = Variable.check_name binding; |
60407 | 344 |
val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt |
19779 | 345 |
in ((x, T, mx), ctxt') end; |
346 |
||
20004
e6d3f2b031e6
guess: proper context for polymorphic parameters;
wenzelm
parents:
19978
diff
changeset
|
347 |
fun polymorphic ctxt vars = |
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19844
diff
changeset
|
348 |
let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) |
19779 | 349 |
in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; |
18693 | 350 |
|
60379 | 351 |
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
|
352 |
let |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
353 |
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
|
354 |
val ctxt = Proof.context_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
355 |
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
|
356 |
|
60448 | 357 |
val (thesis_var, thesis) = #1 (obtain_thesis ctxt); |
60379 | 358 |
val vars = ctxt |
359 |
|> fold_map prep_var raw_vars |-> fold_map inferred_type |
|
360 |
|> fst |> polymorphic ctxt; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
361 |
|
19978 | 362 |
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
|
363 |
let |
19978 | 364 |
val ((parms, rule), ctxt') = |
20308 | 365 |
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
|
366 |
val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt'; |
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset
|
367 |
val ps = xs ~~ map (#2 o #1) parms; |
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset
|
368 |
val ts = map Free ps; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
369 |
val asms = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
370 |
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
|
371 |
|> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), [])); |
19779 | 372 |
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
|
373 |
in |
19978 | 374 |
state' |
375 |
|> Proof.map_context (K ctxt') |
|
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
376 |
|> 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
|
377 |
|> `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
|
378 |
(obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts)) |
63352 | 379 |
[] [] [(Binding.empty_atts, asms)]) |
60401 | 380 |
|> 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
|
381 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
382 |
|
19779 | 383 |
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
|
384 |
val pos = Position.thread_data (); |
19779 | 385 |
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
|
386 |
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
|
387 |
val before_qed = |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
388 |
Method.primitive_text (fn ctxt => |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
389 |
Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> |
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
52456
diff
changeset
|
390 |
(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
|
391 |
fun after_qed (result_ctxt, results) state' = |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
392 |
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
|
393 |
in |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
394 |
state' |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
395 |
|> Proof.end_block |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
396 |
|> guess_context (check_result ctxt thesis res) |
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset
|
397 |
end; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
398 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
399 |
state |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
400 |
|> Proof.enter_forward |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
401 |
|> Proof.begin_block |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35845
diff
changeset
|
402 |
|> 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
|
403 |
|> Proof.chain_facts chain_facts |
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60481
diff
changeset
|
404 |
|> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess" |
60461 | 405 |
(SOME before_qed) after_qed |
63352 | 406 |
[] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])] |
60461 | 407 |
|> snd |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61654
diff
changeset
|
408 |
|> Proof.refine_singleton |
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61654
diff
changeset
|
409 |
(Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis))) |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
410 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
411 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
412 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
413 |
|
60379 | 414 |
val guess = gen_guess Proof_Context.cert_var; |
415 |
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
|
416 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
417 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
418 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
419 |
end; |