# HG changeset patch
# User haftmann
# Date 1161333876 -7200
# Node ID 361e62500ab74576393a2cfede11c292d3b2e869
# Parent  a32d357dfd702e19f42942536f49ac6977afc01b
added if_delayed

diff -r a32d357dfd70 -r 361e62500ab7 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Fri Oct 20 10:44:35 2006 +0200
+++ b/src/HOL/Code_Generator.thy	Fri Oct 20 10:44:36 2006 +0200
@@ -115,7 +115,9 @@
   fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 defs
-  eq_def: "eq x y \<equiv> (x = y)"
+  eq_def [normal post]: "eq \<equiv> (op =)"
+
+lemmas [symmetric, code inline] = eq_def
 
 
 subsubsection {* bool type *}
@@ -134,9 +136,6 @@
 lemma [code func]:
   "eq p False = (\<not> p)" unfolding eq_def by auto
 
-code_constname
-  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
-
 
 subsubsection {* preprocessors *}
 
@@ -155,8 +154,6 @@
 in CodegenData.add_constrains constrain_op_eq end
 *}
 
-declare eq_def [symmetric, code inline]
-
 
 subsubsection {* Haskell *}
 
@@ -190,6 +187,22 @@
 end;
 *}
 
-hide (open) const eq
+text {* lazy @{const If} *}
+
+definition
+  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a"
+  "if_delayed b f g = (if b then f True else g False)"
+
+lemma [code func]:
+  shows "if_delayed True f g = f True"
+    and "if_delayed False f g = g False"
+  unfolding if_delayed_def by simp_all
+
+lemma [normal pre, symmetric, normal post]:
+  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
+  unfolding if_delayed_def ..
+
+
+hide (open) const eq if_delayed
 
 end
\ No newline at end of file
diff -r a32d357dfd70 -r 361e62500ab7 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Fri Oct 20 10:44:35 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri Oct 20 10:44:36 2006 +0200
@@ -2,7 +2,7 @@
     Authors:    Klaus Aehlig, Tobias Nipkow
 *)
 
-header "Test of normalization function"
+header {* Test of normalization function *}
 
 theory NormalForm
 imports Main
@@ -11,6 +11,7 @@
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code func]
 lemma "((P | Q) | R) = (P | (Q | R))" by normalization
+declare disj_assoc [code nofunc]
 lemma "0 + (n::nat) = n" by normalization
 lemma "0 + Suc n = Suc n" by normalization
 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
@@ -110,30 +111,8 @@
 normal_form "min 0 (x::nat)"
 lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
 
-(* Delaying if: FIXME move to HOL.thy(?) *)
-
-definition delayed_if :: "bool \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
-"delayed_if b f g = (if b then f() else g())"
-
-lemma [normal_pre]: "(if b then x else y) == delayed_if b (%u. x) (%u. y)"
-unfolding delayed_if_def by simp
-
-lemma [normal_post]: "delayed_if b f g == (if b then f() else g())"
-unfolding delayed_if_def by simp
+lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
 
-lemma [code func]:
- shows "delayed_if True f g = f()" and "delayed_if False f g = g()"
-by (auto simp:delayed_if_def)
-
-hide (open) const delayed_if
-
-normal_form "Code_Generator.eq [2..<4] [2,3]"
-(*lemma "Code_Generator.eq [2..<4] [2,3]" by normalization*)
-
-definition
- andalso :: "bool \<Rightarrow> bool \<Rightarrow> bool"
-"andalso x y = (if x then y else False)"
-
-lemma "andalso a b = (if a then b else False)" by normalization
+normal_form "Suc 0 \<in> set ms"
 
 end