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