--- a/src/HOLCF/IOA/ABP/Correctness.thy Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Sat Sep 03 16:50:22 2005 +0200
@@ -1,47 +1,49 @@
(* Title: HOLCF/IOA/ABP/Correctness.thy
ID: $Id$
Author: Olaf Müller
-
-The main correctness proof: System_fin implements System.
*)
-Correctness = IOA + Env + Impl + Impl_finite +
+header {* The main correctness proof: System_fin implements System *}
+
+theory Correctness
+imports IOA Env Impl Impl_finite
+begin
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_Nil "reduce [] = []"
- reduce_Cons "reduce(x#xs) =
- (case xs of
- [] => [x]
- | y#ys => (if (x=y)
- then reduce xs
+ reduce_Nil: "reduce [] = []"
+ reduce_Cons: "reduce(x#xs) =
+ (case xs of
+ [] => [x]
+ | y#ys => (if (x=y)
+ then reduce xs
else (x#(reduce xs))))"
-
+
defs
-
-system_def
+
+system_def:
"system_ioa == (env_ioa || impl_ioa)"
-system_fin_def
+system_fin_def:
"system_fin_ioa == (env_ioa || impl_fin_ioa)"
-
-abs_def "abs ==
- (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
+
+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
+axioms
- sys_IOA "IOA system_ioa"
- sys_fin_IOA "IOA system_fin_ioa"
-
+ sys_IOA: "IOA system_ioa"
+ sys_fin_IOA: "IOA system_fin_ioa"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
-
-