src/HOL/UNITY/ELT.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13798 4c1a53627500
child 13819 78f5885b76a9
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
paulson@8044
     1
(*  Title:      HOL/UNITY/ELT
paulson@8044
     2
    ID:         $Id$
paulson@8044
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8044
     4
    Copyright   1999  University of Cambridge
paulson@8044
     5
paulson@8044
     6
leadsTo strengthened with a specification of the allowable sets transient parts
paulson@8122
     7
paulson@8122
     8
TRY INSTEAD (to get rid of the {} and to gain strong induction)
paulson@8122
     9
paulson@8122
    10
  elt :: "['a set set, 'a program, 'a set] => ('a set) set"
paulson@8122
    11
paulson@8122
    12
inductive "elt CC F B"
paulson@13790
    13
  intros 
paulson@8122
    14
paulson@13790
    15
    Weaken:  "A <= B ==> A : elt CC F B"
paulson@8122
    16
paulson@13790
    17
    ETrans:  "[| F : A ensures A';  A-A' : CC;  A' : elt CC F B |]
paulson@13790
    18
	      ==> A : elt CC F B"
paulson@8122
    19
paulson@13790
    20
    Union:  "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B"
paulson@8122
    21
paulson@8122
    22
  monos Pow_mono
paulson@8044
    23
*)
paulson@8044
    24
paulson@13798
    25
header{*Progress Under Allowable Sets*}
paulson@13798
    26
paulson@13790
    27
theory ELT = Project:
paulson@8044
    28
paulson@8044
    29
consts
paulson@8044
    30
paulson@8044
    31
  (*LEADS-TO constant for the inductive definition*)
paulson@8044
    32
  elt :: "['a set set, 'a program] => ('a set * 'a set) set"
paulson@8044
    33
paulson@8044
    34
paulson@8044
    35
inductive "elt CC F"
paulson@13790
    36
 intros 
paulson@8044
    37
paulson@13790
    38
   Basis:  "[| F : A ensures B;  A-B : (insert {} CC) |] ==> (A,B) : elt CC F"
paulson@8044
    39
paulson@13790
    40
   Trans:  "[| (A,B) : elt CC F;  (B,C) : elt CC F |] ==> (A,C) : elt CC F"
paulson@8044
    41
paulson@13790
    42
   Union:  "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
paulson@8044
    43
paulson@8044
    44
paulson@8044
    45
constdefs
paulson@8128
    46
  
paulson@8128
    47
  (*the set of all sets determined by f alone*)
paulson@8128
    48
  givenBy :: "['a => 'b] => 'a set set"
nipkow@10834
    49
    "givenBy f == range (%B. f-` B)"
paulson@8044
    50
paulson@8044
    51
  (*visible version of the LEADS-TO relation*)
paulson@8044
    52
  leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
paulson@8044
    53
                                        ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
paulson@8044
    54
    "leadsETo A CC B == {F. (A,B) : elt CC F}"
paulson@8044
    55
paulson@8044
    56
  LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
paulson@8044
    57
                                        ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80)
paulson@8044
    58
    "LeadsETo A CC B ==
nipkow@10834
    59
      {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}"
paulson@8044
    60
paulson@13790
    61
paulson@13790
    62
(*** givenBy ***)
paulson@13790
    63
paulson@13790
    64
lemma givenBy_id [simp]: "givenBy id = UNIV"
paulson@13790
    65
by (unfold givenBy_def, auto)
paulson@13790
    66
paulson@13790
    67
lemma givenBy_eq_all: "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}"
paulson@13790
    68
apply (unfold givenBy_def, safe)
paulson@13790
    69
apply (rule_tac [2] x = "v ` ?u" in image_eqI, auto)
paulson@13790
    70
done
paulson@13790
    71
paulson@13790
    72
lemma givenByI: "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v"
paulson@13790
    73
by (subst givenBy_eq_all, blast)
paulson@13790
    74
paulson@13790
    75
lemma givenByD: "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A"
paulson@13790
    76
by (unfold givenBy_def, auto)
paulson@13790
    77
paulson@13790
    78
lemma empty_mem_givenBy [iff]: "{} : givenBy v"
paulson@13790
    79
by (blast intro!: givenByI)
paulson@13790
    80
paulson@13790
    81
lemma givenBy_imp_eq_Collect: "A: givenBy v ==> EX P. A = {s. P(v s)}"
paulson@13790
    82
apply (rule_tac x = "%n. EX s. v s = n & s : A" in exI)
paulson@13790
    83
apply (simp (no_asm_use) add: givenBy_eq_all)
paulson@13790
    84
apply blast
paulson@13790
    85
done
paulson@13790
    86
paulson@13790
    87
lemma Collect_mem_givenBy: "{s. P(v s)} : givenBy v"
paulson@13790
    88
by (unfold givenBy_def, best)
paulson@13790
    89
paulson@13790
    90
