# HG changeset patch
# User nipkow
# Date 779723300 -7200
# Node ID 6254f50e5ec959f80a288ad36dfc71094573b9cd
# Parent  3226f25f88e7d9bfead832ae1df93fd8b2fe0f4b
Definition of C was not truly prim rec because C was called inside Gamma
instead of outside.

diff -r 3226f25f88e7 -r 6254f50e5ec9 IMP/Denotation.thy
--- a/IMP/Denotation.thy	Thu Sep 15 18:42:12 1994 +0200
+++ b/IMP/Denotation.thy	Fri Sep 16 15:48:20 1994 +0200
@@ -8,11 +8,12 @@
 
 Denotation = Com + 
 
+types com_den = "(state*state)set"
 consts
   A     :: "aexp => state => nat"
   B     :: "bexp => state => bool"
-  C     :: "com => (state*state)set"
-  Gamma :: "[bexp,com,(state*state)set] => (state*state)set"
+  C     :: "com => com_den"
+  Gamma :: "[bexp,com_den] => (com_den => com_den)"
 
 primrec A aexp
   A_nat	"A(N(n)) = (%s. n)"
@@ -29,17 +30,17 @@
   B_or	  "B(b0 ori b1) = (%s. B(b0,s) | B(b1,s))"
 
 defs
-  Gamma_def	"Gamma(b,c) ==   \
-\		   (%phi.{io. io : (phi O C(c)) & B(b,fst(io))} Un \
-\	                 {io. io : id & ~B(b,fst(io))})"
+  Gamma_def	"Gamma(b,cd) ==   \
+\		   (%phi.{st. st : (phi O cd) & B(b,fst(st))} Un \
+\	                 {st. st : id & ~B(b,fst(st))})"
 
 primrec C com
   C_skip    "C(skip) = id"
-  C_assign  "C(x := a) = {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
+  C_assign  "C(x := a) = {st . snd(st) = fst(st)[A(a,fst(st))/x]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
   C_if	    "C(ifc b then c0 else c1) =   \
-\		   {io. io:C(c0) & B(b,fst(io))} Un \
-\	           {io. io:C(c1) & ~B(b,fst(io))}"
-  C_while   "C(while b do c) = lfp(Gamma(b,c))"
+\		   {st. st:C(c0) & B(b,fst(st))} Un \
+\	           {st. st:C(c1) & ~B(b,fst(st))}"
+  C_while   "C(while b do c) = lfp(Gamma(b,C(c)))"
 
 end