1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy Wed Apr 30 11:24:14 1997 +0200
1.3 @@ -0,0 +1,49 @@
1.4 +(* Title: HOLCF/IOA/ABP/Correctness.thy
1.5 + ID: $Id$
1.6 + Author: Olaf Mueller
1.7 + Copyright 1995 TU Muenchen
1.8 +
1.9 +The main correctness proof: System_fin implements System
1.10 +*)
1.11 +
1.12 +Correctness = IOA + Env + Impl + Impl_finite +
1.13 +
1.14 +consts
1.15 +
1.16 +reduce :: 'a list => 'a list
1.17 +
1.18 +abs :: 'c
1.19 +system_ioa :: "('m action, bool * 'm impl_state)ioa"
1.20 +system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
1.21 +
1.22 +primrec
1.23 + reduce List.list
1.24 + reduce_Nil "reduce [] = []"
1.25 + reduce_Cons "reduce(x#xs) =
1.26 + (case xs of
1.27 + [] => [x]
1.28 + | y#ys => (if (x=y)
1.29 + then reduce xs
1.30 + else (x#(reduce xs))))"
1.31 +
1.32 +
1.33 +defs
1.34 +
1.35 +system_def
1.36 + "system_ioa == (env_ioa || impl_ioa)"
1.37 +
1.38 +system_fin_def
1.39 + "system_fin_ioa == (env_ioa || impl_fin_ioa)"
1.40 +
1.41 +abs_def "abs ==
1.42 + (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
1.43 + (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
1.44 +
1.45 +rules
1.46 +
1.47 + sys_IOA "IOA system_ioa"
1.48 + sys_fin_IOA "IOA system_fin_ioa"
1.49 +
1.50 +end
1.51 +
1.52 +