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