author | wenzelm |
Thu, 04 Dec 2014 20:45:11 +0100 | |
changeset 59089 | da2fef2faa83 |
parent 59068 | 8606f2ee11b1 |
child 59112 | e670969f34df |
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 |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
18 |
this text block.\<close> -- \<open>The same works for small side-comments.\<close> |
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" |
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
|
36 |
by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>) -- \<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> |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58889
diff
changeset
|
43 |
Outer_Syntax.command @{command_spec "cartouche"} "" |
55033 | 44 |
(Parse.cartouche >> (fn s => |
45 |
Toplevel.imperative (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 |
val mk_nib = |
57 |
Syntax.const o Lexicon.mark_const o |
|
58 |
fst o Term.dest_Const o HOLogic.mk_nibble; |
|
59 |
||
60 |
fun mk_char (s, pos) = |
|
61 |
let |
|
62 |
val c = |
|
63 |
if Symbol.is_ascii s then ord s |
|
55036 | 64 |
else if s = "\<newline>" then 10 |
55033 | 65 |
else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); |
66 |
in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end; |
|
67 |
||
68 |
fun mk_string [] = Const (@{const_syntax Nil}, @{typ string}) |
|
69 |
| mk_string (s :: ss) = |
|
70 |
Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss; |
|
71 |
||
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
72 |
in |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
73 |
fun string_tr content args = |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
74 |
let fun err () = raise TERM ("string_tr", args) in |
55033 | 75 |
(case args of |
76 |
[(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => |
|
77 |
(case Term_Position.decode_position p of |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
78 |
SOME (pos, _) => c $ mk_string (content (s, pos)) $ p |
55033 | 79 |
| NONE => err ()) |
80 |
| _ => err ()) |
|
81 |
end; |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
82 |
end; |
59068 | 83 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
84 |
|
55133 | 85 |
syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
86 |
|
59068 | 87 |
parse_translation \<open> |
55133 | 88 |
[(@{syntax_const "_cartouche_string"}, |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
89 |
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] |
59068 | 90 |
\<close> |
55033 | 91 |
|
55133 | 92 |
term "\<open>\<close>" |
93 |
term "\<open>abc\<close>" |
|
94 |
term "\<open>abc\<close> @ \<open>xyz\<close>" |
|
95 |
term "\<open>\<newline>\<close>" |
|
96 |
term "\<open>\001\010\100\<close>" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
97 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
98 |
|
59068 | 99 |
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
|
100 |
|
59068 | 101 |
subsubsection \<open>Nested quotes\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
102 |
|
55133 | 103 |
syntax "_string_string" :: "string_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
104 |
|
59068 | 105 |
parse_translation \<open> |
55133 | 106 |
[(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))] |
59068 | 107 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
108 |
|
55133 | 109 |
term "\"\"" |
110 |
term "\"abc\"" |
|
111 |
term "\"abc\" @ \"xyz\"" |
|
112 |
term "\"\<newline>\"" |
|
113 |
term "\"\001\010\100\"" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
114 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
115 |
|
59068 | 116 |
subsubsection \<open>Term cartouche and regular quotes\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
117 |
|
59068 | 118 |
ML \<open> |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58889
diff
changeset
|
119 |
Outer_Syntax.command @{command_spec "term_cartouche"} "" |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
120 |
(Parse.inner_syntax Parse.cartouche >> (fn s => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
121 |
Toplevel.keep (fn state => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
122 |
let |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
123 |
val ctxt = Toplevel.context_of state; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
124 |
val t = Syntax.read_term ctxt s; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
125 |
in writeln (Syntax.string_of_term ctxt t) end))) |
59068 | 126 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
127 |
|
55133 | 128 |
term_cartouche \<open>""\<close> |
129 |
term_cartouche \<open>"abc"\<close> |
|
130 |
term_cartouche \<open>"abc" @ "xyz"\<close> |
|
131 |
term_cartouche \<open>"\<newline>"\<close> |
|
132 |
term_cartouche \<open>"\001\010\100"\<close> |
|
55033 | 133 |
|
55047 | 134 |
|
59068 | 135 |
subsubsection \<open>Further nesting: antiquotations\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
136 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
137 |
setup -- "ML antiquotation" |
59068 | 138 |
\<open> |
56072 | 139 |
ML_Antiquotation.inline @{binding term_cartouche} |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
140 |
(Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
141 |
(fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) |
59068 | 142 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
143 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
144 |
setup -- "document antiquotation" |
59068 | 145 |
\<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
146 |
Thy_Output.antiquotation @{binding ML_cartouche} |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
147 |
(Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source => |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
148 |
let |
59067 | 149 |
val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");"; |
59064 | 150 |
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
|
151 |
in "" end); |
59068 | 152 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
153 |
|
59068 | 154 |
ML \<open> |
55133 | 155 |
@{term_cartouche \<open>""\<close>}; |
156 |
@{term_cartouche \<open>"abc"\<close>}; |
|
157 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
158 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
159 |
@{term_cartouche \<open>"\001\010\100"\<close>}; |
|
59068 | 160 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
161 |
|
59068 | 162 |
text \<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
163 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
164 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
165 |
( |
55133 | 166 |
@{term_cartouche \<open>""\<close>}; |
167 |
@{term_cartouche \<open>"abc"\<close>}; |
|
168 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
169 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
170 |
@{term_cartouche \<open>"\001\010\100"\<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 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
173 |
} |
59068 | 174 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
175 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
176 |
|
59068 | 177 |
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
|
178 |
|
59068 | 179 |
ML \<open> |
55110
917e799f19da
avoid breakdown of document preparation, which does not understand cartouche tokens yet;
wenzelm
parents:
55109
diff
changeset
|
180 |
Outer_Syntax.command |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
181 |
@{command_spec "text_cartouche"} "" |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58991
diff
changeset
|
182 |
(Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.document_command) |
59068 | 183 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
184 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
185 |
text_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
186 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
187 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
188 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
189 |
( |
55133 | 190 |
@{term_cartouche \<open>""\<close>}; |
191 |
@{term_cartouche \<open>"abc"\<close>}; |
|
192 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
193 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
194 |
@{term_cartouche \<open>"\001\010\100"\<close>} |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
195 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
196 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
197 |
} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
198 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
199 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
200 |
|
59068 | 201 |
subsection \<open>Proof method syntax: ML tactic expression\<close> |
55047 | 202 |
|
59068 | 203 |
ML \<open> |
55047 | 204 |
structure ML_Tactic: |
205 |
sig |
|
206 |
val set: (Proof.context -> tactic) -> Proof.context -> Proof.context |
|
59064 | 207 |
val ml_tactic: Input.source -> Proof.context -> tactic |
55047 | 208 |
end = |
209 |
struct |
|
210 |
structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac); |
|
211 |
||
212 |
val set = Data.put; |
|
213 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
214 |
fun ml_tactic source ctxt = |
55047 | 215 |
let |
216 |
val ctxt' = ctxt |> Context.proof_map |
|
59064 | 217 |
(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
|
218 |
"Context.map_proof (ML_Tactic.set tactic)" |
59067 | 219 |
(ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source)); |
55047 | 220 |
in Data.get ctxt' ctxt end; |
221 |
end; |
|
59068 | 222 |
\<close> |
55047 | 223 |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
224 |
|
59068 | 225 |
subsubsection \<open>Explicit version: method with cartouche argument\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
226 |
|
59068 | 227 |
method_setup ml_tactic = \<open> |
55047 | 228 |
Scan.lift Args.cartouche_source_position |
229 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
|
59068 | 230 |
\<close> |
55047 | 231 |
|
232 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
233 |
apply (ml_tactic \<open>rtac @{thm impI} 1\<close>) |
|
234 |
apply (ml_tactic \<open>etac @{thm conjE} 1\<close>) |
|
235 |
apply (ml_tactic \<open>rtac @{thm conjI} 1\<close>) |
|
236 |
apply (ml_tactic \<open>ALLGOALS atac\<close>) |
|
237 |
done |
|
238 |
||
239 |
lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>) |
|
240 |
||
59068 | 241 |
ML \<open>@{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close> |
55047 | 242 |
|
59068 | 243 |
text \<open>@{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"}\<close> |
55047 | 244 |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
245 |
|
59068 | 246 |
subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
247 |
|
59068 | 248 |
method_setup "cartouche" = \<open> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
249 |
Scan.lift Args.cartouche_source_position |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
250 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
59068 | 251 |
\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
252 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
253 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
254 |
apply \<open>rtac @{thm impI} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
255 |
apply \<open>etac @{thm conjE} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
256 |
apply \<open>rtac @{thm conjI} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
257 |
apply \<open>ALLGOALS atac\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
258 |
done |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
259 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
260 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
261 |
by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+) |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
262 |
|
55033 | 263 |
end |