src/HOLCF/IOA/meta_theory/Simulations.thy
author wenzelm
Thu, 22 Nov 2007 14:51:34 +0100
changeset 25456 6f79698f294d
parent 25135 4f8176c940cf
child 35174 e15040ae75d7
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
     2
    ID:         $Id$
12218
wenzelm
parents: 10835
diff changeset
     3
    Author:     Olaf Müller
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
     4
*)
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
     5
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     6
header {* Simulations in HOLCF/IOA *}
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
     7
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     8
theory Simulations
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     9
imports RefCorrectness
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    10
begin
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    11
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    12
defaultsort type
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    13
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    14
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    15
  is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    16
  "is_simulation R C A =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    17
   ((!s:starts_of C. R``{s} Int starts_of A ~= {}) &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    18
   (!s s' t a. reachable C s &
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    19
               s -a--C-> t   &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    20
               (s,s') : R
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    21
               --> (? t' ex. (t,t'):R & move A ex s' a t')))"
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    22
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    23
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    24
  is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    25
  "is_backward_simulation R C A =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    26
   ((!s:starts_of C. R``{s} <= starts_of A) &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    27
   (!s t t' a. reachable C s &
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    28
               s -a--C-> t   &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    29
               (t,t') : R
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    30
               --> (? ex s'. (s,s'):R & move A ex s' a t')))"
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    31
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    32
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    33
  is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    34
  "is_forw_back_simulation R C A =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    35
   ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    36
   (!s S' t a. reachable C s &
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    37
               s -a--C-> t   &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    38
               (s,S') : R
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    39
               --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))"
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    40
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    41
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    42
  is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    43
  "is_back_forw_simulation R C A =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    44
   ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    45
   (!s t T' a. reachable C s &
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    46
               s -a--C-> t   &
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    47
               (t,T') : R
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    48
               --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))"
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    49
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    50
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    51
  is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    52
  "is_history_relation R C A = (is_simulation R C A &
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    53
                                is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    54
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    55
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    56
  is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    57
  "is_prophecy_relation R C A = (is_backward_simulation R C A &
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    58
                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    59
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    60
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    61
lemma set_non_empty: "(A~={}) = (? x. x:A)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    62
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    63
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    64
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    65
lemma Int_non_empty: "(A Int B ~= {}) = (? x. x: A & x:B)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    66
apply (simp add: set_non_empty)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    67
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    68
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    69
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    70
lemma Sim_start_convert:
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    71
"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    72
apply (unfold Image_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    73
apply (simp add: Int_non_empty)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    74
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    75
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    76
declare Sim_start_convert [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    77
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    78
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19741
diff changeset
    79
lemma ref_map_is_simulation:
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    80
"!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    81
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    82
apply (unfold is_ref_map_def is_simulation_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    83
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    84
done
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    85
4565
ea467ce15040 added forward simulation correectness;
mueller
parents:
diff changeset
    86
end