1 (* Title: ZF/UNITY/Increasing |
1 (* Title: ZF/UNITY/Increasing |
2 ID: $Id$ |
2 ID: $Id \<in> Increasing.thy,v 1.2 2003/06/02 09:17:52 paulson Exp $ |
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4 Copyright 2001 University of Cambridge |
4 Copyright 2001 University of Cambridge |
5 |
|
6 The "Increasing" relation of Charpentier. |
|
7 |
5 |
8 Increasing's parameters are a state function f, a domain A and an order |
6 Increasing's parameters are a state function f, a domain A and an order |
9 relation r over the domain A. |
7 relation r over the domain A. |
10 *) |
8 *) |
11 |
9 |
12 Increasing = Constrains + Monotonicity + |
10 header{*Charpentier's "Increasing" Relation*} |
|
11 |
|
12 theory Increasing = Constrains + Monotonicity: |
|
13 |
13 constdefs |
14 constdefs |
14 |
15 |
15 increasing :: [i, i, i=>i] => i ("increasing[_]'(_, _')") |
16 increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')") |
16 "increasing[A](r, f) == |
17 "increasing[A](r, f) == |
17 {F:program. (ALL k:A. F: stable({s:state. <k, f(s)>:r})) & |
18 {F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) & |
18 (ALL x:state. f(x):A)}" |
19 (\<forall>x \<in> state. f(x):A)}" |
19 |
20 |
20 Increasing :: [i, i, i=>i] => i ("Increasing[_]'(_, _')") |
21 Increasing :: "[i, i, i=>i] => i" ("Increasing[_]'(_, _')") |
21 "Increasing[A](r, f) == |
22 "Increasing[A](r, f) == |
22 {F:program. (ALL k:A. F:Stable({s:state. <k, f(s)>:r})) & |
23 {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) & |
23 (ALL x:state. f(x):A)}" |
24 (\<forall>x \<in> state. f(x):A)}" |
24 |
25 |
25 syntax |
26 syntax |
26 IncWrt :: [i=>i, i, i] => i ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60) |
27 IncWrt :: "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60) |
27 |
28 |
28 translations |
29 translations |
29 "IncWrt(f,r,A)" => "Increasing[A](r,f)" |
30 "IncWrt(f,r,A)" => "Increasing[A](r,f)" |
30 |
31 |
|
32 |
|
33 (** increasing **) |
|
34 |
|
35 lemma increasing_type: "increasing[A](r, f) <= program" |
|
36 by (unfold increasing_def, blast) |
|
37 |
|
38 lemma increasing_into_program: "F \<in> increasing[A](r, f) ==> F \<in> program" |
|
39 by (unfold increasing_def, blast) |
|
40 |
|
41 lemma increasing_imp_stable: |
|
42 "[| F \<in> increasing[A](r, f); x \<in> A |] ==>F \<in> stable({s \<in> state. <x, f(s)>:r})" |
|
43 by (unfold increasing_def, blast) |
|
44 |
|
45 lemma increasingD: |
|
46 "F \<in> increasing[A](r,f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)" |
|
47 apply (unfold increasing_def) |
|
48 apply (subgoal_tac "\<exists>x. x \<in> state") |
|
49 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) |
|
50 done |
|
51 |
|
52 lemma increasing_constant [simp]: |
|
53 "F \<in> increasing[A](r, %s. c) <-> F \<in> program & c \<in> A" |
|
54 apply (unfold increasing_def stable_def) |
|
55 apply (subgoal_tac "\<exists>x. x \<in> state") |
|
56 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) |
|
57 done |
|
58 |
|
59 lemma subset_increasing_comp: |
|
60 "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> |
|
61 increasing[A](r, f) <= increasing[B](s, g comp f)" |
|
62 apply (unfold increasing_def stable_def part_order_def |
|
63 constrains_def mono1_def metacomp_def, clarify, simp) |
|
64 apply clarify |
|
65 apply (subgoal_tac "xa \<in> state") |
|
66 prefer 2 apply (blast dest!: ActsD) |
|
67 apply (subgoal_tac "<f (xb), f (xb) >:r") |
|
68 prefer 2 apply (force simp add: refl_def) |
|
69 apply (rotate_tac 5) |
|
70 apply (drule_tac x = "f (xb) " in bspec) |
|
71 apply (rotate_tac [2] -1) |
|
72 apply (drule_tac [2] x = act in bspec, simp_all) |
|
73 apply (drule_tac A = "act``?u" and c = xa in subsetD, blast) |
|
74 apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec]) |
|
75 apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD) |
|
76 apply simp_all |
|
77 done |
|
78 |
|
79 lemma imp_increasing_comp: |
|
80 "[| F \<in> increasing[A](r, f); mono1(A, r, B, s, g); |
|
81 refl(A, r); trans[B](s) |] ==> F \<in> increasing[B](s, g comp f)" |
|
82 by (rule subset_increasing_comp [THEN subsetD], auto) |
|
83 |
|
84 lemma strict_increasing: |
|
85 "increasing[nat](Le, f) <= increasing[nat](Lt, f)" |
|
86 by (unfold increasing_def Lt_def, auto) |
|
87 |
|
88 lemma strict_gt_increasing: |
|
89 "increasing[nat](Ge, f) <= increasing[nat](Gt, f)" |
|
90 apply (unfold increasing_def Gt_def Ge_def, auto) |
|
91 apply (erule natE) |
|
92 apply (auto simp add: stable_def) |
|
93 done |
|
94 |
|
95 (** Increasing **) |
|
96 |
|
97 lemma increasing_imp_Increasing: |
|
98 "F \<in> increasing[A](r, f) ==> F \<in> Increasing[A](r, f)" |
|
99 |
|
100 apply (unfold increasing_def Increasing_def) |
|
101 apply (auto intro: stable_imp_Stable) |
|
102 done |
|
103 |
|
104 lemma Increasing_type: "Increasing[A](r, f) <= program" |
|
105 by (unfold Increasing_def, auto) |
|
106 |
|
107 lemma Increasing_into_program: "F \<in> Increasing[A](r, f) ==> F \<in> program" |
|
108 by (unfold Increasing_def, auto) |
|
109 |
|
110 lemma Increasing_imp_Stable: |
|
111 "[| F \<in> Increasing[A](r, f); a \<in> A |] ==> F \<in> Stable({s \<in> state. <a,f(s)>:r})" |
|
112 by (unfold Increasing_def, blast) |
|
113 |
|
114 lemma IncreasingD: |
|
115 "F \<in> Increasing[A](r, f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)" |
|
116 apply (unfold Increasing_def) |
|
117 apply (subgoal_tac "\<exists>x. x \<in> state") |
|
118 apply (auto intro: st0_in_state) |
|
119 done |
|
120 |
|
121 lemma Increasing_constant [simp]: |
|
122 "F \<in> Increasing[A](r, %s. c) <-> F \<in> program & (c \<in> A)" |
|
123 apply (subgoal_tac "\<exists>x. x \<in> state") |
|
124 apply (auto dest!: IncreasingD intro: st0_in_state increasing_imp_Increasing) |
|
125 done |
|
126 |
|
127 lemma subset_Increasing_comp: |
|
128 "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> |
|
129 Increasing[A](r, f) <= Increasing[B](s, g comp f)" |
|
130 apply (unfold Increasing_def Stable_def Constrains_def part_order_def |
|
131 constrains_def mono1_def metacomp_def, safe) |
|
132 apply (simp_all add: ActsD) |
|
133 apply (subgoal_tac "xb \<in> state & xa \<in> state") |
|
134 prefer 2 apply (simp add: ActsD) |
|
135 apply (subgoal_tac "<f (xb), f (xb) >:r") |
|
136 prefer 2 apply (force simp add: refl_def) |
|
137 apply (rotate_tac 5) |
|
138 apply (drule_tac x = "f (xb) " in bspec) |
|
139 apply simp_all |
|
140 apply clarify |
|
141 apply (rotate_tac -2) |
|
142 apply (drule_tac x = act in bspec) |
|
143 apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, simp_all, blast) |
|
144 apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec]) |
|
145 apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD) |
|
146 apply simp_all |
|
147 done |
|
148 |
|
149 lemma imp_Increasing_comp: |
|
150 "[| F \<in> Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] |
|
151 ==> F \<in> Increasing[B](s, g comp f)" |
|
152 apply (rule subset_Increasing_comp [THEN subsetD], auto) |
|
153 done |
|
154 |
|
155 lemma strict_Increasing: "Increasing[nat](Le, f) <= Increasing[nat](Lt, f)" |
|
156 by (unfold Increasing_def Lt_def, auto) |
|
157 |
|
158 lemma strict_gt_Increasing: "Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)" |
|
159 apply (unfold Increasing_def Ge_def Gt_def, auto) |
|
160 apply (erule natE) |
|
161 apply (auto simp add: Stable_def) |
|
162 done |
|
163 |
|
164 (** Two-place monotone operations **) |
|
165 |
|
166 lemma imp_increasing_comp2: |
|
167 "[| F \<in> increasing[A](r, f); F \<in> increasing[B](s, g); |
|
168 mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] |
|
169 ==> F \<in> increasing[C](t, %x. h(f(x), g(x)))" |
|
170 apply (unfold increasing_def stable_def |
|
171 part_order_def constrains_def mono2_def, clarify, simp) |
|
172 apply clarify |
|
173 apply (rename_tac xa xb) |
|
174 apply (subgoal_tac "xb \<in> state & xa \<in> state") |
|
175 prefer 2 apply (blast dest!: ActsD) |
|
176 apply (subgoal_tac "<f (xb), f (xb) >:r & <g (xb), g (xb) >:s") |
|
177 prefer 2 apply (force simp add: refl_def) |
|
178 apply (rotate_tac 6) |
|
179 apply (drule_tac x = "f (xb) " in bspec) |
|
180 apply (rotate_tac [2] 1) |
|
181 apply (drule_tac [2] x = "g (xb) " in bspec) |
|
182 apply simp_all |
|
183 apply (rotate_tac -1) |
|
184 apply (drule_tac x = act in bspec) |
|
185 apply (rotate_tac [2] -3) |
|
186 apply (drule_tac [2] x = act in bspec, simp_all) |
|
187 apply (drule_tac A = "act``?u" and c = xa in subsetD) |
|
188 apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, blast, blast) |
|
189 apply (rotate_tac -4) |
|
190 apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec]) |
|
191 apply (rotate_tac [3] -1) |
|
192 apply (drule_tac [3] x = "g (xa) " and x1 = "g (xb) " in bspec [THEN bspec]) |
|
193 apply simp_all |
|
194 apply (rule_tac b = "h (f (xb), g (xb))" and A = C in trans_onD) |
|
195 apply simp_all |
|
196 done |
|
197 |
|
198 lemma imp_Increasing_comp2: |
|
199 "[| F \<in> Increasing[A](r, f); F \<in> Increasing[B](s, g); |
|
200 mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> |
|
201 F \<in> Increasing[C](t, %x. h(f(x), g(x)))" |
|
202 apply (unfold Increasing_def stable_def |
|
203 part_order_def constrains_def mono2_def Stable_def Constrains_def, safe) |
|
204 apply (simp_all add: ActsD) |
|
205 apply (subgoal_tac "xa \<in> state & x \<in> state") |
|
206 prefer 2 apply (blast dest!: ActsD) |
|
207 apply (subgoal_tac "<f (xa), f (xa) >:r & <g (xa), g (xa) >:s") |
|
208 prefer 2 apply (force simp add: refl_def) |
|
209 apply (rotate_tac 6) |
|
210 apply (drule_tac x = "f (xa) " in bspec) |
|
211 apply (rotate_tac [2] 1) |
|
212 apply (drule_tac [2] x = "g (xa) " in bspec) |
|
213 apply simp_all |
|
214 apply clarify |
|
215 apply (rotate_tac -2) |
|
216 apply (drule_tac x = act in bspec) |
|
217 apply (rotate_tac [2] -3) |
|
218 apply (drule_tac [2] x = act in bspec, simp_all) |
|
219 apply (drule_tac A = "act``?u" and c = x in subsetD) |
|
220 apply (drule_tac [2] A = "act``?u" and c = x in subsetD, blast, blast) |
|
221 apply (rotate_tac -9) |
|
222 apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec]) |
|
223 apply (rotate_tac [3] -1) |
|
224 apply (drule_tac [3] x = "g (x) " and x1 = "g (xa) " in bspec [THEN bspec]) |
|
225 apply simp_all |
|
226 apply (rule_tac b = "h (f (xa), g (xa))" and A = C in trans_onD) |
|
227 apply simp_all |
|
228 done |
|
229 |
31 |
230 |
32 end |
231 end |