src/HOLCF/IOA/meta_theory/LiveIOA.thy
author huffman
Thu Feb 18 13:29:59 2010 -0800 (2010-02-18)
changeset 35215 a03462cbf86f
parent 35174 e15040ae75d7
child 36452 d37c6eed8117
permissions -rw-r--r--
get rid of warnings about duplicate simp rules in all HOLCF theories
     1 (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 header {* Live I/O automata -- specified by temproal formulas *}
     6 
     7 theory LiveIOA
     8 imports TLS
     9 begin
    10 
    11 defaultsort type
    12 
    13 types
    14   ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
    15 
    16 definition
    17   validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
    18   "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)"
    19 
    20 definition
    21   WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    22   "WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
    23 definition
    24   SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    25   "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
    26 
    27 definition
    28   liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
    29   "liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    30 definition
    31   livetraces :: "('a,'s)live_ioa => 'a trace set" where
    32   "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    33 definition
    34   live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
    35   "live_implements CL AM = ((inp (fst CL) = inp (fst AM)) &
    36                             (out (fst CL) = out (fst AM)) &
    37                             livetraces CL <= livetraces AM)"
    38 definition
    39   is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
    40   "is_live_ref_map f CL AM =
    41            (is_ref_map f (fst CL ) (fst AM) &
    42             (! exec : executions (fst CL). (exec |== (snd CL)) -->
    43                                            ((corresp_ex (fst AM) f exec) |== (snd AM))))"
    44 
    45 
    46 lemma live_implements_trans:
    47 "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
    48       ==> live_implements (A,LA) (C,LC)"
    49 apply (unfold live_implements_def)
    50 apply auto
    51 done
    52 
    53 
    54 subsection "Correctness of live refmap"
    55 
    56 lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);
    57                    is_live_ref_map f (C,M) (A,L) |]
    58                 ==> live_implements (C,M) (A,L)"
    59 apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
    60 apply auto
    61 apply (rule_tac x = "corresp_ex A f ex" in exI)
    62 apply auto
    63   (* Traces coincide, Lemma 1 *)
    64   apply (tactic {* pair_tac @{context} "ex" 1 *})
    65   apply (erule lemma_1 [THEN spec, THEN mp])
    66   apply (simp (no_asm) add: externals_def)
    67   apply (auto)[1]
    68   apply (simp add: executions_def reachable.reachable_0)
    69 
    70   (* corresp_ex is execution, Lemma 2 *)
    71   apply (tactic {* pair_tac @{context} "ex" 1 *})
    72   apply (simp add: executions_def)
    73   (* start state *)
    74   apply (rule conjI)
    75   apply (simp add: is_ref_map_def corresp_ex_def)
    76   (* is-execution-fragment *)
    77   apply (erule lemma_2 [THEN spec, THEN mp])
    78   apply (simp add: reachable.reachable_0)
    79 
    80 done
    81 
    82 end