src/HOL/ex/Cartouche_Examples.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 60754 02924903a6fd
child 61457 3e21699bb83b
permissions -rw-r--r--
prefer symbols;
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@55109
    10
  "cartouche" "term_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@56499
    16
text \<open>Text cartouches may be used in the outer syntax category "text",
wenzelm@56499
    17
  as alternative to the traditional "verbatim" tokens.  An example is
wenzelm@56499
    18
  this text block.\<close>  -- \<open>The same works for small side-comments.\<close>
wenzelm@56499
    19
wenzelm@56499
    20
notepad
wenzelm@56499
    21
begin
wenzelm@56499
    22
  txt \<open>Moreover, cartouches work as additional syntax in the
wenzelm@56499
    23
    "altstring" category, for literal fact references.  For example:\<close>
wenzelm@56499
    24
wenzelm@56499
    25
  fix x y :: 'a
wenzelm@56499
    26
  assume "x = y"
wenzelm@56499
    27
  note \<open>x = y\<close>
wenzelm@56499
    28
  have "x = y" by (rule \<open>x = y\<close>)
wenzelm@56499
    29
  from \<open>x = y\<close> have "x = y" .
wenzelm@56499
    30
wenzelm@56499
    31
  txt \<open>Of course, this can be nested inside formal comments and
wenzelm@56499
    32
    antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
wenzelm@56499
    33
    [OF \<open>x = y\<close>]}.\<close>
wenzelm@56500
    34
wenzelm@56500
    35
  have "x = y"
wenzelm@60754
    36
    by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
wenzelm@56499
    37
end
wenzelm@56499
    38
wenzelm@56499
    39
wenzelm@59068
    40
subsection \<open>Outer syntax: cartouche within command syntax\<close>
wenzelm@55033
    41
wenzelm@59068
    42
ML \<open>
wenzelm@59936
    43
  Outer_Syntax.command @{command_keyword cartouche} ""
wenzelm@55033
    44
    (Parse.cartouche >> (fn s =>
wenzelm@60189
    45
      Toplevel.keep (fn _ => writeln s)))
wenzelm@59068
    46
\<close>
wenzelm@55033
    47
wenzelm@55033
    48
cartouche \<open>abc\<close>
wenzelm@55033
    49
cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close>
wenzelm@55033
    50
wenzelm@55033
    51
wenzelm@59068
    52
subsection \<open>Inner syntax: string literals via cartouche\<close>
wenzelm@55033
    53
wenzelm@59068
    54
ML \<open>
wenzelm@55109
    55
  local
wenzelm@55033
    56
    val mk_nib =
wenzelm@55033
    57
      Syntax.const o Lexicon.mark_const o
wenzelm@55033
    58
        fst o Term.dest_Const o HOLogic.mk_nibble;
wenzelm@55033
    59
wenzelm@55033
    60
    fun mk_char (s, pos) =
wenzelm@55033
    61
      let
wenzelm@55033
    62
        val c =
wenzelm@55033
    63
          if Symbol.is_ascii s then ord s
wenzelm@55036
    64
          else if s = "\<newline>" then 10
wenzelm@55033
    65
          else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
wenzelm@55033
    66
      in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end;
wenzelm@55033
    67
wenzelm@55033
    68
    fun mk_string [] = Const (@{const_syntax Nil}, @{typ string})
wenzelm@55033
    69
      | mk_string (s :: ss) =
wenzelm@55033
    70
          Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss;
wenzelm@55033
    71
wenzelm@55109
    72
  in
wenzelm@55109
    73
    fun string_tr content args =
wenzelm@55109
    74
      let fun err () = raise TERM ("string_tr", args) in
