src/HOL/ex/Cartouche_Examples.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63120 629a4c5e953e
child 67382 39e4668ded4f
permissions -rw-r--r--
bundle lifting_syntax;
wenzelm@59089
     1
(*  Title:      HOL/ex/Cartouche_Examples.thy
wenzelm@59089
     2
    Author:     Makarius
wenzelm@59089
     3
*)
wenzelm@59089
     4
wenzelm@59068
     5
section \<open>Some examples with text cartouches\<close>
wenzelm@55033
     6
wenzelm@55033
     7
theory Cartouche_Examples
wenzelm@55033
     8
imports Main
wenzelm@55109
     9
keywords
wenzelm@63120
    10
  "cartouche" :: diag and
wenzelm@55109
    11
  "text_cartouche" :: thy_decl
wenzelm@55033
    12
begin
wenzelm@55033
    13
wenzelm@59068
    14
subsection \<open>Regular outer syntax\<close>
wenzelm@56499
    15
wenzelm@63054
    16
text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>,
wenzelm@63054
    17
  as alternative to the traditional \<open>verbatim\<close> tokens.  An example is
wenzelm@61933
    18
  this text block.\<close>  \<comment> \<open>The same works for small side-comments.\<close>
wenzelm@56499
    19
wenzelm@56499
    20
notepad
wenzelm@56499
    21
begin
wenzelm@63120
    22
  txt \<open>Cartouches work as additional syntax for embedded language tokens
wenzelm@63120
    23
    (types, terms, props) and as a replacement for the \<open>altstring\<close> category
wenzelm@63120
    24
    (for literal fact references). For example:\<close>
wenzelm@56499
    25
wenzelm@56499
    26
  fix x y :: 'a
wenzelm@63120
    27
  assume \<open>x = y\<close>
wenzelm@56499
    28
  note \<open>x = y\<close>
wenzelm@63120
    29
  have \<open>x = y\<close> by (rule \<open>x = y\<close>)
wenzelm@63120
    30
  from \<open>x = y\<close> have \<open>x = y\<close> .
wenzelm@56499
    31
wenzelm@56499
    32
  txt \<open>Of course, this can be nested inside formal comments and
wenzelm@56499
    33
    antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
wenzelm@56499
    34
    [OF \<open>x = y\<close>]}.\<close>
wenzelm@56500
    35
wenzelm@63120
    36
  have \<open>x = y\<close>
wenzelm@63120
    37
    by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>)
wenzelm@63120
    38
      \<comment> \<open>more cartouches involving ML\<close>
wenzelm@56499
    39
end
wenzelm@56499
    40
wenzelm@56499
    41
wenzelm@59068
    42
subsection \<open>Outer syntax: cartouche within command syntax\<close>
wenzelm@55033
    43
wenzelm@59068
    44
ML \<open>
wenzelm@59936
    45
  Outer_Syntax.command @{command_keyword cartouche} ""
wenzelm@55033
    46
    (Parse.cartouche >> (fn s =>
wenzelm@60189
    47
      Toplevel.keep (fn _ => writeln s)))
wenzelm@59068
    48
\<close>
wenzelm@55033
    49
wenzelm@55033
    50
cartouche \<open>abc\<close>
wenzelm@55033
    51
cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close>
wenzelm@55033
    52
wenzelm@55033
    53
wenzelm@59068
    54
subsection \<open>Inner syntax: string literals via cartouche\<close>
wenzelm@55033
    55
wenzelm@59068
    56
ML \<open>
wenzelm@55109
    57
  local
wenzelm@55033
    58
    fun mk_char (s, pos) =
wenzelm@55033
    59
      let
wenzelm@55033
    60
        val c =
wenzelm@55033
    61
          if Symbol.is_ascii s then ord s
wenzelm@55036
    62
          else if s = "\<newline>" then 10
wenzelm@55033
    63
          else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
haftmann@62597
    64
      in Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c end;
wenzelm@55033
    65
wenzelm@55033
    66
    fun mk_string [] = Const (@{const_syntax Nil}, @{typ string})
wenzelm@55033
    67
      | mk_string (s :: ss) =
wenzelm@55033
    68
          Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss;
wenzelm@55033
    69
wenzelm@55109
    70
  in
wenzelm@55109
    71
    fun string_tr content args =
wenzelm@55109
    72
      let fun err () = raise TERM ("string_tr", args) in
