# HG changeset patch
# User haftmann
# Date 1160551998 -7200
# Node ID 5294baa984687b95eda264148d7871e2a5f37f1f
# Parent  1df105407f8781edfa25a74f72d29ecb9d863b0f
added examples for nested let

diff -r 1df105407f87 -r 5294baa98468 src/HOL/ex/Codegenerator.thy
--- 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