src/HOL/IOA/ABP/Correctness.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1476 608483c2122a
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
     1 (*  Title:      HOL/IOA/example/Correctness.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 
     6 The main correctness proof: System_fin implements System
     7 *)
     8 
     9 Correctness = Solve + Env + Impl + Impl_finite + 
    10 
    11 consts
    12 
    13 reduce           :: 'a list => 'a list
    14 
    15 abs              :: 'c
    16 system_ioa       :: "('m action, bool * 'm impl_state)ioa"
    17 system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
    18   
    19 primrec
    20   reduce List.list  
    21   reduce_Nil  "reduce [] = []"
    22   reduce_Cons "reduce(x#xs) =   
    23                  (case xs of   
    24                      [] => [x]   
    25                |   y#ys => (if (x=y)   
    26                               then reduce xs   
    27                               else (x#(reduce xs))))"
    28 
    29   
    30 defs
    31   
    32 system_def
    33   "system_ioa == (env_ioa || impl_ioa)"
    34 
    35 system_fin_def
    36   "system_fin_ioa == (env_ioa || impl_fin_ioa)"
    37   
    38 abs_def "abs  ==   
    39         (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
    40          (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
    41 
    42 rules
    43 
    44   sys_IOA     "IOA system_ioa"
    45   sys_fin_IOA "IOA system_fin_ioa"
    46   
    47 end
    48 
    49