# HG changeset patch
# User haftmann
# Date 1284562051 -7200
# Node ID b6a77cffc231667e55766f0744b68929058d5538
# Parent  a8c337299bc18f36f3f1ddfb55a61addb765cfd6
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy

diff -r a8c337299bc1 -r b6a77cffc231 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 15 15:40:36 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 15 16:47:31 2010 +0200
@@ -1802,21 +1802,10 @@
 
 subsubsection {* Generic code generator foundation *}
 
-text {* Datatypes *}
+text {* Datatype @{typ bool} *}
 
 code_datatype True False
 
-code_datatype "TYPE('a\<Colon>{})"
-
-code_datatype "prop" Trueprop
-
-text {* Code equations *}
-
-lemma [code]:
-  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
-    and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
-    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
-
 lemma [code]:
   shows "False \<and> P \<longleftrightarrow> False"
     and "True \<and> P \<longleftrightarrow> P"
@@ -1835,6 +1824,23 @@
     and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
     and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
 
+text {* More about @{typ prop} *}
+
+lemma [code nbe]:
+  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
+    and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
+    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
+
+lemma Trueprop_code [code]:
+  "Trueprop True \<equiv> Code_Generator.holds"
+  by (auto intro!: equal_intr_rule holds)
+
+declare Trueprop_code [symmetric, code_post]
+
+text {* Equality *}
+
+declare simp_thms(6) [code nbe]
+
 instantiation itself :: (type) equal
 begin
 
@@ -1850,10 +1856,6 @@
   "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   by (simp add: equal)
 
-text {* Equality *}
-
-declare simp_thms(6) [code nbe]
-
 setup {*
   Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
 *}
diff -r a8c337299bc1 -r b6a77cffc231 src/Tools/Code_Generator.thy
--- 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