src/HOL/ex/Commands.thy
author wenzelm
Sat Jan 05 17:24:33 2019 +0100 (10 months ago)
changeset 69597 ff784d5a5bfb
parent 67096 e77f13a6a501
child 70308 7f568724d67e
permissions -rw-r--r--
isabelle update -u control_cartouches;
wenzelm@59090
     1
(*  Title:      HOL/ex/Commands.thy
wenzelm@59090
     2
    Author:     Makarius
wenzelm@59090
     3
*)
wenzelm@59090
     4
wenzelm@59090
     5
section \<open>Some Isar command definitions\<close>
wenzelm@59090
     6
wenzelm@59090
     7
theory Commands
wenzelm@59090
     8
imports Main
wenzelm@59090
     9
keywords
wenzelm@59090
    10
  "print_test" :: diag and
wenzelm@59090
    11
  "global_test" :: thy_decl and
wenzelm@59090
    12
  "local_test" :: thy_decl
wenzelm@59090
    13
begin
wenzelm@59090
    14
wenzelm@59090
    15
subsection \<open>Diagnostic command: no state change\<close>
wenzelm@59090
    16
wenzelm@59090
    17
ML \<open>
wenzelm@69597
    18
  Outer_Syntax.command \<^command_keyword>\<open>print_test\<close> "print term test"
wenzelm@59090
    19
    (Parse.term >> (fn s => Toplevel.keep (fn st =>
wenzelm@59090
    20
      let
wenzelm@59090
    21
        val ctxt = Toplevel.context_of st;
wenzelm@59090
    22
        val t = Syntax.read_term ctxt s;
wenzelm@67096
    23
        val ctxt' = Variable.auto_fixes t ctxt;
wenzelm@67096
    24
      in Pretty.writeln (Syntax.pretty_term ctxt' t) end)));
wenzelm@59090
    25
\<close>
wenzelm@59090
    26
wenzelm@59090
    27
print_test x
wenzelm@59090
    28
print_test "\<lambda>x. x = a"
wenzelm@59090
    29
wenzelm@59090
    30
wenzelm@59090
    31
subsection \<open>Old-style global theory declaration\<close>
wenzelm@59090
    32
wenzelm@59090
    33
ML \<open>
wenzelm@69597
    34
  Outer_Syntax.command \<^command_keyword>\<open>global_test\<close> "test constant declaration"
wenzelm@59090
    35
    (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
wenzelm@59090
    36
      let
wenzelm@69597
    37
        val thy' = Sign.add_consts [(b, \<^typ>\<open>'a\<close>, NoSyn)] thy;
wenzelm@59090
    38
      in thy' end)));
wenzelm@59090
    39
\<close>
wenzelm@59090
    40
wenzelm@59090
    41
global_test a
wenzelm@59090
    42
global_test b
wenzelm@59090
    43
print_test a
wenzelm@59090
    44
wenzelm@59090
    45
wenzelm@59090
    46
subsection \<open>Local theory specification\<close>
wenzelm@59090
    47
wenzelm@59090
    48
ML \<open>
wenzelm@69597
    49
  Outer_Syntax.local_theory \<^command_keyword>\<open>local_test\<close> "test local definition"
wenzelm@69597
    50
    (Parse.binding -- (\<^keyword>\<open>=\<close> |-- Parse.term) >> (fn (b, s) => fn lthy =>
wenzelm@59090
    51
      let
wenzelm@59090
    52
        val t = Syntax.read_term lthy s;
wenzelm@59090
    53
        val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy;
wenzelm@59090
    54
      in lthy' end));
wenzelm@59090
    55
\<close>
wenzelm@59090
    56
wenzelm@59090
    57
local_test true = True
wenzelm@59090
    58
print_test true
wenzelm@59090
    59
thm true_def
wenzelm@59090
    60
wenzelm@59090
    61
local_test identity = "\<lambda>x. x"
wenzelm@59090
    62
print_test "identity x"
wenzelm@59090
    63
thm identity_def
wenzelm@59090
    64
wenzelm@59090
    65
context fixes x y :: nat
wenzelm@59090
    66
begin
wenzelm@59090
    67
wenzelm@59090
    68
local_test test = "x + y"
wenzelm@59090
    69
print_test test
wenzelm@59090
    70
thm test_def
wenzelm@59090
    71
wenzelm@59090
    72
end
wenzelm@59090
    73
wenzelm@59090
    74
print_test "test 0 1"
wenzelm@59090
    75
thm test_def
wenzelm@59090
    76
wenzelm@59090
    77
end