800 specifications of function definitions, inductive predicates and so on. In |
800 specifications of function definitions, inductive predicates and so on. In |
801 Chapter~\ref{chp:package}, for example, we will need to parse specifications |
801 Chapter~\ref{chp:package}, for example, we will need to parse specifications |
802 for inductive predicates of the form: |
802 for inductive predicates of the form: |
803 *} |
803 *} |
804 |
804 |
|
805 |
805 simple_inductive |
806 simple_inductive |
806 even and odd |
807 even and odd |
807 where |
808 where |
808 even0: "even 0" |
809 even0: "even 0" |
809 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
810 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
810 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
811 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
811 |
|
812 |
812 |
813 text {* |
813 text {* |
814 For this we are going to use the parser: |
814 For this we are going to use the parser: |
815 *} |
815 *} |
816 |
816 |
1200 |
1200 |
1201 (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory}) |
1201 (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory}) |
1202 |
1202 |
1203 *} |
1203 *} |
1204 |
1204 |
1205 ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*} |
1205 ML {* |
|
1206 structure Result = Proof_Data( |
|
1207 type T = unit -> term |
|
1208 fun init thy () = error "Result") |
|
1209 |
|
1210 val result_cookie = (Result.get, Result.put, "Result.put") |
|
1211 *} |
|
1212 |
1206 ML{*let |
1213 ML{*let |
1207 fun after_qed thm_name thms lthy = |
1214 fun after_qed thm_name thms lthy = |
1208 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
1215 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
1209 |
1216 |
1210 fun setup_proof (thm_name, (txt, pos)) lthy = |
1217 fun setup_proof (thm_name, (txt, pos)) lthy = |
1211 let |
1218 let |
1212 val trm = ML_Context.evaluate lthy true ("r", r) txt |
1219 val trm = Code_Runtime.value lthy result_cookie ("", txt) |
1213 in |
1220 in |
1214 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
1221 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
1215 end |
1222 end |
1216 |
1223 |
1217 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
1224 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
|
1225 |
1218 in |
1226 in |
1219 Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
1227 Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
1220 Keyword.thy_goal (parser >> setup_proof) |
1228 Keyword.thy_goal (parser >> setup_proof) |
1221 end*} |
1229 end*} |
1222 |
1230 |
|
1231 (* |
1223 foobar_prove test: {* @{prop "True"} *} |
1232 foobar_prove test: {* @{prop "True"} *} |
1224 apply(rule TrueI) |
1233 apply(rule TrueI) |
1225 done |
1234 done |
|
1235 *) |
1226 |
1236 |
1227 (* |
1237 (* |
1228 ML {* |
1238 ML {* |
1229 structure TacticData = ProofDataFun |
1239 structure TacticData = ProofDataFun |
1230 ( |
1240 ( |