summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Pure/Isar/proof.ML

changeset 47431 | d9dd4a9f18fc |

parent 47416 | df8fc0567a3d |

child 47815 | 43f677b3ae91 |

1.1 --- a/src/Pure/Isar/proof.ML Thu Apr 12 11:28:36 2012 +0200 1.2 +++ b/src/Pure/Isar/proof.ML Thu Apr 12 11:34:50 2012 +0200 1.3 @@ -198,6 +198,9 @@ 1.4 val context_of = #context o current; 1.5 val theory_of = Proof_Context.theory_of o context_of; 1.6 1.7 +fun map_node_context f = 1.8 + map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 1.9 + 1.10 fun map_context f = 1.11 map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 1.12 1.13 @@ -292,24 +295,27 @@ 1.14 1.15 (* nested goal *) 1.16 1.17 -fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = 1.18 +fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) = 1.19 let 1.20 val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; 1.21 val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); 1.22 - in State (make_node (f context, facts, mode, SOME goal'), nodes) end 1.23 - | map_goal f g (State (nd, node :: nodes)) = 1.24 - let val State (node', nodes') = map_goal f g (State (node, nodes)) 1.25 - in map_context f (State (nd, node' :: nodes')) end 1.26 - | map_goal _ _ state = state; 1.27 + val node' = map_node_context h node; 1.28 + in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end 1.29 + | map_goal f g h (State (nd, node :: nodes)) = 1.30 + let 1.31 + val nd' = map_node_context f nd; 1.32 + val State (node', nodes') = map_goal f g h (State (node, nodes)); 1.33 + in State (nd', node' :: nodes') end 1.34 + | map_goal _ _ _ state = state; 1.35 1.36 fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => 1.37 - (statement, [], using, goal, before_qed, after_qed)); 1.38 + (statement, [], using, goal, before_qed, after_qed)) I; 1.39 1.40 fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => 1.41 - (statement, msg :: messages, using, goal, before_qed, after_qed)); 1.42 + (statement, msg :: messages, using, goal, before_qed, after_qed)) I; 1.43 1.44 fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) => 1.45 - (statement, [], using, goal, before_qed, after_qed)); 1.46 + (statement, [], using, goal, before_qed, after_qed)) I; 1.47 1.48 local 1.49 fun find i state = 1.50 @@ -407,7 +413,7 @@ 1.51 |> map_goal 1.52 (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #> 1.53 Proof_Context.add_cases true meth_cases) 1.54 - (K (statement, [], using, goal', before_qed, after_qed))) 1.55 + (K (statement, [], using, goal', before_qed, after_qed)) I) 1.56 end; 1.57 1.58 fun select_goals n meth state = 1.59 @@ -717,7 +723,7 @@ 1.60 let 1.61 val ctxt = context_of state'; 1.62 val ths = maps snd named_facts; 1.63 - in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); 1.64 + in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I); 1.65 1.66 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; 1.67 fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); 1.68 @@ -1074,7 +1080,9 @@ 1.69 val _ = assert_backward state; 1.70 val (goal_ctxt, (_, goal)) = find_goal state; 1.71 val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal; 1.72 - val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt); 1.73 + val goal_tfrees = 1.74 + fold Term.add_tfrees 1.75 + (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) []; 1.76 1.77 val _ = is_relevant state andalso error "Cannot fork relevant proof"; 1.78 1.79 @@ -1090,8 +1098,8 @@ 1.80 1.81 val result_ctxt = 1.82 state 1.83 - |> map_contexts (fold Variable.declare_term goal_txt) 1.84 |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed')) 1.85 + (fold (Variable.declare_typ o TFree) goal_tfrees) 1.86 |> fork_proof; 1.87 1.88 val future_thm = result_ctxt |> Future.map (fn (_, x) => 1.89 @@ -1099,7 +1107,7 @@ 1.90 val finished_goal = Goal.future_result goal_ctxt future_thm prop'; 1.91 val state' = 1.92 state 1.93 - |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) 1.94 + |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I 1.95 |> done; 1.96 in (Future.map #1 result_ctxt, state') end; 1.97