src/HOL/UNITY/ELT.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45605 a89b4bc311a5
child 46577 e5438c5797ae
permissions -rw-r--r--
Quotient_Info stores only relation maps
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
paulson@13798
    24
header{*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)
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"
haftmann@44106
   189
  using leadsETo_Union [of "{A, B}" F CC C] by auto
paulson@13790
   190
paulson@13790
   191
lemma single_leadsETo_I:
paulson@13790
   192
     "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
paulson@13819
   193
by (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
paulson@13790
   194
paulson@13790
   195
paulson@13790
   196
lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B"
paulson@13819
   197
by (simp add: subset_imp_ensures [THEN leadsETo_Basis] 
paulson@13819
   198
              Diff_eq_empty_iff [THEN iffD2])
paulson@13790
   199
paulson@13790
   200
lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp]
paulson@13790
   201
paulson@13790
   202
paulson@13790
   203
paulson@13790
   204
(** Weakening laws **)
paulson@13790
   205
paulson@13790
   206
lemma leadsETo_weaken_R:
paulson@13790
   207
     "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'"
paulson@13819
   208
by (blast intro: subset_imp_leadsETo leadsETo_Trans)
paulson@13790
   209
paulson@13798
   210
lemma leadsETo_weaken_L [rule_format]:
paulson@13790
   211
     "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
paulson@13819
   212
by (blast intro: leadsETo_Trans subset_imp_leadsETo)
paulson@13790
   213
paulson@13790
   214
(*Distributes over binary unions*)
paulson@13790
   215
lemma leadsETo_Un_distrib:
paulson@13790
   216
     "F : (A Un B) leadsTo[CC] C  =   
paulson@13790
   217
      (F : A leadsTo[CC] C & F : B leadsTo[CC] C)"
paulson@13819
   218
by (blast intro: leadsETo_Un leadsETo_weaken_L)
paulson@13790
   219
paulson@13790
   220
lemma leadsETo_UN_distrib:
paulson@13790
   221
     "F : (UN i:I. A i) leadsTo[CC] B  =   
paulson@13790
   222
      (ALL i : I. F : (A i) leadsTo[CC] B)"
paulson@13819
   223
by (blast intro: leadsETo_UN leadsETo_weaken_L)
paulson@13790
   224
paulson@13790
   225
lemma leadsETo_Union_distrib:
paulson@13790
   226
     "F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
paulson@13819
   227
by (blast intro: leadsETo_Union leadsETo_weaken_L)
paulson@13790
   228
paulson@13790
   229
lemma leadsETo_weaken:
paulson@13790
   230
     "[| F : A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC |]  
paulson@13790
   231
      ==> F : B leadsTo[CC] B'"
paulson@13790
   232
apply (drule leadsETo_mono [THEN subsetD], assumption)
paulson@13819
   233
