src/HOL/ex/Cartouche_Examples.thy
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 56072 31e427387ab5
child 56278 2576d3a40ed6
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
     1 header {* Some examples with text cartouches *}
     2 
     3 theory Cartouche_Examples
     4 imports Main
     5 keywords
     6   "cartouche" "term_cartouche" :: diag and
     7   "text_cartouche" :: thy_decl
     8 begin
     9 
    10 subsection {* Outer syntax: cartouche within command syntax *}
    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 
    22 subsection {* Inner syntax: string literals via cartouche *}
    23 
    24 ML {*
    25   local
    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
    34           else if s = "\<newline>" then 10
    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 
    42   in
    43     fun string_tr content args =
    44       let fun err () = raise TERM ("string_tr", args) in
    45         (case args of
    46           [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
    47             (case Term_Position.decode_position p of
    48               SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
    49             | NONE => err ())
    50         | _ => err ())
    51       end;
    52   end;
    53 *}
    54 
    55 syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string"  ("_")
    56 
    57 parse_translation {*
    58   [(@{syntax_const "_cartouche_string"},
    59     K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
    60 *}
    61 
    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>"
    67 
    68 
    69 subsection {* Alternate outer and inner syntax: string literals *}
    70 
    71 subsubsection {* Nested quotes *}
    72 
    73 syntax "_string_string" :: "string_position \<Rightarrow> string"  ("_")
    74 
    75 parse_translation {*
    76   [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
    77 *}
    78 
    79 term "\"\""
    80 term "\"abc\""
    81 term "\"abc\" @ \"xyz\""
    82 term "\"\<newline>\""
    83 term "\"\001\010\100\""
    84 
    85 
    86 subsubsection {* Term cartouche and regular quotes *}
    87 
    88 ML {*
    89   Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
    90     (Parse.inner_syntax Parse.cartouche >> (fn s =>
    91       Toplevel.keep (fn state =>
    92         let
    93           val ctxt = Toplevel.context_of state;
    94           val t = Syntax.read_term ctxt s;
    95         in writeln (Syntax.string_of_term ctxt t) end)))
    96 *}
    97 
    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>
   103 
   104 
   105 subsubsection {* Further nesting: antiquotations *}
   106 
   107 setup -- "ML antiquotation"
   108 {*
   109   ML_Antiquotation.inline @{binding term_cartouche}
   110     (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
   111       (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
   112 *}
   113 
   114 setup -- "document antiquotation"
   115 {*
   116   Thy_Output.antiquotation @{binding ML_cartouche}
   117     (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
   118       let
   119         val toks =
   120           ML_Lex.read Position.none "fn _ => (" @
   121           ML_Lex.read_source source @
   122           ML_Lex.read Position.none ");";
   123         val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
   124       in "" end);
   125 *}
   126 
   127 ML {*
   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>};
   133 *}
   134 
   135 text {*
   136   @{ML_cartouche
   137     \<open>
   138       (
   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>}
   144       )
   145     \<close>
   146   }
   147 *}
   148 
   149 
   150 subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *}
   151 
   152 ML {*
   153   Outer_Syntax.command
   154     @{command_spec "text_cartouche"} ""
   155     (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup)
   156 *}
   157 
   158 text_cartouche
   159 \<open>
   160   @{ML_cartouche
   161     \<open>
   162       (
   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>}
   168       )
   169     \<close>
   170   }
   171 \<close>
   172 
   173 
   174 subsection {* Proof method syntax: ML tactic expression *}
   175 
   176 ML {*
   177 structure ML_Tactic:
   178 sig
   179   val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
   180   val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic
   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 
   187   fun ml_tactic source ctxt =
   188     let
   189       val ctxt' = ctxt |> Context.proof_map
   190         (ML_Context.expression (#pos source)
   191           "fun tactic (ctxt : Proof.context) : tactic"
   192           "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source source));
   193     in Data.get ctxt' ctxt end;
   194 end;
   195 *}
   196 
   197 
   198 subsubsection {* Explicit version: method with cartouche argument *}
   199 
   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 
   218 
   219 subsubsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
   220 
   221 method_setup "cartouche" = {*
   222   Scan.lift Args.cartouche_source_position
   223     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
   224 *}
   225 
   226 lemma "A \<and> B \<longrightarrow> B \<and> A"
   227   apply \<open>rtac @{thm impI} 1\<close>
   228   apply \<open>etac @{thm conjE} 1\<close>
   229   apply \<open>rtac @{thm conjI} 1\<close>
   230   apply \<open>ALLGOALS atac\<close>
   231   done
   232 
   233 lemma "A \<and> B \<longrightarrow> B \<and> A"
   234   by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
   235 
   236 end