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