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