Quelle Code_Generator.thy Sprache: 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 P \ PROP holds) \ PROP holds"
  "(PROP holds \ PROP P) \ PROP P"
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

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.