--- a/src/HOL/IOA/ABP/Correctness.thy Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Correctness.thy Wed May 31 10:45:00 1995 +0200
@@ -1,6 +1,6 @@
-(* Title: HOL/IOA/ABP/Correctness.thy
+(* Title: HOL/IOA/example/Correctness.thy
ID: $Id$
- Author: Tobias Nipkow & Olaf Mueller
+ Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
The main correctness proof: System_fin implements System
@@ -10,8 +10,12 @@
consts
-reduce :: "'a list => 'a list"
+reduce :: "'a list => 'a list"
+abs :: "'c"
+system_ioa :: "('m action, bool * 'm impl_state)ioa"
+system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
+
primrec
reduce List.list
reduce_Nil "reduce [] = []"
@@ -22,6 +26,24 @@
\ then reduce xs \
\ else (x#(reduce xs))))"
+
+defs
+
+system_def
+ "system_ioa == (env_ioa || impl_ioa)"
+
+system_fin_def
+ "system_fin_ioa == (env_ioa || impl_fin_ioa)"
+
+abs_def "abs == \
+\ (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), \
+\ (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
+
+rules
+
+ sys_IOA "IOA system_ioa"
+ sys_fin_IOA "IOA system_fin_ioa"
+
end