src/ZF/UNITY/UNITY.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/UNITY.thy
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Computer Laboratory
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     3
    Copyright   2001  University of Cambridge
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     4
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     5
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
     6
header {*The Basic UNITY Theory*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 16183
diff changeset
     8
theory UNITY imports State begin
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
     9
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
    10
text{*The basic UNITY theory (revised version, based upon the "co" operator)
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
    11
From Misra, "A Logic for Concurrent Programming", 1994.
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
    12
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
    13
This ZF theory was ported from its HOL equivalent.*}
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
    14
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    15
consts
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
    16
  "constrains" :: "[i, i] => i"  (infixl "co"     60)
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
    17
  op_unless    :: "[i, i] => i"  (infixl "unless" 60)
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    18
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    19
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    20
  program  :: i  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    21
  "program == {<init, acts, allowed>:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    22
               Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)).
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    23
               id(state) \<in> acts & id(state) \<in> allowed}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    24
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    25
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    26
  mk_program :: "[i,i,i]=>i"  where
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    27
  --{* The definition yields a program thanks to the coercions
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    28
       init \<inter> state, acts \<inter> Pow(state*state), etc. *}
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    29
  "mk_program(init, acts, allowed) ==
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    30
    <init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)),
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    31
              cons(id(state), allowed \<inter> Pow(state*state))>"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    32
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    33
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    34
  SKIP :: i  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    35
  "SKIP == mk_program(state, 0, Pow(state*state))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    36
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    37
  (* Coercion from anything to program *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    38
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    39
  programify :: "i=>i"  where
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    40
  "programify(F) == if F \<in> program then F else SKIP"
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    41
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    42
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    43
  RawInit :: "i=>i"  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    44
  "RawInit(F) == fst(F)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    45
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    46
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    47
  Init :: "i=>i"  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    48
  "Init(F) == RawInit(programify(F))"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    49
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    50
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    51
  RawActs :: "i=>i"  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    52
  "RawActs(F) == cons(id(state), fst(snd(F)))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    53
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    54
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    55
  Acts :: "i=>i"  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    56
  "Acts(F) == RawActs(programify(F))"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    57
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    58
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    59
  RawAllowedActs :: "i=>i"  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    60
  "RawAllowedActs(F) == cons(id(state), snd(snd(F)))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    61
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    62
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    63
  AllowedActs :: "i=>i"  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    64
  "AllowedActs(F) == RawAllowedActs(programify(F))"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    65
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    66
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    67
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    68
  Allowed :: "i =>i"  where
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    69
  "Allowed(F) == {G \<in> program. Acts(G) \<subseteq> AllowedActs(F)}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    70
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    71
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    72
  initially :: "i=>i"  where
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    73
  "initially(A) == {F \<in> program. Init(F)\<subseteq>A}"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    74
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    75
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    76
  stable     :: "i=>i"  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    77
   "stable(A) == A co A"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    78
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    79
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    80
  strongest_rhs :: "[i, i] => i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    81
  "strongest_rhs(F, A) == \<Inter>({B \<in> Pow(state). F \<in> A co B})"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    82
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    83
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    84
  invariant :: "i => i"  where
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    85
  "invariant(A) == initially(A) \<inter> stable(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    86
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    87
  (* meta-function composition *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    88
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    89
  metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65)  where
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    90
  "f comp g == %x. f(g(x))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    91
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    92
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    93
  pg_compl :: "i=>i"  where
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    94
  "pg_compl(X)== program - X"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    95
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    96
defs
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    97
  constrains_def:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    98
     "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
    99
    --{* the condition @{term "st_set(A)"} makes the definition slightly
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   100
         stronger than the HOL one *}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   101
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   102
  unless_def:    "A unless B == (A - B) co (A \<union> B)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   103
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   104
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   105
text{*SKIP*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   106
lemma SKIP_in_program [iff,TC]: "SKIP \<in> program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   107
by (force simp add: SKIP_def program_def mk_program_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   108
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   109
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   110
subsection{*The function @{term programify}, the coercion from anything to
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   111
 program*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   112
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   113
lemma programify_program [simp]: "F \<in> program ==> programify(F)=F"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   114
by (force simp add: programify_def) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   115
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   116
lemma programify_in_program [iff,TC]: "programify(F) \<in> program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   117
by (force simp add: programify_def) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   118
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   119
text{*Collapsing rules: to remove programify from expressions*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   120
lemma programify_idem [simp]: "programify(programify(F))=programify(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   121
by (force simp add: programify_def) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   122
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   123
lemma Init_programify [simp]: "Init(programify(F)) = Init(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   124
by (simp add: Init_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   125
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   126
lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   127
by (simp add: Acts_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   128
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   129
lemma AllowedActs_programify [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   130
     "AllowedActs(programify(F)) = AllowedActs(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   131
by (simp add: AllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   132
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   133
subsection{*The Inspectors for Programs*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   134
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   135
lemma id_in_RawActs: "F \<in> program ==>id(state) \<in> RawActs(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   136
by (auto simp add: program_def RawActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   137
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   138
lemma id_in_Acts [iff,TC]: "id(state) \<in> Acts(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   139
by (simp add: id_in_RawActs Acts_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   140
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   141
lemma id_in_RawAllowedActs: "F \<in> program ==>id(state) \<in> RawAllowedActs(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   142
by (auto simp add: program_def RawAllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   143
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   144
lemma id_in_AllowedActs [iff,TC]: "id(state) \<in> AllowedActs(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   145
by (simp add: id_in_RawAllowedActs AllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   146
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   147
lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   148
by (simp add: cons_absorb)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   149
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   150
lemma cons_id_AllowedActs [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   151
     "cons(id(state), AllowedActs(F)) = AllowedActs(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   152
by (simp add: cons_absorb)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   153
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   154
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   155
subsection{*Types of the Inspectors*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   156
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   157
lemma RawInit_type: "F \<in> program ==> RawInit(F)\<subseteq>state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   158
by (auto simp add: program_def RawInit_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   159
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   160
lemma RawActs_type: "F \<in> program ==> RawActs(F)\<subseteq>Pow(state*state)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   161
by (auto simp add: program_def RawActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   162
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   163
lemma RawAllowedActs_type:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   164
     "F \<in> program ==> RawAllowedActs(F)\<subseteq>Pow(state*state)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   165
by (auto simp add: program_def RawAllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   166
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   167
lemma Init_type: "Init(F)\<subseteq>state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   168
by (simp add: RawInit_type Init_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   169
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   170
lemmas InitD = Init_type [THEN subsetD]
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   171
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   172
lemma st_set_Init [iff]: "st_set(Init(F))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   173
apply (unfold st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   174
apply (rule Init_type)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   175
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   176
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   177
lemma Acts_type: "Acts(F)\<subseteq>Pow(state*state)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   178
by (simp add: RawActs_type Acts_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   179
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   180
lemma AllowedActs_type: "AllowedActs(F) \<subseteq> Pow(state*state)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   181
by (simp add: RawAllowedActs_type AllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   182
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   183
text{*Needed in Behaviors*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   184
lemma ActsD: "[| act \<in> Acts(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   185
by (blast dest: Acts_type [THEN subsetD])
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   186
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   187
lemma AllowedActsD:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   188
     "[| act \<in> AllowedActs(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   189
by (blast dest: AllowedActs_type [THEN subsetD])
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   190
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   191
subsection{*Simplification rules involving @{term state}, @{term Init}, 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   192
  @{term Acts}, and @{term AllowedActs}*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   193
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   194
text{*But are they really needed?*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   195
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   196
lemma state_subset_is_Init_iff [iff]: "state \<subseteq> Init(F) \<longleftrightarrow> Init(F)=state"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   197
by (cut_tac F = F in Init_type, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   198
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   199
lemma Pow_state_times_state_is_subset_Acts_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   200
     "Pow(state*state) \<subseteq> Acts(F) \<longleftrightarrow> Acts(F)=Pow(state*state)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   201
by (cut_tac F = F in Acts_type, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   202
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   203
lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   204
     "Pow(state*state) \<subseteq> AllowedActs(F) \<longleftrightarrow> AllowedActs(F)=Pow(state*state)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   205
by (cut_tac F = F in AllowedActs_type, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   206
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   207
subsubsection{*Eliminating @{text "\<inter> state"} from expressions*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   208
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   209
lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   210
by (cut_tac F = F in Init_type, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   211
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   212
lemma state_Int_Init [simp]: "state \<inter> Init(F) = Init(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   213
by (cut_tac F = F in Init_type, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   214
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   215
lemma Acts_Int_Pow_state_times_state [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   216
     "Acts(F) \<inter> Pow(state*state) = Acts(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   217
by (cut_tac F = F in Acts_type, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   218
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   219
lemma state_times_state_Int_Acts [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   220
     "Pow(state*state) \<inter> Acts(F) = Acts(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   221
by (cut_tac F = F in Acts_type, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   222
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   223
lemma AllowedActs_Int_Pow_state_times_state [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   224
     "AllowedActs(F) \<inter> Pow(state*state) = AllowedActs(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   225
by (cut_tac F = F in AllowedActs_type, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   226
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   227
lemma state_times_state_Int_AllowedActs [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   228
     "Pow(state*state) \<inter> AllowedActs(F) = AllowedActs(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   229
by (cut_tac F = F in AllowedActs_type, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   230
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   231
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   232
subsubsection{*The Operator @{term mk_program}*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   233
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   234
lemma mk_program_in_program [iff,TC]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   235
     "mk_program(init, acts, allowed) \<in> program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   236
by (auto simp add: mk_program_def program_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   237
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   238
lemma RawInit_eq [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   239
     "RawInit(mk_program(init, acts, allowed)) = init \<inter> state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   240
by (auto simp add: mk_program_def RawInit_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   241
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   242
lemma RawActs_eq [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   243
     "RawActs(mk_program(init, acts, allowed)) = 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   244
      cons(id(state), acts \<inter> Pow(state*state))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   245
by (auto simp add: mk_program_def RawActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   246
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   247
lemma RawAllowedActs_eq [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   248
     "RawAllowedActs(mk_program(init, acts, allowed)) =
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   249
      cons(id(state), allowed \<inter> Pow(state*state))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   250
by (auto simp add: mk_program_def RawAllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   251
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   252
lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \<inter> state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   253
by (simp add: Init_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   254
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   255
lemma Acts_eq [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   256
     "Acts(mk_program(init, acts, allowed)) = 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   257
      cons(id(state), acts  \<inter> Pow(state*state))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   258
by (simp add: Acts_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   259
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   260
lemma AllowedActs_eq [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   261
     "AllowedActs(mk_program(init, acts, allowed))=
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   262
      cons(id(state), allowed \<inter> Pow(state*state))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   263
by (simp add: AllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   264
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   265
text{*Init, Acts, and AlowedActs  of SKIP *}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   266
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   267
lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   268
by (simp add: SKIP_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   269
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   270
lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   271
by (force simp add: SKIP_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   272
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   273
lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   274
by (force simp add: SKIP_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   275
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   276
lemma Init_SKIP [simp]: "Init(SKIP) = state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   277
by (force simp add: SKIP_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   278
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   279
lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   280
by (force simp add: SKIP_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   281
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   282
lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   283
by (force simp add: SKIP_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   284
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   285
text{*Equality of UNITY programs*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   286
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   287
lemma raw_surjective_mk_program:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   288
     "F \<in> program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   289
apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   290
            RawAllowedActs_def, blast+)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   291
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   292
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   293
lemma surjective_mk_program [simp]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   294
  "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   295
by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   296
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   297
lemma program_equalityI:                             
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   298
    "[|Init(F) = Init(G); Acts(F) = Acts(G);
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   299
       AllowedActs(F) = AllowedActs(G); F \<in> program; G \<in> program |] ==> F = G"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   300
apply (subgoal_tac "programify(F) = programify(G)") 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   301
apply simp 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   302
apply (simp only: surjective_mk_program [symmetric]) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   303
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   304
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   305
lemma program_equalityE:                             
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   306
 "[|F = G;
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   307
    [|Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   308
    ==> P |] 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   309
  ==> P"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   310
by force
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   311
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   312
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   313
lemma program_equality_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   314
    "[| F \<in> program; G \<in> program |] ==>(F=G)  \<longleftrightarrow>
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   315
     (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   316
by (blast intro: program_equalityI program_equalityE)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   317
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   318
subsection{*These rules allow "lazy" definition expansion*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   319
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   320
lemma def_prg_Init:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   321
     "F == mk_program (init,acts,allowed) ==> Init(F) = init \<inter> state"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   322
by auto
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   323
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   324
lemma def_prg_Acts:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   325
     "F == mk_program (init,acts,allowed)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   326
      ==> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   327
by auto
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   328
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   329
lemma def_prg_AllowedActs:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   330
     "F == mk_program (init,acts,allowed)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   331
      ==> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   332
by auto
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   333
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   334
lemma def_prg_simps:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   335
    "[| F == mk_program (init,acts,allowed) |]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   336
     ==> Init(F) = init \<inter> state & 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   337
         Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) &
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   338
         AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   339
by auto
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   340
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   341
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   342
text{*An action is expanded only if a pair of states is being tested against it*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   343
lemma def_act_simp:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   344
     "[| act == {<s,s'> \<in> A*B. P(s, s')} |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   345
      ==> (<s,s'> \<in> act) \<longleftrightarrow> (<s,s'> \<in> A*B & P(s, s'))"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   346
by auto
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   347
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   348
text{*A set is expanded only if an element is being tested against it*}
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   349
lemma def_set_simp: "A == B ==> (x \<in> A) \<longleftrightarrow> (x \<in> B)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   350
by auto
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   351
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   352
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   353
subsection{*The Constrains Operator*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   354
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   355
lemma constrains_type: "A co B \<subseteq> program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   356
by (force simp add: constrains_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   357
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   358
lemma constrainsI:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   359
    "[|(!!act s s'. [| act: Acts(F);  <s,s'> \<in> act; s \<in> A|] ==> s' \<in> A');
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   360
        F \<in> program; st_set(A) |]  ==> F \<in> A co A'"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   361
by (force simp add: constrains_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   362
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   363
lemma constrainsD:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   364
   "F \<in> A co B ==> \<forall>act \<in> Acts(F). act``A\<subseteq>B"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   365
by (force simp add: constrains_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   366
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   367
lemma constrainsD2: "F \<in> A co B ==> F \<in> program & st_set(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   368
by (force simp add: constrains_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   369
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   370
lemma constrains_empty [iff]: "F \<in> 0 co B \<longleftrightarrow> F \<in> program"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   371
by (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   372
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   373
lemma constrains_empty2 [iff]: "(F \<in> A co 0) \<longleftrightarrow> (A=0 & F \<in> program)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   374
by (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   375
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   376
lemma constrains_state [iff]: "(F \<in> state co B) \<longleftrightarrow> (state\<subseteq>B & F \<in> program)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   377
apply (cut_tac F = F in Acts_type)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   378
apply (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   379
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   380
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   381
lemma constrains_state2 [iff]: "F \<in> A co state \<longleftrightarrow> (F \<in> program & st_set(A))"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   382
apply (cut_tac F = F in Acts_type)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   383
apply (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   384
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   385
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   386
text{*monotonic in 2nd argument*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   387
lemma constrains_weaken_R:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   388
    "[| F \<in> A co A'; A'\<subseteq>B' |] ==> F \<in> A co B'"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   389
apply (unfold constrains_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   390
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   391
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   392
text{*anti-monotonic in 1st argument*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   393
lemma constrains_weaken_L:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   394
    "[| F \<in> A co A'; B\<subseteq>A |] ==> F \<in> B co A'"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   395
apply (unfold constrains_def st_set_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   396
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   397
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   398
lemma constrains_weaken:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   399
   "[| F \<in> A co A'; B\<subseteq>A; A'\<subseteq>B' |] ==> F \<in> B co B'"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   400
apply (drule constrains_weaken_R)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   401
apply (drule_tac [2] constrains_weaken_L, blast+)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   402
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   403
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   404
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   405
subsection{*Constrains and Union*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   406
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   407
lemma constrains_Un:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   408
    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   409
by (auto simp add: constrains_def st_set_def, force)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   410
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   411
lemma constrains_UN:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   412
     "[|!!i. i \<in> I ==> F \<in> A(i) co A'(i); F \<in> program |]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   413
      ==> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   414
by (force simp add: constrains_def st_set_def) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   415
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   416
lemma constrains_Un_distrib:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   417
     "(A \<union> B) co C = (A co C) \<inter> (B co C)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   418
by (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   419
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   420
lemma constrains_UN_distrib:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   421
   "i \<in> I ==> (\<Union>i \<in> I. A(i)) co B = (\<Inter>i \<in> I. A(i) co B)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   422
by (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   423
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   424
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   425
subsection{*Constrains and Intersection*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   426
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   427
lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   428
by (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   429
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   430
lemma constrains_INT_distrib:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   431
     "x \<in> I ==> A co (\<Inter>i \<in> I. B(i)) = (\<Inter>i \<in> I. A co B(i))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   432
by (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   433
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   434
lemma constrains_Int:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   435
    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   436
by (force simp add: constrains_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   437
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   438
lemma constrains_INT [rule_format]:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   439
     "[| \<forall>i \<in> I. F \<in> A(i) co A'(i); F \<in> program|]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   440
      ==> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   441
apply (case_tac "I=0")
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   442
 apply (simp add: Inter_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   443
apply (erule not_emptyE)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   444
apply (auto simp add: constrains_def st_set_def, blast) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   445
apply (drule bspec, assumption, force) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   446
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   447
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   448
(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   449
lemma constrains_All:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   450
"[| \<forall>z. F:{s \<in> state. P(s, z)} co {s \<in> state. Q(s, z)}; F \<in> program |]==>
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   451
    F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   452
by (unfold constrains_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   453
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   454
lemma constrains_imp_subset:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   455
  "[| F \<in> A co A' |] ==> A \<subseteq> A'"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   456
by (unfold constrains_def st_set_def, force)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   457
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   458
text{*The reasoning is by subsets since "co" refers to single actions
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   459
  only.  So this rule isn't that useful.*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   460
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   461
lemma constrains_trans: "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   462
by (unfold constrains_def st_set_def, auto, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   463
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   464
lemma constrains_cancel:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   465
"[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   466
apply (drule_tac A = B in constrains_imp_subset)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   467
apply (blast intro: constrains_weaken_R)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   468
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   469
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   470
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   471
subsection{*The Unless Operator*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   472
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   473
lemma unless_type: "A unless B \<subseteq> program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   474
by (force simp add: unless_def constrains_def) 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   475
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   476
lemma unlessI: "[| F \<in> (A-B) co (A \<union> B) |] ==> F \<in> A unless B"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   477
apply (unfold unless_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   478
apply (blast dest: constrainsD2)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   479
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   480
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   481
lemma unlessD: "F :A unless B ==> F \<in> (A-B) co (A \<union> B)"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   482
by (unfold unless_def, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   483
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   484
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   485
subsection{*The Operator @{term initially}*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   486
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   487
lemma initially_type: "initially(A) \<subseteq> program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   488
by (unfold initially_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   489
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   490
lemma initiallyI: "[| F \<in> program; Init(F)\<subseteq>A |] ==> F \<in> initially(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   491
by (unfold initially_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   492
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   493
lemma initiallyD: "F \<in> initially(A) ==> Init(F)\<subseteq>A"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   494
by (unfold initially_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   495
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   496
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   497
subsection{*The Operator @{term stable}*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   498
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   499
lemma stable_type: "stable(A)\<subseteq>program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   500
by (unfold stable_def constrains_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   501
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   502
lemma stableI: "F \<in> A co A ==> F \<in> stable(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   503
by (unfold stable_def, assumption)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   504
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   505
lemma stableD: "F \<in> stable(A) ==> F \<in> A co A"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   506
by (unfold stable_def, assumption)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   507
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   508
lemma stableD2: "F \<in> stable(A) ==> F \<in> program & st_set(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   509
by (unfold stable_def constrains_def, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   510
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   511
lemma stable_state [simp]: "stable(state) = program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   512
by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD])
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   513
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   514
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   515
lemma stable_unless: "stable(A)= A unless 0"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   516
by (auto simp add: unless_def stable_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   517
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   518
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   519
subsection{*Union and Intersection with @{term stable}*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   520
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   521
lemma stable_Un:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   522
    "[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable(A \<union> A')"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   523
apply (unfold stable_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   524
apply (blast intro: constrains_Un)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   525
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   526
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   527
lemma stable_UN:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   528
     "[|!!i. i\<in>I ==> F \<in> stable(A(i)); F \<in> program |] 
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   529
      ==> F \<in> stable (\<Union>i \<in> I. A(i))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   530
apply (unfold stable_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   531
apply (blast intro: constrains_UN)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   532
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   533
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   534
lemma stable_Int:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   535
    "[| F \<in> stable(A);  F \<in> stable(A') |] ==> F \<in> stable (A \<inter> A')"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   536
apply (unfold stable_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   537
apply (blast intro: constrains_Int)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   538
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   539
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   540
lemma stable_INT:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   541
     "[| !!i. i \<in> I ==> F \<in> stable(A(i)); F \<in> program |]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   542
      ==> F \<in> stable (\<Inter>i \<in> I. A(i))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   543
apply (unfold stable_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   544
apply (blast intro: constrains_INT)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   545
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   546
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   547
lemma stable_All:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   548
    "[|\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program|]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   549
     ==> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   550
apply (unfold stable_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   551
apply (rule constrains_All, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   552
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   553
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   554
lemma stable_constrains_Un:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   555
     "[| F \<in> stable(C); F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   556
apply (unfold stable_def constrains_def st_set_def, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   557
apply (blast dest!: bspec)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   558
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   559
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   560
lemma stable_constrains_Int:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   561
     "[| F \<in> stable(C); F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   562
by (unfold stable_def constrains_def st_set_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   563
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   564
(* [| F \<in> stable(C); F  \<in> (C \<inter> A) co A |] ==> F \<in> stable(C \<inter> A) *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   565
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI]
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   566
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   567
subsection{*The Operator @{term invariant}*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   568
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   569
lemma invariant_type: "invariant(A) \<subseteq> program"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   570
apply (unfold invariant_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   571
apply (blast dest: stable_type [THEN subsetD])
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   572
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   573
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   574
lemma invariantI: "[| Init(F)\<subseteq>A;  F \<in> stable(A) |] ==> F \<in> invariant(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   575
apply (unfold invariant_def initially_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   576
apply (frule stable_type [THEN subsetD], auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   577
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   578
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   579
lemma invariantD: "F \<in> invariant(A) ==> Init(F)\<subseteq>A & F \<in> stable(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   580
by (unfold invariant_def initially_def, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   581
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   582
lemma invariantD2: "F \<in> invariant(A) ==> F \<in> program & st_set(A)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   583
apply (unfold invariant_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   584
apply (blast dest: stableD2)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   585
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   586
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   587
text{*Could also say
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   588
      @{term "invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)"}*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   589
lemma invariant_Int:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   590
  "[| F \<in> invariant(A);  F \<in> invariant(B) |] ==> F \<in> invariant(A \<inter> B)"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   591
apply (unfold invariant_def initially_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   592
apply (simp add: stable_Int, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   593
done
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   594
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   595
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   596
subsection{*The Elimination Theorem*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   597
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   598
(** The "free" m has become universally quantified!
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   599
 Should the premise be !!m instead of \<forall>m ? Would make it harder
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   600
 to use in forward proof. **)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   601
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   602
text{*The general case is easier to prove than the special case!*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   603
lemma "elimination":
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   604
    "[| \<forall>m \<in> M. F \<in> {s \<in> A. x(s) = m} co B(m); F \<in> program  |]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   605
     ==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   606
by (auto simp add: constrains_def st_set_def, blast)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   607
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 14077
diff changeset
   608
text{*As above, but for the special case of A=state*}
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   609
lemma elimination2:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   610
     "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} co B(m); F \<in> program  |]
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   611
     ==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   612
by (rule UNITY.elimination, auto)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   613
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   614
subsection{*The Operator @{term strongest_rhs}*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   615
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   616
lemma constrains_strongest_rhs:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   617
    "[| F \<in> program; st_set(A) |] ==> F \<in> A co (strongest_rhs(F,A))"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   618
by (auto simp add: constrains_def strongest_rhs_def st_set_def
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   619
              dest: Acts_type [THEN subsetD])
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   620
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   621
lemma strongest_rhs_is_strongest:
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   622
     "[| F \<in> A co B; st_set(B) |] ==> strongest_rhs(F,A) \<subseteq> B"
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   623
by (auto simp add: constrains_def strongest_rhs_def st_set_def)
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   624
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
   625
ML {*
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
   626
fun simp_of_act def = def RS @{thm def_act_simp};
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
   627
fun simp_of_set def = def RS @{thm def_set_simp};
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   628
*}
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14046
diff changeset
   629
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   630
end