summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Wed, 13 Nov 2002 15:34:35 +0100 | |

changeset 13712 | 82d7fc25a225 |

parent 13711 | 5ace1cccb612 |

child 13713 | 34ef15959ce7 |

Added simple_prove_goal_cterm.

src/Pure/goals.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/goals.ML Wed Nov 13 15:34:01 2002 +0100 +++ b/src/Pure/goals.ML Wed Nov 13 15:34:35 2002 +0100 @@ -72,6 +72,7 @@ val prove_goalw_cterm_nocheck : thm list->cterm->(thm list->tactic list)->thm val quick_and_dirty_prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm + val simple_prove_goal_cterm : cterm->(thm list->tactic list)->thm val push_proof : unit -> unit val read : string -> term val ren : string -> int -> unit @@ -972,6 +973,21 @@ fun Goal s = atomic_goal (Context.the_context ()) s; fun Goalw thms s = atomic_goalw (Context.the_context ()) thms s; +(*simple version with minimal amount of checking and postprocessing*) +fun simple_prove_goal_cterm G f = + let + val As = Drule.strip_imp_prems G; + val B = Drule.strip_imp_concl G; + val asms = map (norm_hhf_rule o assume) As; + fun check None = error "prove_goal: tactic failed" + | check (Some (thm, _)) = (case nprems_of thm of + 0 => thm + | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!")) + in + standard (implies_intr_list As + (check (Seq.pull (EVERY (f asms) (trivial B))))) + end; + (*Proof step "by" the given tactic -- apply tactic to the proof state*) fun by_com tac ((th,ths), pairs) : gstack =