lemma givenBy_eq_Collect: "givenBy v = {A. EX P. A = {s. P(v s)}}"
paulson@13790
    91
by (blast intro: Collect_mem_givenBy givenBy_imp_eq_Collect)
paulson@13790
    92
paulson@13790
    93
(*preserving v preserves properties given by v*)
paulson@13790
    94
lemma preserves_givenBy_imp_stable:
paulson@13790
    95
     "[| F : preserves v;  D : givenBy v |] ==> F : stable D"
paulson@13798
    96
by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)
paulson@13790
    97
paulson@13790
    98
lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v"
paulson@13790
    99
apply (simp (no_asm) add: givenBy_eq_Collect)
paulson@13790
   100
apply best 
paulson@13790
   101
done
paulson@13790
   102
paulson@13790
   103
lemma givenBy_DiffI:
paulson@13790
   104
     "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v"
paulson@13790
   105
apply (simp (no_asm_use) add: givenBy_eq_Collect)
paulson@13790
   106
apply safe
paulson@13790
   107
apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
paulson@13790
   108
apply (tactic "deepen_tac (set_cs addSIs [equalityI]) 0 1")
paulson@13790
   109
done
paulson@13790
   110
paulson@13790
   111
paulson@13790
   112
(** Standard leadsTo rules **)
paulson@13790
   113
paulson@13790
   114
lemma leadsETo_Basis [intro]: 
paulson@13790
   115
     "[| F: A ensures B;  A-B: insert {} CC |] ==> F : A leadsTo[CC] B"
paulson@13790
   116
apply (unfold leadsETo_def)
paulson@13790
   117
apply (blast intro: elt.Basis)
paulson@13790
   118
done
paulson@13790
   119
paulson@13790
   120
lemma leadsETo_Trans: 
paulson@13790
   121
     "[| F : A leadsTo[CC] B;  F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C"
paulson@13790
   122
apply (unfold leadsETo_def)
paulson@13790
   123
apply (blast intro: elt.Trans)
paulson@13790
   124
done
paulson@13790
   125
paulson@13790
   126
paulson@13790
   127
(*Useful with cancellation, disjunction*)
paulson@13790
   128
lemma leadsETo_Un_duplicate:
paulson@13790
   129
     "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'"
paulson@13790
   130
apply (simp add: Un_ac)
paulson@13790
   131
done
paulson@13790
   132
paulson@13790
   133
lemma leadsETo_Un_duplicate2:
paulson@13790
   134
     "F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)"
paulson@13790
   135
by (simp add: Un_ac)
paulson@13790
   136
paulson@13790
   137
(*The Union introduction rule as we should have liked to state it*)
paulson@13790
   138
lemma leadsETo_Union:
paulson@13790
   139
    "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B"
paulson@13790
   140
apply (unfold leadsETo_def)
paulson@13790
   141
apply (blast intro: elt.Union)
paulson@13790
   142
done
paulson@13790
   143
paulson@13790
   144
lemma leadsETo_UN:
paulson@13790
   145
    "(!!i. i : I ==> F : (A i) leadsTo[CC] B)  
paulson@13790
   146
     ==> F : (UN i:I. A i) leadsTo[CC] B"
paulson@13790
   147
apply (subst Union_image_eq [symmetric])
paulson@13790
   148
apply (blast intro: leadsETo_Union)
paulson@13790
   149
done
paulson@13790
   150
paulson@13790
   151
(*The INDUCTION rule as we should have liked to state it*)
paulson@13790
   152
lemma leadsETo_induct:
paulson@13790
   153
  "[| F : za leadsTo[CC] zb;   
paulson@13790
   154
      !!A B. [| F : A ensures B;  A-B : insert {} CC |] ==> P A B;  
paulson@13790
   155
      !!A B C. [| F : A leadsTo[CC] B; P A B; F : B leadsTo[CC] C; P B C |]  
paulson@13790
   156
               ==> P A C;  
paulson@13790
   157
      !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B  
paulson@13790
   158
   |] ==> P za zb"
paulson@13790
   159
apply (unfold leadsETo_def)
paulson@13790
   160
apply (drule CollectD) 
paulson@13790
   161
apply (erule elt.induct, blast+)
paulson@13790
   162
done
paulson@13790
   163
paulson@13790
   164
paulson@13790
   165
(** New facts involving leadsETo **)
paulson@13790
   166
paulson@13790
   167
lemma leadsETo_mono: "CC' <= CC ==> (A leadsTo[CC'] B) <= (A leadsTo[CC] B)"
paulson@13790
   168
apply safe
paulson@13790
   169
apply (erule leadsETo_induct)
paulson@13790
   170
prefer 3 apply (blast intro: leadsETo_Union)
paulson@13790
   171
prefer 2 apply (blast intro: leadsETo_Trans)
paulson@13790
   172
apply (blast intro: leadsETo_Basis)
paulson@13790
   173
