--- a/src/HOL/ex/Codegenerator.thy Wed Oct 11 08:57:47 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy Wed Oct 11 09:33:18 2006 +0200
@@ -42,11 +42,13 @@
k :: "int"
"k = -42"
-consts
- fac :: "int => int"
+function
+ fac :: "int => int" where
+ "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
+ by pat_completeness auto
+termination by (auto_term "measure nat")
-recdef fac "measure nat"
- "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
+declare fac.simps [code]
subsection {* sums *}
@@ -84,6 +86,17 @@
definition
"mystring = ''my home is my castle''"
+subsection {* nested lets and such *}
+
+definition
+ "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
+
+definition
+ "nested_let x = (let (y, z) = x in let w = y z in w * w)"
+
+definition
+ "case_let x = (let (y, z) = x in case y of () => z)"
+
subsection {* heavy usage of names *}
definition
@@ -151,6 +164,8 @@
f g h
code_gen
apply_tower Codegenerator.keywords shadow
+code_gen
+ abs_let nested_let case_let
code_gen "0::int" "1::int"
(SML) (Haskell)
code_gen n