author | wenzelm |
Wed, 12 Mar 2014 22:57:50 +0100 | |
changeset 56072 | 31e427387ab5 |
parent 55828 | 42ac3cfb89f6 |
child 56275 | 600f432ab556 |
permissions | -rw-r--r-- |
55033 | 1 |
header {* Some examples with text cartouches *} |
2 |
||
3 |
theory Cartouche_Examples |
|
4 |
imports Main |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
5 |
keywords |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
6 |
"cartouche" "term_cartouche" :: diag and |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
7 |
"text_cartouche" :: thy_decl |
55033 | 8 |
begin |
9 |
||
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
10 |
subsection {* Outer syntax: cartouche within command syntax *} |
55033 | 11 |
|
12 |
ML {* |
|
13 |
Outer_Syntax.improper_command @{command_spec "cartouche"} "" |
|
14 |
(Parse.cartouche >> (fn s => |
|
15 |
Toplevel.imperative (fn () => writeln s))) |
|
16 |
*} |
|
17 |
||
18 |
cartouche \<open>abc\<close> |
|
19 |
cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close> |
|
20 |
||
21 |
||
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
22 |
subsection {* Inner syntax: string literals via cartouche *} |
55033 | 23 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
24 |
ML {* |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
25 |
local |
55033 | 26 |
val mk_nib = |
27 |
Syntax.const o Lexicon.mark_const o |
|
28 |
fst o Term.dest_Const o HOLogic.mk_nibble; |
|
29 |
||
30 |
fun mk_char (s, pos) = |
|
31 |
let |
|
32 |
val c = |
|
33 |
if Symbol.is_ascii s then ord s |
|
55036 | 34 |
else if s = "\<newline>" then 10 |
55033 | 35 |
else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); |
36 |
in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end; |
|
37 |
||
38 |
fun mk_string [] = Const (@{const_syntax Nil}, @{typ string}) |
|
39 |
| mk_string (s :: ss) = |
|
40 |
Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss; |
|
41 |
||
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
42 |
in |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
43 |
fun string_tr content args = |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
44 |
let fun err () = raise TERM ("string_tr", args) in |
55033 | 45 |
(case args of |
46 |
[(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => |
|
47 |
(case Term_Position.decode_position p of |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
48 |
SOME (pos, _) => c $ mk_string (content (s, pos)) $ p |
55033 | 49 |
| NONE => err ()) |
50 |
| _ => err ()) |
|
51 |
end; |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
52 |
end; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
53 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
54 |
|
55133 | 55 |
syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
56 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
57 |
parse_translation {* |
55133 | 58 |
[(@{syntax_const "_cartouche_string"}, |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
59 |
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] |
55033 | 60 |
*} |
61 |
||
55133 | 62 |
term "\<open>\<close>" |
63 |
term "\<open>abc\<close>" |
|
64 |
term "\<open>abc\<close> @ \<open>xyz\<close>" |
|
65 |
term "\<open>\<newline>\<close>" |
|
66 |
term "\<open>\001\010\100\<close>" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
67 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
68 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
69 |
subsection {* Alternate outer and inner syntax: string literals *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
70 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
71 |
subsubsection {* Nested quotes *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
72 |
|
55133 | 73 |
syntax "_string_string" :: "string_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
74 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
75 |
parse_translation {* |
55133 | 76 |
[(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))] |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
77 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
78 |
|
55133 | 79 |
term "\"\"" |
80 |
term "\"abc\"" |
|
81 |
term "\"abc\" @ \"xyz\"" |
|
82 |
term "\"\<newline>\"" |
|
83 |
term "\"\001\010\100\"" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
84 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
85 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
86 |
subsubsection {* Term cartouche and regular quotes *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
87 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
88 |
ML {* |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
89 |
Outer_Syntax.improper_command @{command_spec "term_cartouche"} "" |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
90 |
(Parse.inner_syntax Parse.cartouche >> (fn s => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
91 |
Toplevel.keep (fn state => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
92 |
let |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
93 |
val ctxt = Toplevel.context_of state; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
94 |
val t = Syntax.read_term ctxt s; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
95 |
in writeln (Syntax.string_of_term ctxt t) end))) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
96 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
97 |
|
55133 | 98 |
term_cartouche \<open>""\<close> |
99 |
term_cartouche \<open>"abc"\<close> |
|
100 |
term_cartouche \<open>"abc" @ "xyz"\<close> |
|
101 |
term_cartouche \<open>"\<newline>"\<close> |
|
102 |
term_cartouche \<open>"\001\010\100"\<close> |
|
55033 | 103 |
|
55047 | 104 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
105 |
subsubsection {* Further nesting: antiquotations *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
106 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
107 |
setup -- "ML antiquotation" |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
108 |
{* |
56072 | 109 |
ML_Antiquotation.inline @{binding term_cartouche} |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
110 |
(Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
111 |
(fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
112 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
113 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
114 |
setup -- "document antiquotation" |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
115 |
{* |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
116 |
Thy_Output.antiquotation @{binding ML_cartouche} |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
117 |
(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
|
118 |
let |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
119 |
val toks = |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
120 |
ML_Lex.read Position.none "fn _ => (" @ |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
121 |
ML_Lex.read_source source @ |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
122 |
ML_Lex.read Position.none ");"; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
123 |
val _ = ML_Context.eval_in (SOME context) false (#pos source) toks; |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
124 |
in "" end); |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
125 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
126 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
127 |
ML {* |
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>}; |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
133 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
134 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
135 |
text {* |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
136 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
137 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
138 |
( |
55133 | 139 |
@{term_cartouche \<open>""\<close>}; |
140 |
@{term_cartouche \<open>"abc"\<close>}; |
|
141 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
142 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
143 |
@{term_cartouche \<open>"\001\010\100"\<close>} |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
144 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
145 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
146 |
} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
147 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
148 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
149 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
150 |
subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
151 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
152 |
ML {* |
55110
917e799f19da
avoid breakdown of document preparation, which does not understand cartouche tokens yet;
wenzelm
parents:
55109
diff
changeset
|
153 |
Outer_Syntax.command |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
154 |
@{command_spec "text_cartouche"} "" |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
155 |
(Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
156 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
157 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
158 |
text_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
159 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
160 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
161 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
162 |
( |
55133 | 163 |
@{term_cartouche \<open>""\<close>}; |
164 |
@{term_cartouche \<open>"abc"\<close>}; |
|
165 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
166 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
167 |
@{term_cartouche \<open>"\001\010\100"\<close>} |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
168 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
169 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
170 |
} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
171 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
172 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
173 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
174 |
subsection {* Proof method syntax: ML tactic expression *} |
55047 | 175 |
|
176 |
ML {* |
|
177 |
structure ML_Tactic: |
|
178 |
sig |
|
179 |
val set: (Proof.context -> tactic) -> Proof.context -> Proof.context |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
180 |
val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic |
55047 | 181 |
end = |
182 |
struct |
|
183 |
structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac); |
|
184 |
||
185 |
val set = Data.put; |
|
186 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
187 |
fun ml_tactic source ctxt = |
55047 | 188 |
let |
189 |
val ctxt' = ctxt |> Context.proof_map |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
190 |
(ML_Context.expression (#pos source) |
55047 | 191 |
"fun tactic (ctxt : Proof.context) : tactic" |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
192 |
"Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source source)); |
55047 | 193 |
in Data.get ctxt' ctxt end; |
194 |
end; |
|
195 |
*} |
|
196 |
||
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
197 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
198 |
subsubsection {* Explicit version: method with cartouche argument *} |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
199 |
|
55047 | 200 |
method_setup ml_tactic = {* |
201 |
Scan.lift Args.cartouche_source_position |
|
202 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
|
203 |
*} |
|
204 |
||
205 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
206 |
apply (ml_tactic \<open>rtac @{thm impI} 1\<close>) |
|
207 |
apply (ml_tactic \<open>etac @{thm conjE} 1\<close>) |
|
208 |
apply (ml_tactic \<open>rtac @{thm conjI} 1\<close>) |
|
209 |
apply (ml_tactic \<open>ALLGOALS atac\<close>) |
|
210 |
done |
|
211 |
||
212 |
lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>) |
|
213 |
||
214 |
ML {* @{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)} *} |
|
215 |
||
216 |
text {* @{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"} *} |
|
217 |
||
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
218 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
219 |
subsubsection {* Implicit version: method with special name "cartouche" (dynamic!) *} |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
220 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
221 |
method_setup "cartouche" = {* |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
222 |
Scan.lift Args.cartouche_source_position |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
223 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
224 |
*} |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
225 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
226 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
227 |
apply \<open>rtac @{thm impI} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
228 |
apply \<open>etac @{thm conjE} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
229 |
apply \<open>rtac @{thm conjI} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
230 |
apply \<open>ALLGOALS atac\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
231 |
done |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
232 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
233 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
234 |
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
|
235 |
|
55033 | 236 |
end |