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