apply (blast del: subsetCE 
paulson@13819
   234
             intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
paulson@13790
   235
done
paulson@13790
   236
paulson@13790
   237
lemma leadsETo_givenBy:
paulson@13790
   238
     "[| F : A leadsTo[CC] A';  CC <= givenBy v |]  
paulson@13790
   239
      ==> F : A leadsTo[givenBy v] A'"
paulson@13790
   240
by (blast intro: empty_mem_givenBy leadsETo_weaken)
paulson@13790
   241
paulson@13790
   242
paulson@13790
   243
(*Set difference*)
paulson@13790
   244
lemma leadsETo_Diff:
paulson@13790
   245
     "[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C |]  
paulson@13790
   246
      ==> F : A leadsTo[CC] C"
paulson@13790
   247
by (blast intro: leadsETo_Un leadsETo_weaken)
paulson@13790
   248
paulson@13790
   249
paulson@13790
   250
(*Binary union version*)
paulson@13790
   251
lemma leadsETo_Un_Un:
paulson@13790
   252
     "[| F : A leadsTo[CC] A';  F : B leadsTo[CC] B' |]  
paulson@13790
   253
      ==> F : (A Un B) leadsTo[CC] (A' Un B')"
paulson@13790
   254
by (blast intro: leadsETo_Un leadsETo_weaken_R)
paulson@13790
   255
paulson@13790
   256
paulson@13790
   257
(** The cancellation law **)
paulson@13790
   258
paulson@13790
   259
lemma leadsETo_cancel2:
paulson@13790
   260
     "[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B' |]  
paulson@13790
   261
      ==> F : A leadsTo[CC] (A' Un B')"
paulson@13790
   262
by (blast intro: leadsETo_Un_Un subset_imp_leadsETo leadsETo_Trans)
paulson@13790
   263
paulson@13790
   264
lemma leadsETo_cancel1:
paulson@13790
   265
     "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B' |]  
paulson@13790
   266
    ==> F : A leadsTo[CC] (B' Un A')"
paulson@13790
   267
apply (simp add: Un_commute)
paulson@13790
   268
apply (blast intro!: leadsETo_cancel2)
paulson@13790
   269
done
paulson@13790
   270
paulson@13790
   271
lemma leadsETo_cancel_Diff1:
paulson@13790
   272
     "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]  
paulson@13790
   273
    ==> F : A leadsTo[CC] (B' Un A')"
paulson@13790
   274
apply (rule leadsETo_cancel1)
paulson@13812
   275
 prefer 2 apply assumption
paulson@13812
   276
apply simp_all
paulson@13790
   277
done
paulson@13790
   278
paulson@13790
   279
paulson@13790
   280
(** PSP: Progress-Safety-Progress **)
paulson@13790
   281
paulson@13790
   282
(*Special case of PSP: Misra's "stable conjunction"*)
paulson@13790
   283
lemma e_psp_stable: 
paulson@13790
   284
   "[| F : A leadsTo[CC] A';  F : stable B;  ALL C:CC. C Int B : CC |]  
paulson@13790
   285
    ==> F : (A Int B) leadsTo[CC] (A' Int B)"
paulson@13790
   286
apply (unfold stable_def)
paulson@13790
   287
apply (erule leadsETo_induct)
paulson@13790
   288
prefer 3 apply (blast intro: leadsETo_Union_Int)
paulson@13790
   289
prefer 2 apply (blast intro: leadsETo_Trans)
paulson@13790
   290
apply (rule leadsETo_Basis)
paulson@13790
   291
prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric])
paulson@13819
   292
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] 
paulson@13819
   293
                 Int_Un_distrib2 [symmetric])
paulson@13790
   294
apply (blast intro: transient_strengthen constrains_Int)
paulson@13790
   295
done
paulson@13790
   296
paulson@13790
   297
lemma e_psp_stable2:
paulson@13790
   298
     "[| F : A leadsTo[CC] A'; F : stable B;  ALL C:CC. C Int B : CC |]  
paulson@13790
   299
      ==> F : (B Int A) leadsTo[CC] (B Int A')"
paulson@13790
   300
by (simp (no_asm_simp) add: e_psp_stable Int_ac)
paulson@13790
   301
paulson@13790
   302
lemma e_psp:
paulson@13790
   303
     "[| F : A leadsTo[CC] A'; F : B co B';   
paulson@13790
   304
         ALL C:CC. C Int B Int B' : CC |]  
paulson@13790
   305
      ==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))"
paulson@13790
   306
apply (erule leadsETo_induct)
paulson@13790
   307
prefer 3 apply (blast intro: leadsETo_Union_Int)
paulson@13790
   308
(*Transitivity case has a delicate argument involving "cancellation"*)
paulson@13790
   309
apply (rule_tac [2] leadsETo_Un_duplicate2)
paulson@13790
   310
apply (erule_tac [2] leadsETo_cancel_Diff1)
paulson@13790
   311
prefer 2
paulson@13790
   312
 apply (simp add: Int_Diff Diff_triv)
paulson@13790
   313
 apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset)
paulson@13790
   314
(*Basis case*)
paulson@13790
   315
apply (rule leadsETo_Basis)
paulson@13790
   316
apply (blast intro: psp_ensures)
paulson@13790
   317
apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'")
paulson@13790
   318
apply auto
paulson@13790
   319
done
paulson@13790
   320
paulson@13790
   321
lemma e_psp2:
paulson@13790
   322
     "[| F : A leadsTo[CC] A'; F : B co B';   
paulson@13790
   323
         ALL C:CC. C Int B Int B' : CC |]  
paulson@13790
   324
      ==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))"
paulson@13790
   325
by (simp add: e_psp Int_ac)
paulson@13790
   326
paulson@13790
   327
paulson@13790
   328
(*** Special properties involving the parameter [CC] ***)
paulson@13790
   329
paulson@13790
   330
(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
paulson@13790
   331
lemma gen_leadsETo_imp_Join_leadsETo:
paulson@13790
   332
     "[| F: (A leadsTo[givenBy v] B);  G : preserves v;   
paulson@13819
   333
         F\<squnion>G : stable C |]  
paulson@13819
   334
      ==> F\<squnion>G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
paulson@13790
   335
apply (erule leadsETo_induct)
paulson@13790
   336
  prefer 3
paulson@13790
   337
  apply (subst Int_Union) 
paulson@13790
   338
  apply (blast intro: leadsETo_UN)
paulson@13790
   339
prefer 2
paulson@13790
   340
 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
paulson@13790
   341
apply (rule leadsETo_Basis)
paulson@13819
   342
apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] 
paulson@13819
   343
                      Int_Diff ensures_def givenBy_eq_Collect Join_transient)
paulson@13790
   344
prefer 3 apply (blast intro: transient_strengthen)
paulson@13790
   345
apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
paulson@13790
   346
apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
paulson@13790
   347
apply (unfold stable_def)
paulson@13790
   348
apply (blast intro: constrains_Int [THEN constrains_weaken])+
paulson@13790
   349
done
paulson@13790
   350
paulson@13790
   351
(**** Relationship with traditional "leadsTo", strong & weak ****)
paulson@13790
   352
paulson@13790
   353
(** strong **)
paulson@13790
   354
paulson@13790
   355
lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)"
paulson@13790
   356
apply safe
paulson@13790
   357
apply (erule leadsETo_induct)
paulson@13819
   358
  prefer 3 apply (blast intro: leadsTo_Union)
paulson@13819
   359
 prefer 2 apply (blast intro: leadsTo_Trans, blast)
paulson@13790
   360
done
paulson@13790
   361
paulson@13790
   362
lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)"
paulson@13790
   363
apply safe
paulson@13790
   364
apply (erule leadsETo_subset_leadsTo [THEN subsetD])
paulson@13790
   365
(*right-to-left case*)
paulson@13790
   366
apply (erule leadsTo_induct)
paulson@13819
   367
  prefer 3 apply (blast intro: leadsETo_Union)
paulson@13819
   368
 prefer 2 apply (blast intro: leadsETo_Trans, blast)
paulson@13790
   369
done
paulson@13790
   370
paulson@13790
   371
(**** weak ****)
paulson@13790
   372
paulson@13790
   373
lemma LeadsETo_eq_leadsETo: 
paulson@13790
   374
     "A LeadsTo[CC] B =  
paulson@13790
   375
        {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC]  
paulson@13790
   376
        (reachable F Int B)}"
paulson@13790
   377
apply (unfold LeadsETo_def)
paulson@13790
   378
apply (blast dest: e_psp_stable2 intro: leadsETo_weaken)
paulson@13790
   379
done
paulson@13790
   380
paulson@13790
   381
(*** Introduction rules: Basis, Trans, Union ***)
paulson@13790
   382
paulson@13790
   383
lemma LeadsETo_Trans:
paulson@13790
   384
     "[| F : A LeadsTo[CC] B;  F : B LeadsTo[CC] C |]  
paulson@13790
   385
      ==> F : A LeadsTo[CC] C"
paulson@13790
   386
apply (simp add: LeadsETo_eq_leadsETo)
paulson@13790
   387
apply (blast intro: leadsETo_Trans)
paulson@13790
   388
