src/HOL/ex/NormalForm.thy
changeset 20922 14873e42659c
parent 20921 24b8536dcf93
child 21046 fe1db2f991a7
--- a/src/HOL/ex/NormalForm.thy	Mon Oct 09 12:20:39 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy	Mon Oct 09 12:51:31 2006 +0200
@@ -118,6 +118,9 @@
 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 [code func]:
  shows "delayed_if True f g = f()" and "delayed_if False f g = g()"
 by (auto simp:delayed_if_def)
@@ -127,4 +130,10 @@
 normal_form "OperationalEquality.eq [2..<4] [2,3]"
 (*lemma "OperationalEquality.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
+
 end