# HG changeset patch
# User haftmann
# Date 1290880264 -3600
# Node ID e3d4f2522a5f96a8fec319eb8ba24fe91ccfc102
# Parent  5288144b43582aea55fa4281f931bba886e2959e
added equation for Queue;
tuned proofs

diff -r 5288144b4358 -r e3d4f2522a5f doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy	Sat Nov 27 18:51:04 2010 +0100
+++ b/doc-src/Codegen/Thy/Refinement.thy	Sat Nov 27 18:51:04 2010 +0100
@@ -131,34 +131,40 @@
 
 lemma %quote empty_AQueue [code]:
   "empty = AQueue [] []"
-  unfolding AQueue_def empty_def by simp
+  by (simp add: AQueue_def empty_def)
 
 lemma %quote enqueue_AQueue [code]:
   "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
-  unfolding AQueue_def by simp
+  by (simp add: AQueue_def)
 
 lemma %quote dequeue_AQueue [code]:
   "dequeue (AQueue xs []) =
     (if xs = [] then (None, AQueue [] [])
     else dequeue (AQueue [] (rev xs)))"
   "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
-  unfolding AQueue_def by simp_all
+  by (simp_all add: AQueue_def)
 
 text {*
-  \noindent For completeness, we provide a substitute for the
-  @{text case} combinator on queues:
+  \noindent It is good style, although no absolute requirement, to
+  provide code equations for the original artefacts of the implemented
+  type, if possible; in our case, these are the datatype constructor
+  @{const Queue} and the case combinator @{const queue_case}:
 *}
 
+lemma %quote Queue_AQueue [code]:
+  "Queue = AQueue []"
+  by (simp add: AQueue_def fun_eq_iff)
+
 lemma %quote queue_case_AQueue [code]:
   "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
-  unfolding AQueue_def by simp
+  by (simp add: AQueue_def)
 
 text {*
   \noindent The resulting code looks as expected:
 *}
 
 text %quotetypewriter {*
-  @{code_stmts empty enqueue dequeue (SML)}
+  @{code_stmts empty enqueue dequeue Queue queue_case (SML)}
 *}
 
 text {*
@@ -260,7 +266,7 @@
 text {*
   Typical data structures implemented by representations involving
   invariants are available in the library, e.g.~theories @{theory
-  Fset} and @{theory Mapping} specify sets (type @{typ "'a fset"}) and
+  Cset} and @{theory Mapping} specify sets (type @{typ "'a Cset.set"}) and
   key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively;
   these can be implemented by distinct lists as presented here as
   example (theory @{theory Dlist}) and red-black-trees respectively