wenzelm@55033
    75
        (case args of
wenzelm@55033
    76
          [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
wenzelm@55033
    77
            (case Term_Position.decode_position p of
wenzelm@55109
    78
              SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
wenzelm@55033
    79
            | NONE => err ())
wenzelm@55033
    80
        | _ => err ())
wenzelm@55033
    81
      end;
wenzelm@55109
    82
  end;
wenzelm@59068
    83
\<close>
wenzelm@55109
    84
wenzelm@55133
    85
syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string"  ("_")
wenzelm@55109
    86
wenzelm@59068
    87
parse_translation \<open>
wenzelm@55133
    88
  [(@{syntax_const "_cartouche_string"},
wenzelm@55109
    89
    K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
wenzelm@59068
    90
\<close>
wenzelm@55033
    91
wenzelm@55133
    92
term "\<open>\<close>"
wenzelm@55133
    93
term "\<open>abc\<close>"
wenzelm@55133
    94
term "\<open>abc\<close> @ \<open>xyz\<close>"
wenzelm@55133
    95
term "\<open>\<newline>\<close>"
wenzelm@55133
    96
term "\<open>\001\010\100\<close>"
wenzelm@55109
    97
wenzelm@55109
    98
wenzelm@59068
    99
subsection \<open>Alternate outer and inner syntax: string literals\<close>
wenzelm@55109
   100
wenzelm@59068
   101
subsubsection \<open>Nested quotes\<close>
wenzelm@55109
   102
wenzelm@55133
   103
syntax "_string_string" :: "string_position \<Rightarrow> string"  ("_")
wenzelm@55109
   104
wenzelm@59068
   105
parse_translation \<open>
wenzelm@55133
   106
  [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
wenzelm@59068
   107
\<close>
wenzelm@55109
   108
wenzelm@55133
   109
term "\"\""
wenzelm@55133
   110
term "\"abc\""
wenzelm@55133
   111
term "\"abc\" @ \"xyz\""
wenzelm@55133
   112
term "\"\<newline>\""
wenzelm@55133
   113
term "\"\001\010\100\""
wenzelm@55109
   114
wenzelm@55109
   115
wenzelm@59068
   116
subsubsection \<open>Term cartouche and regular quotes\<close>
wenzelm@55109
   117
wenzelm@59068
   118
ML \<open>
wenzelm@59936
   119
  Outer_Syntax.command @{command_keyword term_cartouche} ""
wenzelm@55109
   120
    (Parse.inner_syntax Parse.cartouche >> (fn s =>
wenzelm@55109
   121
      Toplevel.keep (fn state =>
wenzelm@55109
   122
        let
wenzelm@55109
   123
          val ctxt = Toplevel.context_of state;
wenzelm@55109
   124
          val t = Syntax.read_term ctxt s;
wenzelm@55109
   125
        in writeln (Syntax.string_of_term ctxt t) end)))
wenzelm@59068
   126
\<close>
wenzelm@55109
   127
wenzelm@55133
   128
term_cartouche \<open>""\<close>
wenzelm@55133
   129
term_cartouche \<open>"abc"\<close>
wenzelm@55133
   130
term_cartouche \<open>"abc" @ "xyz"\<close>
wenzelm@55133
   131
term_cartouche \<open>"\<newline>"\<close>
wenzelm@55133
   132
term_cartouche \<open>"\001\010\100"\<close>
wenzelm@55033
   133
wenzelm@55047
   134
wenzelm@59068
   135
subsubsection \<open>Further nesting: antiquotations\<close>
wenzelm@55109
   136
wenzelm@55109
   137
setup -- "ML antiquotation"
wenzelm@59068
   138
\<open>
wenzelm@56072
   139
  ML_Antiquotation.inline @{binding term_cartouche}
wenzelm@55109
   140
    (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
wenzelm@55109
   141
      (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
wenzelm@59068
   142
\<close>
wenzelm@55109
   143
wenzelm@55109
   144
setup -- "document antiquotation"
wenzelm@59068
   145
\<open>
wenzelm@55109
   146
  Thy_Output.antiquotation @{binding ML_cartouche}
wenzelm@59809
   147
    (Scan.lift Args.cartouche_input) (fn {context, ...} => fn source =>
wenzelm@55109
   148
      let
wenzelm@59067
   149
        val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
wenzelm@59064
   150
        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
wenzelm@55109
   151
      in "" end);
wenzelm@59068
   152
\<close>
wenzelm@55109
   153
wenzelm@59068
   154
ML \<open>
wenzelm@55133
   155
  @{term_cartouche \<open>""\<close>};
wenzelm@55133
   156
  @{term_cartouche \<open>"abc"\<close>};
wenzelm@55133
   157
  @{term_cartouche \<open>"abc" @ "xyz"\<close>};
wenzelm@55133
   158
  @{term_cartouche \<open>"\<newline>"\<close>};
wenzelm@55133
   159
  @{term_cartouche \<open>"\001\010\100"\<close>};
wenzelm@59068
   160
\<close>
wenzelm@55109
   161
wenzelm@59068
   162
text \<open>
wenzelm@55109
   163
  @{ML_cartouche
wenzelm@55109
   164
    \<open>
wenzelm@55109
   165
      (
wenzelm@55133
   166
        @{term_cartouche \<open>""\<close>};
wenzelm@55133
   167
        @{term_cartouche \<open>"abc"\<close>};
wenzelm@55133
   168
        @{term_cartouche \<open>"abc" @ "xyz"\<close>};
wenzelm@55133
   169
        @{term_cartouche \<open>"\<newline>"\<close>};
wenzelm@55133
   170
        @{term_cartouche \<open>"\001\010\100"\<close>}
wenzelm@55109
   171
      )
wenzelm@55109
   172
    \<close>
wenzelm@55109
   173
  }
wenzelm@59068
   174
\<close>
wenzelm@55109
   175
wenzelm@55109
   176
wenzelm@59068
   177
subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close>
wenzelm@55109
   178
wenzelm@59068
   179
ML \<open>
wenzelm@55110
   180
  Outer_Syntax.command
wenzelm@59936
   181
    @{command_keyword text_cartouche} ""
wenzelm@59809
   182
    (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
wenzelm@59068
   183
\<close>
wenzelm@55109
   184
wenzelm@55109
   185
text_cartouche
wenzelm@55109
   186
\<open>
wenzelm@55109
   187
  @{ML_cartouche
wenzelm@55109
   188
    \<open>
wenzelm@55109
   189
      (
wenzelm@55133
   190
        @{term_cartouche \<open>""\<close>};
wenzelm@55133
   191
        @{term_cartouche \<open>"abc"\<close>};
wenzelm@55133
   192
        @{term_cartouche \<open>"abc" @ "xyz"\<close>};
wenzelm@55133
   193
        @{term_cartouche \<open>"\<newline>"\<close>};
wenzelm@55133
   194
        @{term_cartouche \<open>"\001\010\100"\<close>}
wenzelm@55109
   195
      )
wenzelm@55109
   196
    \<close>
wenzelm@55109
   197
  }
wenzelm@55109
   198
\<close>
wenzelm@55109
   199
wenzelm@55109
   200
wenzelm@59068
   201
subsection \<open>Proof method syntax: ML tactic expression\<close>
wenzelm@55047
   202
wenzelm@59068
   203
ML \<open>
wenzelm@55047
   204
structure ML_Tactic:
wenzelm@55047
   205
sig
wenzelm@55047
   206
  val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
wenzelm@59064
   207
  val ml_tactic: Input.source -> Proof.context -> tactic
wenzelm@55047
   208
end =
wenzelm@55047
   209
struct
wenzelm@55047
   210
  structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
wenzelm@55047
   211
wenzelm@55047
   212
  val set = Data.put;
wenzelm@55047
   213
wenzelm@55828
   214
  fun ml_tactic source ctxt =
wenzelm@55047
   215
    let
wenzelm@55047
   216
      val ctxt' = ctxt |> Context.proof_map
wenzelm@59064
   217
        (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
wenzelm@58991
   218
          "Context.map_proof (ML_Tactic.set tactic)"
wenzelm@59067
   219
          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
wenzelm@55047
   220
    in Data.get ctxt' ctxt end;
wenzelm@55047
   221
end;
wenzelm@59068
   222
\<close>
wenzelm@55047
   223
wenzelm@55048
   224
wenzelm@59068
   225
subsubsection \<open>Explicit version: method with cartouche argument\<close>
wenzelm@55048
   226
wenzelm@59068
   227
method_setup ml_tactic = \<open>
wenzelm@59809
   228
  Scan.lift Args.cartouche_input
wenzelm@55047
   229
    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
wenzelm@59068
   230
\<close>
wenzelm@55047
   231
wenzelm@55047
   232
lemma "A \<and> B \<longrightarrow> B \<and> A"
wenzelm@60754
   233
  apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>)
wenzelm@60754
   234
  apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>)
wenzelm@60754
   235
  apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
wenzelm@60754
   236
  apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>)
wenzelm@55047
   237
  done
wenzelm@55047
   238
wenzelm@55047
   239
lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
wenzelm@55047
   240
wenzelm@59068
   241
ML \<open>@{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
wenzelm@55047
   242
wenzelm@59068
   243
text \<open>@{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"}\<close>
wenzelm@55047
   244
wenzelm@55048
   245
wenzelm@59068
   246
subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close>
wenzelm@55048
   247
wenzelm@59068
   248
method_setup "cartouche" = \<open>
wenzelm@59809
   249
  Scan.lift Args.cartouche_input
wenzelm@55048
   250
    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
wenzelm@59068
   251
\<close>
wenzelm@55048
   252
wenzelm@55048
   253
lemma "A \<and> B \<longrightarrow> B \<and> A"
wenzelm@60754
   254
  apply \<open>resolve_tac @{context} @{thms impI} 1\<close>
wenzelm@60754
   255
  apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close>
wenzelm@60754
   256
  apply \<open>resolve_tac @{context} @{thms conjI} 1\<close>
wenzelm@60754
   257
  apply \<open>ALLGOALS (assume_tac @{context})\<close>
wenzelm@55048
   258
  done
wenzelm@55048
   259
wenzelm@55048
   260
lemma "A \<and> B \<longrightarrow> B \<and> A"
wenzelm@60754
   261
  by (\<open>resolve_tac @{context} @{thms impI} 1\<close>,
wenzelm@60754
   262
    \<open>eresolve_tac @{context} @{thms conjE} 1\<close>,
wenzelm@60754
   263
    \<open>resolve_tac @{context} @{thms conjI} 1\<close>,
wenzelm@60754
   264
    \<open>assume_tac @{context} 1\<close>+)
wenzelm@55048
   265
wenzelm@59112
   266
wenzelm@59128
   267
subsection \<open>ML syntax\<close>
wenzelm@59112
   268
wenzelm@59128
   269
text \<open>Input source with position information:\<close>
wenzelm@59112
   270
ML \<open>
wenzelm@59135
   271
  val s: Input.source = \<open>abc123def456\<close>;
wenzelm@59184
   272
  Output.information ("Look here!" ^ Position.here (Input.pos_of s));
wenzelm@59112
   273
wenzelm@59112
   274
  \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
wenzelm@59112
   275
    if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
wenzelm@59112
   276
\<close>
wenzelm@59112
   277
wenzelm@59128
   278
text \<open>Nested ML evaluation:\<close>
wenzelm@59128
   279
ML \<open>
wenzelm@59128
   280
  val ML = ML_Context.eval_source ML_Compiler.flags;
wenzelm@59128
   281
wenzelm@59128
   282
  ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
wenzelm@59128
   283
  ML \<open>val b = @{thm sym}\<close>;
wenzelm@59128
   284
  val c = @{thm trans}
wenzelm@59128
   285
  val thms = [a, b, c];
wenzelm@59128
   286
\<close>
wenzelm@59128
   287
wenzelm@55033
   288
end