src/ZF/UNITY/Union.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
child 60770 240563fbf41d
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/Union.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
Unions of programs
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     6
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
     7
Partly from Misra's Chapter 5 \<in> Asynchronous Compositions of Programs
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     8
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     9
Theory ported form HOL..
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    10
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    11
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    12
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    13
theory Union imports SubstAx FP
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
begin
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    15
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    16
definition
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    17
  (*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    18
  ok :: "[i, i] => o"     (infixl "ok" 65)  where
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    19
    "F ok G == Acts(F) \<subseteq> AllowedActs(G) &
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    20
               Acts(G) \<subseteq> AllowedActs(F)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    21
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    22
definition
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    23
  (*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    24
  OK  :: "[i, i=>i] => o"  where
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    25
    "OK(I,F) == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts(F(i)) \<subseteq> AllowedActs(F(j)))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    26
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    27
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    28
  JOIN  :: "[i, i=>i] => i"  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    29
  "JOIN(I,F) == if I = 0 then SKIP else
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    30
                 mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)),
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    31
                 \<Inter>i \<in> I. AllowedActs(F(i)))"
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
  Join :: "[i, i] => i"    (infixl "Join" 65)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    35
  "F Join G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G),
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    36
                                AllowedActs(F) \<inter> AllowedActs(G))"
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    37
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    38
  (*Characterizes safety properties.  Used with specifying AllowedActs*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    39
  safety_prop :: "i => o"  where
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    40
  "safety_prop(X) == X\<subseteq>program &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    41
      SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    42
35427
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35112
diff changeset
    43
notation (xsymbols)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35112
diff changeset
    44
  SKIP  ("\<bottom>") and
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35112
diff changeset
    45
  Join  (infixl "\<squnion>" 65)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35112
diff changeset
    46
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    47
syntax
35112
ff6f60e6ab85 numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents: 32960
diff changeset
    48
  "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    49
  "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _ \<in> _./ _)" 10)
35427
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35112
diff changeset
    50
syntax (xsymbols)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35112
diff changeset
    51
  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 35112
