src/HOL/UNITY/Constrains.thy
author wenzelm
Sun, 20 May 2018 22:04:46 +0200
changeset 68238 eb57621568bb
parent 67613 ce654b0e6d69
child 69313 b021008c5397
permissions -rw-r--r--
avoid undeclared frees;
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: 23767
diff changeset
     1
(*  Title:      HOL/UNITY/Constrains.thy
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     3
    Copyright   1998  University of Cambridge
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     4
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
     5
Weak safety relations: restricted to the set of reachable states.
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     6
*)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     7
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
     8
section\<open>Weak Safety\<close>
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
     9
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13812
diff changeset
    10
theory Constrains imports UNITY begin
6535
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    11
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    12
  (*Initial states and program => (final state, reversed trace to it)...
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    13
    Arguments MUST be curried in an inductive definition*)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    14
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    15
inductive_set
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    16
  traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    17
  for init :: "'a set" and acts :: "('a * 'a)set set"
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    18
  where
6535
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    19
         (*Initial trace is empty*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    20
    Init:  "s \<in> init ==> (s,[]) \<in> traces init acts"
6535
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    21
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    22
  | Acts:  "[| act \<in> acts;  (s,evs) \<in> traces init acts;  (s,s') \<in> act |]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23767
diff changeset
    23
            ==> (s', s#evs) \<in> traces init acts"
6535
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    24
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 5784
diff changeset
    25
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    26
inductive_set
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    27
  reachable :: "'a program => 'a set"
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    28
  for F :: "'a program"
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    29
  where
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    30
    Init:  "s \<in> Init F ==> s \<in> reachable F"
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    31
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    32
  | Acts:  "[| act \<in> Acts F;  s \<in> reachable F;  (s,s') \<in> act |]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23767
diff changeset
    33
            ==> s' \<in> reachable F"
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    34
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    35
definition Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) where
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    36
    "A Co B == {F. F \<in> (reachable F \<inter> A)  co  B}"
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    37
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    38
definition Unless  :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) where
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    39
    "A Unless B == (A-B) Co (A \<union> B)"
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    40
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    41
definition Stable     :: "'a set => 'a program set" where
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    42
    "Stable A == A Co A"
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    43
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
    44
  (*Always is the weak form of "invariant"*)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    45