done
paulson@13790
   174
paulson@13790
   175
lemma leadsETo_Trans_Un:
paulson@13790
   176
     "[| F : A leadsTo[CC] B;  F : B leadsTo[DD] C |]  
paulson@13790
   177
      ==> F : A leadsTo[CC Un DD] C"
paulson@13790
   178
by (blast intro: leadsETo_mono [THEN subsetD] leadsETo_Trans)
paulson@13790
   179
paulson@13790
   180
lemma leadsETo_Union_Int:
paulson@13790
   181
 "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) 
paulson@13790
   182
  ==> F : (Union S Int C) leadsTo[CC] B"
paulson@13790
   183
apply (unfold leadsETo_def)
paulson@13790
   184
apply (simp only: Int_Union_Union)
paulson@13790
   185
apply (blast intro: elt.Union)
paulson@13790
   186
done
paulson@13790
   187
paulson@13790
   188
(*Binary union introduction rule*)
paulson@13790
   189
lemma leadsETo_Un:
paulson@13790
   190
     "[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |] 
paulson@13790
   191
      ==> F : (A Un B) leadsTo[CC] C"
paulson@13790
   192
apply (subst Un_eq_Union)
paulson@13790
   193
apply (blast intro: leadsETo_Union)
paulson@13790
   194
done
paulson@13790
   195
paulson@13790
   196
lemma single_leadsETo_I:
paulson@13790
   197
     "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
paulson@13790
   198
apply (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
paulson@13790
   199
done
paulson@13790
   200
paulson@13790
   201
paulson@13790
   202
lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B"
paulson@13790
   203
by (simp add: subset_imp_ensures [THEN leadsETo_Basis] Diff_eq_empty_iff [THEN iffD2])
paulson@13790
   204
paulson@13790
   205
lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp]
paulson@13790
   206
paulson@13790
   207
paulson@13790
   208
paulson@13790
   209
(** Weakening laws **)
paulson@13790
   210
paulson@13790
   211
lemma leadsETo_weaken_R:
paulson@13790
   212
     "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'"
paulson@13790
   213
apply (blast intro: subset_imp_leadsETo leadsETo_Trans)
paulson@13790
   214
done
paulson@13790
   215
paulson@13798
   216
lemma leadsETo_weaken_L [rule_format]:
paulson@13790
   217
     "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
paulson@13790
   218
apply (blast intro: leadsETo_Trans subset_imp_leadsETo)
paulson@13790
   219
done
paulson@13790
   220
paulson@13790
   221
(*Distributes over binary unions*)
paulson@13790
   222
lemma leadsETo_Un_distrib:
paulson@13790
   223
     "F : (A Un B) leadsTo[CC] C  =   
paulson@13790
   224
      (F : A leadsTo[CC] C & F : B leadsTo[CC] C)"
paulson@13790
   225
apply (blast intro: leadsETo_Un leadsETo_weaken_L)
paulson@13790
   226
done
paulson@13790
   227
paulson@13790
   228
lemma leadsETo_UN_distrib:
paulson@13790
   229
     "F : (UN i:I. A i) leadsTo[CC] B  =   
paulson@13790
   230
      (ALL i : I. F : (A i) leadsTo[CC] B)"
paulson@13790
   231
apply (blast intro: leadsETo_UN leadsETo_weaken_L)
paulson@13790
   232
done
paulson@13790
   233
paulson@13790
   234
lemma leadsETo_Union_distrib:
paulson@13790
   235
     "F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
paulson@13790
   236
apply (blast intro: leadsETo_Union leadsETo_weaken_L)
paulson@13790
   237
done
paulson@13790
   238
paulson@13790
   239
lemma leadsETo_weaken:
paulson@13790
   240
     "[| F : A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC |]  
paulson@13790
   241
      ==> F : B leadsTo[CC] B'"
paulson@13790
   242
apply (drule leadsETo_mono [THEN subsetD], assumption)
paulson@13790
   243
