319
|
1 |
theory Command
|
|
2 |
imports Main
|
514
|
3 |
keywords "foobar" "foobar_trace" :: thy_decl and
|
|
4 |
"foobar_goal" "foobar_prove" :: thy_goal
|
319
|
5 |
begin
|
321
|
6 |
|
565
|
7 |
ML \<open>
|
319
|
8 |
let
|
449
|
9 |
val do_nothing = Scan.succeed (Local_Theory.background_theory I)
|
319
|
10 |
in
|
520
|
11 |
Outer_Syntax.local_theory @{command_spec "foobar"}
|
|
12 |
"description of foobar"
|
|
13 |
do_nothing
|
319
|
14 |
end
|
565
|
15 |
\<close>
|
319
|
16 |
|
565
|
17 |
ML \<open>
|
319
|
18 |
let
|
321
|
19 |
fun trace_prop str =
|
449
|
20 |
Local_Theory.background_theory (fn lthy => (tracing str; lthy))
|
426
|
21 |
val trace_prop_parser = Parse.prop >> trace_prop
|
321
|
22 |
in
|
520
|
23 |
Outer_Syntax.local_theory @{command_spec "foobar_trace"}
|
|
24 |
"traces a proposition"
|
|
25 |
trace_prop_parser
|
321
|
26 |
end
|
565
|
27 |
\<close>
|
321
|
28 |
|
565
|
29 |
ML \<open>
|
321
|
30 |
let
|
|
31 |
fun prove_prop str lthy =
|
|
32 |
let
|
|
33 |
val prop = Syntax.read_prop lthy str
|
|
34 |
in
|
422
|
35 |
Proof.theorem NONE (K I) [[(prop,[])]] lthy
|
321
|
36 |
end;
|
426
|
37 |
val prove_prop_parser = Parse.prop >> prove_prop
|
321
|
38 |
in
|
520
|
39 |
Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"}
|
|
40 |
"proving a proposition"
|
|
41 |
prove_prop_parser
|
321
|
42 |
end
|
565
|
43 |
\<close>
|
321
|
44 |
|
565
|
45 |
ML \<open>
|
451
|
46 |
structure Result = Proof_Data(
|
|
47 |
type T = unit -> term
|
|
48 |
fun init thy () = error "Result")
|
|
49 |
|
|
50 |
val result_cookie = (Result.get, Result.put, "Result.put")
|
565
|
51 |
\<close>
|
451
|
52 |
|
565
|
53 |
ML\<open>
|
321
|
54 |
let
|
324
|
55 |
fun after_qed thm_name thms lthy =
|
394
|
56 |
Local_Theory.note (thm_name, (flat thms)) lthy |> snd
|
324
|
57 |
|
553
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
fun setup_proof (thm_name, {text, ...}) lthy =
|
321
|
59 |
let
|
553
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
val trm = Code_Runtime.value lthy result_cookie ("", text)
|
321
|
61 |
in
|
422
|
62 |
Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
|
324
|
63 |
end
|
321
|
64 |
|
426
|
65 |
val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
|
324
|
66 |
|
321
|
67 |
in
|
520
|
68 |
Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"}
|
|
69 |
"proving a proposition"
|
|
70 |
(parser >> setup_proof)
|
565
|
71 |
end\<close>
|
324
|
72 |
|
321
|
73 |
|
319
|
74 |
|
451
|
75 |
|
319
|
76 |
end
|