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;
 src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions
```--- 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') #>
-          (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 =
+        (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;
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.7582157,"math_prob":0.9697493,"size":3872,"snap":"2022-40-2023-06","text_gpt3_token_len":1200,"char_repetition_ratio":0.19777663,"word_repetition_ratio":0.23316912,"special_character_ratio":0.37164256,"punctuation_ratio":0.29973474,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.96488446,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2023-01-28T04:26:53Z\",\"WARC-Record-ID\":\"<urn:uuid:5823f78c-7b53-429d-be8c-51bd0d5caa2a>\",\"Content-Length\":\"13958\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:66a5de84-cf64-4b48-8d81-54a21b5e75ca>\",\"WARC-Concurrent-To\":\"<urn:uuid:ba7e0f21-c54e-4e3e-8d17-2b3cbf69de37>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"https://isabelle.in.tum.de/repos/testboard/rev/d9dd4a9f18fc\",\"WARC-Payload-Digest\":\"sha1:OKLVTULAVQYAHOG2V7UHN6JIQ6YKSJDF\",\"WARC-Block-Digest\":\"sha1:FBKDOTRWYHKJE2EFQCPELA3VANIE4ALH\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2023/CC-MAIN-2023-06/CC-MAIN-2023-06_segments_1674764499470.19_warc_CC-MAIN-20230128023233-20230128053233-00622.warc.gz\"}"}