src/HOLCF/IOA/meta_theory/LiveIOA.thy
author wenzelm
Sun Oct 21 16:27:42 2007 +0200 (2007-10-21)
changeset 25135 4f8176c940cf
parent 19741 f65265d71426
child 26359 6d437bde2f1d
permissions -rw-r--r--
modernized specifications ('definition', 'axiomatization');
     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 definition
    18   validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
    19   "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)"
    20 
    21 definition
    22   WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    23   "WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
    24 definition
    25   SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    26   "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
    27 
    28 definition
    29   liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
    30   "liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    31 definition
    32   livetraces :: "('a,'s)live_ioa => 'a trace set" where
    33   "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    34 definition
    35   live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
    36   "live_implements CL AM = ((inp (fst CL) = inp (fst AM)) &
    37                             (out (fst CL) = out (fst AM)) &
    38                             livetraces CL <= livetraces AM)"
    39 definition
    40   is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
    41   "is_live_ref_map f CL AM =
    42            (is_ref_map f (fst CL ) (fst AM) &
    43             (! exec : executions (fst CL). (exec |== (snd CL)) -->
    44                                            ((corresp_ex (fst AM) f exec) |== (snd AM))))"
    45 
    46 
    47 declare split_paired_Ex [simp del]
    48 
    49 lemma live_implements_trans:
    50 "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
    51       ==> live_implements (A,LA) (C,LC)"
    52 apply (unfold live_implements_def)
    53 apply auto
    54 done
    55 
    56 
    57 subsection "Correctness of live refmap"
    58 
    59 lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);
    60                    is_live_ref_map f (C,M) (A,L) |]
    61                 ==> live_implements (C,M) (A,L)"
    62 apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
    63 apply (tactic "safe_tac set_cs")
    64 apply (rule_tac x = "corresp_ex A f ex" in exI)
    65 apply (tactic "safe_tac set_cs")
    66   (* Traces coincide, Lemma 1 *)
    67   apply (tactic {* pair_tac "ex" 1 *})
    68   apply (erule lemma_1 [THEN spec, THEN mp])
    69   apply (simp (no_asm) add: externals_def)
    70   apply (auto)[1]
    71   apply (simp add: executions_def reachable.reachable_0)
    72 
    73   (* corresp_ex is execution, Lemma 2 *)
    74   apply (tactic {* pair_tac "ex" 1 *})
    75   apply (simp add: executions_def)
    76   (* start state *)
    77   apply (rule conjI)
    78   apply (simp add: is_ref_map_def corresp_ex_def)
    79   (* is-execution-fragment *)
    80   apply (erule lemma_2 [THEN spec, THEN mp])
    81   apply (simp add: reachable.reachable_0)
    82 
    83  (* Liveness *)
    84 apply auto
    85 done
    86 
    87 end