# HG changeset patch
# User nipkow
# Date 1160389239 -7200
# Node ID 24b8536dcf937666aa13d519e784ebfec3f455ed
# Parent  07f27994066414253a9eda15528035bd4d21e108
added delayed_if

diff -r 07f279940664 -r 24b8536dcf93 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Mon Oct 09 12:16:29 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy	Mon Oct 09 12:20:39 2006 +0200
@@ -110,4 +110,21 @@
 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 [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 "OperationalEquality.eq [2..<4] [2,3]"
+(*lemma "OperationalEquality.eq [2..<4] [2,3]" by normalization*)
+
 end