(* Title: HOL/IOA/example/Correctness.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
The main correctness proof: System_fin implements System
*)
Correctness = Solve + Env + Impl + Impl_finite +
consts
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 [] = []"
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_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