--- a/src/Tools/Code_Generator.thy Wed Sep 15 15:40:36 2010 +0200
+++ b/src/Tools/Code_Generator.thy Wed Sep 15 16:47:31 2010 +0200
@@ -21,10 +21,39 @@
"~~/src/Tools/Code/code_ml.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/Code/code_scala.ML"
- "~~/src/Tools/Code/code_runtime.ML"
+ ("~~/src/Tools/Code/code_runtime.ML")
"~~/src/Tools/nbe.ML"
begin
+code_datatype "TYPE('a\<Colon>{})"
+
+definition holds :: "prop" where
+ "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
+
+lemma holds: "PROP holds"
+ by (unfold holds_def) (rule reflexive)
+
+code_datatype holds
+
+lemma implies_code [code]:
+ "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
+ "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
+proof -
+ show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
+ proof
+ assume "PROP holds \<Longrightarrow> PROP P"
+ then show "PROP P" using holds .
+ next
+ assume "PROP P"
+ then show "PROP P" .
+ qed
+next
+ show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
+ by rule (rule holds)+
+qed
+
+use "~~/src/Tools/Code/code_runtime.ML"
+
setup {*
Auto_Solve.setup
#> Code_Preproc.setup
@@ -37,4 +66,6 @@
#> Quickcheck.setup
*}
+hide_const (open) holds
+
end