author | wenzelm |
Mon, 03 Jul 2006 19:33:09 +0200 | |
changeset 19978 | df19a7876183 |
parent 19906 | c23a0e65b285 |
child 20004 | e6d3f2b031e6 |
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 |
ID: $Id$ |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
4 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
5 |
The 'obtain' and 'guess' language elements -- generalized existence at |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
6 |
the level of proof texts: 'obtain' involves a proof that certain |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
7 |
fixes/assumes may be introduced into the present context; 'guess' is |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
8 |
similar, but derives these elements from the course of reasoning! |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
9 |
|
9468 | 10 |
<chain_facts> |
18870 | 11 |
obtain x where "A x" <proof> == |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
12 |
|
18870 | 13 |
have "!!thesis. (!!x. A x ==> thesis) ==> thesis" |
12970 | 14 |
proof succeed |
9468 | 15 |
fix thesis |
18870 | 16 |
assume that [intro?]: "!!x. A x ==> thesis" |
17 |
<chain_facts> |
|
18 |
show thesis |
|
19 |
apply (insert that) |
|
20 |
<proof> |
|
12970 | 21 |
qed |
18870 | 22 |
fix x assm <<obtain_export>> "A x" |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
23 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
24 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
25 |
<chain_facts> |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
26 |
guess x <proof body> <proof end> == |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
27 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
28 |
{ |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
29 |
fix thesis |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
30 |
<chain_facts> have "PROP ?guess" |
18870 | 31 |
apply magic -- {* turns goal into "thesis ==> #thesis" *} |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
32 |
<proof body> |
18870 | 33 |
apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into |
34 |
"#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
35 |
<proof end> |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
36 |
} |
18870 | 37 |
fix x assm <<obtain_export>> "A x" |
8094 | 38 |
*) |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
39 |
|
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
40 |
signature OBTAIN = |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
41 |
sig |
19844 | 42 |
val obtain: string -> (string * string option * mixfix) list -> |
19585 | 43 |
((string * Attrib.src list) * (string * string list) list) list |
17357 | 44 |
-> bool -> Proof.state -> Proof.state |
19844 | 45 |
val obtain_i: string -> (string * typ option * mixfix) list -> |
19585 | 46 |
((string * attribute list) * (term * term list) list) list |
17357 | 47 |
-> bool -> Proof.state -> Proof.state |
19844 | 48 |
val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
49 |
val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
|
18897 | 50 |
val statement: (string * ((string * 'typ option) list * 'term list)) list -> |
51 |
(('typ, 'term, 'fact) Element.ctxt list * |
|
19585 | 52 |
((string * Attrib.src list) * ('term * 'term list) list) list) * |
53 |
(((string * Attrib.src list) * (term * term list) list) list -> Proof.context -> |
|
54 |
(((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context) |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
55 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
56 |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
57 |
structure Obtain: OBTAIN = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
58 |
struct |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
59 |
|
8094 | 60 |
|
18670 | 61 |
(** obtain_export **) |
62 |
||
18870 | 63 |
(* |
18897 | 64 |
[x, A x] |
65 |
: |
|
66 |
B |
|
67 |
-------- |
|
68 |
B |
|
18870 | 69 |
*) |
18678 | 70 |
fun obtain_export ctxt parms rule cprops thm = |
9468 | 71 |
let |
19978 | 72 |
val {thy, prop, ...} = Thm.rep_thm thm; |
73 |
val concl = Logic.strip_assums_concl prop; |
|
74 |
val bads = Term.fold_aterms (fn v as Free (x, _) => |
|
75 |
if member (op =) parms x then insert (op aconv) v else I | _ => I) concl []; |
|
9468 | 76 |
|
19978 | 77 |
val thm' = thm |> Drule.implies_intr_protected cprops; |
78 |
val thm'' = thm' |> Thm.generalize ([], parms) (Thm.maxidx_of thm' + 1); |
|
18040
c67505cdecad
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17974
diff
changeset
|
79 |
val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI); |
9468 | 80 |
in |
81 |
if not (null bads) then |
|
18678 | 82 |
error ("Conclusion contains obtained parameters: " ^ |
83 |
space_implode " " (map (ProofContext.string_of_term ctxt) bads)) |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
84 |
else if not (ObjectLogic.is_judgment thy concl) then |
19978 | 85 |
error "Conclusion in obtained context must be object-logic judgment" |
86 |
else (Tactic.rtac thm'' THEN' RANGE elim_tacs) 1 rule |
|
9468 | 87 |
end; |
88 |
||
89 |
||
90 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
91 |
(** obtain **) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
92 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
93 |
fun bind_judgment ctxt name = |
18670 | 94 |
let |
95 |
val (bind, _) = ProofContext.bind_fixes [name] ctxt; |
|
96 |
val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name); |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
97 |
in (v, t) end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
98 |
|
18897 | 99 |
val thatN = "that"; |
100 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
101 |
local |
8094 | 102 |
|
18897 | 103 |
fun gen_obtain prep_att prep_vars prep_propp |
104 |
name raw_vars raw_asms int state = |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
105 |
let |
9468 | 106 |
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
|
107 |
val ctxt = Proof.context_of state; |
18678 | 108 |
val thy = Proof.theory_of state; |
17357 | 109 |
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
110 |
|
8543 | 111 |
(*obtain vars*) |
19844 | 112 |
val (vars, vars_ctxt) = prep_vars raw_vars ctxt; |
18670 | 113 |
val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
114 |
val xs = map #1 vars; |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
115 |
|
8543 | 116 |
(*obtain asms*) |
11890 | 117 |
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19300
diff
changeset
|
118 |
val asm_props = maps (map fst) proppss; |
18678 | 119 |
val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; |
10464 | 120 |
|
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19844
diff
changeset
|
121 |
val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
122 |
|
12970 | 123 |
(*obtain statements*) |
16606 | 124 |
val thesisN = Term.variant xs AutoBind.thesisN; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
125 |
val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN; |
9468 | 126 |
|
10582 | 127 |
fun occs_var x = Library.get_first (fn t => |
18151 | 128 |
Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props; |
19978 | 129 |
val parms = |
130 |
map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (map occs_var xs ~~ xs); |
|
10582 | 131 |
|
18897 | 132 |
val that_name = if name = "" then thatN else name; |
10582 | 133 |
val that_prop = |
19978 | 134 |
Term.list_all_free (map #1 parms, Logic.list_implies (asm_props, thesis)) |
135 |
|> Library.curry Logic.list_rename_params (map #2 parms); |
|
12970 | 136 |
val obtain_prop = |
137 |
Logic.list_rename_params ([AutoBind.thesisN], |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
138 |
Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis))); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
139 |
|
18124 | 140 |
fun after_qed _ = |
17357 | 141 |
Proof.local_qed (NONE, false) |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
142 |
#> Seq.map (`Proof.the_fact #-> (fn rule => |
19844 | 143 |
Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars) |
19978 | 144 |
#> Proof.assm_i (K (obtain_export ctxt (map (#1 o #1) parms) rule)) asms)); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
145 |
in |
8094 | 146 |
state |
9468 | 147 |
|> Proof.enter_forward |
19585 | 148 |
|> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
149 |
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd |
19844 | 150 |
|> Proof.fix_i [(thesisN, NONE, NoSyn)] |
19585 | 151 |
|> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])] |
16842 | 152 |
|> `Proof.the_facts |
17357 | 153 |
||> Proof.chain_facts chain_facts |
19585 | 154 |
||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false |
18907 | 155 |
|-> Proof.refine_insert |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
156 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
157 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
158 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
159 |
|
18728 | 160 |
val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp; |
17111 | 161 |
val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp; |
8094 | 162 |
|
163 |
end; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
164 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
165 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
166 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
167 |
(** guess **) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
168 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
169 |
local |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
170 |
|
19978 | 171 |
fun unify_params vars thesis_name raw_rule ctxt = |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
172 |
let |
18678 | 173 |
val thy = ProofContext.theory_of ctxt; |
19978 | 174 |
val certT = Thm.ctyp_of thy; |
175 |
val cert = Thm.cterm_of thy; |
|
17891 | 176 |
val string_of_typ = ProofContext.string_of_typ ctxt; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
177 |
val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt); |
17891 | 178 |
|
18678 | 179 |
fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
180 |
|
19978 | 181 |
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; |
19779 | 182 |
val rule = Thm.incr_indexes (maxidx + 1) raw_rule; |
183 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
184 |
val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
185 |
val m = length vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
186 |
val n = length params; |
19779 | 187 |
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
|
188 |
|
19779 | 189 |
fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) |
190 |
handle Type.TUNIFY => |
|
191 |
err ("Failed to unify variable " ^ |
|
192 |
string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ |
|
193 |
string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule; |
|
19978 | 194 |
val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params)) |
19779 | 195 |
(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
|
196 |
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
|
197 |
|
19978 | 198 |
val xs = map (apsnd norm_type o fst) vars; |
19779 | 199 |
val ys = map (apsnd norm_type) (Library.drop (m, params)); |
19906 | 200 |
val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys; |
19978 | 201 |
val terms = map (Drule.mk_term o cert o Free) (xs @ ys'); |
19779 | 202 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
203 |
val instT = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
204 |
fold (Term.add_tvarsT o #2) params [] |
19978 | 205 |
|> map (TVar #> (fn T => (certT T, certT (norm_type T)))); |
206 |
val (rule' :: terms', ctxt') = |
|
207 |
Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt; |
|
17891 | 208 |
|
19978 | 209 |
val vars' = |
210 |
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ |
|
211 |
(map snd vars @ replicate (length ys) NoSyn); |
|
212 |
val rule'' = Thm.generalize ([], [thesis_name]) (Thm.maxidx_of rule' + 1) rule'; |
|
213 |
in ((vars', rule''), ctxt') end; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
214 |
|
18693 | 215 |
fun inferred_type (x, _, mx) ctxt = |
18769 | 216 |
let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt |
19779 | 217 |
in ((x, T, mx), ctxt') end; |
218 |
||
219 |
fun polymorphic (vars, ctxt) = |
|
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19844
diff
changeset
|
220 |
let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) |
19779 | 221 |
in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; |
18693 | 222 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
223 |
fun gen_guess prep_vars raw_vars int state = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
224 |
let |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
225 |
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
|
226 |
val thy = Proof.theory_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
227 |
val ctxt = Proof.context_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
228 |
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
|
229 |
|
19978 | 230 |
val ((thesis_name, _), thesis) = bind_judgment ctxt AutoBind.thesisN; |
19844 | 231 |
val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
232 |
|
17974 | 233 |
fun check_result th = |
234 |
(case Thm.prems_of th of |
|
235 |
[prem] => |
|
236 |
if Thm.concl_of th aconv thesis andalso |
|
237 |
Logic.strip_assums_concl prem aconv thesis then () |
|
18678 | 238 |
else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th) |
239 |
| [] => error "Goal solved -- nothing guessed." |
|
240 |
| _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th)); |
|
17891 | 241 |
|
19978 | 242 |
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
|
243 |
let |
19978 | 244 |
val ((parms, rule), ctxt') = |
245 |
unify_params vars thesis_name raw_rule (Proof.context_of state'); |
|
246 |
val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt'; |
|
247 |
val ts = map (bind o Free o #1) parms; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
248 |
val ps = map dest_Free ts; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
249 |
val asms = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
250 |
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |
19585 | 251 |
|> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), [])); |
19779 | 252 |
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
|
253 |
in |
19978 | 254 |
state' |
255 |
|> Proof.map_context (K ctxt') |
|
256 |
|> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms) |
|
257 |
|> Proof.assm_i (K (obtain_export ctxt' (map #1 ps) rule)) [(("", []), asms)] |
|
258 |
|> Proof.add_binds_i AutoBind.no_facts |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
259 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
260 |
|
19779 | 261 |
val goal = Var (("guess", 0), propT); |
262 |
fun print_result ctxt' (k, [(s, [_, th])]) = |
|
263 |
ProofDisplay.print_results int ctxt' (k, [(s, [th])]); |
|
264 |
val before_qed = SOME (Method.primitive_text (Goal.conclude #> (fn th => |
|
265 |
Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)))); |
|
266 |
fun after_qed [[_, res]] = |
|
19978 | 267 |
(check_result res; Proof.end_block #> Seq.map (guess_context res)); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
268 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
269 |
state |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
270 |
|> Proof.enter_forward |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
271 |
|> Proof.begin_block |
19844 | 272 |
|> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)] |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
273 |
|> Proof.chain_facts chain_facts |
19779 | 274 |
|> Proof.local_goal print_result (K I) (apsnd (rpair I)) |
275 |
"guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])] |
|
18151 | 276 |
|> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
277 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
278 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
279 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
280 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
281 |
val guess = gen_guess ProofContext.read_vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
282 |
val guess_i = gen_guess ProofContext.cert_vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
283 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
284 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
285 |
|
18897 | 286 |
|
287 |
||
288 |
(** statements with several cases **) |
|
289 |
||
290 |
fun statement cases = |
|
291 |
let |
|
18907 | 292 |
val names = |
293 |
cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); |
|
18897 | 294 |
val elems = cases |> map (fn (_, (vars, _)) => |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19300
diff
changeset
|
295 |
Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))); |
19585 | 296 |
val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props)); |
18897 | 297 |
|
298 |
fun mk_stmt stmt ctxt = |
|
299 |
let |
|
300 |
val thesis = |
|
301 |
ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; |
|
18907 | 302 |
val atts = map Attrib.internal |
303 |
[RuleCases.consumes (~ (length cases)), RuleCases.case_names names]; |
|
304 |
||
18897 | 305 |
fun assume_case ((name, (vars, _)), (_, propp)) ctxt' = |
306 |
let |
|
307 |
val xs = map fst vars; |
|
308 |
val props = map fst propp; |
|
309 |
val (parms, ctxt'') = |
|
310 |
ctxt' |
|
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19844
diff
changeset
|
311 |
|> fold Variable.declare_term props |
18897 | 312 |
|> fold_map ProofContext.inferred_param xs; |
313 |
val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); |
|
314 |
in |
|
315 |
ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); |
|
316 |
ctxt' |> ProofContext.add_assms_i ProofContext.assume_export |
|
19585 | 317 |
[((name, [ContextRules.intro_query NONE]), [(asm, [])])] |
18897 | 318 |
|>> (fn [(_, [th])] => th) |
319 |
end; |
|
320 |
val (ths, ctxt') = ctxt |
|
321 |
|> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) |
|
322 |
|> fold_map assume_case (cases ~~ stmt) |
|
323 |
|-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths); |
|
19585 | 324 |
in (([(("", atts), [(thesis, [])])], ths), ctxt') end; |
18897 | 325 |
in ((elems, concl), mk_stmt) end; |
326 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
327 |
end; |