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
mueller@1138
     1
(*  Title:      HOL/IOA/example/Correctness.thy
nipkow@1050
     2
    ID:         $Id$
mueller@1138
     3
    Author:     Tobias Nipkow & Konrad Slind
nipkow@1050
     4
    Copyright   1994  TU Muenchen
nipkow@1050
     5
nipkow@1050
     6
The main correctness proof: System_fin implements System
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
Correctness = Solve + Env + Impl + Impl_finite + 
nipkow@1050
    10
nipkow@1050
    11
consts
nipkow@1050
    12
clasohm@1376
    13
reduce           :: 'a list => 'a list
nipkow@1050
    14
clasohm@1376
    15
abs              :: 'c
mueller@1138
    16
system_ioa       :: "('m action, bool * 'm impl_state)ioa"
mueller@1138
    17
system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
mueller@1138
    18
  
nipkow@1050
    19
primrec
nipkow@1050
    20
  reduce List.list  
nipkow@1050
    21
  reduce_Nil  "reduce [] = []"
clasohm@1151
    22
  reduce_Cons "reduce(x#xs) =   
clasohm@1476
    23
                 (case xs of   
clasohm@1476
    24
                     [] => [x]   
clasohm@1476
    25
               |   y#ys => (if (x=y)   
clasohm@1476
    26
                              then reduce xs   
clasohm@1476
    27
                              else (x#(reduce xs))))"
nipkow@1050
    28
mueller@1138
    29
  
mueller@1138
    30
defs
mueller@1138
    31
  
mueller@1138
    32
system_def
mueller@1138
    33
  "system_ioa == (env_ioa || impl_ioa)"
mueller@1138
    34
mueller@1138
    35
system_fin_def
mueller@1138
    36
  "system_fin_ioa == (env_ioa || impl_fin_ioa)"
mueller@1138
    37
  
clasohm@1151
    38
abs_def "abs  ==   
clasohm@1476
    39
        (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
clasohm@1476
    40
         (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
mueller@1138
    41
mueller@1138
    42
rules
mueller@1138
    43
mueller@1138
    44
  sys_IOA     "IOA system_ioa"
mueller@1138
    45
  sys_fin_IOA "IOA system_fin_ioa"
mueller@1138
    46
  
nipkow@1050
    47
end
nipkow@1050
    48
nipkow@1050
    49