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