diff changeset
    52
  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    53
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    54
translations
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    55
  "JN x \<in> A. B"   == "CONST JOIN(A, (%x. B))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    56
  "JN x y. B"   == "JN x. JN y. B"
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    57
  "JN x. B"     == "CONST JOIN(CONST state,(%x. B))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    58
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    59
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    60
subsection{*SKIP*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    61
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    62
lemma reachable_SKIP [simp]: "reachable(SKIP) = state"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    63
by (force elim: reachable.induct intro: reachable.intros)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    64
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    65
text{*Elimination programify from ok and Join*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    66
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    67
lemma ok_programify_left [iff]: "programify(F) ok G \<longleftrightarrow> F ok G"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    68
by (simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    69
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    70
lemma ok_programify_right [iff]: "F ok programify(G) \<longleftrightarrow> F ok G"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    71
by (simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    72
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    73
lemma Join_programify_left [simp]: "programify(F) Join G = F Join G"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    74
by (simp add: Join_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    75
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    76
lemma Join_programify_right [simp]: "F Join programify(G) = F Join G"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    77
by (simp add: Join_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    78
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    79
subsection{*SKIP and safety properties*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    80
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    81
lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) \<longleftrightarrow> (A\<subseteq>B & st_set(A))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    82
by (unfold constrains_def st_set_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    83
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    84
lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B)\<longleftrightarrow> (state \<inter> A\<subseteq>B)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    85
by (unfold Constrains_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    86
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    87
lemma SKIP_in_stable [iff]: "SKIP \<in> stable(A) \<longleftrightarrow> st_set(A)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    88
by (auto simp add: stable_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    89
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    90
lemma SKIP_in_Stable [iff]: "SKIP \<in> Stable(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    91
by (unfold Stable_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    92
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    93
subsection{*Join and JOIN types*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    94
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    95
lemma Join_in_program [iff,TC]: "F Join G \<in> program"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    96
by (unfold Join_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    97
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    98
lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \<in> program"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    99
by (unfold JOIN_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   100
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   101
subsection{*Init, Acts, and AllowedActs of Join and JOIN*}
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   102
lemma Init_Join [simp]: "Init(F Join G) = Init(F) \<inter> Init(G)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   103
by (simp add: Int_assoc Join_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   104
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   105
lemma Acts_Join [simp]: "Acts(F Join G) = Acts(F) \<union> Acts(G)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   106
by (simp add: Int_Un_distrib2 cons_absorb Join_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   107
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   108
lemma AllowedActs_Join [simp]: "AllowedActs(F Join G) =
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   109
  AllowedActs(F) \<inter> AllowedActs(G)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   110
apply (simp add: Int_assoc cons_absorb Join_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   111
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   112
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   113
subsection{*Join's algebraic laws*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   114
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   115
lemma Join_commute: "F Join G = G Join F"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   116
by (simp add: Join_def Un_commute Int_commute)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   117
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   118
lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   119
apply (simp add: Join_def Int_Un_distrib2 cons_absorb)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   120
apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   121
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   122
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   123
lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   124
by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   125
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   126
subsection{*Needed below*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   127
lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   128
by auto
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   129
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   130
lemma Join_SKIP_left [simp]: "SKIP Join F = programify(F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   131
apply (unfold Join_def SKIP_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   132
apply (auto simp add: Int_absorb cons_eq)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   133
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   134
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   135
lemma Join_SKIP_right [simp]: "F Join SKIP =  programify(F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   136
apply (subst Join_commute)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   137
apply (simp add: Join_SKIP_left)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   138
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   139
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   140
lemma Join_absorb [simp]: "F Join F = programify(F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   141
by (rule program_equalityI, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   142
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   143
lemma Join_left_absorb: "F Join (F Join G) = F Join G"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   144
by (simp add: Join_assoc [symmetric])
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   145
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   146
subsection{*Join is an AC-operator*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   147
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   148
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   149
subsection{*Eliminating programify form JN and OK expressions*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   150
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   151
lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) \<longleftrightarrow> OK(I, F)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   152
by (simp add: OK_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   153
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   154
lemma JN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   155
by (simp add: JOIN_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   156
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   157
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   158
subsection{*JN*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   159
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   160
lemma JN_empty [simp]: "JOIN(0, F) = SKIP"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   161
by (unfold JOIN_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   162
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   163
lemma Init_JN [simp]:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   164
     "Init(\<Squnion>i \<in> I. F(i)) = (if I=0 then state else (\<Inter>i \<in> I. Init(F(i))))"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14093
diff changeset
   165
by (simp add: JOIN_def INT_extend_simps del: INT_simps)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   166
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   167
lemma Acts_JN [simp]:
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   168
     "Acts(JOIN(I,F)) = cons(id(state), \<Union>i \<in> I.  Acts(F(i)))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   169
apply (unfold JOIN_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   170
apply (auto simp del: INT_simps UN_simps)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   171
apply (rule equalityI)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   172
apply (auto dest: Acts_type [THEN subsetD])
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   173
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   174
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   175
lemma AllowedActs_JN [simp]:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   176
     "AllowedActs(\<Squnion>i \<in> I. F(i)) =
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   177
      (if I=0 then Pow(state*state) else (\<Inter>i \<in> I. AllowedActs(F(i))))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   178
apply (unfold JOIN_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   179
apply (rule equalityI)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   180
apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD])
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   181
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   182
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   183
lemma JN_cons [simp]: "(\<Squnion>i \<in> cons(a,I). F(i)) = F(a) Join (\<Squnion>i \<in> I. F(i))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   184
by (rule program_equalityI, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   185
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   186
lemma JN_cong [cong]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   187
    "[| I=J;  !!i. i \<in> J ==> F(i) = G(i) |] ==>
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   188
     (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   189
by (simp add: JOIN_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   190
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   191
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   192
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   193
subsection{*JN laws*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   194
lemma JN_absorb: "k \<in> I ==>F(k) Join (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> I. F(i))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   195
apply (subst JN_cons [symmetric])
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   196
apply (auto simp add: cons_absorb)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   197
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   198
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   199
lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F(i)) = ((\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> J. F(i)))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   200
apply (rule program_equalityI)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   201
apply (simp_all add: UN_Un INT_Un)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   202
apply (simp_all del: INT_simps add: INT_extend_simps, blast)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   203
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   204
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   205
lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I=0 then SKIP else programify(c))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   206
by (rule program_equalityI, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   207
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   208
lemma JN_Join_distrib:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   209
     "(\<Squnion>i \<in> I. F(i) Join G(i)) = (\<Squnion>i \<in> I. F(i))  Join  (\<Squnion>i \<in> I. G(i))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   210
apply (rule program_equalityI)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   211
apply (simp_all add: INT_Int_distrib, blast)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   212
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   213
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   214
lemma JN_Join_miniscope: "(\<Squnion>i \<in> I. F(i) Join G) = ((\<Squnion>i \<in> I. F(i) Join G))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   215
by (simp add: JN_Join_distrib JN_constant)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   216
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   217
text{*Used to prove guarantees_JN_I*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   218
lemma JN_Join_diff: "i \<in> I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   219
apply (rule program_equalityI)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   220
apply (auto elim!: not_emptyE)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   221
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   222
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   223
subsection{*Safety: co, stable, FP*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   224
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   225
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   226
(*Fails if I=0 because it collapses to SKIP \<in> A co B, i.e. to A\<subseteq>B.  So an
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   227
  alternative precondition is A\<subseteq>B, but most proofs using this rule require
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   228
  I to be nonempty for other reasons anyway.*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   229
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   230
lemma JN_constrains:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   231
 "i \<in> I==>(\<Squnion>i \<in> I. F(i)) \<in> A co B \<longleftrightarrow> (\<forall>i \<in> I. programify(F(i)) \<in> A co B)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   232
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   233
apply (unfold constrains_def JOIN_def st_set_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   234
prefer 2 apply blast
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   235
apply (rename_tac j act y z)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   236
apply (cut_tac F = "F (j) " in Acts_type)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   237
apply (drule_tac x = act in bspec, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   238
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   239
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   240
lemma Join_constrains [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   241
     "(F Join G \<in> A co B) \<longleftrightarrow> (programify(F) \<in> A co B & programify(G) \<in> A co B)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   242
by (auto simp add: constrains_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   243
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   244
lemma Join_unless [iff]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   245
     "(F Join G \<in> A unless B) \<longleftrightarrow>
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   246
    (programify(F) \<in> A unless B & programify(G) \<in> A unless B)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   247
by (simp add: Join_constrains unless_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   248
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   249
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   250
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   251
  reachable (F Join G) could be much bigger than reachable F, reachable G
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   252
*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   253
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   254
lemma Join_constrains_weaken:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   255
     "[| F \<in> A co A';  G \<in> B co B' |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   256
      ==> F Join G \<in> (A \<inter> B) co (A' \<union> B')"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   257
apply (subgoal_tac "st_set (A) & st_set (B) & F \<in> program & G \<in> program")
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   258
prefer 2 apply (blast dest: constrainsD2, simp)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   259
apply (blast intro: constrains_weaken)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   260
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   261
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   262
(*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   263
lemma JN_constrains_weaken:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   264
  assumes major: "(!!i. i \<in> I ==> F(i) \<in> A(i) co A'(i))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   265
      and minor: "i \<in> I"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   266
  shows "(\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   267
apply (cut_tac minor)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   268
apply (simp (no_asm_simp) add: JN_constrains)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   269
apply clarify
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   270
apply (rename_tac "j")
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   271
apply (frule_tac i = j in major)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   272
apply (frule constrainsD2, simp)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   273
apply (blast intro: constrains_weaken)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   274
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   275
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   276
lemma JN_stable:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   277
     "(\<Squnion>i \<in> I. F(i)) \<in>  stable(A) \<longleftrightarrow> ((\<forall>i \<in> I. programify(F(i)) \<in> stable(A)) & st_set(A))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   278
apply (auto simp add: stable_def constrains_def JOIN_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   279
apply (cut_tac F = "F (i) " in Acts_type)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   280
apply (drule_tac x = act in bspec, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   281
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   282
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   283
lemma initially_JN_I:
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   284
  assumes major: "(!!i. i \<in> I ==>F(i) \<in> initially(A))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   285
      and minor: "i \<in> I"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   286
  shows  "(\<Squnion>i \<in> I. F(i)) \<in> initially(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   287
apply (cut_tac minor)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   288
apply (auto elim!: not_emptyE simp add: Inter_iff initially_def)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   289
apply (frule_tac i = x in major)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   290
apply (auto simp add: initially_def)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   291
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   292
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   293
lemma invariant_JN_I:
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   294
  assumes major: "(!!i. i \<in> I ==> F(i) \<in> invariant(A))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   295
      and minor: "i \<in> I"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   296
  shows "(\<Squnion>i \<in> I. F(i)) \<in> invariant(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   297
apply (cut_tac minor)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   298
apply (auto intro!: initially_JN_I dest: major simp add: invariant_def JN_stable)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   299
apply (erule_tac V = "i \<in> I" in thin_rl)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   300
apply (frule major)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   301
apply (drule_tac [2] major)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   302
apply (auto simp add: invariant_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   303
apply (frule stableD2, force)+
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   304
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   305
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   306
lemma Join_stable [iff]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   307
     " (F Join G \<in> stable(A)) \<longleftrightarrow>
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   308
      (programify(F) \<in> stable(A) & programify(G) \<in>  stable(A))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   309
by (simp add: stable_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   310
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   311
lemma initially_JoinI [intro!]:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   312
     "[| F \<in> initially(A); G \<in> initially(A) |] ==> F Join G \<in> initially(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   313
by (unfold initially_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   314
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   315
lemma invariant_JoinI:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   316
     "[| F \<in> invariant(A); G \<in> invariant(A) |]
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   317
      ==> F Join G \<in> invariant(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   318
apply (subgoal_tac "F \<in> program&G \<in> program")
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   319
prefer 2 apply (blast dest: invariantD2)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   320
apply (simp add: invariant_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   321
apply (auto intro: Join_in_program)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   322
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   323
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   324
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   325
(* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   326
lemma FP_JN: "i \<in> I ==> FP(\<Squnion>i \<in> I. F(i)) = (\<Inter>i \<in> I. FP (programify(F(i))))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   327
by (auto simp add: FP_def Inter_def st_set_def JN_stable)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   328
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   329
subsection{*Progress: transient, ensures*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   330
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   331
lemma JN_transient:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   332
     "i \<in> I ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   333
      (\<Squnion>i \<in> I. F(i)) \<in> transient(A) \<longleftrightarrow> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   334
apply (auto simp add: transient_def JOIN_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   335
apply (unfold st_set_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   336
apply (drule_tac [2] x = act in bspec)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   337
apply (auto dest: Acts_type [THEN subsetD])
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   338
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   339
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   340
lemma Join_transient [iff]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   341
     "F Join G \<in> transient(A) \<longleftrightarrow>
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   342
      (programify(F) \<in> transient(A) | programify(G) \<in> transient(A))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   343
apply (auto simp add: transient_def Join_def Int_Un_distrib2)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   344
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   345
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   346
lemma Join_transient_I1: "F \<in> transient(A) ==> F Join G \<in> transient(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   347
by (simp add: Join_transient transientD2)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   348
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   349
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   350
lemma Join_transient_I2: "G \<in> transient(A) ==> F Join G \<in> transient(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   351
by (simp add: Join_transient transientD2)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   352
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   353
(*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   354
lemma JN_ensures:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   355
     "i \<in> I ==>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   356
      (\<Squnion>i \<in> I. F(i)) \<in> A ensures B \<longleftrightarrow>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   357
      ((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A \<union> B)) &
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   358
      (\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   359
by (auto simp add: ensures_def JN_constrains JN_transient)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   360
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   361
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   362
lemma Join_ensures:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   363
     "F Join G \<in> A ensures B  \<longleftrightarrow>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   364
      (programify(F) \<in> (A-B) co (A \<union> B) & programify(G) \<in> (A-B) co (A \<union> B) &
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   365
       (programify(F) \<in>  transient (A-B) | programify(G) \<in> transient (A-B)))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   366
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   367
apply (unfold ensures_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   368
apply (auto simp add: Join_transient)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   369
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   370
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   371
lemma stable_Join_constrains:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   372
    "[| F \<in> stable(A);  G \<in> A co A' |]
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   373
     ==> F Join G \<in> A co A'"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   374
apply (unfold stable_def constrains_def Join_def st_set_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   375
apply (cut_tac F = F in Acts_type)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   376
apply (cut_tac F = G in Acts_type, force)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   377
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   378
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   379
(*Premise for G cannot use Always because  F \<in> Stable A  is
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   380
   weaker than G \<in> stable A *)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   381
lemma stable_Join_Always1:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   382
     "[| F \<in> stable(A);  G \<in> invariant(A) |] ==> F Join G \<in> Always(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   383
apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ")
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   384
prefer 2 apply (blast dest: invariantD2 stableD2)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   385
apply (simp add: Always_def invariant_def initially_def Stable_eq_stable)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   386
apply (force intro: stable_Int)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   387
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   388
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   389
(*As above, but exchanging the roles of F and G*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   390
lemma stable_Join_Always2:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   391
     "[| F \<in> invariant(A);  G \<in> stable(A) |] ==> F Join G \<in> Always(A)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   392
apply (subst Join_commute)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   393
apply (blast intro: stable_Join_Always1)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   394
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   395
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   396
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   397
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   398
lemma stable_Join_ensures1:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   399
     "[| F \<in> stable(A);  G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   400
apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ")
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   401
prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD])
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   402
apply (simp (no_asm_simp) add: Join_ensures)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   403
apply (simp add: stable_def ensures_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   404
apply (erule constrains_weaken, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   405
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   406
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   407
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   408
(*As above, but exchanging the roles of F and G*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   409
lemma stable_Join_ensures2:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   410
     "[| F \<in> A ensures B;  G \<in> stable(A) |] ==> F Join G \<in> A ensures B"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   411
apply (subst Join_commute)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   412
apply (blast intro: stable_Join_ensures1)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   413
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   414
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   415
subsection{*The ok and OK relations*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   416
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   417
lemma ok_SKIP1 [iff]: "SKIP ok F"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   418
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   419
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   420
lemma ok_SKIP2 [iff]: "F ok SKIP"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   421
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   422
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   423
lemma ok_Join_commute:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   424
     "(F ok G & (F Join G) ok H) \<longleftrightarrow> (G ok H & F ok (G Join H))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   425
by (auto simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   426
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   427
lemma ok_commute: "(F ok G) \<longleftrightarrow>(G ok F)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   428
by (auto simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   429
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 35427
diff changeset
   430
lemmas ok_sym = ok_commute [THEN iffD1]
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   431
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   432
lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) \<longleftrightarrow> (F ok G & (F Join G) ok H)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   433
by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   434
                 Int_Un_distrib2 Ball_def,  safe, force+)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   435
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   436
lemma ok_Join_iff1 [iff]: "F ok (G Join H) \<longleftrightarrow> (F ok G & F ok H)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   437
by (auto simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   438
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   439
lemma ok_Join_iff2 [iff]: "(G Join H) ok F \<longleftrightarrow> (G ok F & H ok F)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   440
by (auto simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   441
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   442
(*useful?  Not with the previous two around*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   443
lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   444
by (auto simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   445
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   446
lemma ok_JN_iff1 [iff]: "F ok JOIN(I,G) \<longleftrightarrow> (\<forall>i \<in> I. F ok G(i))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   447
by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   448
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   449
lemma ok_JN_iff2 [iff]: "JOIN(I,G) ok F   \<longleftrightarrow>  (\<forall>i \<in> I. G(i) ok F)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   450
apply (auto elim!: not_emptyE simp add: ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   451
apply (blast dest: Acts_type [THEN subsetD])
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   452
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   453
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   454
lemma OK_iff_ok: "OK(I,F) \<longleftrightarrow> (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F(i) ok (F(j)))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   455
by (auto simp add: ok_def OK_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   456
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   457
lemma OK_imp_ok: "[| OK(I,F); i \<in> I; j \<in> I; i\<noteq>j|] ==> F(i) ok F(j)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   458
by (auto simp add: OK_iff_ok)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   459
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   460
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   461
lemma OK_0 [iff]: "OK(0,F)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   462
by (simp add: OK_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   463
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   464
lemma OK_cons_iff:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   465
     "OK(cons(i, I), F) \<longleftrightarrow>
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   466
      (i \<in> I & OK(I, F)) | (i\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   467
apply (simp add: OK_iff_ok)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   468
apply (blast intro: ok_sym)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   469
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   470
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14092
diff changeset
   471
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   472
subsection{*Allowed*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   473
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   474
lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   475
by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   476
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   477
lemma Allowed_Join [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   478
     "Allowed(F Join G) =
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   479
   Allowed(programify(F)) \<inter> Allowed(programify(G))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   480
apply (auto simp add: Allowed_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   481
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   482
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   483
lemma Allowed_JN [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   484
     "i \<in> I ==>
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   485
   Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   486
apply (auto simp add: Allowed_def, blast)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   487
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   488
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   489
lemma ok_iff_Allowed:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   490
     "F ok G \<longleftrightarrow> (programify(F) \<in> Allowed(programify(G)) &
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   491
   programify(G) \<in> Allowed(programify(F)))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   492
by (simp add: ok_def Allowed_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   493
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   494
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   495
lemma OK_iff_Allowed:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   496
     "OK(I,F) \<longleftrightarrow>
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   497
  (\<forall>i \<in> I. \<forall>j \<in> I-{i}. programify(F(i)) \<in> Allowed(programify(F(j))))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   498
apply (auto simp add: OK_iff_ok ok_iff_Allowed)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   499
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   500
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   501
subsection{*safety_prop, for reasoning about given instances of "ok"*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   502
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   503
lemma safety_prop_Acts_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   504
     "safety_prop(X) ==> (Acts(G) \<subseteq> cons(id(state), (\<Union>F \<in> X. Acts(F)))) \<longleftrightarrow> (programify(G) \<in> X)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   505
apply (simp (no_asm_use) add: safety_prop_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   506
apply clarify
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   507
apply (case_tac "G \<in> program", simp_all, blast, safe)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   508
prefer 2 apply force
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   509
apply (force simp add: programify_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   510
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   511
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   512
lemma safety_prop_AllowedActs_iff_Allowed:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   513
     "safety_prop(X) ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   514
  (\<Union>G \<in> X. Acts(G)) \<subseteq> AllowedActs(F) \<longleftrightarrow> (X \<subseteq> Allowed(programify(F)))"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   515
apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym]
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   516
                 safety_prop_def, blast)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   517
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   518
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   519
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   520
lemma Allowed_eq:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   521
     "safety_prop(X) ==> Allowed(mk_program(init, acts, \<Union>F \<in> X. Acts(F))) = X"
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   522
apply (subgoal_tac "cons (id (state), \<Union>(RepFun (X, Acts)) \<inter> Pow (state * state)) = \<Union>(RepFun (X, Acts))")
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   523
apply (rule_tac [2] equalityI)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   524
  apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   525
apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   526
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   527
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   528
lemma def_prg_Allowed:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   529
     "[| F == mk_program (init, acts, \<Union>F \<in> X. Acts(F)); safety_prop(X) |]
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   530
      ==> Allowed(F) = X"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   531
by (simp add: Allowed_eq)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   532
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   533
(*For safety_prop to hold, the property must be satisfiable!*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   534
lemma safety_prop_constrains [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   535
     "safety_prop(A co B) \<longleftrightarrow> (A \<subseteq> B & st_set(A))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   536
by (simp add: safety_prop_def constrains_def st_set_def, blast)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   537
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   538
(* To be used with resolution *)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   539
lemma safety_prop_constrainsI [iff]:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   540
     "[| A\<subseteq>B; st_set(A) |] ==>safety_prop(A co B)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   541
by auto
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   542
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   543
lemma safety_prop_stable [iff]: "safety_prop(stable(A)) \<longleftrightarrow> st_set(A)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   544
by (simp add: stable_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   545
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   546
lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   547
by auto
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   548
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   549
lemma safety_prop_Int [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   550
     "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X \<inter> Y)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   551
apply (simp add: safety_prop_def, safe, blast)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   552
apply (drule_tac [2] B = "\<Union>(RepFun (X \<inter> Y, Acts))" and C = "\<Union>(RepFun (Y, Acts))" in subset_trans)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   553
apply (drule_tac B = "\<Union>(RepFun (X \<inter> Y, Acts))" and C = "\<Union>(RepFun (X, Acts))" in subset_trans)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   554
apply blast+
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   555
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   556
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   557
(* If I=0 the conclusion becomes safety_prop(0) which is false *)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   558
lemma safety_prop_Inter:
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   559
  assumes major: "(!!i. i \<in> I ==>safety_prop(X(i)))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   560
      and minor: "i \<in> I"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   561
  shows "safety_prop(\<Inter>i \<in> I. X(i))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   562
apply (simp add: safety_prop_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   563
apply (cut_tac minor, safe)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   564
apply (simp (no_asm_use) add: Inter_iff)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   565
apply clarify
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   566
apply (frule major)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   567
apply (drule_tac [2] i = xa in major)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   568
apply (frule_tac [4] i = xa in major)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   569
apply (auto simp add: safety_prop_def)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   570
apply (drule_tac B = "\<Union>(RepFun (\<Inter>(RepFun (I, X)), Acts))" and C = "\<Union>(RepFun (X (xa), Acts))" in subset_trans)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   571
apply blast+
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   572
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   573
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   574
lemma def_UNION_ok_iff:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   575
"[| F == mk_program(init,acts, \<Union>G \<in> X. Acts(G)); safety_prop(X) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   576
      ==> F ok G \<longleftrightarrow> (programify(G) \<in> X & acts \<inter> Pow(state*state) \<subseteq> AllowedActs(G))"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   577
apply (unfold ok_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   578
apply (drule_tac G = G in safety_prop_Acts_iff)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   579
apply (cut_tac F = G in AllowedActs_type)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   580
apply (cut_tac F = G in Acts_type, auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   581
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
   582
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   583
end