src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
author wenzelm
Wed, 30 Dec 2015 21:57:52 +0100
changeset 62002 f1599e98c4d0
parent 62000 8cba509ace9c
child 62004 8c6226d88ced
permissions -rw-r--r--
isabelle update_cartouches -c -t;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41476
diff changeset
     1
(*  Title:      HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
     2
    Author:     Olaf Müller
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     3
*)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     4
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 62000
diff changeset
     5
section \<open>Live I/O automata -- specified by temproal formulas\<close>
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     6
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     7
theory LiveIOA
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     8
imports TLS
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     9
begin
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    10
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35215
diff changeset
    11
default_sort type
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    12
41476
0fa9629aa399 types -> type_synonym
huffman
parents: 40945
diff changeset
    13
type_synonym
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    14
  ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    15
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    16
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    17
  validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    18
  "validLIOA AL P = validIOA (fst AL) ((snd AL) \<^bold>\<longrightarrow> P)"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    19
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    20
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    21
  WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    22
  "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    23
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    24
  SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    25
  "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    26
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    27
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    28
  liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    29
  "liveexecutions AP = {exec. exec : executions (fst AP) & (exec \<TTurnstile> (snd AP))}"
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    30
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    31
  livetraces :: "('a,'s)live_ioa => 'a trace set" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    32
  "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    33
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    34
  live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    35
  "live_implements CL AM = ((inp (fst CL) = inp (fst AM)) &
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    36
                            (out (fst CL) = out (fst AM)) &
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    37
                            livetraces CL <= livetraces AM)"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    38
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    39
  is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    40
  "is_live_ref_map f CL AM =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    41
           (is_ref_map f (fst CL ) (fst AM) &
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    42
            (! exec : executions (fst CL). (exec \<TTurnstile> (snd CL)) -->
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    43
                                           ((corresp_ex (fst AM) f exec) \<TTurnstile> (snd AM))))"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    44
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    45
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    46
lemma live_implements_trans:
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    47
"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    48
      ==> live_implements (A,LA) (C,LC)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    49
apply (unfold live_implements_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    50
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    51
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    52
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    53
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    54
subsection "Correctness of live refmap"
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    55
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    56
lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    57
                   is_live_ref_map f (C,M) (A,L) |]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    58
                ==> live_implements (C,M) (A,L)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    59
apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
26359
6d437bde2f1d more antiquotations
haftmann
parents: 25135
diff changeset
    60
apply auto
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    61
apply (rule_tac x = "corresp_ex A f ex" in exI)
26359
6d437bde2f1d more antiquotations
haftmann
parents: 25135
diff changeset
    62
apply auto
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    63
  (* Traces coincide, Lemma 1 *)
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 62000
diff changeset
    64
  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    65
  apply (erule lemma_1 [THEN spec, THEN mp])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    66
  apply (simp (no_asm) add: externals_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    67
  apply (auto)[1]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    68
  apply (simp add: executions_def reachable.reachable_0)
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    69
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    70
  (* corresp_ex is execution, Lemma 2 *)
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 62000
diff changeset
    71
  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    72
  apply (simp add: executions_def)
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    73
  (* start state *)
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    74
  apply (rule conjI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    75
  apply (simp add: is_ref_map_def corresp_ex_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    76
  (* is-execution-fragment *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    77
  apply (erule lemma_2 [THEN spec, THEN mp])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    78
  apply (simp add: reachable.reachable_0)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    79
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    80
done
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    81
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    82
end