apply (blast del: subsetCE intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
paulson@13790
   244
done
paulson@13790
   245
paulson@13790
   246
lemma leadsETo_givenBy:
paulson@13790
   247
     "[| F : A leadsTo[CC] A';  CC <= givenBy v |]  
paulson@13790
   248
      ==> F : A leadsTo[givenBy v] A'"
paulson@13790
   249
by (blast intro: empty_mem_givenBy leadsETo_weaken)
paulson@13790
   250
paulson@13790
   251
paulson@13790
   252
(*Set difference*)
paulson@13790
   253
lemma leadsETo_Diff:
paulson@13790
   254
     "[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C |]  
paulson@13790
   255
      ==> F : A leadsTo[CC] C"
paulson@13790
   256
by (blast intro: leadsETo_Un leadsETo_weaken)
paulson@13790
   257
paulson@13790
   258
paulson@13790
   259
(*Binary union version*)
paulson@13790
   260
lemma leadsETo_Un_Un:
paulson@13790
   261
     "[| F : A leadsTo[CC] A';  F : B leadsTo[CC] B' |]  
paulson@13790
   262
      ==> F : (A Un B) leadsTo[CC] (A' Un B')"
paulson@13790
   263
by (blast intro: leadsETo_Un leadsETo_weaken_R)
paulson@13790
   264
paulson@13790
   265
paulson@13790
   266
(** The cancellation law **)
paulson@13790
   267
paulson@13790
   268
lemma leadsETo_cancel2:
paulson@13790
   269
     "[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B' |]  
paulson@13790
   270
      ==> F : A leadsTo[CC] (A' Un B')"
paulson@13790
   271
by (blast intro: leadsETo_Un_Un subset_imp_leadsETo leadsETo_Trans)
paulson@13790
   272
paulson@13790
   273
lemma leadsETo_cancel1:
paulson@13790
   274
     "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B' |]  
paulson@13790
   275
    ==> F : A leadsTo[CC] (B' Un A')"
paulson@13790
   276
apply (simp add: Un_commute)
paulson@13790
   277
apply (blast intro!: leadsETo_cancel2)
paulson@13790
   278
done
paulson@13790
   279
paulson@13790
   280
lemma leadsETo_cancel_Diff1:
paulson@13790
   281
     "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]  
paulson@13790
   282
    ==> F : A leadsTo[CC] (B' Un A')"
paulson@13790
   283
apply (rule leadsETo_cancel1)
paulson@13812
   284
 prefer 2 apply assumption
paulson@13812
   285
apply simp_all
paulson@13790
   286
done
paulson@13790
   287
paulson@13790
   288
paulson@13790
   289
paulson@13790
   290
(** PSP: Progress-Safety-Progress **)
paulson@13790
   291
paulson@13790
   292
(*Special case of PSP: Misra's "stable conjunction"*)
paulson@13790
   293
lemma e_psp_stable: 
paulson@13790
   294
   "[| F : A leadsTo[CC] A';  F : stable B;  ALL C:CC. C Int B : CC |]  
paulson@13790
   295
    ==> F : (A Int B) leadsTo[CC] (A' Int B)"
paulson@13790
   296
apply (unfold stable_def)
paulson@13790
   297
apply (erule leadsETo_induct)
paulson@13790
   298
prefer 3 apply (blast intro: leadsETo_Union_Int)
paulson@13790
   299
prefer 2 apply (blast intro: leadsETo_Trans)
paulson@13790
   300
apply (rule leadsETo_Basis)
paulson@13790
   301
prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric])
paulson@13790
   302
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
paulson@13790
   303
apply (blast intro: transient_strengthen constrains_Int)
paulson@13790
   304
done
paulson@13790
   305
paulson@13790
   306
lemma e_psp_stable2:
paulson@13790
   307
     "[| F : A leadsTo[CC] A'; F : stable B;  ALL C:CC. C Int B : CC |]  
paulson@13790
   308
      ==> F : (B Int A) leadsTo[CC] (B Int A')"
paulson@13790
   309
by (simp (no_asm_simp) add: e_psp_stable Int_ac)
paulson@13790
   310
paulson@13790
   311
lemma e_psp:
paulson@13790
   312
     "[| F : A leadsTo[CC] A'; F : B co B';   
paulson@13790
   313
         ALL C:CC. C Int B Int B' : CC |]  
paulson@13790
   314
      ==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))"
paulson@13790
   315
apply (erule leadsETo_induct)
paulson@13790
   316
prefer 3 apply (blast intro: leadsETo_Union_Int)
paulson@13790
   317
(*Transitivity case has a delicate argument involving "cancellation"*)
paulson@13790
   318
apply (rule_tac [2] leadsETo_Un_duplicate2)
paulson@13790
   319
apply (erule_tac [2] leadsETo_cancel_Diff1)
paulson@13790
   320
prefer 2
paulson@13790
   321
 apply (simp add: Int_Diff Diff_triv)
paulson@13790
   322
 apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset)
paulson@13790
   323
(*Basis case*)
paulson@13790
   324
apply (rule leadsETo_Basis)
paulson@13790
   325
apply (blast intro: psp_ensures)
paulson@13790
   326
apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'")
paulson@13790
   327
apply auto
paulson@13790
   328
done
paulson@13790
   329
paulson@13790
   330
lemma e_psp2:
paulson@13790
   331
     "[| F : A leadsTo[CC] A'; F : B co B';   
paulson@13790
   332
         ALL C:CC. C Int B Int B' : CC |]  
paulson@13790
   333
      ==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))"
paulson@13790
   334
by (simp add: e_psp Int_ac)
paulson@13790
   335
paulson@13790
   336
paulson@13790
   337
(*** Special properties involving the parameter [CC] ***)
paulson@13790
   338
paulson@13790
   339
