1(*  Title:   Tools/Code_Generator.thy
2    Author:  Florian Haftmann, TU Muenchen
3*)
4
5section \<open>Loading the code generator and related modules\<close>
6
7theory Code_Generator
8imports Pure
9keywords
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" "file_prefix"
15    "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
16    :: quasi_command
17begin
18
19ML_file \<open>~~/src/Tools/cache_io.ML\<close>
20ML_file \<open>~~/src/Tools/Code/code_preproc.ML\<close>
21ML_file \<open>~~/src/Tools/Code/code_symbol.ML\<close>
22ML_file \<open>~~/src/Tools/Code/code_thingol.ML\<close>
23ML_file \<open>~~/src/Tools/Code/code_simp.ML\<close>
24ML_file \<open>~~/src/Tools/Code/code_printer.ML\<close>
25ML_file \<open>~~/src/Tools/Code/code_target.ML\<close>
26ML_file \<open>~~/src/Tools/Code/code_namespace.ML\<close>
27ML_file \<open>~~/src/Tools/Code/code_ml.ML\<close>
28ML_file \<open>~~/src/Tools/Code/code_haskell.ML\<close>
29ML_file \<open>~~/src/Tools/Code/code_scala.ML\<close>
30
31code_datatype "TYPE('a::{})"
32
33definition holds :: "prop" where
34  "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
35
36lemma holds: "PROP holds"
37  by (unfold holds_def) (rule reflexive)
38
39code_datatype holds
40
41lemma implies_code [code]:
42  "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
43  "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
44proof -
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
53next
54  show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
55    by rule (rule holds)+
56qed  
57
58ML_file \<open>~~/src/Tools/Code/code_runtime.ML\<close>
59ML_file \<open>~~/src/Tools/nbe.ML\<close>
60
61hide_const (open) holds
62
63end
64