more examples;
authorwenzelm
Thu Dec 04 20:56:38 2014 +0100 (2014-12-04)
changeset 59090a0a05a4edb36
parent 59089 da2fef2faa83
child 59091 4c8205fe3644
more examples;
src/Doc/Implementation/Integration.thy
src/HOL/ROOT
src/HOL/ex/Commands.thy
     1.1 --- a/src/Doc/Implementation/Integration.thy	Thu Dec 04 20:45:11 2014 +0100
     1.2 +++ b/src/Doc/Implementation/Integration.thy	Thu Dec 04 20:56:38 2014 +0100
     1.3 @@ -150,6 +150,10 @@
     1.4    \end{description}
     1.5  \<close>
     1.6  
     1.7 +text %mlex \<open>The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example
     1.8 +Isar command definitions, with the all-important theory header declarations
     1.9 +for outer syntax keywords.\<close>
    1.10 +
    1.11  
    1.12  section \<open>Theory loader database\<close>
    1.13  
     2.1 --- a/src/HOL/ROOT	Thu Dec 04 20:45:11 2014 +0100
     2.2 +++ b/src/HOL/ROOT	Thu Dec 04 20:56:38 2014 +0100
     2.3 @@ -539,6 +539,7 @@
     2.4      "~~/src/HOL/Library/Transitive_Closure_Table"
     2.5      Cartouche_Examples
     2.6    theories
     2.7 +    Commands
     2.8      Adhoc_Overloading_Examples
     2.9      Iff_Oracle
    2.10      Coercion_Examples
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Commands.thy	Thu Dec 04 20:56:38 2014 +0100
     3.3 @@ -0,0 +1,76 @@
     3.4 +(*  Title:      HOL/ex/Commands.thy
     3.5 +    Author:     Makarius
     3.6 +*)
     3.7 +
     3.8 +section \<open>Some Isar command definitions\<close>
     3.9 +
    3.10 +theory Commands
    3.11 +imports Main
    3.12 +keywords
    3.13 +  "print_test" :: diag and
    3.14 +  "global_test" :: thy_decl and
    3.15 +  "local_test" :: thy_decl
    3.16 +begin
    3.17 +
    3.18 +subsection \<open>Diagnostic command: no state change\<close>
    3.19 +
    3.20 +ML \<open>
    3.21 +  Outer_Syntax.command @{command_spec "print_test"} "print term test"
    3.22 +    (Parse.term >> (fn s => Toplevel.keep (fn st =>
    3.23 +      let
    3.24 +        val ctxt = Toplevel.context_of st;
    3.25 +        val t = Syntax.read_term ctxt s;
    3.26 +      in Pretty.writeln (Syntax.pretty_term ctxt t) end)));
    3.27 +\<close>
    3.28 +
    3.29 +print_test x
    3.30 +print_test "\<lambda>x. x = a"
    3.31 +
    3.32 +
    3.33 +subsection \<open>Old-style global theory declaration\<close>
    3.34 +
    3.35 +ML \<open>
    3.36 +  Outer_Syntax.command @{command_spec "global_test"} "test constant declaration"
    3.37 +    (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
    3.38 +      let
    3.39 +        val thy' = Sign.add_consts [(b, @{typ 'a}, NoSyn)] thy;
    3.40 +      in thy' end)));
    3.41 +\<close>
    3.42 +
    3.43 +global_test a
    3.44 +global_test b
    3.45 +print_test a
    3.46 +
    3.47 +
    3.48 +subsection \<open>Local theory specification\<close>
    3.49 +
    3.50 +ML \<open>
    3.51 +  Outer_Syntax.local_theory @{command_spec "local_test"} "test local definition"
    3.52 +    (Parse.binding -- (@{keyword "="} |-- Parse.term) >> (fn (b, s) => fn lthy =>
    3.53 +      let
    3.54 +        val t = Syntax.read_term lthy s;
    3.55 +        val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy;
    3.56 +      in lthy' end));
    3.57 +\<close>
    3.58 +
    3.59 +local_test true = True
    3.60 +print_test true
    3.61 +thm true_def
    3.62 +
    3.63 +local_test identity = "\<lambda>x. x"
    3.64 +print_test "identity x"
    3.65 +thm identity_def
    3.66 +
    3.67 +context fixes x y :: nat
    3.68 +begin
    3.69 +
    3.70 +local_test test = "x + y"
    3.71 +print_test test
    3.72 +thm test_def
    3.73 +
    3.74 +end
    3.75 +
    3.76 +print_test "test 0 1"
    3.77 +thm test_def
    3.78 +
    3.79 +end