38 *) |
38 *) |
39 |
39 |
40 signature OBTAIN = |
40 signature OBTAIN = |
41 sig |
41 sig |
42 val obtain: string -> (string * string option) list -> |
42 val obtain: string -> (string * string option) list -> |
43 ((string * Attrib.src list) * (string * (string list * string list)) list) list |
43 ((string * Attrib.src list) * (string * string list) list) list |
44 -> bool -> Proof.state -> Proof.state |
44 -> bool -> Proof.state -> Proof.state |
45 val obtain_i: string -> (string * typ option) list -> |
45 val obtain_i: string -> (string * typ option) list -> |
46 ((string * attribute list) * (term * (term list * term list)) list) list |
46 ((string * attribute list) * (term * term list) list) list |
47 -> bool -> Proof.state -> Proof.state |
47 -> bool -> Proof.state -> Proof.state |
48 val guess: (string * string option) list -> bool -> Proof.state -> Proof.state |
48 val guess: (string * string option) list -> bool -> Proof.state -> Proof.state |
49 val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state |
49 val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state |
50 val statement: (string * ((string * 'typ option) list * 'term list)) list -> |
50 val statement: (string * ((string * 'typ option) list * 'term list)) list -> |
51 (('typ, 'term, 'fact) Element.ctxt list * |
51 (('typ, 'term, 'fact) Element.ctxt list * |
52 ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list) * |
52 ((string * Attrib.src list) * ('term * 'term list) list) list) * |
53 (((string * Attrib.src list) * (term * (term list * term list)) list) list -> Proof.context -> |
53 (((string * Attrib.src list) * (term * term list) list) list -> Proof.context -> |
54 (((string * Attrib.src list) * (term * (term list * term list)) list) list * thm list) * |
54 (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context) |
55 Proof.context) |
|
56 end; |
55 end; |
57 |
56 |
58 structure Obtain: OBTAIN = |
57 structure Obtain: OBTAIN = |
59 struct |
58 struct |
60 |
59 |
149 Proof.fix_i (xs ~~ map #2 vars) |
148 Proof.fix_i (xs ~~ map #2 vars) |
150 #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms)); |
149 #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms)); |
151 in |
150 in |
152 state |
151 state |
153 |> Proof.enter_forward |
152 |> Proof.enter_forward |
154 |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int |
153 |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int |
155 |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |
154 |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |
156 |> Proof.fix_i [(thesisN, NONE)] |
155 |> Proof.fix_i [(thesisN, NONE)] |
157 |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])] |
156 |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])] |
158 |> `Proof.the_facts |
157 |> `Proof.the_facts |
159 ||> Proof.chain_facts chain_facts |
158 ||> Proof.chain_facts chain_facts |
160 ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false |
159 ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false |
161 |-> Proof.refine_insert |
160 |-> Proof.refine_insert |
162 end; |
161 end; |
163 |
162 |
164 in |
163 in |
165 |
164 |
244 val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt; |
243 val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt; |
245 val ts = map (bind o Free) parms; |
244 val ts = map (bind o Free) parms; |
246 val ps = map dest_Free ts; |
245 val ps = map dest_Free ts; |
247 val asms = |
246 val asms = |
248 Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |
247 Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |
249 |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], []))); |
248 |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), [])); |
250 val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed"); |
249 val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed"); |
251 in |
250 in |
252 Proof.fix_i (map (apsnd SOME) parms) |
251 Proof.fix_i (map (apsnd SOME) parms) |
253 #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)] |
252 #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)] |
254 #> Proof.add_binds_i AutoBind.no_facts |
253 #> Proof.add_binds_i AutoBind.no_facts |
283 let |
282 let |
284 val names = |
283 val names = |
285 cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); |
284 cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); |
286 val elems = cases |> map (fn (_, (vars, _)) => |
285 val elems = cases |> map (fn (_, (vars, _)) => |
287 Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))); |
286 Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))); |
288 val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props)); |
287 val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props)); |
289 |
288 |
290 fun mk_stmt stmt ctxt = |
289 fun mk_stmt stmt ctxt = |
291 let |
290 let |
292 val thesis = |
291 val thesis = |
293 ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; |
292 ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; |
304 |> fold_map ProofContext.inferred_param xs; |
303 |> fold_map ProofContext.inferred_param xs; |
305 val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); |
304 val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); |
306 in |
305 in |
307 ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); |
306 ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); |
308 ctxt' |> ProofContext.add_assms_i ProofContext.assume_export |
307 ctxt' |> ProofContext.add_assms_i ProofContext.assume_export |
309 [((name, [ContextRules.intro_query NONE]), [(asm, ([], []))])] |
308 [((name, [ContextRules.intro_query NONE]), [(asm, [])])] |
310 |>> (fn [(_, [th])] => th) |
309 |>> (fn [(_, [th])] => th) |
311 end; |
310 end; |
312 val (ths, ctxt') = ctxt |
311 val (ths, ctxt') = ctxt |
313 |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) |
312 |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) |
314 |> fold_map assume_case (cases ~~ stmt) |
313 |> fold_map assume_case (cases ~~ stmt) |
315 |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths); |
314 |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths); |
316 in (([(("", atts), [(thesis, ([], []))])], ths), ctxt') end; |
315 in (([(("", atts), [(thesis, [])])], ths), ctxt') end; |
317 in ((elems, concl), mk_stmt) end; |
316 in ((elems, concl), mk_stmt) end; |
318 |
317 |
319 end; |
318 end; |