author | wenzelm |
Mon, 04 Apr 2016 19:48:54 +0200 | |
changeset 62850 | 1f1a2c33ccf4 |
parent 62597 | b3f2b8c906a6 |
child 62910 | f37878ebba65 |
permissions | -rw-r--r-- |
59089 | 1 |
(* Title: HOL/ex/Cartouche_Examples.thy |
2 |
Author: Makarius |
|
3 |
*) |
|
4 |
||
59068 | 5 |
section \<open>Some examples with text cartouches\<close> |
55033 | 6 |
|
7 |
theory Cartouche_Examples |
|
8 |
imports Main |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
9 |
keywords |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
10 |
"cartouche" "term_cartouche" :: diag and |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
11 |
"text_cartouche" :: thy_decl |
55033 | 12 |
begin |
13 |
||
59068 | 14 |
subsection \<open>Regular outer syntax\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
15 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
16 |
text \<open>Text cartouches may be used in the outer syntax category "text", |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
17 |
as alternative to the traditional "verbatim" tokens. An example is |
61933 | 18 |
this text block.\<close> \<comment> \<open>The same works for small side-comments.\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
19 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
20 |
notepad |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
21 |
begin |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
22 |
txt \<open>Moreover, cartouches work as additional syntax in the |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
23 |
"altstring" category, for literal fact references. For example:\<close> |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
24 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
25 |
fix x y :: 'a |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
26 |
assume "x = y" |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
27 |
note \<open>x = y\<close> |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
28 |
have "x = y" by (rule \<open>x = y\<close>) |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
29 |
from \<open>x = y\<close> have "x = y" . |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
30 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
31 |
txt \<open>Of course, this can be nested inside formal comments and |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
32 |
antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
33 |
[OF \<open>x = y\<close>]}.\<close> |
56500
90f17a04567d
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
wenzelm
parents:
56499
diff
changeset
|
34 |
|
90f17a04567d
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
wenzelm
parents:
56499
diff
changeset
|
35 |
have "x = y" |
61933 | 36 |
by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>) \<comment> \<open>more cartouches involving ML\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
37 |
end |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
38 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
39 |
|
59068 | 40 |
subsection \<open>Outer syntax: cartouche within command syntax\<close> |
55033 | 41 |
|
59068 | 42 |
ML \<open> |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59809
diff
changeset
|
43 |
Outer_Syntax.command @{command_keyword cartouche} "" |
55033 | 44 |
(Parse.cartouche >> (fn s => |
60189 | 45 |
Toplevel.keep (fn _ => writeln s))) |
59068 | 46 |
\<close> |
55033 | 47 |
|
48 |
cartouche \<open>abc\<close> |
|
49 |
cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close> |
|
50 |
||
51 |
||
59068 | 52 |
subsection \<open>Inner syntax: string literals via cartouche\<close> |
55033 | 53 |
|
59068 | 54 |
ML \<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
55 |
local |
55033 | 56 |
fun mk_char (s, pos) = |
57 |
let |
|
58 |
val c = |
|
59 |
if Symbol.is_ascii s then ord s |
|
55036 | 60 |
else if s = "\<newline>" then 10 |
55033 | 61 |
else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); |
62597 | 62 |
in Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c end; |
55033 | 63 |
|
64 |
fun mk_string [] = Const (@{const_syntax Nil}, @{typ string}) |
|
65 |
| mk_string (s :: ss) = |
|
66 |
Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss; |
|
67 |
||
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
68 |
in |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
69 |
fun string_tr content args = |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
70 |
let fun err () = raise TERM ("string_tr", args) in |
55033 | 71 |
(case args of |
72 |
[(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => |
|
73 |
(case Term_Position.decode_position p of |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
74 |
SOME (pos, _) => c $ mk_string (content (s, pos)) $ p |
55033 | 75 |
| NONE => err ()) |
76 |
| _ => err ()) |
|
77 |
end; |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
78 |
end; |
59068 | 79 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
80 |
|
55133 | 81 |
syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
82 |
|
59068 | 83 |
parse_translation \<open> |
55133 | 84 |
[(@{syntax_const "_cartouche_string"}, |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
85 |
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] |
59068 | 86 |
\<close> |
55033 | 87 |
|
55133 | 88 |
term "\<open>\<close>" |
89 |
term "\<open>abc\<close>" |
|
90 |
term "\<open>abc\<close> @ \<open>xyz\<close>" |
|
91 |
term "\<open>\<newline>\<close>" |
|
92 |
term "\<open>\001\010\100\<close>" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
93 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
94 |
|
59068 | 95 |
subsection \<open>Alternate outer and inner syntax: string literals\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
96 |
|
59068 | 97 |
subsubsection \<open>Nested quotes\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
98 |
|
55133 | 99 |
syntax "_string_string" :: "string_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
100 |
|
59068 | 101 |
parse_translation \<open> |
55133 | 102 |
[(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))] |
59068 | 103 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
104 |
|
55133 | 105 |
term "\"\"" |
106 |
term "\"abc\"" |
|
107 |
term "\"abc\" @ \"xyz\"" |
|
108 |
term "\"\<newline>\"" |
|
109 |
term "\"\001\010\100\"" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
110 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
111 |
|
59068 | 112 |
subsubsection \<open>Term cartouche and regular quotes\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
113 |
|
59068 | 114 |
ML \<open> |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59809
diff
changeset
|
115 |
Outer_Syntax.command @{command_keyword term_cartouche} "" |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
116 |
(Parse.inner_syntax Parse.cartouche >> (fn s => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
117 |
Toplevel.keep (fn state => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
118 |
let |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
119 |
val ctxt = Toplevel.context_of state; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
120 |
val t = Syntax.read_term ctxt s; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
121 |
in writeln (Syntax.string_of_term ctxt t) end))) |
59068 | 122 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
123 |
|
55133 | 124 |
term_cartouche \<open>""\<close> |
125 |
term_cartouche \<open>"abc"\<close> |
|
126 |
term_cartouche \<open>"abc" @ "xyz"\<close> |
|
127 |
term_cartouche \<open>"\<newline>"\<close> |
|
128 |
term_cartouche \<open>"\001\010\100"\<close> |
|
55033 | 129 |
|
55047 | 130 |
|
59068 | 131 |
subsubsection \<open>Further nesting: antiquotations\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
132 |
|
61933 | 133 |
setup \<comment> "ML antiquotation" |
59068 | 134 |
\<open> |
56072 | 135 |
ML_Antiquotation.inline @{binding term_cartouche} |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
136 |
(Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
137 |
(fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) |
59068 | 138 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
139 |
|
61933 | 140 |
setup \<comment> "document antiquotation" |
59068 | 141 |
\<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
142 |
Thy_Output.antiquotation @{binding ML_cartouche} |
59809 | 143 |
(Scan.lift Args.cartouche_input) (fn {context, ...} => fn source => |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
144 |
let |
59067 | 145 |
val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");"; |
59064 | 146 |
val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks; |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
147 |
in "" end); |
59068 | 148 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
149 |
|
59068 | 150 |
ML \<open> |
55133 | 151 |
@{term_cartouche \<open>""\<close>}; |
152 |
@{term_cartouche \<open>"abc"\<close>}; |
|
153 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
154 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
155 |
@{term_cartouche \<open>"\001\010\100"\<close>}; |
|
59068 | 156 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
157 |
|
59068 | 158 |
text \<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
159 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
160 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
161 |
( |
55133 | 162 |
@{term_cartouche \<open>""\<close>}; |
163 |
@{term_cartouche \<open>"abc"\<close>}; |
|
164 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
165 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
166 |
@{term_cartouche \<open>"\001\010\100"\<close>} |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
167 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
168 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
169 |
} |
59068 | 170 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
171 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
172 |
|
59068 | 173 |
subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
174 |
|
59068 | 175 |
ML \<open> |
55110
917e799f19da
avoid breakdown of document preparation, which does not understand cartouche tokens yet;
wenzelm
parents:
55109
diff
changeset
|
176 |
Outer_Syntax.command |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59809
diff
changeset
|
177 |
@{command_keyword text_cartouche} "" |
61457 | 178 |
(Parse.opt_target -- Parse.input Parse.cartouche |
179 |
>> Thy_Output.document_command {markdown = true}) |
|
59068 | 180 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
181 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
182 |
text_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
183 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
184 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
185 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
186 |
( |
55133 | 187 |
@{term_cartouche \<open>""\<close>}; |
188 |
@{term_cartouche \<open>"abc"\<close>}; |
|
189 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
190 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
191 |
@{term_cartouche \<open>"\001\010\100"\<close>} |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
192 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
193 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
194 |
} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
195 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
196 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
197 |
|
59068 | 198 |
subsection \<open>Proof method syntax: ML tactic expression\<close> |
55047 | 199 |
|
59068 | 200 |
ML \<open> |
55047 | 201 |
structure ML_Tactic: |
202 |
sig |
|
203 |
val set: (Proof.context -> tactic) -> Proof.context -> Proof.context |
|
59064 | 204 |
val ml_tactic: Input.source -> Proof.context -> tactic |
55047 | 205 |
end = |
206 |
struct |
|
207 |
structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac); |
|
208 |
||
209 |
val set = Data.put; |
|
210 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
211 |
fun ml_tactic source ctxt = |
55047 | 212 |
let |
213 |
val ctxt' = ctxt |> Context.proof_map |
|
59064 | 214 |
(ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic" |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
215 |
"Context.map_proof (ML_Tactic.set tactic)" |
59067 | 216 |
(ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source)); |
55047 | 217 |
in Data.get ctxt' ctxt end; |
218 |
end; |
|
59068 | 219 |
\<close> |
55047 | 220 |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
221 |
|
59068 | 222 |
subsubsection \<open>Explicit version: method with cartouche argument\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
223 |
|
59068 | 224 |
method_setup ml_tactic = \<open> |
59809 | 225 |
Scan.lift Args.cartouche_input |
55047 | 226 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
59068 | 227 |
\<close> |
55047 | 228 |
|
229 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
60754 | 230 |
apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>) |
231 |
apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>) |
|
232 |
apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>) |
|
233 |
apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>) |
|
55047 | 234 |
done |
235 |
||
236 |
lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>) |
|
237 |
||
59068 | 238 |
ML \<open>@{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close> |
55047 | 239 |
|
59068 | 240 |
text \<open>@{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"}\<close> |
55047 | 241 |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
242 |
|
59068 | 243 |
subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
244 |
|
59068 | 245 |
method_setup "cartouche" = \<open> |
59809 | 246 |
Scan.lift Args.cartouche_input |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
247 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
59068 | 248 |
\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
249 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
250 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
60754 | 251 |
apply \<open>resolve_tac @{context} @{thms impI} 1\<close> |
252 |
apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close> |
|
253 |
apply \<open>resolve_tac @{context} @{thms conjI} 1\<close> |
|
254 |
apply \<open>ALLGOALS (assume_tac @{context})\<close> |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
255 |
done |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
256 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
257 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
60754 | 258 |
by (\<open>resolve_tac @{context} @{thms impI} 1\<close>, |
259 |
\<open>eresolve_tac @{context} @{thms conjE} 1\<close>, |
|
260 |
\<open>resolve_tac @{context} @{thms conjI} 1\<close>, |
|
261 |
\<open>assume_tac @{context} 1\<close>+) |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
262 |
|
59112 | 263 |
|
59128 | 264 |
subsection \<open>ML syntax\<close> |
59112 | 265 |
|
59128 | 266 |
text \<open>Input source with position information:\<close> |
59112 | 267 |
ML \<open> |
59135 | 268 |
val s: Input.source = \<open>abc123def456\<close>; |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59135
diff
changeset
|
269 |
Output.information ("Look here!" ^ Position.here (Input.pos_of s)); |
59112 | 270 |
|
271 |
\<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) => |
|
272 |
if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ()); |
|
273 |
\<close> |
|
274 |
||
59128 | 275 |
text \<open>Nested ML evaluation:\<close> |
276 |
ML \<open> |
|
277 |
ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>; |
|
278 |
ML \<open>val b = @{thm sym}\<close>; |
|
279 |
val c = @{thm trans} |
|
280 |
val thms = [a, b, c]; |
|
281 |
\<close> |
|
282 |
||
55033 | 283 |
end |