(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
paulson@13790
   340
lemma gen_leadsETo_imp_Join_leadsETo:
paulson@13790
   341
     "[| F: (A leadsTo[givenBy v] B);  G : preserves v;   
paulson@13790
   342
         F Join G : stable C |]  
paulson@13790
   343
      ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
paulson@13790
   344
apply (erule leadsETo_induct)
paulson@13790
   345
  prefer 3
paulson@13790
   346
  apply (subst Int_Union) 
paulson@13790
   347
  apply (blast intro: leadsETo_UN)
paulson@13790
   348
prefer 2
paulson@13790
   349
 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
paulson@13790
   350
apply (rule leadsETo_Basis)
paulson@13790
   351
apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] Int_Diff ensures_def givenBy_eq_Collect Join_transient)
paulson@13790
   352
prefer 3 apply (blast intro: transient_strengthen)
paulson@13790
   353
apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
paulson@13790
   354
apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
paulson@13790
   355
apply (unfold stable_def)
paulson@13790
   356
apply (blast intro: constrains_Int [THEN constrains_weaken])+
paulson@13790
   357
done
paulson@13790
   358
paulson@13790
   359
(**** Relationship with traditional "leadsTo", strong & weak ****)
paulson@13790
   360
paulson@13790
   361
(** strong **)
paulson@13790
   362
paulson@13790
   363
lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)"
paulson@13790
   364
apply safe
paulson@13790
   365
apply (erule leadsETo_induct)
paulson@13790
   366
prefer 3 apply (blast intro: leadsTo_Union)
paulson@13790
   367
prefer 2 apply (blast intro: leadsTo_Trans, blast)
paulson@13790
   368
done
paulson@13790
   369
paulson@13790
   370
lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)"
paulson@13790
   371
apply safe
paulson@13790
   372
apply (erule leadsETo_subset_leadsTo [THEN subsetD])
paulson@13790
   373
(*right-to-left case*)
paulson@13790
   374
apply (erule leadsTo_induct)
paulson@13790
   375
prefer 3 apply (blast intro: leadsETo_Union)
paulson@13790
   376
prefer 2 apply (blast intro: leadsETo_Trans, blast)
paulson@13790
   377
done
paulson@13790
   378
paulson@13790
   379
(**** weak ****)
paulson@13790
   380
paulson@13790
   381
lemma LeadsETo_eq_leadsETo: 
paulson@13790
   382
     "A LeadsTo[CC] B =  
paulson@13790
   383
        {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC]  
paulson@13790
   384
        (reachable F Int B)}"
paulson@13790
   385
apply (unfold LeadsETo_def)
paulson@13790
   386
apply (blast dest: e_psp_stable2 intro: leadsETo_weaken)
paulson@13790
   387
done
paulson@13790
   388
paulson@13790
   389
(*** Introduction rules: Basis, Trans, Union ***)
paulson@13790
   390
paulson@13790
   391
lemma LeadsETo_Trans:
paulson@13790
   392
     "[| F : A LeadsTo[CC] B;  F : B LeadsTo[CC] C |]  
paulson@13790
   393
      ==> F : A LeadsTo[CC] C"
paulson@13790
   394
apply (simp add: LeadsETo_eq_leadsETo)
paulson@13790
   395
apply (blast intro: leadsETo_Trans)
paulson@13790
   396
done
paulson@13790
   397
paulson@13790
   398
lemma LeadsETo_Union:
paulson@13790
   399
     "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
paulson@13790
   400
apply (simp add: LeadsETo_def)
paulson@13790
   401
apply (subst Int_Union)
paulson@13790
   402
apply (blast intro: leadsETo_UN)
paulson@13790
   403
done
paulson@13790
   404
paulson@13790
   405
lemma LeadsETo_UN:
paulson@13790
   406
     "(!!i. i : I ==> F : (A i) LeadsTo[CC] B)  
paulson@13790
   407
      ==> F : (UN i:I. A i) LeadsTo[CC] B"
paulson@13790
   408
apply (simp only: Union_image_eq [symmetric])
paulson@13790
   409
apply (blast intro: LeadsETo_Union)
paulson@13790
   410
done
paulson@13790
   411
paulson@13790
   412
(*Binary union introduction rule*)
paulson@13790
   413
lemma LeadsETo_Un:
paulson@13790
   414
     "[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]  
paulson@13790
   415
      ==> F : (A Un B) LeadsTo[CC] C"
paulson@13790
   416
apply (subst Un_eq_Union)
paulson@13790
   417
apply (blast intro: LeadsETo_Union)
paulson@13790
   418
done
paulson@13790
   419
paulson@13790
   420
(*Lets us look at the starting state*)
paulson@13790
   421
lemma single_LeadsETo_I:
paulson@13790
   422
     "(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B"
paulson@13790
   423
