merged

--- a/src/HOL/HOL.thy	Wed Sep 15 17:05:18 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 15 19:20:50 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"})
 *}

--- a/src/Tools/Code/code_runtime.ML	Wed Sep 15 17:05:18 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Wed Sep 15 19:20:50 2010 +0200
@@ -10,6 +10,8 @@
   val value: string option
     -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
     -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
+  val code_reflect: (string * string list) list -> string list -> string -> string option
+    -> theory -> theory
   val setup: theory -> theory
 end;
 
@@ -20,6 +22,8 @@
 
 val target = "Eval";
 
+val truth_struct = "Code_Truth";
+
 fun value some_target cookie postproc thy t args =
   let
     val ctxt = ProofContext.init_global thy;
@@ -184,7 +188,7 @@
     |> process result module_name some_file
   end;
 
-val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
+val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
 val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
 
 

--- a/src/Tools/Code_Generator.thy	Wed Sep 15 17:05:18 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Wed Sep 15 19:20:50 2010 +0200
@@ -37,4 +37,33 @@
   #> Quickcheck.setup
 *}
 
+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  
+
+hide_const (open) holds
+
 end