src/HOL/UNITY/Transformers.thy
author haftmann
Tue, 09 Aug 2011 20:24:48 +0200
changeset 44106 0e018cbcc0de
parent 37936 1e4c5015a72e
child 44890 22f665a2e91c
permissions -rw-r--r--
tuned proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 35416
diff changeset
     1
(*  Title:      HOL/UNITY/Transformers.thy
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
     3
    Copyright   2003  University of Cambridge
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
     4
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
     5
Predicate Transformers.  From 
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
     6
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
     7
    David Meier and Beverly Sanders,
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
     8
    Composing Leads-to Properties
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
     9
    Theoretical Computer Science 243:1-2 (2000), 339-361.
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
    10
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
    11
    David Meier,
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
    12
    Progress Properties in Program Refinement and Parallel Composition
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
    13
    Swiss Federal Institute of Technology Zurich (1997)
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    14
*)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    15
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    16
header{*Predicate Transformers*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    17
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15236
diff changeset
    18
theory Transformers imports Comp begin
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    19
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    20
subsection{*Defining the Predicate Transformers @{term wp},
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    21
   @{term awp} and  @{term wens}*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    22
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32693
diff changeset
    23
definition wp :: "[('a*'a) set, 'a set] => 'a set" where  
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    24
    --{*Dijkstra's weakest-precondition operator (for an individual command)*}
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    25
    "wp act B == - (act^-1 `` (-B))"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    26
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32693
diff changeset
    27
definition awp :: "['a program, 'a set] => 'a set" where
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    28
    --{*Dijkstra's weakest-precondition operator (for a program)*}
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    29
    "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    30
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32693
diff changeset
    31
definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    32
    --{*The weakest-ensures transformer*}
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    33
    "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    34
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    35
text{*The fundamental theorem for wp*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    36
theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    37
by (force simp add: wp_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    38
13874
0da2141606c6 More on progress sets
paulson
parents: 13866
diff changeset
    39
text{*This lemma is a good deal more intuitive than the definition!*}
0da2141606c6 More on progress sets
paulson
parents: 13866
diff changeset
    40
lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
0da2141606c6 More on progress sets
paulson
parents: 13866
diff changeset
    41
by (simp add: wp_def, blast)
0da2141606c6 More on progress sets
paulson
parents: 13866
diff changeset
    42
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    43
lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    44
by (force simp add: wp_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    45
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    46
lemma wp_empty [simp]: "wp act {} = - (Domain act)"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    47
by (force simp add: wp_def)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    48
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    49
text{*The identity relation is the skip action*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    50
lemma wp_Id [simp]: "wp Id B = B"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    51
by (simp add: wp_def) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    52
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
    53
lemma wp_totalize_act:
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
    54
     "wp (totalize_act act) B = (wp act B \<inter> Domain act) \<union> (B - Domain act)"
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
    55
by (simp add: wp_def totalize_act_def, blast)
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
    56
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    57
lemma awp_subset: "(awp F A \<subseteq> A)"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    58
by (force simp add: awp_def wp_def)
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    59
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    60
lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    61
by (simp add: awp_def wp_def, blast) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    62
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    63
text{*The fundamental theorem for awp*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    64
theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)"
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    65
by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    66
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    67
lemma awp_iff_stable: "(A \<subseteq> awp F A) = (F \<in> stable A)"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    68
by (simp add: awp_iff_constrains stable_def) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    69
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    70
lemma stable_imp_awp_ident: "F \<in> stable A ==> awp F A = A"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    71
apply (rule equalityI [OF awp_subset]) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    72
apply (simp add: awp_iff_stable) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    73
done
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    74
13874
0da2141606c6 More on progress sets
paulson
parents: 13866
diff changeset
    75
lemma wp_mono: "(A \<subseteq> B) ==> wp act A \<subseteq> wp act B"
0da2141606c6 More on progress sets
paulson
parents: 13866
diff changeset
    76
by (simp add: wp_def, blast)
0da2141606c6 More on progress sets
paulson
parents: 13866
diff changeset
    77
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    78
lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    79
by (simp add: awp_def wp_def, blast)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    80
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    81
lemma wens_unfold:
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    82
     "wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    83
apply (simp add: wens_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    84
apply (rule gfp_unfold) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    85
apply (simp add: mono_def wp_def awp_def, blast) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    86
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    87
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    88
lemma wens_Id [simp]: "wens F Id B = B"
32587
caa5ada96a00 Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents: 30971
diff changeset
    89
by (simp add: wens_def gfp_def wp_def awp_def, blast)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
    90
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    91
text{*These two theorems justify the claim that @{term wens} returns the
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    92
weakest assertion satisfying the ensures property*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    93
lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    94
apply (simp add: wens_def ensures_def transient_def, clarify) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    95
apply (rule rev_bexI, assumption) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    96
apply (rule gfp_upperbound)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    97
apply (simp add: constrains_def awp_def wp_def, blast)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    98
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
    99
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   100
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   101
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
32587
caa5ada96a00 Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents: 30971
diff changeset
   102
              ensures_def transient_def, blast)
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   103
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   104
text{*These two results constitute assertion (4.13) of the thesis*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   105
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   106
apply (simp add: wens_def wp_def awp_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   107
apply (rule gfp_mono, blast) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   108
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   109
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   110
lemma wens_weakening: "B \<subseteq> wens F act B"
32587
caa5ada96a00 Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents: 30971
diff changeset
   111
by (simp add: wens_def gfp_def, blast)
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   112
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   113
text{*Assertion (6), or 4.16 in the thesis*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   114
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   115
apply (simp add: wens_def wp_def awp_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   116
apply (rule gfp_upperbound, blast) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   117
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   118
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   119
text{*Assertion 4.17 in the thesis*}
21312
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 21026
diff changeset
   120
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
32587
caa5ada96a00 Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents: 30971
diff changeset
   121
by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13874
diff changeset
   122
  --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13874
diff changeset
   123
      is declared as an iff-rule, then it's almost impossible to prove. 
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13874
diff changeset
   124
      One proof is via @{text meson} after expanding all definitions, but it's
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13874
diff changeset
   125
      slow!*}
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   126
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   127
text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   128
hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   129
lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   130
apply (simp add: stable_def)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   131
apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   132
apply (simp add: Un_Int_distrib2 Compl_partition2) 
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   133
apply (erule constrains_weaken, blast) 
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32587
diff changeset
   134
apply (simp add: wens_weakening)
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   135
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   136
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   137
text{*Assertion 4.20 in the thesis.*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   138
lemma wens_Int_eq_lemma:
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   139
      "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   140
       ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   141
apply (rule subset_wens) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   142
apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   143
apply (simp add: wp_def awp_def, blast)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   144
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   145
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   146
text{*Assertion (8): 4.21 in the thesis. Here we indeed require
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   147
      @{term "act \<in> Acts F"}*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   148
lemma wens_Int_eq:
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   149
      "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   150
       ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   151
apply (rule equalityI)
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32587
diff changeset
   152
 apply (simp_all add: Int_lower1) 
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   153
 apply (rule wens_Int_eq_lemma, assumption+) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   154
apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   155
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   156
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   157
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   158
subsection{*Defining the Weakest Ensures Set*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   159
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 21733
diff changeset
   160
inductive_set
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   161
  wens_set :: "['a program, 'a set] => 'a set set"
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 21733
diff changeset
   162
  for F :: "'a program" and B :: "'a set"
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 21733
diff changeset
   163
where
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   164
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   165
  Basis: "B \<in> wens_set F B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   166
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 21733
diff changeset
   167
| Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   168
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 21733
diff changeset
   169
| Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   170
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   171
lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   172
apply (erule wens_set.induct) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   173
  apply (simp add: constrains_def)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   174
 apply (drule_tac act1=act and A1=X 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   175
        in constrains_Un [OF Diff_wens_constrains]) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   176
 apply (erule constrains_weaken, blast) 
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32587
diff changeset
   177
 apply (simp add: wens_weakening) 
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   178
apply (rule constrains_weaken) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   179
apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   180
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   181
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   182
lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   183
apply (erule wens_set.induct)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   184
  apply (rule leadsTo_refl)  
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   185
 apply (blast intro: wens_ensures leadsTo_Trans) 
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   186
apply (blast intro: leadsTo_Union) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   187
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   188
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   189
lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   190
apply (erule leadsTo_induct_pre)
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   191
  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   192
 apply (clarify, drule ensures_weaken_R, assumption)  
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   193
 apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   194
apply (case_tac "S={}") 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   195
 apply (simp, blast intro: wens_set.Basis)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   196
apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   197
apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   198
apply (blast intro: wens_set.Union) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   199
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   200
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   201
text{*Assertion (9): 4.27 in the thesis.*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   202
lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   203
by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   204
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   205
text{*This is the result that requires the definition of @{term wens_set} to
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   206
  require @{term W} to be non-empty in the Unio case, for otherwise we should
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   207
  always have @{term "{} \<in> wens_set F B"}.*}
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   208
lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   209
apply (erule wens_set.induct) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   210
  apply (blast intro: wens_weakening [THEN subsetD])+
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   211
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   212
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   213
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   214
subsection{*Properties Involving Program Union*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   215
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   216
text{*Assertion (4.30) of thesis, reoriented*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   217
lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   218
by (simp add: awp_def wp_def, blast)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   219
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   220
lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   221
by (subst wens_unfold, fast) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   222
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   223
text{*Assertion (4.31)*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   224
lemma subset_wens_Join:
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   225
      "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   226
       ==> A \<subseteq> wens (F\<squnion>G) act B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   227
apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   228
                    wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   229
 apply (rule subset_wens) 
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32587
diff changeset
   230
 apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   231
 apply (simp add: awp_def wp_def, blast) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   232
apply (insert wens_subset [of F act B], blast) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   233
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   234
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   235
text{*Assertion (4.32)*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   236
lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   237
apply (simp add: wens_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   238
apply (rule gfp_mono)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   239
apply (auto simp add: awp_Join_eq)  
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   240
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   241
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   242
text{*Lemma, because the inductive step is just too messy.*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   243
lemma wens_Union_inductive_step:
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   244
  assumes awpF: "T-B \<subseteq> awp F T"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   245
      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   246
  shows "[|X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y|]
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   247
         ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and>
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   248
             T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   249
apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X")  
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   250
 prefer 2
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   251
 apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   252
apply (rule equalityI) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   253
 prefer 2 apply blast
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32587
diff changeset
   254
apply (simp add: Int_lower1) 
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   255
apply (frule wens_set_imp_subset) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   256
apply (subgoal_tac "T-X \<subseteq> awp F T")  
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   257
 prefer 2 apply (blast intro: awpF [THEN subsetD]) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   258
apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   259
 prefer 2 apply (blast intro!: wens_mono)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   260
apply (subst wens_Int_eq, assumption+) 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   261
apply (rule subset_wens_Join [of _ T], simp, blast)
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   262
apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   263
 prefer 2
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   264
 apply (subst wens_Int_eq [symmetric], assumption+) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   265
 apply (blast intro: wens_weakening [THEN subsetD], simp) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   266
apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   267
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   268
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   269
theorem wens_Union:
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   270
  assumes awpF: "T-B \<subseteq> awp F T"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   271
      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   272
      and major: "X \<in> wens_set F B"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   273
  shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   274
apply (rule wens_set.induct [OF major])
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   275
  txt{*Basis: trivial*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   276
  apply (blast intro: wens_set.Basis)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   277
 txt{*Inductive step*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   278
 apply clarify 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   279
 apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   280
  apply (force intro: wens_set.Wens)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   281
 apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   282
txt{*Union: by Axiom of Choice*}
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   283
apply (simp add: ball_conj_distrib Bex_def) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   284
apply (clarify dest!: bchoice) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   285
apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   286
apply (blast intro: wens_set.Union) 
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   287
done
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   288
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   289
theorem leadsTo_Join:
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   290
  assumes leadsTo: "F \<in> A leadsTo B"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   291
      and awpF: "T-B \<subseteq> awp F T"
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   292
      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   293
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   294
apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   295
apply (rule wens_Union [THEN bexE]) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   296
   apply (rule awpF) 
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   297
  apply (erule awpG, assumption)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   298
apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L])  
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   299
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   300
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   301
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   302
subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   303
text{*Thesis Section 4.3.3*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   304
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   305
text{*We start by proving laws about single-assignment programs*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   306
lemma awp_single_eq [simp]:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   307
     "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   308
by (force simp add: awp_def wp_def) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   309
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   310
lemma wp_Un_subset: "wp act A \<union> wp act B \<subseteq> wp act (A \<union> B)"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   311
by (force simp add: wp_def)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   312
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   313
lemma wp_Un_eq: "single_valued act ==> wp act (A \<union> B) = wp act A \<union> wp act B"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   314
apply (rule equalityI)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   315
 apply (force simp add: wp_def single_valued_def) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   316
apply (rule wp_Un_subset) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   317
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   318
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   319
lemma wp_UN_subset: "(\<Union>i\<in>I. wp act (A i)) \<subseteq> wp act (\<Union>i\<in>I. A i)"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   320
by (force simp add: wp_def)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   321
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   322
lemma wp_UN_eq:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   323
     "[|single_valued act; I\<noteq>{}|]
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   324
      ==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   325
apply (rule equalityI)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   326
 prefer 2 apply (rule wp_UN_subset) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   327
 apply (simp add: wp_def Image_INT_eq) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   328
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   329
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   330
lemma wens_single_eq:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   331
     "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
32587
caa5ada96a00 Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents: 30971
diff changeset
   332
by (simp add: wens_def gfp_def wp_def, blast)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   333
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   334
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   335
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   336
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32693
diff changeset
   337
definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where  
30971
7fbebf75b3ef funpow and relpow with shared "^^" syntax
haftmann
parents: 30952
diff changeset
   338
    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B"
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   339
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32693
diff changeset
   340
definition wens_single :: "[('a*'a) set, 'a set] => 'a set" where
30971
7fbebf75b3ef funpow and relpow with shared "^^" syntax
haftmann
parents: 30952
diff changeset
   341
    "wens_single act B == \<Union>i. (wp act ^^ i) B"
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   342
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   343
lemma wens_single_Un_eq:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   344
      "single_valued act
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   345
       ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   346
apply (rule equalityI)
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32587
diff changeset
   347
 apply (simp_all add: Un_upper1) 
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   348
apply (simp add: wens_single_def wp_UN_eq, clarify) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   349
apply (rule_tac a="Suc(i)" in UN_I, auto) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   350
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   351
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   352
lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   353
by force
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   354
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   355
lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B"
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   356
by (simp add: wens_single_finite_def)
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   357
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   358
lemma wens_single_finite_Suc:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   359
      "single_valued act
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   360
       ==> wens_single_finite act B (Suc k) =
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   361
           wens_single_finite act B k \<union> wp act (wens_single_finite act B k)"
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   362
apply (simp add: wens_single_finite_def image_def 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   363
                 wp_UN_eq [OF _ atMost_nat_nonempty]) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   364
apply (force elim!: le_SucE)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   365
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   366
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   367
lemma wens_single_finite_Suc_eq_wens:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   368
     "single_valued act
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   369
       ==> wens_single_finite act B (Suc k) =
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   370
           wens (mk_program (init, {act}, allowed)) act 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   371
                (wens_single_finite act B k)"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   372
by (simp add: wens_single_finite_Suc wens_single_eq) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   373
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   374
lemma def_wens_single_finite_Suc_eq_wens:
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   375
     "[|F = mk_program (init, {act}, allowed); single_valued act|]
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   376
       ==> wens_single_finite act B (Suc k) =
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   377
           wens F act (wens_single_finite act B k)"
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   378
by (simp add: wens_single_finite_Suc_eq_wens) 
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   379
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   380
lemma wens_single_finite_Un_eq:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   381
      "single_valued act
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   382
       ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   383
           \<in> range (wens_single_finite act B)"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   384
by (simp add: wens_single_finite_Suc [symmetric]) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   385
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   386
lemma wens_single_eq_Union:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   387
      "wens_single act B = \<Union>range (wens_single_finite act B)" 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   388
by (simp add: wens_single_finite_def wens_single_def, blast) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   389
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   390
lemma wens_single_finite_eq_Union:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   391
     "wens_single_finite act B n = (\<Union>k\<in>atMost n. wens_single_finite act B k)"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   392
apply (auto simp add: wens_single_finite_def) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   393
apply (blast intro: le_trans) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   394
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   395
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   396
lemma wens_single_finite_mono:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   397
     "m \<le> n ==> wens_single_finite act B m \<subseteq> wens_single_finite act B n"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   398
by (force simp add:  wens_single_finite_eq_Union [of act B n]) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   399
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   400
lemma wens_single_finite_subset_wens_single:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   401
      "wens_single_finite act B k \<subseteq> wens_single act B"
15236
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   402
by (simp add: wens_single_eq_Union, blast)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   403
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   404
lemma subset_wens_single_finite:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   405
      "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   406
       ==> \<exists>m. \<Union>W = wens_single_finite act B m"
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   407
apply (induct k)
15236
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   408
 apply (rule_tac x=0 in exI, simp, blast)
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   409
apply (auto simp add: atMost_Suc)
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   410
apply (case_tac "wens_single_finite act B (Suc k) \<in> W")
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   411
 prefer 2 apply blast
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   412
apply (drule_tac x="Suc k" in spec)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   413
apply (erule notE, rule equalityI)
15236
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   414
 prefer 2 apply blast
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   415
apply (subst wens_single_finite_eq_Union)
f289e8ba2bb3 Proofs needed to be updated because induction now preserves name of
nipkow
parents: 15102
diff changeset
   416
apply (simp add: atMost_Suc, blast)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   417
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   418
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   419
text{*lemma for Union case*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   420
lemma Union_eq_wens_single:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   421
      "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   422
        W \<subseteq> insert (wens_single act B)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   423
            (range (wens_single_finite act B))\<rbrakk>
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   424
       \<Longrightarrow> \<Union>W = wens_single act B"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   425
apply (case_tac "wens_single act B \<in> W")
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   426
 apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   427
apply (simp add: wens_single_eq_Union) 
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   428
apply (rule equalityI, blast) 
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   429
apply (simp add: UN_subset_iff, clarify)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   430
apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n")  
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   431
 apply (blast intro: wens_single_finite_mono [THEN subsetD]) 
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   432
apply (drule_tac x=i in spec)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   433
apply (force simp add: atMost_def)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   434
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   435
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   436
lemma wens_set_subset_single:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   437
      "single_valued act
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   438
       ==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq> 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   439
           insert (wens_single act B) (range (wens_single_finite act B))"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   440
apply (rule subsetI)  
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   441
apply (erule wens_set.induct)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   442
  txt{*Basis*} 
21733
131dd2a27137 Modified lattice locale
nipkow
parents: 21312
diff changeset
   443
  apply (fastsimp simp add: wens_single_finite_def)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   444
 txt{*Wens inductive step*}
21733
131dd2a27137 Modified lattice locale
nipkow
parents: 21312
diff changeset
   445
 apply (case_tac "acta = Id", simp)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   446
 apply (simp add: wens_single_eq)
21733
131dd2a27137 Modified lattice locale
nipkow
parents: 21312
diff changeset
   447
 apply (elim disjE)
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   448
 apply (simp add: wens_single_Un_eq)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   449
 apply (force simp add: wens_single_finite_Un_eq)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   450
txt{*Union inductive step*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   451
apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   452
 apply (blast dest!: subset_wens_single_finite, simp) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   453
apply (rule disjI1 [OF Union_eq_wens_single], blast+)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   454
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   455
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   456
lemma wens_single_finite_in_wens_set:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   457
      "single_valued act \<Longrightarrow>
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   458
         wens_single_finite act B k
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   459
         \<in> wens_set (mk_program (init, {act}, allowed)) B"
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   460
apply (induct_tac k) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   461
 apply (simp add: wens_single_finite_def wens_set.Basis)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   462
apply (simp add: wens_set.Wens
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   463
                 wens_single_finite_Suc_eq_wens [of act B _ init allowed]) 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   464
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   465
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   466
lemma single_subset_wens_set:
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   467
      "single_valued act
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   468
       ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   469
           wens_set (mk_program (init, {act}, allowed)) B"
44106
0e018cbcc0de tuned proofs
haftmann
parents: 37936
diff changeset
   470
apply (simp add: SUP_def image_def wens_single_eq_Union) 
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   471
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   472
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   473
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   474
text{*Theorem (4.29)*}
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   475
theorem wens_set_single_eq:
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   476
     "[|F = mk_program (init, {act}, allowed); single_valued act|]
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   477
      ==> wens_set F B =
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   478
          insert (wens_single act B) (range (wens_single_finite act B))"
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   479
apply (rule equalityI)
13851
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   480
 apply (simp add: wens_set_subset_single) 
f6923453953a new UNITY examples theory
paulson
parents: 13832
diff changeset
   481
apply (erule ssubst, erule single_subset_wens_set) 
13832
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   482
done
e7649436869c completed proofs for programs consisting of a single assignment
paulson
parents: 13821
diff changeset
   483
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   484
text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   485
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   486
lemma fp_leadsTo_Join:
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   487
    "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   488
apply (rule leadsTo_Join, assumption, blast)
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   489
apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast) 
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   490
done
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   491
13821
0fd39aa77095 new theory Transformers: Meier-Sanders non-interference theory
paulson
parents:
diff changeset
   492
end