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

author | wenzelm |

Thu, 12 Apr 2012 11:34:50 +0200 | |

changeset 47431 | d9dd4a9f18fc |

parent 47430 | b254fdaf1973 |

child 47432 | e1576d13e933 |

more precise declaration of goal_tfrees in forked proof state;

--- a/src/Pure/Isar/proof.ML Thu Apr 12 11:28:36 2012 +0200 +++ b/src/Pure/Isar/proof.ML Thu Apr 12 11:34:50 2012 +0200 @@ -198,6 +198,9 @@ val context_of = #context o current; val theory_of = Proof_Context.theory_of o context_of; +fun map_node_context f = + map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); + fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); @@ -292,24 +295,27 @@ (* nested goal *) -fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = +fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) = let val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); - in State (make_node (f context, facts, mode, SOME goal'), nodes) end - | map_goal f g (State (nd, node :: nodes)) = - let val State (node', nodes') = map_goal f g (State (node, nodes)) - in map_context f (State (nd, node' :: nodes')) end - | map_goal _ _ state = state; + val node' = map_node_context h node; + in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end + | map_goal f g h (State (nd, node :: nodes)) = + let + val nd' = map_node_context f nd; + val State (node', nodes') = map_goal f g h (State (node, nodes)); + in State (nd', node' :: nodes') end + | map_goal _ _ _ state = state; fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => - (statement, [], using, goal, before_qed, after_qed)); + (statement, [], using, goal, before_qed, after_qed)) I; fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => - (statement, msg :: messages, using, goal, before_qed, after_qed)); + (statement, msg :: messages, using, goal, before_qed, after_qed)) I; fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) => - (statement, [], using, goal, before_qed, after_qed)); + (statement, [], using, goal, before_qed, after_qed)) I; local fun find i state = @@ -407,7 +413,7 @@ |> map_goal (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #> Proof_Context.add_cases true meth_cases) - (K (statement, [], using, goal', before_qed, after_qed))) + (K (statement, [], using, goal', before_qed, after_qed)) I) end; fun select_goals n meth state = @@ -717,7 +723,7 @@ let val ctxt = context_of state'; val ths = maps snd named_facts; - in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); + in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I); fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); @@ -1074,7 +1080,9 @@ val _ = assert_backward state; val (goal_ctxt, (_, goal)) = find_goal state; val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal; - val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt); + val goal_tfrees = + fold Term.add_tfrees + (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) []; val _ = is_relevant state andalso error "Cannot fork relevant proof"; @@ -1090,8 +1098,8 @@ val result_ctxt = state - |> map_contexts (fold Variable.declare_term goal_txt) |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed')) + (fold (Variable.declare_typ o TFree) goal_tfrees) |> fork_proof; val future_thm = result_ctxt |> Future.map (fn (_, x) => @@ -1099,7 +1107,7 @@ val finished_goal = Goal.future_result goal_ctxt future_thm prop'; val state' = state - |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) + |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I |> done; in (Future.map #1 result_ctxt, state') end;