src/HOL/ex/Commands.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 59936 b8ffc3dc9e24
child 67096 e77f13a6a501
permissions -rw-r--r--
bundle lifting_syntax;
     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 print_test} "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       in Pretty.writeln (Syntax.pretty_term ctxt t) end)));
    24 \<close>
    25 
    26 print_test x
    27 print_test "\<lambda>x. x = a"
    28 
    29 
    30 subsection \<open>Old-style global theory declaration\<close>
    31 
    32 ML \<open>
    33   Outer_Syntax.command @{command_keyword global_test} "test constant declaration"
    34     (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
    35       let
    36         val thy' = Sign.add_consts [(b, @{typ 'a}, NoSyn)] thy;
    37       in thy' end)));
    38 \<close>
    39 
    40 global_test a
    41 global_test b
    42 print_test a
    43 
    44 
    45 subsection \<open>Local theory specification\<close>
    46 
    47 ML \<open>
    48   Outer_Syntax.local_theory @{command_keyword local_test} "test local definition"
    49     (Parse.binding -- (@{keyword "="} |-- Parse.term) >> (fn (b, s) => fn lthy =>
    50       let
    51         val t = Syntax.read_term lthy s;
    52         val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy;
    53       in lthy' end));
    54 \<close>
    55 
    56 local_test true = True
    57 print_test true
    58 thm true_def
    59 
    60 local_test identity = "\<lambda>x. x"
    61 print_test "identity x"
    62 thm identity_def
    63 
    64 context fixes x y :: nat
    65 begin
    66 
    67 local_test test = "x + y"
    68 print_test test
    69 thm test_def
    70 
    71 end
    72 
    73 print_test "test 0 1"
    74 thm test_def
    75 
    76 end