src/HOLCF/IOA/meta_theory/Abstraction.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1997  TU Muenchen
     5 
     6 Abstraction Theory -- tailored for I/O automata
     7 *)   
     8 
     9 		       
    10 Abstraction = LiveIOA + 
    11 
    12 default term
    13 
    14 
    15 consts
    16 
    17   cex_abs      ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
    18   cex_absSeq   ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq"
    19 
    20   is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
    21 
    22   weakeningIOA       :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" 
    23   temp_weakening     :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" 
    24   temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" 
    25 
    26   state_weakening       :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
    27   state_strengthening   :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
    28 
    29   is_live_abstraction  :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    30 
    31 
    32 defs
    33 
    34 is_abstraction_def
    35   "is_abstraction f C A ==                          
    36    (!s:starts_of(C). f(s):starts_of(A)) &        
    37    (!s t a. reachable C s & s -a--C-> t     
    38             --> (f s) -a--A-> (f t))"
    39 
    40 is_live_abstraction_def
    41   "is_live_abstraction h CL AM == 
    42       is_abstraction h (fst CL) (fst AM) &
    43       temp_weakening (snd AM) (snd CL) h"
    44 
    45 cex_abs_def
    46   "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
    47 
    48 (* equals cex_abs on Sequneces -- after ex2seq application -- *)
    49 cex_absSeq_def
    50   "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s"
    51 
    52 weakeningIOA_def
    53    "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
    54 
    55 temp_weakening_def
    56    "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h"
    57 
    58 temp_strengthening_def
    59    "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)"
    60 
    61 state_weakening_def
    62   "state_weakening Q P h == state_strengthening (.~Q) (.~P) h"
    63 
    64 state_strengthening_def
    65   "state_strengthening Q P h == ! s t a.  Q (h(s),a,h(t)) --> P (s,a,t)"
    66 
    67 rules
    68 
    69 (* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
    70 ex2seq_abs_cex
    71   "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" 
    72 
    73 (* analog to the proved thm strength_Box - proof skipped as trivial *)
    74 weak_Box
    75 "temp_weakening P Q h 
    76  ==> temp_weakening ([] P) ([] Q) h"
    77 
    78 (* analog to the proved thm strength_Next - proof skipped as trivial *)
    79 weak_Next
    80 "temp_weakening P Q h 
    81  ==> temp_weakening (Next P) (Next Q) h"
    82 
    83 end