src/HOLCF/IOA/meta_theory/LiveIOA.thy
changeset 25135 4f8176c940cf
parent 19741 f65265d71426
child 26359 6d437bde2f1d
     1.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sun Oct 21 14:53:44 2007 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sun Oct 21 16:27:42 2007 +0200
     1.3 @@ -14,54 +14,40 @@
     1.4  types
     1.5    ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
     1.6  
     1.7 -consts
     1.8 -
     1.9 -validLIOA   :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool"
    1.10 -
    1.11 -WF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
    1.12 -SF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
    1.13 +definition
    1.14 +  validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
    1.15 +  "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)"
    1.16  
    1.17 -liveexecutions    :: "('a,'s)live_ioa => ('a,'s)execution set"
    1.18 -livetraces        :: "('a,'s)live_ioa => 'a trace set"
    1.19 -live_implements   :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    1.20 -is_live_ref_map   :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
    1.21 -
    1.22 -
    1.23 -defs
    1.24 -
    1.25 -validLIOA_def:
    1.26 -  "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
    1.27 -
    1.28 +definition
    1.29 +  WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    1.30 +  "WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
    1.31 +definition
    1.32 +  SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    1.33 +  "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
    1.34  
    1.35 -WF_def:
    1.36 -  "WF A acts ==  <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    1.37 -
    1.38 -SF_def:
    1.39 -  "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
    1.40 -
    1.41 -
    1.42 -liveexecutions_def:
    1.43 -   "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    1.44 -
    1.45 -livetraces_def:
    1.46 -  "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    1.47 -
    1.48 -live_implements_def:
    1.49 -  "live_implements CL AM == (inp (fst CL) = inp (fst AM)) &
    1.50 +definition
    1.51 +  liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
    1.52 +  "liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    1.53 +definition
    1.54 +  livetraces :: "('a,'s)live_ioa => 'a trace set" where
    1.55 +  "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    1.56 +definition
    1.57 +  live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
    1.58 +  "live_implements CL AM = ((inp (fst CL) = inp (fst AM)) &
    1.59                              (out (fst CL) = out (fst AM)) &
    1.60 -                            livetraces CL <= livetraces AM"
    1.61 -
    1.62 -is_live_ref_map_def:
    1.63 -   "is_live_ref_map f CL AM ==
    1.64 -            is_ref_map f (fst CL ) (fst AM) &
    1.65 +                            livetraces CL <= livetraces AM)"
    1.66 +definition
    1.67 +  is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
    1.68 +  "is_live_ref_map f CL AM =
    1.69 +           (is_ref_map f (fst CL ) (fst AM) &
    1.70              (! exec : executions (fst CL). (exec |== (snd CL)) -->
    1.71 -                                           ((corresp_ex (fst AM) f exec) |== (snd AM)))"
    1.72 +                                           ((corresp_ex (fst AM) f exec) |== (snd AM))))"
    1.73  
    1.74  
    1.75  declare split_paired_Ex [simp del]
    1.76  
    1.77 -lemma live_implements_trans: 
    1.78 -"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]  
    1.79 +lemma live_implements_trans:
    1.80 +"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
    1.81        ==> live_implements (A,LA) (C,LC)"
    1.82  apply (unfold live_implements_def)
    1.83  apply auto
    1.84 @@ -69,9 +55,9 @@
    1.85  
    1.86  
    1.87  subsection "Correctness of live refmap"
    1.88 -	
    1.89 -lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);  
    1.90 -                   is_live_ref_map f (C,M) (A,L) |]  
    1.91 +
    1.92 +lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);
    1.93 +                   is_live_ref_map f (C,M) (A,L) |]
    1.94                  ==> live_implements (C,M) (A,L)"
    1.95  apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
    1.96  apply (tactic "safe_tac set_cs")
    1.97 @@ -83,11 +69,11 @@
    1.98    apply (simp (no_asm) add: externals_def)
    1.99    apply (auto)[1]
   1.100    apply (simp add: executions_def reachable.reachable_0)
   1.101 - 
   1.102 +
   1.103    (* corresp_ex is execution, Lemma 2 *)
   1.104    apply (tactic {* pair_tac "ex" 1 *})
   1.105    apply (simp add: executions_def)
   1.106 -  (* start state *) 
   1.107 +  (* start state *)
   1.108    apply (rule conjI)
   1.109    apply (simp add: is_ref_map_def corresp_ex_def)
   1.110    (* is-execution-fragment *)