done
paulson@13790
   389
paulson@13790
   390
lemma LeadsETo_Union:
paulson@13790
   391
     "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
paulson@13790
   392
apply (simp add: LeadsETo_def)
paulson@13790
   393
apply (subst Int_Union)
paulson@13790
   394
apply (blast intro: leadsETo_UN)
paulson@13790
   395
done
paulson@13790
   396
paulson@13790
   397
lemma LeadsETo_UN:
paulson@13790
   398
     "(!!i. i : I ==> F : (A i) LeadsTo[CC] B)  
paulson@13790
   399
      ==> F : (UN i:I. A i) LeadsTo[CC] B"
paulson@13790
   400
apply (simp only: Union_image_eq [symmetric])
paulson@13790
   401
apply (blast intro: LeadsETo_Union)
paulson@13790
   402
done
paulson@13790
   403
paulson@13790
   404
(*Binary union introduction rule*)
paulson@13790
   405
lemma LeadsETo_Un:
paulson@13790
   406
     "[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]  
paulson@13790
   407
      ==> F : (A Un B) LeadsTo[CC] C"
haftmann@44106
   408
  using LeadsETo_Union [of "{A, B}" F CC C] by auto
paulson@13790
   409
paulson@13790
   410
(*Lets us look at the starting state*)
paulson@13790
   411
lemma single_LeadsETo_I:
paulson@13790
   412
     "(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B"
paulson@13819
   413
by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
paulson@13790
   414
paulson@13790
   415
lemma subset_imp_LeadsETo:
paulson@13790
   416
     "A <= B ==> F : A LeadsTo[CC] B"
paulson@13790
   417
apply (simp (no_asm) add: LeadsETo_def)
paulson@13790
   418
apply (blast intro: subset_imp_leadsETo)
paulson@13790
   419
done
paulson@13790
   420
wenzelm@45605
   421
lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
paulson@13790
   422
paulson@13798
   423
lemma LeadsETo_weaken_R [rule_format]:
paulson@13790
   424
     "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
paulson@13790
   425
apply (simp (no_asm_use) add: LeadsETo_def)
paulson@13790
   426
apply (blast intro: leadsETo_weaken_R)
paulson@13790
   427
done
paulson@13790
   428
paulson@13798
   429
lemma LeadsETo_weaken_L [rule_format]:
paulson@13790
   430
     "[| F : A LeadsTo[CC] A';  B <= A |] ==> F : B LeadsTo[CC] A'"
paulson@13790
   431
apply (simp (no_asm_use) add: LeadsETo_def)
paulson@13790
   432
apply (blast intro: leadsETo_weaken_L)
paulson@13790
   433
done
paulson@13790
   434
paulson@13790
   435
lemma LeadsETo_weaken:
paulson@13790
   436
     "[| F : A LeadsTo[CC'] A';    
paulson@13790
   437
         B <= A;  A' <= B';  CC' <= CC |]  
paulson@13790
   438
      ==> F : B LeadsTo[CC] B'"
paulson@13790
   439
apply (simp (no_asm_use) add: LeadsETo_def)
paulson@13790
   440
apply (blast intro: leadsETo_weaken)
paulson@13790
   441
done
paulson@13790
   442
paulson@13790
   443
lemma LeadsETo_subset_LeadsTo: "(A LeadsTo[CC] B) <= (A LeadsTo B)"
paulson@13790
   444
apply (unfold LeadsETo_def LeadsTo_def)
paulson@13790
   445
apply (blast intro: leadsETo_subset_leadsTo [THEN subsetD])
paulson@13790
   446
done
paulson@13790
   447
paulson@13790
   448
(*Postcondition can be strengthened to (reachable F Int B) *)
paulson@13790
   449
lemma reachable_ensures:
paulson@13790
   450
     "F : A ensures B ==> F : (reachable F Int A) ensures B"
paulson@13790
   451
apply (rule stable_ensures_Int [THEN ensures_weaken_R], auto)
paulson@13790
   452
done
paulson@13790
   453
paulson@13790
   454
