src/HOLCF/IOA/meta_theory/LiveIOA.thy
author wenzelm
Sun May 28 19:54:20 2006 +0200 (2006-05-28)
changeset 19741 f65265d71426
parent 17233 41eee2e7b465
child 25135 4f8176c940cf
permissions -rw-r--r--
removed legacy ML scripts;
     1 (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4 *)
     5 
     6 header {* Live I/O automata -- specified by temproal formulas *}
     7 
     8 theory LiveIOA
     9 imports TLS
    10 begin
    11 
    12 defaultsort type
    13 
    14 types
    15   ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
    16 
    17 consts
    18 
    19 validLIOA   :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool"
    20 
    21 WF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
    22 SF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
    23 
    24 liveexecutions    :: "('a,'s)live_ioa => ('a,'s)execution set"
    25 livetraces        :: "('a,'s)live_ioa => 'a trace set"
    26 live_implements   :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    27 is_live_ref_map   :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    28 
    29 
    30 defs
    31 
    32 validLIOA_def:
    33   "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
    34 
    35 
    36 WF_def:
    37   "WF A acts ==  <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    38 
    39 SF_def:
    40   "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    41 
    42 
    43 liveexecutions_def:
    44    "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    45 
    46 livetraces_def:
    47   "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    48 
    49 live_implements_def:
    50   "live_implements CL AM == (inp (fst CL) = inp (fst AM)) &
    51                             (out (fst CL) = out (fst AM)) &
    52                             livetraces CL <= livetraces AM"
    53 
    54 is_live_ref_map_def:
    55    "is_live_ref_map f CL AM ==
    56             is_ref_map f (fst CL ) (fst AM) &
    57             (! exec : executions (fst CL). (exec |== (snd CL)) -->
    58                                            ((corresp_ex (fst AM) f exec) |== (snd AM)))"
    59 
    60 
    61 declare split_paired_Ex [simp del]
    62 
    63 lemma live_implements_trans: 
    64 "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]  
    65       ==> live_implements (A,LA) (C,LC)"
    66 apply (unfold live_implements_def)
    67 apply auto
    68 done
    69 
    70 
    71 subsection "Correctness of live refmap"
    72 	
    73 lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);  
    74                    is_live_ref_map f (C,M) (A,L) |]  
    75                 ==> live_implements (C,M) (A,L)"
    76 apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
    77 apply (tactic "safe_tac set_cs")
    78 apply (rule_tac x = "corresp_ex A f ex" in exI)
    79 apply (tactic "safe_tac set_cs")
    80   (* Traces coincide, Lemma 1 *)
    81   apply (tactic {* pair_tac "ex" 1 *})
    82   apply (erule lemma_1 [THEN spec, THEN mp])
    83   apply (simp (no_asm) add: externals_def)
    84   apply (auto)[1]
    85   apply (simp add: executions_def reachable.reachable_0)
    86  
    87   (* corresp_ex is execution, Lemma 2 *)
    88   apply (tactic {* pair_tac "ex" 1 *})
    89   apply (simp add: executions_def)
    90   (* start state *) 
    91   apply (rule conjI)
    92   apply (simp add: is_ref_map_def corresp_ex_def)
    93   (* is-execution-fragment *)
    94   apply (erule lemma_2 [THEN spec, THEN mp])
    95   apply (simp add: reachable.reachable_0)
    96 
    97  (* Liveness *)
    98 apply auto
    99 done
   100 
   101 end