src/HOL/UNITY/ProgressSets.thy
author haftmann
Sun, 16 Mar 2014 18:09:04 +0100
changeset 56166 9a241bc276cd
parent 51488 3c886fe611b8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
normalising simp rules for compound operators
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
     1
(*  Title:      HOL/UNITY/ProgressSets.thy
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     3
    Copyright   2003  University of Cambridge
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     4
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     5
Progress Sets.  From 
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     6
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     7
    David Meier and Beverly Sanders,
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     8
    Composing Leads-to Properties
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
     9
    Theoretical Computer Science 243:1-2 (2000), 339-361.
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    10
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    11
    David Meier,
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    12
    Progress Properties in Program Refinement and Parallel Composition
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    13
    Swiss Federal Institute of Technology Zurich (1997)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    14
*)
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    15
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    16
header{*Progress Sets*}
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    17
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15102
diff changeset
    18
theory ProgressSets imports Transformers begin
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    19
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
    20
subsection {*Complete Lattices and the Operator @{term cl}*}
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
    21
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    22
definition lattice :: "'a set set => bool" where
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    23
   --{*Meier calls them closure sets, but they are just complete lattices*}
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    24
   "lattice L ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
    25
         (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    26
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    27
definition cl :: "['a set set, 'a set] => 'a set" where
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    28
   --{*short for ``closure''*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    29
   "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    30
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    31
lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    32
by (force simp add: lattice_def)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    33
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    34
lemma empty_in_lattice: "lattice L ==> {} \<in> L"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    35
by (force simp add: lattice_def)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    36
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    37
lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    38
by (simp add: lattice_def)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    39
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    40
lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    41
by (simp add: lattice_def)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    42
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    43
lemma UN_in_lattice:
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    44
     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
44106
0e018cbcc0de tuned proofs
haftmann
parents: 35416
diff changeset
    45
apply (unfold SUP_def)
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    46
apply (blast intro: Union_in_lattice) 
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    47
done
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    48
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    49
lemma INT_in_lattice:
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    50
     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
44106
0e018cbcc0de tuned proofs
haftmann
parents: 35416
diff changeset
    51
apply (unfold INF_def)
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    52
apply (blast intro: Inter_in_lattice) 
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    53
done
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    54
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    55
lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
44106
0e018cbcc0de tuned proofs
haftmann
parents: 35416
diff changeset
    56
  using Union_in_lattice [of "{x, y}" L] by simp
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    57
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    58
lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
44106
0e018cbcc0de tuned proofs
haftmann
parents: 35416
diff changeset
    59
  using Inter_in_lattice [of "{x, y}" L] by simp
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    60
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    61
lemma lattice_stable: "lattice {X. F \<in> stable X}"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    62
by (simp add: lattice_def stable_def constrains_def, blast)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    63
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    64
text{*The next three results state that @{term "cl L r"} is the minimal
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    65
 element of @{term L} that includes @{term r}.*}
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    66
lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    67
apply (simp add: lattice_def cl_def)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    68
apply (erule conjE)  
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    69
apply (drule spec, erule mp, blast) 
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    70
done
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    71
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    72
lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    73
by (force simp add: cl_def)
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    74
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    75
text{*The next three lemmas constitute assertion (4.61)*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    76
lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    77
by (simp add: cl_def, blast)
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    78
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    79
lemma subset_cl: "r \<subseteq> cl L r"
44918
6a80fbc4e72c tune simpset for Complete_Lattices
noschinl
parents: 44106
diff changeset
    80
by (simp add: cl_def le_Inf_iff)
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    81
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    82
text{*A reformulation of @{thm subset_cl}*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    83
lemma clI: "x \<in> r ==> x \<in> cl L r"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    84
by (simp add: cl_def, blast)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    85
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    86
text{*A reformulation of @{thm cl_least}*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    87
lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    88
by (force simp add: cl_def)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
    89
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    90
lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    91
by (simp add: cl_def, blast)
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
    92
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    93
lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    94
apply (rule equalityI) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    95
 prefer 2 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    96
  apply (simp add: cl_def, blast)
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    97
apply (rule cl_least)
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    98
 apply (blast intro: Un_in_lattice cl_in_lattice)
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
    99
apply (blast intro: subset_cl [THEN subsetD])  
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   100
done
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   101
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   102
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   103
apply (rule equalityI) 
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   104
 prefer 2 apply (simp add: cl_def, blast)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   105
apply (rule cl_least)
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   106
 apply (blast intro: UN_in_lattice cl_in_lattice)
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   107
apply (blast intro: subset_cl [THEN subsetD])  
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   108
done
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   109
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   110
lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   111
by (simp add: cl_def, blast)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   112
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   113
lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   114
by (simp add: cl_def, blast)
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   115
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   116
lemma cl_ident: "r\<in>L ==> cl L r = r" 
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   117
by (force simp add: cl_def)
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   118
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   119
lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   120
by (simp add: cl_ident empty_in_lattice)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   121
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   122
lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   123
by (simp add: cl_ident UNIV_in_lattice)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   124
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   125
text{*Assertion (4.62)*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   126
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   127
apply (rule iffI) 
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   128
 apply (erule subst)
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   129
 apply (erule cl_in_lattice)  
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   130
apply (erule cl_ident) 
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   131
done
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   132
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   133
lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   134
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   135
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   136
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   137
subsection {*Progress Sets and the Main Lemma*}
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   138
text{*A progress set satisfies certain closure conditions and is a 
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   139
simple way of including the set @{term "wens_set F B"}.*}
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   140
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   141
definition closed :: "['a program, 'a set, 'a set,  'a set set] => bool" where
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   142
   "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   143
                              T \<inter> (B \<union> wp act M) \<in> L"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   144
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   145
definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   146
   "progress_set F T B ==
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   147
      {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   148
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   149
lemma closedD:
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   150
   "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
14150
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13888
diff changeset
   151
    ==> T \<inter> (B \<union> wp act M) \<in> L" 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   152
by (simp add: closed_def) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   153
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   154
text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   155
and @{term m} by @{term X}. *}
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   156
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   157
text{*Part of the proof of the claim at the bottom of page 97.  It's
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   158
proved separately because the argument requires a generalization over
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   159
all @{term "act \<in> Acts F"}.*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   160
lemma lattice_awp_lemma:
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   161
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   162
      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   163
      and latt: "lattice C"
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   164
      and TC:   "T \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   165
      and BC:   "B \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   166
      and clos: "closed F T B C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   167
    shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   168
apply (simp del: INT_simps add: awp_def INT_extend_simps) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   169
apply (rule INT_in_lattice [OF latt]) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   170
apply (erule closedD [OF clos]) 
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   171
apply (simp add: subset_trans [OF BsubX Un_upper1]) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   172
apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   173
 prefer 2 apply (blast intro: TC clD) 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   174
apply (erule ssubst) 
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   175
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   176
done
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   177
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   178
text{*Remainder of the proof of the claim at the bottom of page 97.*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   179
lemma lattice_lemma:
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   180
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   181
      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   182
      and act:  "act \<in> Acts F"
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   183
      and latt: "lattice C"
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   184
      and TC:   "T \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   185
      and BC:   "B \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   186
      and clos: "closed F T B C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   187
    shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   188
apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   189
 prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   190
apply (drule Int_in_lattice
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   191
              [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   192
                    latt])
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   193
apply (subgoal_tac
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   194
         "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   195
          T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   196
 prefer 2 apply blast 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   197
apply simp  
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   198
apply (drule Un_in_lattice [OF _ TXC latt])  
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   199
apply (subgoal_tac
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   200
         "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   201
          T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   202
 apply simp 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   203
apply (blast intro: BsubX [THEN subsetD]) 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   204
done
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   205
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   206
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   207
text{*Induction step for the main lemma*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   208
lemma progress_induction_step:
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   209
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   210
      and act:  "act \<in> Acts F"
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   211
      and Xwens: "X \<in> wens_set F B"
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   212
      and latt: "lattice C"
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   213
      and  TC:  "T \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   214
      and  BC:  "B \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   215
      and clos: "closed F T B C"
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   216
      and Fstable: "F \<in> stable T"
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   217
  shows "T \<inter> wens F act X \<in> C"
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   218
proof -
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   219
  from Xwens have BsubX: "B \<subseteq> X"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   220
    by (rule wens_set_imp_subset) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   221
  let ?r = "wens F act X"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   222
  have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   223
    by (simp add: wens_unfold [symmetric])
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   224
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   225
    by blast
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   226
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   227
    by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   228
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   229
    by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   230
  then have "cl C (T\<inter>?r) \<subseteq> 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   231
             cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   232
    by (rule cl_mono) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   233
  then have "cl C (T\<inter>?r) \<subseteq> 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   234
             T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   235
    by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   236
  then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   237
    by blast
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   238
  then have "cl C (T\<inter>?r) \<subseteq> ?r"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   239
    by (blast intro!: subset_wens) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   240
  then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32604
diff changeset
   241
    by (simp add: cl_ident TC
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   242
                  subset_trans [OF cl_mono [OF Int_lower1]]) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   243
  show ?thesis
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   244
    by (rule cl_subset_in_lattice [OF cl_subset latt]) 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   245
qed
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   246
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   247
text{*Proved on page 96 of Meier's thesis.  The special case when
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   248
   @{term "T=UNIV"} states that every progress set for the program @{term F}
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   249
   and set @{term B} includes the set @{term "wens_set F B"}.*}
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   250
lemma progress_set_lemma:
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   251
     "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   252
apply (simp add: progress_set_def, clarify) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   253
apply (erule wens_set.induct) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   254
  txt{*Base*}
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   255
  apply (simp add: Int_in_lattice) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   256
 txt{*The difficult @{term wens} case*}
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   257
 apply (simp add: progress_induction_step) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   258
txt{*Disjunctive case*}
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   259
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 51488
diff changeset
   260
 apply simp 
13861
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   261
apply (blast intro: UN_in_lattice) 
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   262
done
0c18f31d901a Proved the main lemma on progress sets
paulson
parents: 13853
diff changeset
   263
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   264
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   265
subsection {*The Progress Set Union Theorem*}
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   266
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   267
lemma closed_mono:
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   268
  assumes BB':  "B \<subseteq> B'"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   269
      and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   270
      and B'C:  "B' \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   271
      and TC:   "T \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   272
      and latt: "lattice C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   273
  shows "T \<inter> (B' \<union> wp act M) \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   274
proof -
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   275
  from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   276
    by (simp add: Int_Un_distrib)
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   277
  then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   278
    by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   279
  show ?thesis
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   280
    by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   281
        blast intro: BB' [THEN subsetD]) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   282
qed
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   283
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   284
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   285
lemma progress_set_mono:
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   286
    assumes BB':  "B \<subseteq> B'"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   287
    shows
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   288
     "[| B' \<in> C;  C \<in> progress_set F T B|] 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   289
      ==> C \<in> progress_set F T B'"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   290
by (simp add: progress_set_def closed_def closed_mono [OF BB'] 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   291
                 subset_trans [OF BB']) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   292
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   293
theorem progress_set_Union:
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   294
  assumes leadsTo: "F \<in> A leadsTo B'"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   295
      and prog: "C \<in> progress_set F T B"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   296
      and Fstable: "F \<in> stable T"
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   297
      and BB':  "B \<subseteq> B'"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   298
      and B'C:  "B' \<in> C"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   299
      and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   300
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   301
apply (insert prog Fstable) 
13866
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   302
apply (rule leadsTo_Join [OF leadsTo]) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   303
  apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   304
apply (simp add: awp_iff_constrains)
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   305
apply (drule progress_set_mono [OF BB' B'C]) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   306
apply (blast intro: progress_set_lemma Gco constrains_weaken_L 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   307
                    BB' [THEN subsetD]) 
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   308
done
b42d7983a822 More "progress set" material
paulson
parents: 13861
diff changeset
   309
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   310
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   311
subsection {*Some Progress Sets*}
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   312
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   313
lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   314
by (simp add: progress_set_def lattice_def closed_def)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents: 13866
diff changeset
   315
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   316
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   317
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   318
subsubsection {*Lattices and Relations*}
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   319
text{*From Meier's thesis, section 4.5.3*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   320
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   321
definition relcl :: "'a set set => ('a * 'a) set" where
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   322
    -- {*Derived relation from a lattice*}
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   323
    "relcl L == {(x,y). y \<in> cl L {x}}"
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   324
  
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   325
definition latticeof :: "('a * 'a) set => 'a set set" where
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   326
    -- {*Derived lattice from a relation: the set of upwards-closed sets*}
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   327
    "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   328
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   329
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   330
lemma relcl_refl: "(a,a) \<in> relcl L"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   331
by (simp add: relcl_def subset_cl [THEN subsetD])
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   332
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   333
lemma relcl_trans:
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   334
     "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   335
apply (simp add: relcl_def)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   336
apply (blast intro: clD cl_in_lattice)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   337
done
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   338
30198
922f944f03b2 name changes
nipkow
parents: 23767
diff changeset
   339
lemma refl_relcl: "lattice L ==> refl (relcl L)"
922f944f03b2 name changes
nipkow
parents: 23767
diff changeset
   340
by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   341
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   342
lemma trans_relcl: "lattice L ==> trans (relcl L)"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   343
by (blast intro: relcl_trans transI)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   344
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   345
lemma lattice_latticeof: "lattice (latticeof r)"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   346
by (auto simp add: lattice_def latticeof_def)
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   347
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   348
lemma lattice_singletonI:
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   349
     "[|lattice L; !!s. s \<in> X ==> {s} \<in> L|] ==> X \<in> L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   350
apply (cut_tac UN_singleton [of X]) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   351
apply (erule subst) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   352
apply (simp only: UN_in_lattice) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   353
done
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   354
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   355
text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   356
lemma cl_latticeof:
30198
922f944f03b2 name changes
nipkow
parents: 23767
diff changeset
   357
     "[|refl r; trans r|] 
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   358
      ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   359
apply (rule equalityI) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   360
 apply (rule cl_least) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   361
  apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
30198
922f944f03b2 name changes
nipkow
parents: 23767
diff changeset
   362
 apply (simp add: latticeof_def refl_on_def, blast)
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   363
apply (simp add: latticeof_def, clarify)
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   364
apply (unfold cl_def, blast) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   365
done
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   366
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   367
text{*Related to (4.71).*}
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   368
lemma cl_eq_Collect_relcl:
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   369
     "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" 
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   370
apply (cut_tac UN_singleton [of X]) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   371
apply (erule subst) 
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   372
apply (force simp only: relcl_def cl_UN)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   373
done
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   374
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   375
text{*Meier's theorem of section 4.5.3*}
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   376
theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   377
apply (rule equalityI) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   378
 prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   379
apply (rename_tac X)
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   380
apply (rule cl_subset_in_lattice)   
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   381
 prefer 2 apply assumption
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   382
apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2])
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   383
apply (drule equalityD1)   
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   384
apply (rule subset_trans) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   385
 prefer 2 apply assumption
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   386
apply (thin_tac "?U \<subseteq> X") 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   387
apply (cut_tac A=X in UN_singleton) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   388
apply (erule subst) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   389
apply (simp only: cl_UN lattice_latticeof 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   390
                  cl_latticeof [OF refl_relcl trans_relcl]) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   391
apply (simp add: relcl_def) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   392
done
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   393
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   394
theorem relcl_latticeof_eq:
30198
922f944f03b2 name changes
nipkow
parents: 23767
diff changeset
   395
     "[|refl r; trans r|] ==> relcl (latticeof r) = r"
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   396
by (simp add: relcl_def cl_latticeof)
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   397
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   398
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   399
subsubsection {*Decoupling Theorems*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   400
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   401
definition decoupled :: "['a program, 'a program] => bool" where
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   402
   "decoupled F G ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   403
        \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   404
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   405
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   406
text{*Rao's Decoupling Theorem*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   407
lemma stableco: "F \<in> stable A ==> F \<in> A-B co A"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   408
by (simp add: stable_def constrains_def, blast) 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   409
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   410
theorem decoupling:
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   411
  assumes leadsTo: "F \<in> A leadsTo B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   412
      and Gstable: "G \<in> stable B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   413
      and dec:     "decoupled F G"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   414
  shows "F\<squnion>G \<in> A leadsTo B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   415
proof -
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   416
  have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   417
    by (simp add: progress_set_def lattice_stable Gstable closed_def
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   418
                  stable_Un [OF Gstable] dec [unfolded decoupled_def]) 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   419
  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   420
    by (rule progress_set_Union [OF leadsTo prog],
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   421
        simp_all add: Gstable stableco)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   422
  thus ?thesis by simp
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   423
qed
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   424
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   425
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   426
text{*Rao's Weak Decoupling Theorem*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   427
theorem weak_decoupling:
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   428
  assumes leadsTo: "F \<in> A leadsTo B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   429
      and stable: "F\<squnion>G \<in> stable B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   430
      and dec:     "decoupled F (F\<squnion>G)"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   431
  shows "F\<squnion>G \<in> A leadsTo B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   432
proof -
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   433
  have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B" 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   434
    by (simp del: Join_stable
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   435
             add: progress_set_def lattice_stable stable closed_def
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   436
                  stable_Un [OF stable] dec [unfolded decoupled_def])
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   437
  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   438
    by (rule progress_set_Union [OF leadsTo prog],
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   439
        simp_all del: Join_stable add: stable,
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   440
        simp add: stableco) 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   441
  thus ?thesis by simp
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   442
qed
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   443
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   444
text{*The ``Decoupling via @{term G'} Union Theorem''*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   445
theorem decoupling_via_aux:
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   446
  assumes leadsTo: "F \<in> A leadsTo B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   447
      and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   448
      and GG':  "G \<le> G'"  
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   449
               --{*Beware!  This is the converse of the refinement relation!*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   450
  shows "F\<squnion>G \<in> A leadsTo B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   451
proof -
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   452
  from prog have stable: "G' \<in> stable B"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   453
    by (simp add: progress_set_def)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   454
  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   455
    by (rule progress_set_Union [OF leadsTo prog],
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   456
        simp_all add: stable stableco component_stable [OF GG'])
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   457
  thus ?thesis by simp
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   458
qed
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   459
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   460
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   461
subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   462
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   463
subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   464
definition commutes :: "['a program, 'a set, 'a set,  'a set set] => bool" where
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   465
   "commutes F T B L ==
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   466
       \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   467
           cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   468
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   469
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   470
text{*From Meier's thesis, section 4.5.6*}
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   471
lemma commutativity1_lemma:
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   472
  assumes commutes: "commutes F T B L" 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   473
      and lattice:  "lattice L"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   474
      and BL: "B \<in> L"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   475
      and TL: "T \<in> L"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   476
  shows "closed F T B L"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   477
apply (simp add: closed_def, clarify)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   478
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
32693
6c6b1ba5e71e tuned proofs
haftmann
parents: 32604
diff changeset
   479
apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   480
                 cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   481
apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   482
 prefer 2 
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 14150
diff changeset
   483
 apply (cut_tac commutes, simp add: commutes_def) 
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   484
apply (erule subset_trans) 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   485
apply (simp add: cl_ident)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   486
apply (blast intro: rev_subsetD [OF _ wp_mono]) 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   487
done
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   488
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   489
text{*Version packaged with @{thm progress_set_Union}*}
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   490
lemma commutativity1:
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   491
  assumes leadsTo: "F \<in> A leadsTo B"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   492
      and lattice:  "lattice L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   493
      and BL: "B \<in> L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   494
      and TL: "T \<in> L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   495
      and Fstable: "F \<in> stable T"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   496
      and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   497
      and commutes: "commutes F T B L" 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   498
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   499
by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco],
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   500
    simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   501
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   502
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   503
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   504
text{*Possibly move to Relation.thy, after @{term single_valued}*}
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   505
definition funof :: "[('a*'b)set, 'a] => 'b" where
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   506
   "funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   507
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   508
lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   509
by (simp add: funof_def single_valued_def, blast)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   510
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   511
lemma funof_Pair_in:
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   512
     "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   513
by (force simp add: funof_eq) 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   514
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   515
lemma funof_in:
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   516
     "[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   517
by (force simp add: funof_eq)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   518
 
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   519
lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A"
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   520
by (force simp add: in_wp_iff funof_eq)
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   521
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   522
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   523
subsubsection{*Commutativity of Functions and Relation*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   524
text{*Thesis, page 109*}
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   525
32604
8b3e2bc91a46 partially isarified proof
haftmann
parents: 32139
diff changeset
   526
(*FIXME: this proof is still an ungodly mess*)
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   527
text{*From Meier's thesis, section 4.5.6*}
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   528
lemma commutativity2_lemma:
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   529
  assumes dcommutes: 
45477
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   530
      "\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow>
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   531
        s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   532
    and determ: "!!act. act \<in> Acts F ==> single_valued act"
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   533
    and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   534
    and lattice:  "lattice L"
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   535
    and BL: "B \<in> L"
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   536
    and TL: "T \<in> L"
11d9c2768729 tuned proofs;
wenzelm
parents: 44918
diff changeset
   537
    and Fstable: "F \<in> stable T"
13874
0da2141606c6 More on progress sets
paulson
parents: 13870
diff changeset
   538
  shows  "commutes F T B L"
32604
8b3e2bc91a46 partially isarified proof
haftmann
parents: 32139
diff changeset
   539
proof -
51488
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   540
  { fix M and act and t
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   541
    assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   542
    then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   543
      by (force simp add: cl_eq_Collect_relcl [OF lattice])
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   544
    then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   545
      by blast
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   546
    then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   547
      apply (intro ballI impI) 
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   548
      apply (subst cl_ident [symmetric], assumption)
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   549
      apply (simp add: relcl_def)  
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   550
      apply (blast intro: cl_mono [THEN [2] rev_subsetD])
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   551
      done
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   552
    with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   553
      by (force intro!: funof_in 
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   554
        simp add: wp_def stable_def constrains_def determ total)
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   555
    with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   556
      by (intro dcommutes) assumption+ 
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   557
    with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   558
      by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   559
    with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   560
      by (blast intro: funof_imp_wp determ) 
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   561
    with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   562
      by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   563
    then have"t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   564
      by simp
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   565
  }
3c886fe611b8 tuned proof
haftmann
parents: 45477
diff changeset
   566
  then show "commutes F T B L" unfolding commutes_def by clarify
32604
8b3e2bc91a46 partially isarified proof
haftmann
parents: 32139
diff changeset
   567
qed
8b3e2bc91a46 partially isarified proof
haftmann
parents: 32139
diff changeset
   568
  
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   569
text{*Version packaged with @{thm progress_set_Union}*}
13885
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   570
lemma commutativity2:
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   571
  assumes leadsTo: "F \<in> A leadsTo B"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   572
      and dcommutes: 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   573
        "\<forall>act \<in> Acts F. 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   574
         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   575
                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   576
      and determ: "!!act. act \<in> Acts F ==> single_valued act"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   577
      and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   578
      and lattice:  "lattice L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   579
      and BL: "B \<in> L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   580
      and TL: "T \<in> L"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   581
      and Fstable: "F \<in> stable T"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   582
      and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   583
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   584
apply (rule commutativity1 [OF leadsTo lattice]) 
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   585
apply (simp_all add: Gco commutativity2_lemma dcommutes determ total
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   586
                     lattice BL TL Fstable)
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   587
done
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   588
de6fac7d5351 Proofs for section 4.5.3
paulson
parents: 13874
diff changeset
   589
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   590
subsection {*Monotonicity*}
14150
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13888
diff changeset
   591
text{*From Meier's thesis, section 4.5.7, page 110*}
13888
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   592
(*to be continued?*)
16f424af58a2 more comments and tweaks
paulson
parents: 13885
diff changeset
   593
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents:
diff changeset
   594
end