1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory ML_Goal 8imports Main 9keywords "ML_goal" :: thy_goal_stmt 10begin 11 12\<comment>\<open> 13 Defines a new command `ML_goal`. `ML_goal` is similar to @{command lemma} 14 and @{command theorem} in that it specifies a goal and enters a proof state 15 for you prove that goal. 16 17 However, instead of parsing goal terms from user input, `ML_goal` uses 18 an ML block to produce a list of ML terms, and then sets up the proof state 19 to prove those terms as goals. 20 21 Each goal term must be an instance of either @{typ bool} or @{typ prop}. 22 23 There are some concrete examples in @{file ML_Goal_Test.thy}. 24\<close> 25 26ML \<open> 27 28structure ML_goal_data = Proof_Data( 29 type T = term list 30 val init = K [] 31); 32 33local 34 35\<comment>\<open> 36 Why are we stashing something into a `Proof_Data` and then immediately 37 taking it out again? 38 39 In @{ML "fn (pos, source, ctxt: Context.generic) => 40 ML_Context.expression pos source ctxt"}, 41 `source` is a fragment of ML code which gets evaluated in the ML context 42 associated with `ctxt`, which in this case should be the proof context 43 associated with the call to `ML_goal`. The result is a new generic context 44 with a new ML context, updated with the effects of evaluating `source`. 45 46 This means the only way to extract information out of `source` is via 47 its side-effects on the ML context. We have two main options: 48 49 - Declare an @{ML "Unsynchronized.ref"} in this file (ML_Goal), and stash 50 the value described by `source` into that. 51 - This is unlikely to play well with deferred or concurrent proofs. 52 53 - Use an instance of `Proof_Data` to declare some new state that's 54 associated with all proof contexts (in this case "the result of 55 the ML block passed to `ML_goal`"), and evaluate `source` in such a way 56 as to store the result there. 57 - This has more overhead compared to the `ref` solution, but it's 58 still negligible. 59 - This is the 'preferred' way to store 'local state' in contexts. 60 - This is safe for deferred or concurrent proofs. 61\<close> 62fun evaluate_goals source = 63 ML_Context.expression 64 (Input.pos_of source) 65 (ML_Lex.read "Theory.local_setup (ML_goal_data.put ((" 66 @ ML_Lex.read_source source 67 @ ML_Lex.read "): term list))") 68 |> Context.proof_map 69 #> ML_goal_data.get; 70 71fun err_msg_bad_type goal (typ: typ) ctxt = 72 "The goal " ^ (@{make_string} (Syntax.pretty_term ctxt goal)) ^ " " ^ 73 "has unsupported type " ^ (@{make_string} typ) ^ ". " ^ 74 "The ML_goal command expects either a " ^ (@{make_string} @{typ bool}) ^ " " ^ 75 "or a " ^ (@{make_string} @{typ prop}) ^ "."; 76 77fun begin_proof ((name, attrs): Attrib.binding, ml_block: Input.source) ctxt = 78 let 79 \<comment>\<open> 80 In the very common case that a goal is a @{typ bool}, we wrap 81 it in @{term Trueprop} to keep the Proof.theorem command happy. 82 \<close> 83 fun prop_wrap goal = 84 case Term.type_of goal of 85 @{typ bool} => goal |> HOLogic.mk_Trueprop 86 | @{typ prop} => goal 87 | other => error (err_msg_bad_type goal other ctxt); 88 89 val goals = 90 evaluate_goals ml_block ctxt 91 |> List.map prop_wrap 92 93 \<comment>\<open> Ensures free variables are type-consistent. \<close> 94 |> Syntax.check_props ctxt 95 |> List.map (rpair []); 96 97 \<comment>\<open> 98 Figures out that the `folded` in `[folded foo]` means 99 @{attribute folded}. Required for attributes to work. 100 \<close> 101 val parsed_attrs = map (Attrib.check_src ctxt) attrs; 102 val binding = (name, parsed_attrs); 103 104 val start_pos = Position.thread_data (); 105 106 fun after_qed (results: thm list list) ctxt = 107 let 108 val thms = results |> hd; 109 val ((res_name, res), ctxt') = 110 Local_Theory.note (binding, thms) ctxt; 111 val _ = 112 Proof_Display.print_results true start_pos ctxt' 113 (("theorem", res_name), [("", res)]) 114 in ctxt' end 115 in 116 Proof.theorem NONE 117 after_qed 118 [goals] ctxt 119 end; 120 121val ML_goal_cmd = 122 Scan.optional (Parse_Spec.opt_thm_name ":") Binding.empty_atts 123 -- Parse.ML_source 124 >> begin_proof 125 126val _ = 127 Outer_Syntax.local_theory_to_proof 128 \<^command_keyword>\<open>ML_goal\<close> 129 "ML-provided goal" 130 ML_goal_cmd; 131 132in end 133\<close> 134 135end