src/HOL/IOA/ABP/Correctness.thy
author clasohm
Mon, 05 Feb 1996 21:29:06 +0100
changeset 1476 608483c2122a
parent 1376 92f83b9d17e1
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes

(*  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