src/Tools/Code_Generator.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69605 a96320074298
child 70009 435fb018e8ee
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:   Tools/Code_Generator.thy
     2     Author:  Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>Loading the code generator and related modules\<close>
     6 
     7 theory Code_Generator
     8 imports Pure
     9 keywords
    10   "print_codeproc" "code_thms" "code_deps" :: diag and
    11   "export_code" "code_identifier" "code_printing" "code_reserved"
    12     "code_monad" "code_reflect" :: thy_decl and
    13   "checking" and
    14   "datatypes" "functions" "module_name" "file"
    15     "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
    16     :: quasi_command
    17 begin
    18 
    19 ML_file \<open>~~/src/Tools/cache_io.ML\<close>
    20 ML_file \<open>~~/src/Tools/Code/code_preproc.ML\<close>
    21 ML_file \<open>~~/src/Tools/Code/code_symbol.ML\<close>
    22 ML_file \<open>~~/src/Tools/Code/code_thingol.ML\<close>
    23 ML_file \<open>~~/src/Tools/Code/code_simp.ML\<close>
    24 ML_file \<open>~~/src/Tools/Code/code_printer.ML\<close>
    25 ML_file \<open>~~/src/Tools/Code/code_target.ML\<close>
    26 ML_file \<open>~~/src/Tools/Code/code_namespace.ML\<close>
    27 ML_file \<open>~~/src/Tools/Code/code_ml.ML\<close>
    28 ML_file \<open>~~/src/Tools/Code/code_haskell.ML\<close>
    29 ML_file \<open>~~/src/Tools/Code/code_scala.ML\<close>
    30 
    31 code_datatype "TYPE('a::{})"
    32 
    33 definition holds :: "prop" where
    34   "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
    35 
    36 lemma holds: "PROP holds"
    37   by (unfold holds_def) (rule reflexive)
    38 
    39 code_datatype holds
    40 
    41 lemma implies_code [code]:
    42   "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
    43   "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
    44 proof -
    45   show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
    46   proof
    47     assume "PROP holds \<Longrightarrow> PROP P"
    48     then show "PROP P" using holds .
    49   next
    50     assume "PROP P"
    51     then show "PROP P" .
    52   qed
    53 next
    54   show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
    55     by rule (rule holds)+
    56 qed  
    57 
    58 ML_file \<open>~~/src/Tools/Code/code_runtime.ML\<close>
    59 ML_file \<open>~~/src/Tools/nbe.ML\<close>
    60 
    61 hide_const (open) holds
    62 
    63 end