apply (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
paulson@13790
   424
done
paulson@13790
   425
paulson@13790
   426
lemma subset_imp_LeadsETo:
paulson@13790
   427
     "A <= B ==> F : A LeadsTo[CC] B"
paulson@13790
   428
apply (simp (no_asm) add: LeadsETo_def)
paulson@13790
   429
apply (blast intro: subset_imp_leadsETo)
paulson@13790
   430
done
paulson@13790
   431
paulson@13790
   432
lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
paulson@13790
   433
paulson@13798
   434
lemma LeadsETo_weaken_R [rule_format]:
paulson@13790
   435
     "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
paulson@13790
   436
apply (simp (no_asm_use) add: LeadsETo_def)
paulson@13790
   437
apply (blast intro: leadsETo_weaken_R)
paulson@13790
   438
done
paulson@13790
   439
paulson@13798
   440
lemma LeadsETo_weaken_L [rule_format]:
paulson@13790
   441
     "[| F : A LeadsTo[CC] A';  B <= A |] ==> F : B LeadsTo[CC] A'"
paulson@13790
   442
apply (simp (no_asm_use) add: LeadsETo_def)
paulson@13790
   443
apply (blast intro: leadsETo_weaken_L)
paulson@13790
   444
done
paulson@13790
   445
paulson@13790
   446
lemma LeadsETo_weaken:
paulson@13790
   447
     "[| F : A LeadsTo[CC'] A';    
paulson@13790
   448
         B <= A;  A' <= B';  CC' <= CC |]  
paulson@13790
   449
      ==> F : B LeadsTo[CC] B'"
paulson@13790
   450
apply (simp (no_asm_use) add: LeadsETo_def)
paulson@13790
   451
apply (blast intro: leadsETo_weaken)
paulson@13790
   452
done
paulson@13790
   453
paulson@13790
   454
lemma LeadsETo_subset_LeadsTo: "(A LeadsTo[CC] B) <= (A LeadsTo B)"
paulson@13790
   455
apply (unfold LeadsETo_def LeadsTo_def)
paulson@13790
   456
apply (blast intro: leadsETo_subset_leadsTo [THEN subsetD])
paulson@13790
   457
done
paulson@13790
   458
paulson@13790
   459
(*Postcondition can be strengthened to (reachable F Int B) *)
paulson@13790
   460
lemma reachable_ensures:
paulson@13790
   461
     "F : A ensures B ==> F : (reachable F Int A) ensures B"
paulson@13790
   462
apply (rule stable_ensures_Int [THEN ensures_weaken_R], auto)
paulson@13790
   463
done
paulson@13790
   464
paulson@13790
   465
lemma lel_lemma:
paulson@13790
   466
     "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
paulson@13790
   467
apply (erule leadsTo_induct)
paulson@13790
   468
  apply (blast intro: reachable_ensures leadsETo_Basis)
paulson@13790
   469
 apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
paulson@13790
   470
apply (subst Int_Union)
paulson@13790
   471
apply (blast intro: leadsETo_UN)
paulson@13790
   472
done
paulson@13790
   473
paulson@13790
   474
lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)"
paulson@13790
   475
apply safe
paulson@13790
   476
apply (erule LeadsETo_subset_LeadsTo [THEN subsetD])
paulson@13790
   477
(*right-to-left case*)
paulson@13790
   478
apply (unfold LeadsETo_def LeadsTo_def)
paulson@13790
   479
apply (fast elim: lel_lemma [THEN leadsETo_weaken])
paulson@13790
   480
done
paulson@13790
   481
paulson@13790
   482
paulson@13790
   483
(**** EXTEND/PROJECT PROPERTIES ****)
paulson@13790
   484
paulson@13790
   485
lemma (in Extend) givenBy_o_eq_extend_set: "givenBy (v o f) = extend_set h ` (givenBy v)"
paulson@13790
   486
apply (simp (no_asm) add: givenBy_eq_Collect)
paulson@13790
   487
apply best 
paulson@13790
   488
done
paulson@13790
   489
paulson@13790
   490
lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
paulson@13790
   491
apply (simp (no_asm) add: givenBy_eq_Collect)
paulson@13790
   492
apply best
paulson@13790
   493
done
paulson@13790
   494
paulson@13790
   495
lemma (in Extend) extend_set_givenBy_I:
paulson@13790
   496
     "D : givenBy v ==> extend_set h D : givenBy (v o f)"
paulson@13790
   497
apply (simp (no_asm_use) add: givenBy_eq_all)
paulson@13790
   498
apply blast
paulson@13790
   499
done
paulson@13790
   500
paulson@13790
   501
lemma (in Extend) leadsETo_imp_extend_leadsETo:
paulson@13790
   502
     "F : A leadsTo[CC] B  
paulson@13790
   503
      ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]  
paulson@13790
   504
                       (extend_set h B)"
paulson@13790
   505
apply (erule leadsETo_induct)
paulson@13790
   506
  apply (force intro: leadsETo_Basis subset_imp_ensures 
paulson@13790
   507
               simp add: extend_ensures extend_set_Diff_distrib [symmetric])
