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