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