src/ZF/UNITY/Mutex.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
     1
(*  Title:      ZF/UNITY/Mutex.thy
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Computer Laboratory
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     3
    Copyright   2001  University of Cambridge
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
     5
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra.
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
     6
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
     7
Variables' types are introduced globally so that type verification
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
     8
reduces to the usual ZF typechecking \<in> an ill-tyed expression will
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
     9
reduce to the empty set.
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    10
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    11
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    12
header{*Mutual Exclusion*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    13
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    14
theory Mutex
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    15
imports SubstAx
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    16
begin
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    17
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    18
text{*Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    19
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    20
Variables' types are introduced globally so that type verification reduces to
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    21
the usual ZF typechecking: an ill-tyed expressions reduce to the empty set.
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    22
*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    23
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    24
abbreviation "p == Var([0])"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    25
abbreviation "m == Var([1])"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    26
abbreviation "n == Var([0,0])"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    27
abbreviation "u == Var([0,1])"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    28
abbreviation "v == Var([1,0])"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    29
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    30
axiomatization where --{** Type declarations  **}
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    31
  p_type:  "type_of(p)=bool & default_val(p)=0" and
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    32
  m_type:  "type_of(m)=int  & default_val(m)=#0" and
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    33
  n_type:  "type_of(n)=int  & default_val(n)=#0" and
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    34
  u_type:  "type_of(u)=bool & default_val(u)=0" and
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    35
  v_type:  "type_of(v)=bool & default_val(v)=0"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    36
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    37
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    38
  (** The program for process U **)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    39
  "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    40
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    41
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    42
  "U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) &  s`m = #1}"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    43
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    44
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    45
  "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    46
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    47
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    48
  "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    49
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    50
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    51
  "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    52
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    53
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    54
   (** The program for process V **)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    55
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    56
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    57
  "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    58
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    59
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    60
  "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    61
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    62
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    63
  "V2 == {<s,t>:state*state. t  = s(n:=#3) & s`p=1 & s`n = #2}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    64
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    65
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    66
  "V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    67
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    68
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    69
  "V4 == {<s,t>:state*state. t  = s (p:=0, n:=#0) & s`n = #4}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    70
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    71
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    72
  "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    73
              {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    74
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    75
  (** The correct invariants **)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    76
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    77
definition
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    78
  "IU == {s:state. (s`u = 1\<longleftrightarrow>(#1 $<= s`m & s`m $<= #3))
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    79
                     & (s`m = #3 \<longrightarrow> s`p=0)}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    80
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    81
definition
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    82
  "IV == {s:state. (s`v = 1 \<longleftrightarrow> (#1 $<= s`n & s`n $<= #3))
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    83
                      & (s`n = #3 \<longrightarrow> s`p=1)}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    84
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    85
  (** The faulty invariant (for U alone) **)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    86
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    87
definition
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    88
  "bad_IU == {s:state. (s`u = 1 \<longleftrightarrow> (#1 $<= s`m & s`m  $<= #3))&
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    89
                   (#3 $<= s`m & s`m $<= #4 \<longrightarrow> s`p=0)}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    90
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    91
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    92
(** Variables' types **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    93
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    94
declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    95
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    96
lemma u_value_type: "s \<in> state ==>s`u \<in> bool"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    97
apply (unfold state_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    98
apply (drule_tac a = u in apply_type, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    99
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   100
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   101
lemma v_value_type: "s \<in> state ==> s`v \<in> bool"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   102
apply (unfold state_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   103
apply (drule_tac a = v in apply_type, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   104
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   105
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   106
lemma p_value_type: "s \<in> state ==> s`p \<in> bool"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   107
apply (unfold state_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   108
apply (drule_tac a = p in apply_type, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   109
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   110
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   111
lemma m_value_type: "s \<in> state ==> s`m \<in> int"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   112
apply (unfold state_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   113
apply (drule_tac a = m in apply_type, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   114
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   115
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   116
lemma n_value_type: "s \<in> state ==>s`n \<in> int"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   117
apply (unfold state_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   118
apply (drule_tac a = n in apply_type, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   119
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   120
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   121
declare p_value_type [simp] u_value_type [simp] v_value_type [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   122
        m_value_type [simp] n_value_type [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   123
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   124
declare p_value_type [TC] u_value_type [TC] v_value_type [TC]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   125
        m_value_type [TC] n_value_type [TC]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   126
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   127
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   128
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   129
text{*Mutex is a program*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   130
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   131
lemma Mutex_in_program [simp,TC]: "Mutex \<in> program"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   132
by (simp add: Mutex_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   133
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   134
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   135
declare Mutex_def [THEN def_prg_Init, simp]
24051
896fb015079c replaced program_defs_ref by proper context data (via attribute "program");
wenzelm
parents: 16183
diff changeset
   136
declare Mutex_def [program]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   137
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   138
declare  U0_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   139
declare  U1_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   140
declare  U2_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   141
declare  U3_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   142
declare  U4_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   143
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   144
declare  V0_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   145
declare  V1_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   146
declare  V2_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   147
declare  V3_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   148
declare  V4_def [THEN def_act_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   149
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   150
declare  U0_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   151
declare  U1_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   152
declare  U2_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   153
declare  U3_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   154
declare  U4_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   155
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   156
declare  V0_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   157
declare  V1_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   158
declare  V2_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   159
declare  V3_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   160
declare  V4_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   161
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   162
declare  IU_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   163
declare  IV_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   164
declare  bad_IU_def [THEN def_set_simp, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   165
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   166
lemma IU: "Mutex \<in> Always(IU)"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   167
apply (rule AlwaysI, force)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   168
apply (unfold Mutex_def, safety, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   169
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   170
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   171
lemma IV: "Mutex \<in> Always(IV)"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   172
apply (rule AlwaysI, force)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   173
apply (unfold Mutex_def, safety)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   174
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   175
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   176
(*The safety property: mutual exclusion*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   177
lemma mutual_exclusion: "Mutex \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   178
apply (rule Always_weaken)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   179
apply (rule Always_Int_I [OF IU IV], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   180
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   181
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   182
(*The bad invariant FAILS in V1*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   183
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   184
lemma less_lemma: "[| x$<#1; #3 $<= x |] ==> P"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   185
apply (drule_tac j = "#1" and k = "#3" in zless_zle_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   186
apply (drule_tac [2] j = x in zle_zless_trans, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   187
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   188
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   189
lemma "Mutex \<in> Always(bad_IU)"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   190
apply (rule AlwaysI, force)
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15634
diff changeset
   191
apply (unfold Mutex_def, safety, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   192
apply (subgoal_tac "#1 $<= #3")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   193
apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   194
apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   195
apply auto
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   196
(*Resulting state: n=1, p=false, m=4, u=false.
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   197
  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   198
  violating the invariant!*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   199
oops
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   200
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   201
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   202
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   203
(*** Progress for U ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   204
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   205
lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}"
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   206
by (unfold op_Unless_def Mutex_def, safety)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   207
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   208
lemma U_F1:
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   209
     "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   210
by (unfold Mutex_def, ensures U1)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   211
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   212
lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   213
apply (cut_tac IU)
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   214
apply (unfold Mutex_def, ensures U2)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   215
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   216
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   217
lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   218
apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   219
 apply (unfold Mutex_def)
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   220
 apply (ensures U3)
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   221
apply (ensures U4)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   222
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   223
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   224
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   225
lemma U_lemma2: "Mutex \<in> {s \<in> state. s`m = #2} LeadsTo {s \<in> state. s`p=1}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   226
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   227
                             Int_lower2 [THEN subset_imp_LeadsTo]])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   228
apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   229
apply (auto dest!: p_value_type simp add: bool_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   230
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   231
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   232
lemma U_lemma1: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`p =1}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   233
by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   234
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   235
lemma eq_123: "i \<in> int ==> (#1 $<= i & i $<= #3) \<longleftrightarrow> (i=#1 | i=#2 | i=#3)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   236
apply auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   237
apply (auto simp add: neq_iff_zless)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   238
apply (drule_tac [4] j = "#3" and i = i in zle_zless_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   239
apply (drule_tac [2] j = i and i = "#1" in zle_zless_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   240
apply (drule_tac j = i and i = "#1" in zle_zless_trans, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   241
apply (rule zle_anti_sym)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   242
apply (simp_all (no_asm_simp) add: zless_add1_iff_zle [THEN iff_sym])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   243
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   244
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   245
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   246
lemma U_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \<in> state. s`p=1}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   247
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   248
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   249
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   250
(*Misra's F4*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   251
lemma u_Leadsto_p: "Mutex \<in> {s \<in> state. s`u = 1} LeadsTo {s \<in> state. s`p=1}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   252
by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   253
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   254
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   255
(*** Progress for V ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   256
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   257
lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}"
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   258
by (unfold op_Unless_def Mutex_def, safety)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   259
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   260
lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   261
by (unfold Mutex_def, ensures "V1")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   262
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   263
lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   264
apply (cut_tac IV)
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   265
apply (unfold Mutex_def, ensures "V2")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   266
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   267
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   268
lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   269
apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   270
 apply (unfold Mutex_def)
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   271
 apply (ensures V3)
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 41779
diff changeset
   272
apply (ensures V4)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   273
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   274
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   275
lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   276
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   277
                             Int_lower2 [THEN subset_imp_LeadsTo]])
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
   278
apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   279
apply (auto dest!: p_value_type simp add: bool_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   280
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   281
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   282
lemma V_lemma1: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`p = 0}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   283
by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   284
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   285
lemma V_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \<in> state. s`p = 0}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   286
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   287
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   288
(*Misra's F4*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   289
lemma v_Leadsto_not_p: "Mutex \<in> {s \<in> state. s`v = 1} LeadsTo {s \<in> state. s`p = 0}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   290
by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   291
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   292
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   293
(** Absence of starvation **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   294
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   295
(*Misra's F6*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   296
lemma m1_Leadsto_3: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`m = #3}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   297
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   298
apply (rule_tac [2] U_F2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   299
apply (simp add: Collect_conj_eq)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   300
apply (subst Un_commute)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   301
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   302
 apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   303
apply (rule U_F1 [THEN LeadsTo_weaken_R], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   304
apply (auto dest!: v_value_type simp add: bool_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   305
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   306
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   307
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   308
(*The same for V*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   309
lemma n1_Leadsto_3: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`n = #3}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   310
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   311
apply (rule_tac [2] V_F2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   312
apply (simp add: Collect_conj_eq)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   313
apply (subst Un_commute)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   314
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   315
 apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   316
apply (rule V_F1 [THEN LeadsTo_weaken_R], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   317
apply (auto dest!: u_value_type simp add: bool_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   318
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   319
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   320
end