38 |
38 |
39 signature OBTAIN = |
39 signature OBTAIN = |
40 sig |
40 sig |
41 val thatN: string |
41 val thatN: string |
42 val obtain: string -> (binding * string option * mixfix) list -> |
42 val obtain: string -> (binding * string option * mixfix) list -> |
43 (Attrib.binding * (string * string list) list) list -> |
43 (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
44 bool -> Proof.state -> Proof.state |
|
45 val obtain_i: string -> (binding * typ option * mixfix) list -> |
44 val obtain_i: string -> (binding * typ option * mixfix) list -> |
46 ((binding * attribute list) * (term * term list) list) list -> |
45 (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state |
47 bool -> Proof.state -> Proof.state |
|
48 val result: (Proof.context -> tactic) -> thm list -> Proof.context -> |
46 val result: (Proof.context -> tactic) -> thm list -> Proof.context -> |
49 (cterm list * thm list) * Proof.context |
47 (cterm list * thm list) * Proof.context |
50 val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
48 val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
51 val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
49 val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
52 end; |
50 end; |
153 Proof.fix_i vars |
151 Proof.fix_i vars |
154 #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms); |
152 #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms); |
155 in |
153 in |
156 state |
154 state |
157 |> Proof.enter_forward |
155 |> Proof.enter_forward |
158 |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int |
156 |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int |
159 |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |
157 |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |
160 |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)] |
158 |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)] |
161 |> Proof.assume_i |
159 |> Proof.assume_i |
162 [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])] |
160 [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])] |
163 |> `Proof.the_facts |
161 |> `Proof.the_facts |
164 ||> Proof.chain_facts chain_facts |
162 ||> Proof.chain_facts chain_facts |
165 ||> Proof.show_i NONE after_qed [((Binding.empty, []), [(thesis, [])])] false |
163 ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false |
166 |-> Proof.refine_insert |
164 |-> Proof.refine_insert |
167 end; |
165 end; |
168 |
166 |
169 in |
167 in |
170 |
168 |
293 in |
291 in |
294 state' |
292 state' |
295 |> Proof.map_context (K ctxt') |
293 |> Proof.map_context (K ctxt') |
296 |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |
294 |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |
297 |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i |
295 |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i |
298 (obtain_export fix_ctxt rule (map cert ts)) [((Binding.empty, []), asms)]) |
296 (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)]) |
299 |> Proof.add_binds_i AutoBind.no_facts |
297 |> Proof.add_binds_i AutoBind.no_facts |
300 end; |
298 end; |
301 |
299 |
302 val goal = Var (("guess", 0), propT); |
300 val goal = Var (("guess", 0), propT); |
303 fun print_result ctxt' (k, [(s, [_, th])]) = |
301 fun print_result ctxt' (k, [(s, [_, th])]) = |
311 |> Proof.enter_forward |
309 |> Proof.enter_forward |
312 |> Proof.begin_block |
310 |> Proof.begin_block |
313 |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)] |
311 |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)] |
314 |> Proof.chain_facts chain_facts |
312 |> Proof.chain_facts chain_facts |
315 |> Proof.local_goal print_result (K I) (apsnd (rpair I)) |
313 |> Proof.local_goal print_result (K I) (apsnd (rpair I)) |
316 "guess" before_qed after_qed [((Binding.empty, []), [Logic.mk_term goal, goal])] |
314 "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])] |
317 |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd |
315 |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd |
318 end; |
316 end; |
319 |
317 |
320 in |
318 in |
321 |
319 |