paulson@13790
   508
 apply (blast intro: leadsETo_Trans)
paulson@13790
   509
apply (simp add: leadsETo_UN extend_set_Union)
paulson@13790
   510
done
paulson@13790
   511
paulson@13790
   512
paulson@13790
   513
(*This version's stronger in the "ensures" precondition
paulson@13790
   514
  BUT there's no ensures_weaken_L*)
paulson@13790
   515
lemma (in Extend) Join_project_ensures_strong:
paulson@13790
   516
     "[| project h C G ~: transient (project_set h C Int (A-B)) |  
paulson@13790
   517
           project_set h C Int (A - B) = {};   
paulson@13790
   518
         extend h F Join G : stable C;   
paulson@13790
   519
         F Join project h C G : (project_set h C Int A) ensures B |]  
paulson@13790
   520
      ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
paulson@13790
   521
apply (subst Int_extend_set_lemma [symmetric])
paulson@13790
   522
apply (rule Join_project_ensures)
paulson@13790
   523
apply (auto simp add: Int_Diff)
paulson@13790
   524
done
paulson@13790
   525
paulson@13812
   526
(*NOT WORKING.  MODIFY AS IN Project.thy
paulson@13790
   527
lemma (in Extend) pld_lemma:
paulson@13790
   528
     "[| extend h F Join G : stable C;   
paulson@13790
   529
         F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
paulson@13790
   530
         G : preserves (v o f) |]  
paulson@13790
   531
      ==> extend h F Join G :  
paulson@13790
   532
            (C Int extend_set h (project_set h C Int A))  