wenzelm@55033
    73
        (case args of
wenzelm@55033
    74
          [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
wenzelm@55033
    75
            (case Term_Position.decode_position p of
wenzelm@55109
    76
              SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
wenzelm@55033
    77
            | NONE => err ())
wenzelm@55033
    78
        | _ => err ())
wenzelm@55033
    79
      end;
wenzelm@55109
    80
  end;
wenzelm@59068
    81
\<close>
wenzelm@55109
    82
wenzelm@63120
    83
syntax "_cartouche_string" :: \<open>cartouche_position \<Rightarrow> string\<close>  ("_")
wenzelm@55109
    84
wenzelm@59068
    85
parse_translation \<open>
wenzelm@55133
    86
  [(@{syntax_const "_cartouche_string"},
wenzelm@55109
    87
    K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
wenzelm@59068
    88
\<close>
wenzelm@55033
    89
wenzelm@63120
    90
term \<open>\<open>\<close>\<close>
wenzelm@63120
    91
term \<open>\<open>abc\<close>\<close>
wenzelm@63120
    92
term \<open>\<open>abc\<close> @ \<open>xyz\<close>\<close>
wenzelm@63120
    93
term \<open>\<open>\<newline>\<close>\<close>
wenzelm@55109
    94
wenzelm@55109
    95
wenzelm@59068
    96
subsection \<open>Alternate outer and inner syntax: string literals\<close>
wenzelm@55109
    97
wenzelm@59068
    98
subsubsection \<open>Nested quotes\<close>
wenzelm@55109
    99
wenzelm@63120
   100
syntax "_string_string" :: \<open>string_position \<Rightarrow> string\<close>  ("_")
wenzelm@55109
   101
wenzelm@59068
   102
parse_translation \<open>
wenzelm@55133
   103
  [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
wenzelm@59068
   104
\<close>
wenzelm@55109
   105
wenzelm@63120
   106
term \<open>""\<close>
wenzelm@63120
   107
term \<open>"abc"\<close>
wenzelm@63120
   108
term \<open>"abc" @ "xyz"\<close>
wenzelm@63120
   109
term \<open>"\<newline>"\<close>
wenzelm@63120
   110
term \<open>"\001\010\100"\<close>
wenzelm@55033
   111
wenzelm@55047
   112
wenzelm@59068
   113
subsubsection \<open>Further nesting: antiquotations\<close>
wenzelm@55109
   114
wenzelm@59068
   115
ML \<open>
wenzelm@63120
   116
  @{term \<open>""\<close>};
wenzelm@63120
   117
  @{term \<open>"abc"\<close>};
wenzelm@63120
   118
  @{term \<open>"abc" @ "xyz"\<close>};
wenzelm@63120
   119
  @{term \<open>"\<newline>"\<close>};
wenzelm@63120
   120
  @{term \<open>"\001\010\100"\<close>};
wenzelm@59068
   121
\<close>
wenzelm@55109
   122
wenzelm@59068
   123
text \<open>
wenzelm@63120
   124
  @{ML
wenzelm@55109
   125
    \<open>
wenzelm@55109
   126
      (
wenzelm@63120
   127
        @{term \<open>""\<close>};
wenzelm@63120
   128
        @{term \<open>"abc"\<close>};
wenzelm@63120
   129
        @{term \<open>"abc" @ "xyz"\<close>};
wenzelm@63120
   130
        @{term \<open>"\<newline>"\<close>};
wenzelm@63120
   131
        @{term \<open>"\001\010\100"\<close>}
wenzelm@55109
   132
      )
wenzelm@55109
   133
    \<close>
wenzelm@55109
   134
  }
wenzelm@59068
   135
\<close>
wenzelm@55109
   136
wenzelm@55109
   137
wenzelm@59068
   138
subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close>
wenzelm@55109
   139
wenzelm@59068
   140
ML \<open>
wenzelm@55110
   141
  Outer_Syntax.command
wenzelm@59936
   142
    @{command_keyword text_cartouche} ""
wenzelm@61457
   143
    (Parse.opt_target -- Parse.input Parse.cartouche
wenzelm@61457
   144
      >> Thy_Output.document_command {markdown = true})
wenzelm@59068
   145
\<close>
wenzelm@55109
   146
wenzelm@55109
   147
text_cartouche
wenzelm@55109
   148
\<open>
wenzelm@63120
   149
  @{ML
wenzelm@55109
   150
    \<open>
wenzelm@55109
   151
      (
wenzelm@63120
   152
        @{term \<open>""\<close>};
wenzelm@63120
   153
        @{term \<open>"abc"\<close>};
wenzelm@63120
   154
        @{term \<open>"abc" @ "xyz"\<close>};
wenzelm@63120
   155
        @{term \<open>"\<newline>"\<close>};
wenzelm@63120
   156
        @{term \<open>"\001\010\100"\<close>}
wenzelm@55109
   157
      )
wenzelm@55109
   158
    \<close>
wenzelm@55109
   159
  }
wenzelm@55109
   160
\<close>
wenzelm@55109
   161
wenzelm@55109
   162
wenzelm@59068
   163
subsection \<open>Proof method syntax: ML tactic expression\<close>
wenzelm@55047
   164
wenzelm@59068
   165
ML \<open>
wenzelm@55047
   166
structure ML_Tactic:
wenzelm@55047
   167
sig
wenzelm@55047
   168
  val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
wenzelm@59064
   169
  val ml_tactic: Input.source -> Proof.context -> tactic
wenzelm@55047
   170
end =
wenzelm@55047
   171
struct
wenzelm@55047
   172
  structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
wenzelm@55047
   173
wenzelm@55047
   174
  val set = Data.put;
wenzelm@55047
   175
wenzelm@55828
   176
  fun ml_tactic source ctxt =
wenzelm@55047
   177
    let
wenzelm@55047
   178
      val ctxt' = ctxt |> Context.proof_map
wenzelm@59064
   179
        (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
wenzelm@58991
   180
          "Context.map_proof (ML_Tactic.set tactic)"
wenzelm@59067
   181
          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
wenzelm@55047
   182
    in Data.get ctxt' ctxt end;
wenzelm@55047
   183
end;
wenzelm@59068
   184
\<close>
wenzelm@55047
   185
wenzelm@55048
   186
wenzelm@59068
   187
subsubsection \<open>Explicit version: method with cartouche argument\<close>
wenzelm@55048
   188
wenzelm@59068
   189
method_setup ml_tactic = \<open>
wenzelm@59809
   190
  Scan.lift Args.cartouche_input
wenzelm@55047
   191
    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
wenzelm@59068
   192
\<close>
wenzelm@55047
   193
wenzelm@63120
   194
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
wenzelm@60754
   195
  apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>)
wenzelm@60754
   196
  apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>)
wenzelm@60754
   197
  apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
wenzelm@60754
   198
  apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>)
wenzelm@55047
   199
  done
wenzelm@55047
   200
wenzelm@63120
   201
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)
wenzelm@55047
   202
wenzelm@63120
   203
ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
wenzelm@55047
   204
wenzelm@63120
   205
text \<open>@{ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>}\<close>
wenzelm@55047
   206
wenzelm@55048
   207
wenzelm@59068
   208
subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close>
wenzelm@55048
   209
wenzelm@59068
   210
method_setup "cartouche" = \<open>
wenzelm@59809
   211
  Scan.lift Args.cartouche_input
wenzelm@55048
   212
    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
wenzelm@59068
   213
\<close>
wenzelm@55048
   214
wenzelm@63120
   215
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
wenzelm@60754
   216
  apply \<open>resolve_tac @{context} @{thms impI} 1\<close>
wenzelm@60754
   217
  apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close>
wenzelm@60754
   218
  apply \<open>resolve_tac @{context} @{thms conjI} 1\<close>
wenzelm@60754
   219
  apply \<open>ALLGOALS (assume_tac @{context})\<close>
wenzelm@55048
   220
  done
wenzelm@55048
   221
wenzelm@63120
   222
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
wenzelm@60754
   223
  by (\<open>resolve_tac @{context} @{thms impI} 1\<close>,
wenzelm@60754
   224
    \<open>eresolve_tac @{context} @{thms conjE} 1\<close>,
wenzelm@60754
   225
    \<open>resolve_tac @{context} @{thms conjI} 1\<close>,
wenzelm@60754
   226
    \<open>assume_tac @{context} 1\<close>+)
wenzelm@55048
   227
wenzelm@59112
   228
wenzelm@59128
   229
subsection \<open>ML syntax\<close>
wenzelm@59112
   230
wenzelm@59128
   231
text \<open>Input source with position information:\<close>
wenzelm@59112
   232
ML \<open>
wenzelm@59135
   233
  val s: Input.source = \<open>abc123def456\<close>;
wenzelm@59184
   234
  Output.information ("Look here!" ^ Position.here (Input.pos_of s));
wenzelm@59112
   235
wenzelm@59112
   236
  \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
wenzelm@59112
   237
    if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
wenzelm@59112
   238
\<close>
wenzelm@59112
   239
wenzelm@55033
   240
end