# HG changeset patch # User wenzelm # Date 975611212 -3600 # Node ID 7f239ef89c5031c156d683c56eb964a5f40757e9 # Parent a177b85710262b9885da8cdb0c153254b340285b removed get_goal; suffer schematic (top-level) goals; diff -r a177b8571026 -r 7f239ef89c50 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Nov 30 20:05:54 2000 +0100 +++ b/src/Pure/Isar/proof.ML Thu Nov 30 20:06:52 2000 +0100 @@ -28,7 +28,6 @@ val reset_thms: string -> state -> state val the_facts: state -> thm list val the_fact: state -> thm - val get_goal: state -> term * (thm list * thm) val goal_facts: (state -> thm list) -> state -> state val use_facts: state -> state val reset_facts: state -> state @@ -244,14 +243,11 @@ (* goal *) -fun find_goal i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal)) - | find_goal i (State (Node {goal = None, ...}, node :: nodes)) = - find_goal (i + 1) (State (node, nodes)) - | find_goal _ (state as State (_, [])) = err_malformed "find_goal" state; - -fun get_goal state = - let val (_, (_, (((_, _, t), goal), _))) = find_goal 0 state - in (t, goal) end; +local + fun find i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal)) + | find i (State (Node {goal = None, ...}, node :: nodes)) = find (i + 1) (State (node, nodes)) + | find _ (state as State (_, [])) = err_malformed "find_goal" state; +in val find_goal = find 0 end; fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal)); @@ -351,14 +347,14 @@ else "")), Pretty.str ""] @ (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @ (if ! verbose orelse mode = Forward then - (pretty_facts "" facts @ pretty_goal (find_goal 0 state)) + (pretty_facts "" facts @ pretty_goal (find_goal state)) else if mode = ForwardChain then pretty_facts "picking " facts - else pretty_goal (find_goal 0 state)) + else pretty_goal (find_goal state)) in Pretty.writeln (Pretty.chunks prts) end; fun pretty_goals main_goal state = - let val (_, (_, ((_, (_, thm)), _))) = find_goal 0 state - in Locale.pretty_sub_goals main_goal (!goals_limit) thm end; + let val (_, (_, ((_, (_, thm)), _))) = find_goal state + in Locale.pretty_sub_goals main_goal (! goals_limit) thm end; @@ -383,7 +379,7 @@ fun gen_refine current_context meth_fun state = let - val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal 0 state; + val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal state; val Method meth = meth_fun (if current_context then context_of state else goal_ctxt); fun refn (thm', cases) = @@ -416,7 +412,7 @@ fun export_goal print_rule raw_rule inner state = let - val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state; + val (outer, (_, ((result, (facts, thm)), f))) = find_goal state; val (exp_tac, tacs) = ProofContext.export_wrt true inner (Some outer); fun exp_rule rule = let @@ -465,7 +461,7 @@ in if not (null bad_hyps) then err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps)) - else if not (t aconv prop) then + else if not (Pattern.matches (Sign.tsig_of (sign_of state)) (t, prop)) then err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) else thm end; @@ -593,7 +589,16 @@ |> map_context_result (fn ct => prepp (ct, [[raw_propp]])); val cprop = Thm.cterm_of (sign_of state') prop; val goal = Drule.mk_triv_goal cprop; + + val tvars = Term.term_tvars prop; + val vars = Term.term_vars prop; in + if null tvars then () + else raise STATE ("Goal statement contains illegal schematic type variable(s): " ^ + commas (map (Syntax.string_of_vname o #1) tvars), state); + if null vars then () + else warning ("Goal statement contains unbound schematic variable(s): " ^ + commas (map (Sign.string_of_term (sign_of state)) vars)); state' |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds)) |> map_context (ProofContext.add_cases (RuleCases.make true goal [antN])) @@ -608,10 +613,10 @@ fun global_goal prepp kind name atts x thy = setup_goal I prepp kind Seq.single name atts x (init_state thy); -val theorem = global_goal ProofContext.bind_propp Theorem; -val theorem_i = global_goal ProofContext.bind_propp_i Theorem; -val lemma = global_goal ProofContext.bind_propp Lemma; -val lemma_i = global_goal ProofContext.bind_propp_i Lemma; +val theorem = global_goal ProofContext.bind_propp_schematic Theorem; +val theorem_i = global_goal ProofContext.bind_propp_schematic_i Theorem; +val lemma = global_goal ProofContext.bind_propp_schematic Lemma; +val lemma_i = global_goal ProofContext.bind_propp_schematic_i Lemma; (*local goals*) @@ -712,7 +717,7 @@ val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state); in (thy', {kind = kind_name kind, name = name, thm = result'}) end; -(*Note: should inspect first result only, backtracking may destroy theory*) +(*note: clients should inspect first result only, as backtracking may destroy theory*) fun global_qed finalize state = state |> end_proof true