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