lemma lel_lemma:
paulson@13790
   455
     "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
paulson@13790
   456
apply (erule leadsTo_induct)
paulson@13790
   457
  apply (blast intro: reachable_ensures leadsETo_Basis)
paulson@13790
   458
 apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
paulson@13790
   459
apply (subst Int_Union)
paulson@13790
   460
apply (blast intro: leadsETo_UN)
paulson@13790
   461
done
paulson@13790
   462
paulson@13790
   463
lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)"
paulson@13790
   464
apply safe
paulson@13790
   465
apply (erule LeadsETo_subset_LeadsTo [THEN subsetD])
paulson@13790
   466
(*right-to-left case*)
paulson@13790
   467
apply (unfold LeadsETo_def LeadsTo_def)
paulson@13836
   468
apply (blast intro: lel_lemma [THEN leadsETo_weaken])
paulson@13790
   469
done
paulson@13790
   470
paulson@13790
   471
paulson@13790
   472
(**** EXTEND/PROJECT PROPERTIES ****)
paulson@13790
   473
paulson@13819
   474
lemma (in Extend) givenBy_o_eq_extend_set:
paulson@13819
   475
     "givenBy (v o f) = extend_set h ` (givenBy v)"
paulson@13836
   476
apply (simp add: givenBy_eq_Collect)
paulson@13836
   477
apply (rule equalityI, best)
paulson@13836
   478
apply blast 
paulson@13836
   479
done
paulson@13790
   480
paulson@13790
   481
lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
paulson@13836
   482
by (simp add: givenBy_eq_Collect, best)
paulson@13790
   483
paulson@13790
   484
lemma (in Extend) extend_set_givenBy_I:
paulson@13790
   485
     "D : givenBy v ==> extend_set h D : givenBy (v o f)"
paulson@13836
   486
apply (simp (no_asm_use) add: givenBy_eq_all, blast)
paulson@13790
   487
done
paulson@13790
   488
paulson@13790
   489
lemma (in Extend) leadsETo_imp_extend_leadsETo:
paulson@13790
   490
     "F : A leadsTo[CC] B  
paulson@13790
   491
      ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]  
paulson@13790
   492
                       (extend_set h B)"
paulson@13790
   493
apply (erule leadsETo_induct)
paulson@13790
   494
  apply (force intro: leadsETo_Basis subset_imp_ensures 
paulson@13790
   495
               simp add: extend_ensures extend_set_Diff_distrib [symmetric])
paulson@13790
   496
 apply (blast intro: leadsETo_Trans)
paulson@13790
   497
apply (simp add: leadsETo_UN extend_set_Union)
paulson@13790
   498
done
paulson@13790
   499
paulson@13790
   500
paulson@13790
   501
(*This version's stronger in the "ensures" precondition
paulson@13790
   502
  BUT there's no ensures_weaken_L*)
paulson@13790
   503
lemma (in Extend) Join_project_ensures_strong:
paulson@13790
   504
     "[| project h C G ~: transient (project_set h C Int (A-B)) |  
paulson@13790
   505
           project_set h C Int (A - B) = {};   
paulson@13819
   506
         extend h F\<squnion>G : stable C;   
paulson@13819
   507
         F\<squnion>project h C G : (project_set h C Int A) ensures B |]  
paulson@13819
   508
      ==> extend h F\<squnion>G : (C Int extend_set h A) ensures (extend_set h B)"
paulson@13790
   509
apply (subst Int_extend_set_lemma [symmetric])
paulson@13790
   510
apply (rule Join_project_ensures)
paulson@13790
   511
apply (auto simp add: Int_Diff)
paulson@13790
   512
done
paulson@13790
   513
paulson@13812
   514
(*NOT WORKING.  MODIFY AS IN Project.thy
paulson@13790
   515
lemma (in Extend) pld_lemma:
paulson@13819
   516
     "[| extend h F\<squnion>G : stable C;   
paulson@13819
   517
         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
   518
         G : preserves (v o f) |]  
paulson@13819
   519
      ==> extend h F\<squnion>G :  
