src/HOL/UNITY/Union.thy
author wenzelm
Tue, 02 Mar 2010 23:59:54 +0100
changeset 35427 ad039d29e01c
parent 35068 544867142ea4
child 35434 a4babce15c67
permissions -rw-r--r--
proper (type_)notation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Union.thy
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     3
    Copyright   1998  University of Cambridge
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30304
diff changeset
     5
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs.
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     6
*)
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     7
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
     8
header{*Unions of Programs*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
     9
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14150
diff changeset
    10
theory Union imports SubstAx FP begin
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    11
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    12
constdefs
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9685
diff changeset
    13
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    14
  (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    15
  ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    16
    "F ok G == Acts F \<subseteq> AllowedActs G &
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    17
               Acts G \<subseteq> AllowedActs F"
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9685
diff changeset
    18
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    19
  (*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    20
  OK  :: "['a set, 'a => 'b program] => bool"
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    21
    "OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9685
diff changeset
    22
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    23
  JOIN  :: "['a set, 'a => 'b program] => 'b program"
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    24
    "JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30304
diff changeset
    25
                             \<Inter>i \<in> I. AllowedActs (F i))"
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    26
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    27
  Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    28
    "F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30304
diff changeset
    29
                             AllowedActs F \<inter> AllowedActs G)"
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    30
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    31
  SKIP :: "'a program"
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9685
diff changeset
    32
    "SKIP == mk_program (UNIV, {}, UNIV)"
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9685
diff changeset
    33
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    34
  (*Characterizes safety properties.  Used with specifying Allowed*)
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9685
diff changeset
    35
  safety_prop :: "'a program set => bool"
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    36
    "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
5259
86d80749453f Null program and a few new results
paulson
parents: 5252
diff changeset
    37
35427
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35068
diff changeset
    38
notation
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35068
diff changeset
    39
  SKIP  ("\<bottom>") and
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35068
diff changeset
    40
  Join  (infixl "\<squnion>" 65)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35068
diff changeset
    41
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    42
syntax
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32960
diff changeset
    43
  "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32960
diff changeset
    44
  "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
35427
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35068
diff changeset
    45
syntax (xsymbols)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35068
diff changeset
    46
  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35068
diff changeset
    47
  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    48
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    49
translations
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32960
diff changeset
    50
  "JN x: A. B" == "CONST JOIN A (%x. B)"
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32960
diff changeset
    51
  "JN x y. B" == "JN x. JN y. B"
35068
544867142ea4 modernized translations;
wenzelm
parents: 35054
diff changeset
    52
  "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    53
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    54
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
    55
subsection{*SKIP*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    56
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    57
lemma Init_SKIP [simp]: "Init SKIP = UNIV"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    58
by (simp add: SKIP_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    59
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    60
lemma Acts_SKIP [simp]: "Acts SKIP = {Id}"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    61
by (simp add: SKIP_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    62
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    63
lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    64
by (auto simp add: SKIP_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    65
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    66
lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    67
by (force elim: reachable.induct intro: reachable.intros)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    68
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
    69
subsection{*SKIP and safety properties*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    70
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    71
lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    72
by (unfold constrains_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    73
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    74
lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B) = (A \<subseteq> B)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    75
by (unfold Constrains_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    76
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    77
lemma SKIP_in_stable [iff]: "SKIP \<in> stable A"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    78
by (unfold stable_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    79
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    80
declare SKIP_in_stable [THEN stable_imp_Stable, iff]
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    81
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    82
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
    83
subsection{*Join*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    84
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    85
lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    86
by (simp add: Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    87
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    88
lemma Acts_Join [simp]: "Acts (F\<squnion>G) = Acts F \<union> Acts G"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    89
by (auto simp add: Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    90
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    91
lemma AllowedActs_Join [simp]:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    92
     "AllowedActs (F\<squnion>G) = AllowedActs F \<inter> AllowedActs G"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    93
by (auto simp add: Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    94
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    95
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
    96
subsection{*JN*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    97
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    98
lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
    99
by (unfold JOIN_def SKIP_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   100
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   101
lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a)\<squnion>(\<Squnion>i \<in> I. F i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   102
apply (rule program_equalityI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   103
apply (auto simp add: JOIN_def Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   104
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   105
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   106
lemma Init_JN [simp]: "Init (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. Init (F i))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   107
by (simp add: JOIN_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   108
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   109
lemma Acts_JN [simp]: "Acts (\<Squnion>i \<in> I. F i) = insert Id (\<Union>i \<in> I. Acts (F i))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   110
by (auto simp add: JOIN_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   111
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   112
lemma AllowedActs_JN [simp]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   113
     "AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   114
by (auto simp add: JOIN_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   115
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   116
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   117
lemma JN_cong [cong]: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   118
    "[| I=J;  !!i. i \<in> J ==> F i = G i |] ==> (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> J. G i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   119
by (simp add: JOIN_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   120
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   121
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
   122
subsection{*Algebraic laws*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   123
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   124
lemma Join_commute: "F\<squnion>G = G\<squnion>F"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   125
by (simp add: Join_def Un_commute Int_commute)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   126
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   127
lemma Join_assoc: "(F\<squnion>G)\<squnion>H = F\<squnion>(G\<squnion>H)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   128
by (simp add: Un_ac Join_def Int_assoc insert_absorb)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   129
 
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   130
lemma Join_left_commute: "A\<squnion>(B\<squnion>C) = B\<squnion>(A\<squnion>C)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   131
by (simp add: Un_ac Int_ac Join_def insert_absorb)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   132
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   133
lemma Join_SKIP_left [simp]: "SKIP\<squnion>F = F"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   134
apply (unfold Join_def SKIP_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   135
apply (rule program_equalityI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   136
apply (simp_all (no_asm) add: insert_absorb)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   137
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   138
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   139
lemma Join_SKIP_right [simp]: "F\<squnion>SKIP = F"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   140
apply (unfold Join_def SKIP_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   141
apply (rule program_equalityI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   142
apply (simp_all (no_asm) add: insert_absorb)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   143
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   144
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   145
lemma Join_absorb [simp]: "F\<squnion>F = F"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   146
apply (unfold Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   147
apply (rule program_equalityI, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   148
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   149
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   150
lemma Join_left_absorb: "F\<squnion>(F\<squnion>G) = F\<squnion>G"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   151
apply (unfold Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   152
apply (rule program_equalityI, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   153
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   154
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   155
(*Join is an AC-operator*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   156
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   157
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   158
14150
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13819
diff changeset
   159
subsection{*Laws Governing @{text "\<Squnion>"}*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   160
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   161
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   162
lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   163
by (auto intro!: program_equalityI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   164
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   165
lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i)\<squnion>(\<Squnion>i \<in> J. F i))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   166
by (auto intro!: program_equalityI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   167
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   168
lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   169
by (rule program_equalityI, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   170
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   171
lemma JN_Join_distrib:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   172
     "(\<Squnion>i \<in> I. F i\<squnion>G i) = (\<Squnion>i \<in> I. F i) \<squnion> (\<Squnion>i \<in> I. G i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   173
by (auto intro!: program_equalityI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   174
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   175
lemma JN_Join_miniscope:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   176
     "i \<in> I ==> (\<Squnion>i \<in> I. F i\<squnion>G) = ((\<Squnion>i \<in> I. F i)\<squnion>G)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   177
by (auto simp add: JN_Join_distrib JN_constant)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   178
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   179
(*Used to prove guarantees_JN_I*)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   180
lemma JN_Join_diff: "i \<in> I ==> F i\<squnion>JOIN (I - {i}) F = JOIN I F"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   181
apply (unfold JOIN_def Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   182
apply (rule program_equalityI, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   183
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   184
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   185
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
   186
subsection{*Safety: co, stable, FP*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   187
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   188
(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B.  So an
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   189
  alternative precondition is A \<subseteq> B, but most proofs using this rule require
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   190
  I to be nonempty for other reasons anyway.*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   191
lemma JN_constrains: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   192
    "i \<in> I ==> (\<Squnion>i \<in> I. F i) \<in> A co B = (\<forall>i \<in> I. F i \<in> A co B)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   193
by (simp add: constrains_def JOIN_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   194
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   195
lemma Join_constrains [simp]:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   196
     "(F\<squnion>G \<in> A co B) = (F \<in> A co B & G \<in> A co B)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   197
by (auto simp add: constrains_def Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   198
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   199
lemma Join_unless [simp]:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   200
     "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   201
by (simp add: Join_constrains unless_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   202
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   203
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   204
  reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   205
*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   206
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   207
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   208
lemma Join_constrains_weaken:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   209
     "[| F \<in> A co A';  G \<in> B co B' |]  
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   210
      ==> F\<squnion>G \<in> (A \<inter> B) co (A' \<union> B')"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   211
by (simp, blast intro: constrains_weaken)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   212
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   213
(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   214
lemma JN_constrains_weaken:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   215
     "[| \<forall>i \<in> I. F i \<in> A i co A' i;  i \<in> I |]  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   216
      ==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   217
apply (simp (no_asm_simp) add: JN_constrains)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   218
apply (blast intro: constrains_weaken)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   219
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   220
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   221
lemma JN_stable: "(\<Squnion>i \<in> I. F i) \<in> stable A = (\<forall>i \<in> I. F i \<in> stable A)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   222
by (simp add: stable_def constrains_def JOIN_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   223
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   224
lemma invariant_JN_I:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   225
     "[| !!i. i \<in> I ==> F i \<in> invariant A;  i \<in> I |]   
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   226
       ==> (\<Squnion>i \<in> I. F i) \<in> invariant A"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   227
by (simp add: invariant_def JN_stable, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   228
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   229
lemma Join_stable [simp]:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   230
     "(F\<squnion>G \<in> stable A) =  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   231
      (F \<in> stable A & G \<in> stable A)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   232
by (simp add: stable_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   233
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   234
lemma Join_increasing [simp]:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   235
     "(F\<squnion>G \<in> increasing f) =  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   236
      (F \<in> increasing f & G \<in> increasing f)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   237
by (simp add: increasing_def Join_stable, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   238
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   239
lemma invariant_JoinI:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   240
     "[| F \<in> invariant A; G \<in> invariant A |]   
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   241
      ==> F\<squnion>G \<in> invariant A"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   242
by (simp add: invariant_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   243
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   244
lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   245
by (simp add: FP_def JN_stable INTER_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   246
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   247
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
   248
subsection{*Progress: transient, ensures*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   249
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   250
lemma JN_transient:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   251
     "i \<in> I ==>  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   252
    (\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   253
by (auto simp add: transient_def JOIN_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   254
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   255
lemma Join_transient [simp]:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   256
     "F\<squnion>G \<in> transient A =  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   257
      (F \<in> transient A | G \<in> transient A)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   258
by (auto simp add: bex_Un transient_def Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   259
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   260
lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   261
by (simp add: Join_transient)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   262
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   263
lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   264
by (simp add: Join_transient)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   265
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   266
(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   267
lemma JN_ensures:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   268
     "i \<in> I ==>  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   269
      (\<Squnion>i \<in> I. F i) \<in> A ensures B =  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   270
      ((\<forall>i \<in> I. F i \<in> (A-B) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   271
by (auto simp add: ensures_def JN_constrains JN_transient)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   272
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   273
lemma Join_ensures: 
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   274
     "F\<squnion>G \<in> A ensures B =      
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   275
      (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   276
       (F \<in> transient (A-B) | G \<in> transient (A-B)))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   277
by (auto simp add: ensures_def Join_transient)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   278
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   279
lemma stable_Join_constrains: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   280
    "[| F \<in> stable A;  G \<in> A co A' |]  
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   281
     ==> F\<squnion>G \<in> A co A'"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   282
apply (unfold stable_def constrains_def Join_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   283
apply (simp add: ball_Un, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   284
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   285
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   286
(*Premise for G cannot use Always because  F \<in> Stable A  is weaker than
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   287
  G \<in> stable A *)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   288
lemma stable_Join_Always1:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   289
     "[| F \<in> stable A;  G \<in> invariant A |] ==> F\<squnion>G \<in> Always A"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   290
apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   291
apply (force intro: stable_Int)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   292
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   293
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   294
(*As above, but exchanging the roles of F and G*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   295
lemma stable_Join_Always2:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   296
     "[| F \<in> invariant A;  G \<in> stable A |] ==> F\<squnion>G \<in> Always A"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   297
apply (subst Join_commute)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   298
apply (blast intro: stable_Join_Always1)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   299
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   300
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   301
lemma stable_Join_ensures1:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   302
     "[| F \<in> stable A;  G \<in> A ensures B |] ==> F\<squnion>G \<in> A ensures B"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   303
apply (simp (no_asm_simp) add: Join_ensures)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   304
apply (simp add: stable_def ensures_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   305
apply (erule constrains_weaken, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   306
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   307
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   308
(*As above, but exchanging the roles of F and G*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   309
lemma stable_Join_ensures2:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   310
     "[| F \<in> A ensures B;  G \<in> stable A |] ==> F\<squnion>G \<in> A ensures B"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   311
apply (subst Join_commute)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   312
apply (blast intro: stable_Join_ensures1)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   313
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   314
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   315
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
   316
subsection{*the ok and OK relations*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   317
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   318
lemma ok_SKIP1 [iff]: "SKIP ok F"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   319
by (simp add: ok_def)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   320
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   321
lemma ok_SKIP2 [iff]: "F ok SKIP"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   322
by (simp add: ok_def)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   323
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   324
lemma ok_Join_commute:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   325
     "(F ok G & (F\<squnion>G) ok H) = (G ok H & F ok (G\<squnion>H))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   326
by (auto simp add: ok_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   327
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   328
lemma ok_commute: "(F ok G) = (G ok F)"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   329
by (auto simp add: ok_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   330
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   331
lemmas ok_sym = ok_commute [THEN iffD1, standard]
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   332
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   333
lemma ok_iff_OK:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   334
     "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
16977
7c04742abac3 no eq_commute;
wenzelm
parents: 16417
diff changeset
   335
apply (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
7c04742abac3 no eq_commute;
wenzelm
parents: 16417
diff changeset
   336
              all_conj_distrib)
7c04742abac3 no eq_commute;
wenzelm
parents: 16417
diff changeset
   337
apply blast
7c04742abac3 no eq_commute;
wenzelm
parents: 16417
diff changeset
   338
done
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   339
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   340
lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   341
by (auto simp add: ok_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   342
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   343
lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   344
by (auto simp add: ok_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   345
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   346
(*useful?  Not with the previous two around*)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   347
lemma ok_Join_commute_I: "[| F ok G; (F\<squnion>G) ok H |] ==> F ok (G\<squnion>H)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   348
by (auto simp add: ok_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   349
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   350
lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   351
by (auto simp add: ok_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   352
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   353
lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (\<forall>i \<in> I. G i ok F)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   354
by (auto simp add: ok_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   355
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   356
lemma OK_iff_ok: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. (F i) ok (F j))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   357
by (auto simp add: ok_def OK_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   358
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   359
lemma OK_imp_ok: "[| OK I F; i \<in> I; j \<in> I; i \<noteq> j|] ==> (F i) ok (F j)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   360
by (auto simp add: OK_iff_ok)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   361
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   362
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
   363
subsection{*Allowed*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   364
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   365
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   366
by (auto simp add: Allowed_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   367
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   368
lemma Allowed_Join [simp]: "Allowed (F\<squnion>G) = Allowed F \<inter> Allowed G"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   369
by (auto simp add: Allowed_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   370
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   371
lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   372
by (auto simp add: Allowed_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   373
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   374
lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   375
by (simp add: ok_def Allowed_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   376
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   377
lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   378
by (auto simp add: OK_iff_ok ok_iff_Allowed)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   379
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   380
subsection{*@{term safety_prop}, for reasoning about
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
   381
 given instances of "ok"*}
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   382
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   383
lemma safety_prop_Acts_iff:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   384
     "safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   385
by (auto simp add: safety_prop_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   386
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   387
lemma safety_prop_AllowedActs_iff_Allowed:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   388
     "safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   389
by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   390
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   391
lemma Allowed_eq:
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   392
     "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   393
by (simp add: Allowed_def safety_prop_Acts_iff)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   394
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   395
(*For safety_prop to hold, the property must be satisfiable!*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   396
lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   397
by (simp add: safety_prop_def constrains_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   398
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   399
lemma safety_prop_stable [iff]: "safety_prop (stable A)"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   400
by (simp add: stable_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   401
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   402
lemma safety_prop_Int [simp]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   403
     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   404
by (simp add: safety_prop_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   405
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   406
lemma safety_prop_INTER1 [simp]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   407
     "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   408
by (auto simp add: safety_prop_def, blast)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30304
diff changeset
   409
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   410
lemma safety_prop_INTER [simp]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   411
     "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   412
by (auto simp add: safety_prop_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   413
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   414
lemma def_prg_Allowed:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   415
     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   416
      ==> Allowed F = X"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   417
by (simp add: Allowed_eq)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   418
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   419
lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   420
by (simp add: Allowed_def) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   421
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   422
lemma def_total_prg_Allowed:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   423
     "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   424
      ==> Allowed F = X"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   425
by (simp add: mk_total_program_def def_prg_Allowed) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   426
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   427
lemma def_UNION_ok_iff:
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   428
     "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   429
      ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12114
diff changeset
   430
by (auto simp add: ok_def safety_prop_Acts_iff)
9685
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8055
diff changeset
   431
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   432
text{*The union of two total programs is total.*}
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   433
lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   434
by (simp add: program_equalityI totalize_def Join_def image_Un)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   435
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   436
lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F\<squnion>G)"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   437
by (simp add: all_total_def, blast)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   438
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   439
lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   440
by (simp add: program_equalityI totalize_def JOIN_def image_UN)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   441
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   442
lemma all_total_JN: "(!!i. i\<in>I ==> all_total (F i)) ==> all_total(\<Squnion>i\<in>I. F i)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   443
by (simp add: all_total_iff_totalize totalize_JN [symmetric])
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   444
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
   445
end