paulson@13790
   533
            leadsTo[(%D. C Int extend_set h D)`givenBy v]  (extend_set h B)"
paulson@13790
   534
apply (erule leadsETo_induct)
paulson@13790
   535
  prefer 3
paulson@13790
   536
  apply (simp del: UN_simps add: Int_UN_distrib leadsETo_UN extend_set_Union)
paulson@13790
   537
 prefer 2
paulson@13790
   538
 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
paulson@13790
   539
txt{*Base case is hard*}
paulson@13790
   540
apply auto
paulson@13790
   541
apply (force intro: leadsETo_Basis subset_imp_ensures)
paulson@13790
   542
apply (rule leadsETo_Basis)
paulson@13790
   543
 prefer 2
paulson@13790
   544
 apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
paulson@13790
   545
apply (rule Join_project_ensures_strong)
paulson@13812
   546
apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
paulson@13790
   547
apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
paulson@13790
   548
done
paulson@13790
   549
paulson@13790
   550
lemma (in Extend) project_leadsETo_D_lemma:
paulson@13790
   551
     "[| extend h F Join G : stable C;   
paulson@13790
   552
         F Join project h C G :  
paulson@13790
   553
             (project_set h C Int A)  
paulson@13790
   554
             leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
paulson@13790
   555
         G : preserves (v o f) |]  
paulson@13790
   556
      ==> extend h F Join G : (C Int extend_set h A)  
paulson@13790
   557
            leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
paulson@13790
   558
apply (rule pld_lemma [THEN leadsETo_weaken])
paulson@13790
   559
apply (auto simp add: split_extended_all)
paulson@13790
   560
done
paulson@13790
   561
paulson@13790
   562
lemma (in Extend) project_leadsETo_D:
paulson@13790
   563
     "[| F Join project h UNIV G : A leadsTo[givenBy v] B;   
paulson@13790
   564
         G : preserves (v o f) |]   
paulson@13790
   565
      ==> extend h F Join G : (extend_set h A)  
paulson@13790
   566
            leadsTo[givenBy (v o f)] (extend_set h B)"
paulson@13790
   567
apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto) 
paulson@13790
   568
apply (erule leadsETo_givenBy)
paulson@13790
   569
apply (rule givenBy_o_eq_extend_set [THEN equalityD2])
paulson@13790
   570
done
paulson@13790
   571
paulson@13790
   572
lemma (in Extend) project_LeadsETo_D:
paulson@13790
   573
     "[| F Join project h (reachable (extend h F Join G)) G  
paulson@13790
   574
             : A LeadsTo[givenBy v] B;   
paulson@13790
   575
         G : preserves (v o f) |]  
paulson@13790
   576
      ==> extend h F Join G :  
paulson@13790
   577
            (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)"
paulson@13790
   578
apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma])
paulson@13790
   579
apply (auto simp add: LeadsETo_def)
paulson@13790
   580
 apply (erule leadsETo_mono [THEN [2] rev_subsetD])
paulson@13790
   581
 apply (blast intro: extend_set_givenBy_I)
paulson@13790
   582
apply (simp add: project_set_reachable_extend_eq [symmetric])
paulson@13790
   583
done
paulson@13790
   584
paulson@13790
   585
lemma (in Extend) extending_leadsETo: 
paulson@13790
   586
     "(ALL G. extend h F ok G --> G : preserves (v o f))  
paulson@13790
   587
      ==> extending (%G. UNIV) h F  
paulson@13790
   588
                (extend_set h A leadsTo[givenBy (v o f)] extend_set h B)  
paulson@13790
   589
                (A leadsTo[givenBy v] B)"
paulson@13790
   590
apply (unfold extending_def)
paulson@13790
   591
apply (auto simp add: project_leadsETo_D)
paulson@13790
   592
done
paulson@13790
   593
paulson@13790
   594
lemma (in Extend) extending_LeadsETo: 
paulson@13790
   595
     "(ALL G. extend h F ok G --> G : preserves (v o f))  
paulson@13790
   596
      ==> extending (%G. reachable (extend h F Join G)) h F  
paulson@13790
   597
                (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)  
paulson@13790
   598
                (A LeadsTo[givenBy v]  B)"
paulson@13790
   599
apply (unfold extending_def)
paulson@13790
   600
apply (blast intro: project_LeadsETo_D)
paulson@13790
   601
done
paulson@13812
   602
*)
paulson@13790
   603
paulson@13790
   604
paulson@13790
   605
(*** leadsETo in the precondition ***)
paulson@13790
   606
paulson@13790
   607
(*Lemma for the Trans case*)
paulson@13790
   608
lemma (in Extend) pli_lemma:
paulson@13790
   609
     "[| extend h F Join G : stable C;     
paulson@13790
   610
         F Join project h C G     
paulson@13790
   611
           : project_set h C Int project_set h A leadsTo project_set h B |]  
paulson@13790
   612
      ==> F Join project h C G     
paulson@13790
   613
            : project_set h C Int project_set h A leadsTo     
paulson@13790
   614
              project_set h C Int project_set h B"
paulson@13790
   615
apply (rule psp_stable2 [THEN leadsTo_weaken_L])
paulson@13790
   616
apply (auto simp add: project_stable_project_set extend_stable_project_set)
paulson@13790
   617
done
paulson@13790
   618
paulson@13790
   619
lemma (in Extend) project_leadsETo_I_lemma:
paulson@13790
   620
     "[| extend h F Join G : stable C;   
paulson@13790
   621
         extend h F Join G :  
paulson@13790
   622
           (C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]   
paulson@13790
   623
  ==> F Join project h C G   
paulson@13790
   624
    : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
paulson@13790
   625
apply (erule leadsETo_induct)
paulson@13790
   626
  prefer 3
paulson@13790
   627
  apply (simp only: Int_UN_distrib project_set_Union)
paulson@13790
   628
  apply (blast intro: leadsTo_UN)
paulson@13790
   629
 prefer 2 apply (blast intro: leadsTo_Trans pli_lemma)
paulson@13790
   630
apply (simp add: givenBy_eq_extend_set)
paulson@13790
   631
apply (rule leadsTo_Basis)
paulson@13790
   632
apply (blast intro: ensures_extend_set_imp_project_ensures)
paulson@13790
   633
done
paulson@13790
   634
paulson@13790
   635
lemma (in Extend) project_leadsETo_I:
paulson@13790
   636
     "extend h F Join G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
paulson@13790
   637
      ==> F Join project h UNIV G : A leadsTo B"
paulson@13790
   638
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
paulson@13790
   639
done
paulson@13790
   640
paulson@13790
   641
lemma (in Extend) project_LeadsETo_I:
paulson@13790
   642
     "extend h F Join G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B) 
paulson@13790
   643
      ==> F Join project h (reachable (extend h F Join G)) G   
paulson@13790
   644
           : A LeadsTo B"
paulson@13790
   645
apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def)
paulson@13790
   646
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken])
paulson@13790
   647
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
paulson@13790
   648
done
paulson@13790
   649
paulson@13790
   650
lemma (in Extend) projecting_leadsTo: 
paulson@13790
   651
     "projecting (%G. UNIV) h F  
paulson@13790
   652
                 (extend_set h A leadsTo[givenBy f] extend_set h B)  
paulson@13790
   653
                 (A leadsTo B)"
paulson@13790
   654
apply (unfold projecting_def)
paulson@13790
   655
apply (force dest: project_leadsETo_I)
paulson@13790
   656
done
paulson@13790
   657
paulson@13790
   658
lemma (in Extend) projecting_LeadsTo: 
paulson@13790
   659
     "projecting (%G. reachable (extend h F Join G)) h F  
paulson@13790
   660
                 (extend_set h A LeadsTo[givenBy f] extend_set h B)  
paulson@13790
   661
                 (A LeadsTo B)"
paulson@13790
   662
apply (unfold projecting_def)
paulson@13790
   663
apply (force dest: project_LeadsETo_I)
paulson@13790
   664
done
paulson@13790
   665
paulson@8044
   666
end