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