paulson@13790
   520
            (C Int extend_set h (project_set h C Int A))  
paulson@13790
   521
            leadsTo[(%D. C Int extend_set h D)`givenBy v]  (extend_set h B)"
paulson@13790
   522
apply (erule leadsETo_induct)
paulson@13790
   523
  prefer 3
paulson@13790
   524
  apply (simp del: UN_simps add: Int_UN_distrib leadsETo_UN extend_set_Union)
paulson@13790
   525
 prefer 2
paulson@13790
   526
 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
paulson@13790
   527
txt{*Base case is hard*}
paulson@13790
   528
apply auto
paulson@13790
   529
apply (force intro: leadsETo_Basis subset_imp_ensures)
paulson@13790
   530
apply (rule leadsETo_Basis)
paulson@13790
   531
 prefer 2
paulson@13790
   532
 apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
paulson@13790
   533
apply (rule Join_project_ensures_strong)
paulson@13812
   534
apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
paulson@13790
   535
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
   536
done
paulson@13790
   537
paulson@13790
   538
lemma (in Extend) project_leadsETo_D_lemma:
paulson@13819
   539
     "[| extend h F\<squnion>G : stable C;   
paulson@13819
   540
         F\<squnion>project h C G :  
paulson@13790
   541
             (project_set h C Int A)  
paulson@13790
   542
             leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
paulson@13790
   543
         G : preserves (v o f) |]  
paulson@13819
   544
      ==> extend h F\<squnion>G : (C Int extend_set h A)  
paulson@13790
   545
            leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
paulson@13790
   546
apply (rule pld_lemma [THEN leadsETo_weaken])
paulson@13790
   547
apply (auto simp add: split_extended_all)
paulson@13790
   548
done
paulson@13790
   549
paulson@13790
   550
lemma (in Extend) project_leadsETo_D:
paulson@13819
   551
     "[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B;   
paulson@13790
   552
         G : preserves (v o f) |]   
paulson@13819
   553
      ==> extend h F\<squnion>G : (extend_set h A)  
paulson@13790
   554
            leadsTo[givenBy (v o f)] (extend_set h B)"
paulson@13790
   555
apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto) 
paulson@13790
   556
apply (erule leadsETo_givenBy)
paulson@13790
   557
apply (rule givenBy_o_eq_extend_set [THEN equalityD2])
paulson@13790
   558
done
paulson@13790
   559
paulson@13790
   560
lemma (in Extend) project_LeadsETo_D:
paulson@13819
   561
     "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G  
paulson@13790
   562
             : A LeadsTo[givenBy v] B;   
paulson@13790
   563
         G : preserves (v o f) |]  
paulson@13819
   564
      ==> extend h F\<squnion>G :  
paulson@13790
   565
            (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)"
paulson@13790
   566
apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma])
paulson@13790
   567
apply (auto simp add: LeadsETo_def)
paulson@13790
   568
 apply (erule leadsETo_mono [THEN [2] rev_subsetD])
paulson@13790
   569
 apply (blast intro: extend_set_givenBy_I)
paulson@13790
   570
apply (simp add: project_set_reachable_extend_eq [symmetric])
paulson@13790
   571
done
paulson@13790
   572
paulson@13790
   573
lemma (in Extend) extending_leadsETo: 
paulson@13790
   574
     "(ALL G. extend h F ok G --> G : preserves (v o f))  
paulson@13790
   575
      ==> extending (%G. UNIV) h F  
paulson@13790
   576
                (extend_set h A leadsTo[givenBy (v o f)] extend_set h B)  
paulson@13790
   577
                (A leadsTo[givenBy v] B)"
paulson@13790
   578
apply (unfold extending_def)
paulson@13790
   579
apply (auto simp add: project_leadsETo_D)
paulson@13790
   580
done
paulson@13790
   581
paulson@13790
   582
lemma (in Extend) extending_LeadsETo: 
paulson@13790
   583
     "(ALL G. extend h F ok G --> G : preserves (v o f))  
paulson@13819
   584
      ==> extending (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   585
                (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)  
paulson@13790
   586
                (A LeadsTo[givenBy v]  B)"
paulson@13790
   587
apply (unfold extending_def)
paulson@13790
   588
apply (blast intro: project_LeadsETo_D)
paulson@13790
   589
done
paulson@13812
   590
*)
paulson@13790
   591
paulson@13790
   592
paulson@13790
   593
(*** leadsETo in the precondition ***)
paulson@13790
   594
paulson@13790
   595
(*Lemma for the Trans case*)
paulson@13790
   596
lemma (in Extend) pli_lemma:
paulson@13819
   597
     "[| extend h F\<squnion>G : stable C;     
paulson@13819
   598
         F\<squnion>project h C G     
paulson@13790
   599
           : project_set h C Int project_set h A leadsTo project_set h B |]  
paulson@13819
   600
      ==> F\<squnion>project h C G     
paulson@13790
   601
            : project_set h C Int project_set h A leadsTo     
paulson@13790
   602
              project_set h C Int project_set h B"
paulson@13790
   603
apply (rule psp_stable2 [THEN leadsTo_weaken_L])
paulson@13790
   604
apply (auto simp add: project_stable_project_set extend_stable_project_set)
paulson@13790
   605
done
paulson@13790
   606
paulson@13790
   607
lemma (in Extend) project_leadsETo_I_lemma:
paulson@13819
   608
     "[| extend h F\<squnion>G : stable C;   
paulson@13819
   609
         extend h F\<squnion>G :  
paulson@13790
   610
           (C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]   
paulson@13819
   611
  ==> F\<squnion>project h C G   
paulson@13790
   612
    : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
paulson@13790
   613
apply (erule leadsETo_induct)
paulson@13790
   614
  prefer 3
paulson@13790
   615
  apply (simp only: Int_UN_distrib project_set_Union)
paulson@13790
   616
  apply (blast intro: leadsTo_UN)
paulson@13790
   617
 prefer 2 apply (blast intro: leadsTo_Trans pli_lemma)
paulson@13790
   618
apply (simp add: givenBy_eq_extend_set)
paulson@13790
   619
apply (rule leadsTo_Basis)
paulson@13790
   620
apply (blast intro: ensures_extend_set_imp_project_ensures)
paulson@13790
   621
done
paulson@13790
   622
paulson@13790
   623
lemma (in Extend) project_leadsETo_I:
paulson@13819
   624
     "extend h F\<squnion>G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
paulson@13819
   625
      ==> F\<squnion>project h UNIV G : A leadsTo B"
paulson@13790
   626
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
paulson@13790
   627
done
paulson@13790
   628
paulson@13790
   629
lemma (in Extend) project_LeadsETo_I:
paulson@13819
   630
     "extend h F\<squnion>G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B) 
paulson@13819
   631
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G   
paulson@13790
   632
           : A LeadsTo B"
paulson@13790
   633
apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def)
paulson@13790
   634
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken])
paulson@13790
   635
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
paulson@13790
   636
done
paulson@13790
   637
paulson@13790
   638
lemma (in Extend) projecting_leadsTo: 
paulson@13790
   639
     "projecting (%G. UNIV) h F  
paulson@13790
   640
                 (extend_set h A leadsTo[givenBy f] extend_set h B)  
paulson@13790
   641
                 (A leadsTo B)"
paulson@13790
   642
apply (unfold projecting_def)
paulson@13790
   643
apply (force dest: project_leadsETo_I)
paulson@13790
   644
done
paulson@13790
   645
paulson@13790
   646
lemma (in Extend) projecting_LeadsTo: 
paulson@13819
   647
     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
paulson@13790
   648
                 (extend_set h A LeadsTo[givenBy f] extend_set h B)  
paulson@13790
   649
                 (A LeadsTo B)"
paulson@13790
   650
apply (unfold projecting_def)
paulson@13790
   651
apply (force dest: project_LeadsETo_I)
paulson@13790
   652
done
paulson@13790
   653
paulson@8044
   654
end