Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Code_Generator.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:   Tools/Code_Generator.thy
    Author:  Florian Haftmann, TU Muenchen
*)

section \<open>Loading the code generator and related modules\<close>

theory Code_Generator
imports Pure
keywords
  "print_codeproc" "code_thms" "code_deps" :: diag and
  "export_code" "code_identifier" "code_printing" "code_reserved"
    "code_monad" "code_reflect" :: thy_decl and
  "checking" and
  "datatypes" "functions" "module_name" "file" "file_prefix"
    "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
    :: quasi_command
begin

ML_file \<open>~~/src/Tools/cache_io.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_preproc.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_symbol.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_thingol.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_simp.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_printer.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_target.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_namespace.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_ml.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_haskell.ML\<close>
ML_file \<open>~~/src/Tools/Code/code_scala.ML\<close>

code_datatype "TYPE('a::{})"

definition holds :: "prop" where
  "holds \ ((\x::prop. x) \ (\x. x))"

lemma holds: "PROP holds"
  by (unfold holds_def) (rule reflexive)

code_datatype holds

lemma implies_code [code]:
  "(PROP holds \ PROP P) \ PROP P"
  "(PROP P \ PROP holds) \ PROP holds"
proof -
  show "(PROP holds \ PROP P) \ PROP P"
  proof
    assume "PROP holds \ PROP P"
    then show "PROP P" using holds .
  next
    assume "PROP P"
    then show "PROP P" .
  qed
next
  show "(PROP P \ PROP holds) \ PROP holds"
    by rule (rule holds)+
qed

ML_file \<open>~~/src/Tools/Code/code_runtime.ML\<close>
ML_file \<open>~~/src/Tools/nbe.ML\<close>

hide_const (open) holds

end

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.