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