author | nipkow |
Tue, 09 Jan 2001 15:32:27 +0100 | |
changeset 10834 | a7897aebbffc |
parent 10064 | 1a77667b21ef |
child 11220 | db536a42dfc5 |
permissions | -rw-r--r-- |
5899 | 1 |
(* Title: HOL/UNITY/PPROD.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
5 |
|
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
6 |
Abstraction over replicated components (PLam) |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
7 |
General products of programs (Pi operation) |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
8 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
9 |
Some dead wood here! |
5899 | 10 |
*) |
11 |
||
12 |
(*** Basic properties ***) |
|
13 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
14 |
Goal "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
15 |
by (simp_tac (simpset() addsimps [PLam_def, lift_def, lift_set_def]) 1); |
6842 | 16 |
qed "Init_PLam"; |
5972 | 17 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
18 |
Addsimps [Init_PLam]; |
7947 | 19 |
|
6842 | 20 |
Goal "PLam {} F = SKIP"; |
21 |
by (simp_tac (simpset() addsimps [PLam_def]) 1); |
|
22 |
qed "PLam_empty"; |
|
5899 | 23 |
|
6842 | 24 |
Goal "(plam i: I. SKIP) = SKIP"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
25 |
by (simp_tac (simpset() addsimps [PLam_def,lift_SKIP,JN_constant]) 1); |
6842 | 26 |
qed "PLam_SKIP"; |
6299 | 27 |
|
6842 | 28 |
Addsimps [PLam_SKIP, PLam_empty]; |
5899 | 29 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
30 |
Goalw [PLam_def] "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"; |
5899 | 31 |
by Auto_tac; |
6842 | 32 |
qed "PLam_insert"; |
5899 | 33 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
34 |
Goal "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)"; |
7947 | 35 |
by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1); |
36 |
qed "PLam_component_iff"; |
|
37 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
38 |
Goalw [PLam_def] "i : I ==> lift i (F i) <= (PLam I F)"; |
5972 | 39 |
(*blast_tac doesn't use HO unification*) |
40 |
by (fast_tac (claset() addIs [component_JN]) 1); |
|
6842 | 41 |
qed "component_PLam"; |
5899 | 42 |
|
5972 | 43 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
44 |
(** Safety & Progress: but are they used anywhere? **) |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
45 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
46 |
Goal "[| i : I; ALL j. F j : preserves snd |] ==> \ |
8703 | 47 |
\ (PLam I F : (lift_set i (A <*> UNIV)) co \ |
48 |
\ (lift_set i (B <*> UNIV))) = \ |
|
49 |
\ (F i : (A <*> UNIV) co (B <*> UNIV))"; |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
50 |
by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
51 |
by (stac (insert_Diff RS sym) 1 THEN assume_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
52 |
by (asm_simp_tac (simpset() addsimps [lift_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
53 |
by (blast_tac (claset() addIs [constrains_imp_lift_constrains]) 1); |
6842 | 54 |
qed "PLam_constrains"; |
5899 | 55 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
56 |
Goal "[| i : I; ALL j. F j : preserves snd |] \ |
8703 | 57 |
\ ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = \ |
58 |
\ (F i : stable (A <*> UNIV))"; |
|
6842 | 59 |
by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1); |
60 |
qed "PLam_stable"; |
|
5972 | 61 |
|
7523 | 62 |
Goal "i : I ==> \ |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
63 |
\ PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"; |
7523 | 64 |
by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1); |
65 |
qed "PLam_transient"; |
|
66 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
67 |
(*This holds because the F j cannot change (lift_set i)*) |
8703 | 68 |
Goal "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV); \ |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
69 |
\ ALL j. F j : preserves snd |] ==> \ |
8703 | 70 |
\ PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"; |
7538 | 71 |
by (auto_tac (claset(), |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
72 |
simpset() addsimps [ensures_def, PLam_constrains, PLam_transient, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
73 |
lift_transient_eq_disj, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
74 |
lift_set_Un_distrib RS sym, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
75 |
lift_set_Diff_distrib RS sym, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
76 |
Times_Un_distrib1 RS sym, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
77 |
Times_Diff_distrib1 RS sym])); |
7538 | 78 |
qed "PLam_ensures"; |
79 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
80 |
Goal "[| i : I; \ |
8703 | 81 |
\ F i : ((A <*> UNIV) - (B <*> UNIV)) co \ |
82 |
\ ((A <*> UNIV) Un (B <*> UNIV)); \ |
|
83 |
\ F i : transient ((A <*> UNIV) - (B <*> UNIV)); \ |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
84 |
\ ALL j. F j : preserves snd |] ==> \ |
8703 | 85 |
\ PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"; |
7538 | 86 |
by (rtac (PLam_ensures RS leadsTo_Basis) 1); |
87 |
by (rtac ensuresI 2); |
|
88 |
by (ALLGOALS assume_tac); |
|
7523 | 89 |
qed "PLam_leadsTo_Basis"; |
5972 | 90 |
|
5899 | 91 |
|
5972 | 92 |
(** invariant **) |
93 |
||
8703 | 94 |
Goal "[| F i : invariant (A <*> UNIV); i : I; \ |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
95 |
\ ALL j. F j : preserves snd |] \ |
8703 | 96 |
\ ==> PLam I F : invariant (lift_set i (A <*> UNIV))"; |
5972 | 97 |
by (auto_tac (claset(), |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8703
diff
changeset
|
98 |
simpset() addsimps [PLam_stable, invariant_def])); |
6842 | 99 |
qed "invariant_imp_PLam_invariant"; |
5972 | 100 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
101 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
102 |
Goal "ALL j. F j : preserves snd \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
103 |
\ ==> (PLam I F : preserves (v o sub j o fst)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
104 |
\ (if j: I then F j : preserves (v o fst) else True)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
105 |
by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
106 |
by (Blast_tac 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
107 |
qed "PLam_preserves_fst"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
108 |
Addsimps [PLam_preserves_fst]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
109 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
110 |
Goal "ALL j. F j : preserves snd ==> PLam I F : preserves snd"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
111 |
by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_snd_I]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
112 |
qed "PLam_preserves_snd"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
113 |
Addsimps [PLam_preserves_snd]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
114 |
AddIs [PLam_preserves_snd]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
115 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
116 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
117 |
(*** guarantees properties ***) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
118 |
|
8327 | 119 |
(*This rule looks unsatisfactory because it refers to "lift". One must use |
120 |
lift_guarantees_eq_lift_inv to rewrite the first subgoal and |
|
121 |
something like lift_preserves_sub to rewrite the third. However there's |
|
122 |
no obvious way to alternative for the third premise.*) |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
123 |
Goalw [PLam_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
124 |
"[| lift i (F i): X guarantees Y; i : I; \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
125 |
\ OK I (%i. lift i (F i)) |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
126 |
\ ==> (PLam I F) : X guarantees Y"; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
127 |
by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8251
diff
changeset
|
128 |
qed "guarantees_PLam_I"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
129 |
|
10834 | 130 |
Goal "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
131 |
by (simp_tac (simpset() addsimps [PLam_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
132 |
qed "Allowed_PLam"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
133 |
Addsimps [Allowed_PLam]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
134 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
135 |
Goal "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
136 |
by (simp_tac (simpset() addsimps [PLam_def, lift_def, rename_preserves]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
137 |
qed "PLam_preserves"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
138 |
Addsimps [PLam_preserves]; |
5972 | 139 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
140 |
(**UNUSED |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
141 |
(*The f0 premise ensures that the product is well-defined.*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
142 |
Goal "[| PLam I F : invariant (lift_set i A); i : I; \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
143 |
\ f0: Init (PLam I F) |] ==> F i : invariant A"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
144 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
145 |
simpset() addsimps [invariant_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
146 |
by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
147 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
148 |
qed "PLam_invariant_imp_invariant"; |
5899 | 149 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
150 |
Goal "[| i : I; f0: Init (PLam I F) |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
151 |
\ ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
152 |
by (blast_tac (claset() addIs [invariant_imp_PLam_invariant, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
153 |
PLam_invariant_imp_invariant]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
154 |
qed "PLam_invariant"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
155 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
156 |
(*The f0 premise isn't needed if F is a constant program because then |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
157 |
we get an initial state by replicating that of F*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
158 |
Goal "i : I \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
159 |
\ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
160 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
161 |
simpset() addsimps [invariant_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
162 |
qed "const_PLam_invariant"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
163 |
**) |
5972 | 164 |
|
5899 | 165 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
166 |
(**UNUSED |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
167 |
(** Reachability **) |
5972 | 168 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
169 |
Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
170 |
by (etac reachable.induct 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
171 |
by (auto_tac (claset() addIs reachable.intrs, simpset())); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
172 |
qed "reachable_PLam"; |
5899 | 173 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
174 |
(*Result to justify a re-organization of this file*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
175 |
Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
176 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
177 |
result(); |
6842 | 178 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
179 |
Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
180 |
by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
181 |
qed "reachable_PLam_subset1"; |
5899 | 182 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
183 |
(*simplify using reachable_lift??*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
184 |
Goal "[| i ~: I; A : reachable (F i) |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
185 |
\ ==> ALL f. f : reachable (PLam I F) \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
186 |
\ --> f(i:=A) : reachable (lift i (F i) Join PLam I F)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
187 |
by (etac reachable.induct 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
188 |
by (ALLGOALS Clarify_tac); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
189 |
by (etac reachable.induct 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
190 |
(*Init, Init case*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
191 |
by (force_tac (claset() addIs reachable.intrs, simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
192 |
(*Init of F, action of PLam F case*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
193 |
by (res_inst_tac [("act","act")] reachable.Acts 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
194 |
by (Force_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
195 |
by (assume_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
196 |
by (force_tac (claset() addIs [ext], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
197 |
(*induction over the 2nd "reachable" assumption*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
198 |
by (eres_inst_tac [("xa","f")] reachable.induct 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
199 |
(*Init of PLam F, action of F case*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
200 |
by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
201 |
by (Force_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
202 |
by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
203 |
by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
204 |
(*last case: an action of PLam I F*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
205 |
by (res_inst_tac [("act","acta")] reachable.Acts 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
206 |
by (Force_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
207 |
by (assume_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
208 |
by (force_tac (claset() addIs [ext], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
209 |
qed_spec_mp "reachable_lift_Join_PLam"; |
5899 | 210 |
|
211 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
212 |
(*The index set must be finite: otherwise infinitely many copies of F can |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
213 |
perform actions, and PLam can never catch up in finite time.*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
214 |
Goal "finite I \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
215 |
\ ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
216 |
by (etac finite_induct 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
217 |
by (Simp_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
218 |
by (force_tac (claset() addDs [reachable_lift_Join_PLam], |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
219 |
simpset() addsimps [PLam_insert]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
220 |
qed "reachable_PLam_subset2"; |
5972 | 221 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
222 |
Goal "finite I ==> \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
223 |
\ reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
224 |
by (REPEAT_FIRST (ares_tac [equalityI, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
225 |
reachable_PLam_subset1, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
226 |
reachable_PLam_subset2])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
227 |
qed "reachable_PLam_eq"; |
5899 | 228 |
|
229 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
230 |
(** Co **) |
5972 | 231 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
232 |
Goal "[| F i : A Co B; i: I; finite I |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
233 |
\ ==> PLam I F : (lift_set i A) Co (lift_set i B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
234 |
by (auto_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
235 |
(claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
236 |
simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
237 |
reachable_PLam_eq])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
238 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
239 |
simpset() addsimps [constrains_def, PLam_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
240 |
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
241 |
qed "Constrains_imp_PLam_Constrains"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
242 |
|
5899 | 243 |
|
244 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
245 |
Goal "[| i: I; finite I; f0: Init (PLam I F) |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
246 |
\ ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
247 |
\ (F i : A Co B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
248 |
by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
249 |
PLam_Constrains_imp_Constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
250 |
qed "PLam_Constrains"; |
5972 | 251 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
252 |
Goal "[| i: I; finite I; f0: Init (PLam I F) |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
253 |
\ ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
254 |
by (asm_simp_tac (simpset() delsimps [Init_PLam] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
255 |
addsimps [Stable_def, PLam_Constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
256 |
qed "PLam_Stable"; |
5972 | 257 |
|
258 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
259 |
(** const_PLam (no dependence on i) doesn't require the f0 premise **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
260 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
261 |
Goal "[| i: I; finite I |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
262 |
\ ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
263 |
\ (F : A Co B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
264 |
by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
265 |
const_PLam_Constrains_imp_Constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
266 |
qed "const_PLam_Constrains"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
267 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
268 |
Goal "[| i: I; finite I |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
269 |
\ ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
270 |
by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
271 |
qed "const_PLam_Stable"; |
5972 | 272 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
273 |
Goalw [Increasing_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
274 |
"[| i: I; finite I |] \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
275 |
\ ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
276 |
by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
277 |
by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
278 |
by (asm_full_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
279 |
(simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
280 |
qed "const_PLam_Increasing"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
281 |
**) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8065
diff
changeset
|
282 |