src/HOL/ex/Cartouche_Examples.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 56500 90f17a04567d
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     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 {* Regular outer syntax *}
    11 
    12 text \<open>Text cartouches may be used in the outer syntax category "text",
    13   as alternative to the traditional "verbatim" tokens.  An example is
    14   this text block.\<close>  -- \<open>The same works for small side-comments.\<close>
    15 
    16 notepad
    17 begin
    18   txt \<open>Moreover, cartouches work as additional syntax in the
    19     "altstring" category, for literal fact references.  For example:\<close>
    20 
    21   fix x y :: 'a
    22   assume "x = y"
    23   note \<open>x = y\<close>
    24   have "x = y" by (rule \<open>x = y\<close>)
    25   from \<open>x = y\<close> have "x = y" .
    26 
    27   txt \<open>Of course, this can be nested inside formal comments and
    28     antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
    29     [OF \<open>x = y\<close>]}.\<close>
    30 
    31   have "x = y"
    32     by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
    33 end
    34 
    35 
    36 subsection {* Outer syntax: cartouche within command syntax *}
    37 
    38 ML {*
    39   Outer_Syntax.improper_command @{command_spec "cartouche"} ""
    40     (Parse.cartouche >> (fn s =>
    41       Toplevel.imperative (fn () => writeln s)))
    42 *}
    43 
    44 cartouche \<open>abc\<close>
    45 cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close>
    46 
    47 
    48 subsection {* Inner syntax: string literals via cartouche *}
    49 
    50 ML {*
    51   local
    52     val mk_nib =
    53       Syntax.const o Lexicon.mark_const o
    54         fst o Term.dest_Const o HOLogic.mk_nibble;
    55 
    56     fun mk_char (s, pos) =
    57       let
    58         val c =
    59           if Symbol.is_ascii s then ord s
    60           else if s = "\<newline>" then 10
    61           else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
    62       in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end;
    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 
    68   in
    69     fun string_tr content args =
    70       let fun err () = raise TERM ("string_tr", args) in
    71         (case args of
    72           [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
    73             (case Term_Position.decode_position p of
    74               SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
    75             | NONE => err ())
    76         | _ => err ())
    77       end;
    78   end;
    79 *}
    80 
    81 syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string"  ("_")
    82 
    83 parse_translation {*
    84   [(@{syntax_const "_cartouche_string"},
    85     K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
    86 *}
    87 
    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>"
    93 
    94 
    95 subsection {* Alternate outer and inner syntax: string literals *}
    96 
    97 subsubsection {* Nested quotes *}
    98 
    99 syntax "_string_string" :: "string_position \<Rightarrow> string"  ("_")
   100 
   101 parse_translation {*
   102   [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
   103 *}
   104 
   105 term "\"\""
   106 term "\"abc\""
   107 term "\"abc\" @ \"xyz\""
   108 term "\"\<newline>\""
   109 term "\"\001\010\100\""
   110 
   111 
   112 subsubsection {* Term cartouche and regular quotes *}
   113 
   114 ML {*
   115   Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
   116     (Parse.inner_syntax Parse.cartouche >> (fn s =>
   117       Toplevel.keep (fn state =>
   118         let
   119           val ctxt = Toplevel.context_of state;
   120           val t = Syntax.read_term ctxt s;
   121         in writeln (Syntax.string_of_term ctxt t) end)))
   122 *}
   123 
   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>
   129 
   130 
   131 subsubsection {* Further nesting: antiquotations *}
   132 
   133 setup -- "ML antiquotation"
   134 {*
   135   ML_Antiquotation.inline @{binding term_cartouche}
   136     (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
   137       (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
   138 *}
   139 
   140 setup -- "document antiquotation"
   141 {*
   142   Thy_Output.antiquotation @{binding ML_cartouche}
   143     (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
   144       let
   145         val toks =
   146           ML_Lex.read Position.none "fn _ => (" @
   147           ML_Lex.read_source false source @
   148           ML_Lex.read Position.none ");";
   149         val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks;
   150       in "" end);
   151 *}
   152 
   153 ML {*
   154   @{term_cartouche \<open>""\<close>};
   155   @{term_cartouche \<open>"abc"\<close>};
   156   @{term_cartouche \<open>"abc" @ "xyz"\<close>};
   157   @{term_cartouche \<open>"\<newline>"\<close>};
   158   @{term_cartouche \<open>"\001\010\100"\<close>};
   159 *}
   160 
   161 text {*
   162   @{ML_cartouche
   163     \<open>
   164       (
   165         @{term_cartouche \<open>""\<close>};
   166         @{term_cartouche \<open>"abc"\<close>};
   167         @{term_cartouche \<open>"abc" @ "xyz"\<close>};
   168         @{term_cartouche \<open>"\<newline>"\<close>};
   169         @{term_cartouche \<open>"\001\010\100"\<close>}
   170       )
   171     \<close>
   172   }
   173 *}
   174 
   175 
   176 subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *}
   177 
   178 ML {*
   179   Outer_Syntax.command
   180     @{command_spec "text_cartouche"} ""
   181     (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup)
   182 *}
   183 
   184 text_cartouche
   185 \<open>
   186   @{ML_cartouche
   187     \<open>
   188       (
   189         @{term_cartouche \<open>""\<close>};
   190         @{term_cartouche \<open>"abc"\<close>};
   191         @{term_cartouche \<open>"abc" @ "xyz"\<close>};
   192         @{term_cartouche \<open>"\<newline>"\<close>};
   193         @{term_cartouche \<open>"\001\010\100"\<close>}
   194       )
   195     \<close>
   196   }
   197 \<close>
   198 
   199 
   200 subsection {* Proof method syntax: ML tactic expression *}
   201 
   202 ML {*
   203 structure ML_Tactic:
   204 sig
   205   val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
   206   val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic
   207 end =
   208 struct
   209   structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
   210 
   211   val set = Data.put;
   212 
   213   fun ml_tactic source ctxt =
   214     let
   215       val ctxt' = ctxt |> Context.proof_map
   216         (ML_Context.expression (#pos source)
   217           "fun tactic (ctxt : Proof.context) : tactic"
   218           "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source));
   219     in Data.get ctxt' ctxt end;
   220 end;
   221 *}
   222 
   223 
   224 subsubsection {* Explicit version: method with cartouche argument *}
   225 
   226 method_setup ml_tactic = {*
   227   Scan.lift Args.cartouche_source_position
   228     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
   229 *}
   230 
   231 lemma "A \<and> B \<longrightarrow> B \<and> A"
   232   apply (ml_tactic \<open>rtac @{thm impI} 1\<close>)
   233   apply (ml_tactic \<open>etac @{thm conjE} 1\<close>)
   234   apply (ml_tactic \<open>rtac @{thm conjI} 1\<close>)
   235   apply (ml_tactic \<open>ALLGOALS atac\<close>)
   236   done
   237 
   238 lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
   239 
   240 ML {* @{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)} *}
   241 
   242 text {* @{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"} *}
   243 
   244 
   245 subsubsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
   246 
   247 method_setup "cartouche" = {*
   248   Scan.lift Args.cartouche_source_position
   249     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
   250 *}
   251 
   252 lemma "A \<and> B \<longrightarrow> B \<and> A"
   253   apply \<open>rtac @{thm impI} 1\<close>
   254   apply \<open>etac @{thm conjE} 1\<close>
   255   apply \<open>rtac @{thm conjI} 1\<close>
   256   apply \<open>ALLGOALS atac\<close>
   257   done
   258 
   259 lemma "A \<and> B \<longrightarrow> B \<and> A"
   260   by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
   261 
   262 end