definition Always :: "'a set => 'a program set" where
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    46
    "Always A == {F. Init F \<subseteq> A} \<inter> Stable A"
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    47
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    48
  (*Polymorphic in both states and the meaning of \<le> *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    49
definition Increasing :: "['a => 'b::{order}] => 'a program set" where
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    50
    "Increasing f == \<Inter>z. Stable {s. z \<le> f s}"
5784
54276fba8420 the Increasing operator
paulson
parents: 5648
diff changeset
    51
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    52
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    53
subsection\<open>traces and reachable\<close>
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    54
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    55
lemma reachable_equiv_traces:
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    56
     "reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    57
apply safe
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    58
apply (erule_tac [2] traces.induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    59
apply (erule reachable.induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    60
apply (blast intro: reachable.intros traces.intros)+
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    61
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    62
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    63
lemma Init_subset_reachable: "Init F \<subseteq> reachable F"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    64
by (blast intro: reachable.intros)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    65
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    66
lemma stable_reachable [intro!,simp]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    67
     "Acts G \<subseteq> Acts F ==> G \<in> stable (reachable F)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    68
by (blast intro: stableI constrainsI reachable.intros)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    69
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    70
(*The set of all reachable states is an invariant...*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    71
lemma invariant_reachable: "F \<in> invariant (reachable F)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    72
apply (simp add: invariant_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    73
apply (blast intro: reachable.intros)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    74
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    75
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    76
(*...in fact the strongest invariant!*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    77
lemma invariant_includes_reachable: "F \<in> invariant A ==> reachable F \<subseteq> A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    78
apply (simp add: stable_def constrains_def invariant_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    79
apply (rule subsetI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    80
apply (erule reachable.induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    81
apply (blast intro: reachable.intros)+
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    82
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    83
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    84
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    85
subsection\<open>Co\<close>
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    86
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    87
(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    88
lemmas constrains_reachable_Int =  
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44870
diff changeset
    89
    subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int]
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    90
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    91
(*Resembles the previous definition of Constrains*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    92
lemma Constrains_eq_constrains: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    93
     "A Co B = {F. F \<in> (reachable F  \<inter>  A) co (reachable F  \<inter>  B)}"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    94
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    95
apply (blast dest: constrains_reachable_Int intro: constrains_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    96
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    97
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    98
lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
    99
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   100
apply (blast intro: constrains_weaken_L)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   101
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   102
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   103
lemma stable_imp_Stable: "F \<in> stable A ==> F \<in> Stable A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   104
apply (unfold stable_def Stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   105
apply (erule constrains_imp_Constrains)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   106
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   107
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   108
lemma ConstrainsI: 
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
   109
    "(!!act s s'. [| act \<in> Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s' \<in> A')  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   110
     ==> F \<in> A Co A'"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   111
apply (rule constrains_imp_Constrains)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   112
apply (blast intro: constrainsI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   113
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   114
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   115
lemma Constrains_empty [iff]: "F \<in> {} Co B"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   116
by (unfold Constrains_def constrains_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   117
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   118
lemma Constrains_UNIV [iff]: "F \<in> A Co UNIV"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   119
by (blast intro: ConstrainsI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   120
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   121
lemma Constrains_weaken_R: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   122
    "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   123
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   124
apply (blast intro: constrains_weaken_R)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   125
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   126
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   127
lemma Constrains_weaken_L: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   128
    "[| F \<in> A Co A'; B \<subseteq> A |] ==> F \<in> B Co A'"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   129
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   130
apply (blast intro: constrains_weaken_L)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   131
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   132
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   133
lemma Constrains_weaken: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   134
   "[| F \<in> A Co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B Co B'"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   135
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   136
apply (blast intro: constrains_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   137
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   138
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   139
(** Union **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   140
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   141
lemma Constrains_Un: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   142
    "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   143
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   144
apply (blast intro: constrains_Un [THEN constrains_weaken])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   145
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   146
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   147
lemma Constrains_UN: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   148
  assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   149
  shows "F \<in> (\<Union>i \<in> I. A i) Co (\<Union>i \<in> I. A' i)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   150
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   151
apply (rule CollectI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   152
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   153
                THEN constrains_weaken],   auto)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   154
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   155
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   156
(** Intersection **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   157
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   158
lemma Constrains_Int: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   159
    "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<inter> B) Co (A' \<inter> B')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   160
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   161
apply (blast intro: constrains_Int [THEN constrains_weaken])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   162
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   163
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   164
lemma Constrains_INT: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   165
  assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   166
  shows "F \<in> (\<Inter>i \<in> I. A i) Co (\<Inter>i \<in> I. A' i)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   167
apply (unfold Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   168
apply (rule CollectI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   169
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   170
                THEN constrains_weaken],   auto)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   171
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   172
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   173
lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable F \<inter> A \<subseteq> A'"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   174
by (simp add: constrains_imp_subset Constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   175
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   176
lemma Constrains_trans: "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   177
apply (simp add: Constrains_eq_constrains)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   178
apply (blast intro: constrains_trans constrains_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   179
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   180
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   181
lemma Constrains_cancel:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   182
     "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
44870
0d23a8ae14df speed up slow proof;
wenzelm
parents: 35416
diff changeset
   183
apply (simp add: Constrains_eq_constrains constrains_def)
0d23a8ae14df speed up slow proof;
wenzelm
parents: 35416
diff changeset
   184
apply best
0d23a8ae14df speed up slow proof;
wenzelm
parents: 35416
diff changeset
   185
done
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   186
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   187
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   188
subsection\<open>Stable\<close>
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   189
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   190
(*Useful because there's no Stable_weaken.  [Tanja Vos]*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   191
lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   192
by blast
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   193
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   194
lemma Stable_eq_stable: "(F \<in> Stable A) = (F \<in> stable (reachable F \<inter> A))"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   195
by (simp add: Stable_def Constrains_eq_constrains stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   196
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   197
lemma StableI: "F \<in> A Co A ==> F \<in> Stable A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   198
by (unfold Stable_def, assumption)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   199
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   200
lemma StableD: "F \<in> Stable A ==> F \<in> A Co A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   201
by (unfold Stable_def, assumption)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   202
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   203
lemma Stable_Un: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   204
    "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<union> A')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   205
apply (unfold Stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   206
apply (blast intro: Constrains_Un)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   207
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   208
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   209
lemma Stable_Int: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   210
    "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<inter> A')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   211
apply (unfold Stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   212
apply (blast intro: Constrains_Int)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   213
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   214
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   215
lemma Stable_Constrains_Un: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   216
    "[| F \<in> Stable C; F \<in> A Co (C \<union> A') |]    
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   217
     ==> F \<in> (C \<union> A) Co (C \<union> A')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   218
apply (unfold Stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   219
apply (blast intro: Constrains_Un [THEN Constrains_weaken])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   220
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   221
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   222
lemma Stable_Constrains_Int: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   223
    "[| F \<in> Stable C; F \<in> (C \<inter> A) Co A' |]    
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   224
     ==> F \<in> (C \<inter> A) Co (C \<inter> A')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   225
apply (unfold Stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   226
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   227
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   228
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   229
lemma Stable_UN: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   230
    "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Union>i \<in> I. A i)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   231
by (simp add: Stable_def Constrains_UN) 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   232
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   233
lemma Stable_INT: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   234
    "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Inter>i \<in> I. A i)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   235
by (simp add: Stable_def Constrains_INT) 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   236
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   237
lemma Stable_reachable: "F \<in> Stable (reachable F)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   238
by (simp add: Stable_eq_stable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   239
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   240
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   241
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   242
subsection\<open>Increasing\<close>
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   243
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   244
lemma IncreasingD: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   245
     "F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   246
by (unfold Increasing_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   247
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   248
lemma mono_Increasing_o: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   249
     "mono g ==> Increasing f \<subseteq> Increasing (g o f)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   250
apply (simp add: Increasing_def Stable_def Constrains_def stable_def 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   251
                 constrains_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   252
apply (blast intro: monoD order_trans)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   253
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   254
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   255
lemma strict_IncreasingD: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   256
     "!!z::nat. F \<in> Increasing f ==> F \<in> Stable {s. z < f s}"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   257
by (simp add: Increasing_def Suc_le_eq [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   258
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   259
lemma increasing_imp_Increasing: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   260
     "F \<in> increasing f ==> F \<in> Increasing f"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   261
apply (unfold increasing_def Increasing_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   262
apply (blast intro: stable_imp_Stable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   263
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   264
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44870
diff changeset
   265
lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   266
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   267
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   268
subsection\<open>The Elimination Theorem\<close>
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   269
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   270
(*The "free" m has become universally quantified! Should the premise be !!m
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   271
instead of \<forall>m ?  Would make it harder to use in forward proof.*)
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   272
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   273
lemma Elimination: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   274
    "[| \<forall>m. F \<in> {s. s x = m} Co (B m) |]  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   275
     ==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   276
by (unfold Constrains_def constrains_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   277
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   278
(*As above, but for the trivial case of a one-variable state, in which the
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   279
  state is identified with its one variable.*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   280
lemma Elimination_sing: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   281
    "(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   282
by (unfold Constrains_def constrains_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   283
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   284
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   285
subsection\<open>Specialized laws for handling Always\<close>
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   286
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   287
(** Natural deduction rules for "Always A" **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   288
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   289
lemma AlwaysI: "[| Init F \<subseteq> A;  F \<in> Stable A |] ==> F \<in> Always A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   290
by (simp add: Always_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   291
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   292
lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   293
by (simp add: Always_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   294
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44870
diff changeset
   295
lemmas AlwaysE = AlwaysD [THEN conjE]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44870
diff changeset
   296
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   297
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   298
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   299
(*The set of all reachable states is Always*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   300
lemma Always_includes_reachable: "F \<in> Always A ==> reachable F \<subseteq> A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   301
apply (simp add: Stable_def Constrains_def constrains_def Always_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   302
apply (rule subsetI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   303
apply (erule reachable.induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   304
apply (blast intro: reachable.intros)+
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   305
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   306
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   307
lemma invariant_imp_Always: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   308
     "F \<in> invariant A ==> F \<in> Always A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   309
apply (unfold Always_def invariant_def Stable_def stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   310
apply (blast intro: constrains_imp_Constrains)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   311
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   312
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44870
diff changeset
   313
lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   314
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   315
lemma Always_eq_invariant_reachable:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   316
     "Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   317
apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   318
                 stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   319
apply (blast intro: reachable.intros)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   320
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   321
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   322
(*the RHS is the traditional definition of the "always" operator*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   323
lemma Always_eq_includes_reachable: "Always A = {F. reachable F \<subseteq> A}"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   324
by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   325
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   326
lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   327
by (auto simp add: Always_eq_includes_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   328
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   329
lemma UNIV_AlwaysI: "UNIV \<subseteq> A ==> F \<in> Always A"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   330
by (auto simp add: Always_eq_includes_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   331
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   332
lemma Always_eq_UN_invariant: "Always A = (\<Union>I \<in> Pow A. invariant I)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   333
apply (simp add: Always_eq_includes_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   334
apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   335
                    invariant_includes_reachable [THEN subsetD])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   336
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   337
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   338
lemma Always_weaken: "[| F \<in> Always A; A \<subseteq> B |] ==> F \<in> Always B"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   339
by (auto simp add: Always_eq_includes_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   340
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   341
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   342
subsection\<open>"Co" rules involving Always\<close>
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   343
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   344
lemma Always_Constrains_pre:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   345
     "F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   346
by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   347
              Int_assoc [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   348
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   349
lemma Always_Constrains_post:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   350
     "F \<in> Always INV ==> (F \<in> A Co (INV \<inter> A')) = (F \<in> A Co A')"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   351
by (simp add: Always_includes_reachable [THEN Int_absorb2] 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   352
              Constrains_eq_constrains Int_assoc [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   353
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   354
(* [| F \<in> Always INV;  F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44870
diff changeset
   355
lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1]
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   356
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   357
(* [| F \<in> Always INV;  F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44870
diff changeset
   358
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   359
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   360
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   361
lemma Always_Constrains_weaken:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   362
     "[| F \<in> Always C;  F \<in> A Co A';    
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   363
         C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   364
      ==> F \<in> B Co B'"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   365
apply (rule Always_ConstrainsI, assumption)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   366
apply (drule Always_ConstrainsD, assumption)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   367
apply (blast intro: Constrains_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   368
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   369
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   370
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   371
(** Conjoining Always properties **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   372
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   373
lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   374
by (auto simp add: Always_eq_includes_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   375
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   376
lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   377
by (auto simp add: Always_eq_includes_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   378
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   379
lemma Always_Int_I:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   380
     "[| F \<in> Always A;  F \<in> Always B |] ==> F \<in> Always (A \<inter> B)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   381
by (simp add: Always_Int_distrib)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   382
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   383
(*Allows a kind of "implication introduction"*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   384
lemma Always_Compl_Un_eq:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   385
     "F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   386
by (auto simp add: Always_eq_includes_reachable)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   387
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   388
(*Delete the nearest invariance assumption (which will be the second one
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   389
  used by Always_Int_I) *)
68238
eb57621568bb avoid undeclared frees;
wenzelm
parents: 67613
diff changeset
   390
lemmas Always_thin = thin_rl [of "F \<in> Always A"] for F A
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 6823
diff changeset
   391
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   392
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   393
subsection\<open>Totalize\<close>
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   394
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   395
lemma reachable_imp_reachable_tot:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   396
      "s \<in> reachable F ==> s \<in> reachable (totalize F)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   397
apply (erule reachable.induct)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   398
 apply (rule reachable.Init) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   399
 apply simp 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   400
apply (rule_tac act = "totalize_act act" in reachable.Acts) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   401
apply (auto simp add: totalize_act_def) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   402
done
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   403
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   404
lemma reachable_tot_imp_reachable:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   405
      "s \<in> reachable (totalize F) ==> s \<in> reachable F"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   406
apply (erule reachable.induct)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   407
 apply (rule reachable.Init, simp) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   408
apply (force simp add: totalize_act_def intro: reachable.Acts) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   409
done
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   410
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   411
lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   412
by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   413
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   414
lemma totalize_Constrains_iff [simp]: "(totalize F \<in> A Co B) = (F \<in> A Co B)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   415
by (simp add: Constrains_def) 
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   416
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   417
lemma totalize_Stable_iff [simp]: "(totalize F \<in> Stable A) = (F \<in> Stable A)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   418
by (simp add: Stable_def)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   419
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   420
lemma totalize_Always_iff [simp]: "(totalize F \<in> Always A) = (F \<in> Always A)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   421
by (simp add: Always_def)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   422
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   423
end