--- 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
--- 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