src/HOL/MicroJava/BV/Semilat.thy
 author wenzelm Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) changeset 24850 0cfd722ab579 parent 23757 087b0a241557 child 25592 e8ddaf6bf5df permissions -rw-r--r--
Name.uu, Name.aT;
 kleing@12516 1 (* Title: HOL/MicroJava/BV/Semilat.thy kleing@10496 2 ID: $Id$ kleing@10496 3 Author: Tobias Nipkow kleing@10496 4 Copyright 2000 TUM kleing@10496 5 kleing@10496 6 Semilattices kleing@10496 7 *) kleing@10496 8 kleing@12911 9 header {* kleing@12911 10 \chapter{Bytecode Verifier}\label{cha:bv} kleing@12911 11 \isaheader{Semilattices} kleing@12911 12 *} kleing@10496 13 haftmann@16417 14 theory Semilat imports While_Combinator begin kleing@10496 15 kleing@13006 16 types 'a ord = "'a \ 'a \ bool" kleing@13006 17 'a binop = "'a \ 'a \ 'a" kleing@10496 18 'a sl = "'a set * 'a ord * 'a binop" kleing@10496 19 kleing@10496 20 consts kleing@13006 21 "@lesub" :: "'a \ 'a ord \ 'a \ bool" ("(_ /<='__ _)" [50, 1000, 51] 50) kleing@13006 22 "@lesssub" :: "'a \ 'a ord \ 'a \ bool" ("(_ /<'__ _)" [50, 1000, 51] 50) kleing@10496 23 defs kleing@10496 24 lesub_def: "x <=_r y == r x y" kleing@10496 25 lesssub_def: "x <_r y == x <=_r y & x ~= y" kleing@10496 26 kleing@13649 27 syntax (xsymbols) kleing@13649 28 "@lesub" :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) kleing@13649 29 kleing@10496 30 consts kleing@13006 31 "@plussub" :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /+'__ _)" [65, 1000, 66] 65) kleing@10496 32 defs kleing@10496 33 plussub_def: "x +_f y == f x y" kleing@10496 34 kleing@13649 35 syntax (xsymbols) kleing@13649 36 "@plussub" :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /+\<^sub>_ _)" [65, 1000, 66] 65) kleing@13649 37 kleing@13649 38 syntax (xsymbols) kleing@13649 39 "@plussub" :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /\\<^sub>_ _)" [65, 1000, 66] 65) kleing@13649 40 kleing@10496 41 kleing@10496 42 constdefs kleing@13006 43 order :: "'a ord \ bool" kleing@10496 44 "order r == (!x. x <=_r x) & kleing@13006 45 (!x y. x <=_r y & y <=_r x \ x=y) & kleing@13006 46 (!x y z. x <=_r y & y <=_r z \ x <=_r z)" kleing@10496 47 kleing@13006 48 acc :: "'a ord \ bool" berghofe@22271 49 "acc r == wfP (\y x. x <_r y)" kleing@10496 50 kleing@13006 51 top :: "'a ord \ 'a \ bool" kleing@10496 52 "top r T == !x. x <=_r T" kleing@10496 53 kleing@13006 54 closed :: "'a set \ 'a binop \ bool" kleing@10496 55 "closed A f == !x:A. !y:A. x +_f y : A" kleing@10496 56 kleing@13006 57 semilat :: "'a sl \ bool" kleing@10496 58 "semilat == %(A,r,f). order r & closed A f & kleing@10496 59 (!x:A. !y:A. x <=_r x +_f y) & kleing@10496 60 (!x:A. !y:A. y <=_r x +_f y) & kleing@13006 61 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \ x +_f y <=_r z)" kleing@10496 62 berghofe@22271 63 is_ub :: "'a ord \ 'a \ 'a \ 'a \ bool" berghofe@22271 64 "is_ub r x y u == r x u & r y u" kleing@10496 65 berghofe@22271 66 is_lub :: "'a ord \ 'a \ 'a \ 'a \ bool" berghofe@22271 67 "is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \ r u z)" kleing@10496 68 berghofe@22271 69 some_lub :: "'a ord \ 'a \ 'a \ 'a" nipkow@13074 70 "some_lub r x y == SOME z. is_lub r x y z"; kleing@10496 71 wenzelm@13365 72 locale (open) semilat = nipkow@13074 73 fixes A :: "'a set" nipkow@13074 74 and r :: "'a ord" nipkow@13074 75 and f :: "'a binop" nipkow@13074 76 assumes semilat: "semilat(A,r,f)" kleing@10496 77 kleing@10496 78 lemma order_refl [simp, intro]: kleing@13006 79 "order r \ x <=_r x"; kleing@10496 80 by (simp add: order_def) kleing@10496 81 kleing@10496 82 lemma order_antisym: kleing@13006 83 "\ order r; x <=_r y; y <=_r x \ \ x = y" kleing@10496 84 apply (unfold order_def) nipkow@13074 85 apply (simp (no_asm_simp)) kleing@10496 86 done kleing@10496 87 kleing@10496 88 lemma order_trans: kleing@13006 89 "\ order r; x <=_r y; y <=_r z \ \ x <=_r z" kleing@10496 90 apply (unfold order_def) kleing@10496 91 apply blast kleing@10496 92 done kleing@10496 93 kleing@10496 94 lemma order_less_irrefl [intro, simp]: kleing@13006 95 "order r \ ~ x <_r x" kleing@10496 96 apply (unfold order_def lesssub_def) kleing@10496 97 apply blast kleing@10496 98 done kleing@10496 99 kleing@10496 100 lemma order_less_trans: kleing@13006 101 "\ order r; x <_r y; y <_r z \ \ x <_r z" kleing@10496 102 apply (unfold order_def lesssub_def) kleing@10496 103 apply blast kleing@10496 104 done kleing@10496 105 kleing@10496 106 lemma topD [simp, intro]: kleing@13006 107 "top r T \ x <=_r T" kleing@10496 108 by (simp add: top_def) kleing@10496 109 kleing@10496 110 lemma top_le_conv [simp]: kleing@13006 111 "\ order r; top r T \ \ (T <=_r x) = (x = T)" kleing@10496 112 by (blast intro: order_antisym) kleing@10496 113 kleing@10496 114 lemma semilat_Def: kleing@10496 115 "semilat(A,r,f) == order r & closed A f & kleing@10496 116 (!x:A. !y:A. x <=_r x +_f y) & kleing@10496 117 (!x:A. !y:A. y <=_r x +_f y) & kleing@13006 118 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \ x +_f y <=_r z)" wenzelm@10918 119 apply (unfold semilat_def split_conv [THEN eq_reflection]) kleing@10496 120 apply (rule refl [THEN eq_reflection]) kleing@10496 121 done kleing@10496 122 nipkow@13074 123 lemma (in semilat) orderI [simp, intro]: nipkow@13074 124 "order r" nipkow@13074 125 by (insert semilat) (simp add: semilat_Def) nipkow@13074 126 nipkow@13074 127 lemma (in semilat) closedI [simp, intro]: nipkow@13074 128 "closed A f" nipkow@13074 129 by (insert semilat) (simp add: semilat_Def) nipkow@13074 130 kleing@13077 131 lemma closedD: kleing@13077 132 "\ closed A f; x:A; y:A \ \ x +_f y : A" kleing@13077 133 by (unfold closed_def) blast kleing@13077 134 kleing@13077 135 lemma closed_UNIV [simp]: "closed UNIV f" kleing@13077 136 by (simp add: closed_def) kleing@13077 137 kleing@13077 138 kleing@13077 139 lemma (in semilat) closed_f [simp, intro]: kleing@13077 140 "\x:A; y:A\ \ x +_f y : A" kleing@13077 141 by (simp add: closedD [OF closedI]) kleing@13077 142 kleing@13077 143 lemma (in semilat) refl_r [intro, simp]: kleing@13077 144 "x <=_r x" kleing@13077 145 by simp kleing@13077 146 kleing@13077 147 lemma (in semilat) antisym_r [intro?]: kleing@13077 148 "\ x <=_r y; y <=_r x \ \ x = y" kleing@13077 149 by (rule order_antisym) auto kleing@13077 150 kleing@13077 151 lemma (in semilat) trans_r [trans, intro?]: kleing@13077 152 "\x <=_r y; y <=_r z\ \ x <=_r z" kleing@13077 153 by (auto intro: order_trans) kleing@13077 154 kleing@13077 155 kleing@13077 156 lemma (in semilat) ub1 [simp, intro?]: nipkow@13074 157 "\ x:A; y:A \ \ x <=_r x +_f y" nipkow@13074 158 by (insert semilat) (unfold semilat_Def, simp) nipkow@13074 159 kleing@13077 160 lemma (in semilat) ub2 [simp, intro?]: nipkow@13074 161 "\ x:A; y:A \ \ y <=_r x +_f y" nipkow@13074 162 by (insert semilat) (unfold semilat_Def, simp) kleing@10496 163 kleing@13077 164 lemma (in semilat) lub [simp, intro?]: nipkow@13074 165 "\ x <=_r z; y <=_r z; x:A; y:A; z:A \ \ x +_f y <=_r z"; nipkow@13074 166 by (insert semilat) (unfold semilat_Def, simp) nipkow@13074 167 nipkow@13074 168 nipkow@13074 169 lemma (in semilat) plus_le_conv [simp]: nipkow@13074 170 "\ x:A; y:A; z:A \ \ (x +_f y <=_r z) = (x <=_r z & y <=_r z)" kleing@13077 171 by (blast intro: ub1 ub2 lub order_trans) nipkow@13074 172 nipkow@13074 173 lemma (in semilat) le_iff_plus_unchanged: nipkow@13074 174 "\ x:A; y:A \ \ (x <=_r y) = (x +_f y = y)" nipkow@13074 175 apply (rule iffI) kleing@13077 176 apply (blast intro: antisym_r refl_r lub ub2) nipkow@13074 177 apply (erule subst) kleing@10496 178 apply simp kleing@10496 179 done kleing@10496 180 nipkow@13074 181 lemma (in semilat) le_iff_plus_unchanged2: nipkow@13074 182 "\ x:A; y:A \ \ (x <=_r y) = (y +_f x = y)" kleing@10496 183 apply (rule iffI) nipkow@13074 184 apply (blast intro: order_antisym lub order_refl ub1) kleing@10496 185 apply (erule subst) kleing@10496 186 apply simp kleing@10496 187 done kleing@10496 188 kleing@10496 189 nipkow@13074 190 lemma (in semilat) plus_assoc [simp]: kleing@13068 191 assumes a: "a \ A" and b: "b \ A" and c: "c \ A" kleing@13068 192 shows "a +_f (b +_f c) = a +_f b +_f c" kleing@13068 193 proof - kleing@13068 194 from a b have ab: "a +_f b \ A" .. kleing@13068 195 from this c have abc: "(a +_f b) +_f c \ A" .. kleing@13068 196 from b c have bc: "b +_f c \ A" .. kleing@13068 197 from a this have abc': "a +_f (b +_f c) \ A" .. kleing@13068 198 kleing@13077 199 show ?thesis kleing@13077 200 proof kleing@13068 201 show "a +_f (b +_f c) <=_r (a +_f b) +_f c" nipkow@13074 202 proof - kleing@13068 203 from a b have "a <=_r a +_f b" .. kleing@13068 204 also from ab c have "\ <=_r \ +_f c" .. kleing@13068 205 finally have "a<": "a <=_r (a +_f b) +_f c" . kleing@13068 206 from a b have "b <=_r a +_f b" .. kleing@13068 207 also from ab c have "\ <=_r \ +_f c" .. kleing@13068 208 finally have "b<": "b <=_r (a +_f b) +_f c" . kleing@13068 209 from ab c have "c<": "c <=_r (a +_f b) +_f c" .. kleing@13068 210 from "b<" "c<" b c abc have "b +_f c <=_r (a +_f b) +_f c" .. kleing@13068 211 from "a<" this a bc abc show ?thesis .. kleing@13068 212 qed kleing@13068 213 show "(a +_f b) +_f c <=_r a +_f (b +_f c)" kleing@13068 214 proof - kleing@13068 215 from b c have "b <=_r b +_f c" .. kleing@13068 216 also from a bc have "\ <=_r a +_f \" .. kleing@13068 217 finally have "b<": "b <=_r a +_f (b +_f c)" . kleing@13068 218 from b c have "c <=_r b +_f c" .. kleing@13068 219 also from a bc have "\ <=_r a +_f \" .. kleing@13068 220 finally have "c<": "c <=_r a +_f (b +_f c)" . kleing@13068 221 from a bc have "a<": "a <=_r a +_f (b +_f c)" .. kleing@13068 222 from "a<" "b<" a b abc' have "a +_f b <=_r a +_f (b +_f c)" .. kleing@13068 223 from this "c<" ab c abc' show ?thesis .. kleing@13068 224 qed kleing@13068 225 qed kleing@13068 226 qed kleing@13068 227 nipkow@13074 228 lemma (in semilat) plus_com_lemma: nipkow@13074 229 "\a \ A; b \ A\ \ a +_f b <=_r b +_f a" kleing@13068 230 proof - nipkow@13074 231 assume a: "a \ A" and b: "b \ A" kleing@13077 232 from b a have "a <=_r b +_f a" .. kleing@13077 233 moreover from b a have "b <=_r b +_f a" .. kleing@13077 234 moreover note a b kleing@13077 235 moreover from b a have "b +_f a \ A" .. kleing@13077 236 ultimately show ?thesis .. kleing@13068 237 qed kleing@13068 238 nipkow@13074 239 lemma (in semilat) plus_commutative: nipkow@13074 240 "\a \ A; b \ A\ \ a +_f b = b +_f a" nipkow@13074 241 by(blast intro: order_antisym plus_com_lemma) kleing@13068 242 kleing@10496 243 lemma is_lubD: berghofe@22271 244 "is_lub r x y u \ is_ub r x y u & (!z. is_ub r x y z \ r u z)" kleing@10496 245 by (simp add: is_lub_def) kleing@10496 246 kleing@10496 247 lemma is_ubI: berghofe@22271 248 "\ r x u; r y u \ \ is_ub r x y u" kleing@10496 249 by (simp add: is_ub_def) kleing@10496 250 kleing@10496 251 lemma is_ubD: berghofe@22271 252 "is_ub r x y u \ r x u & r y u" kleing@10496 253 by (simp add: is_ub_def) kleing@10496 254 kleing@10496 255 kleing@10496 256 lemma is_lub_bigger1 [iff]: berghofe@22271 257 "is_lub (r^** ) x y y = r^** x y" kleing@10496 258 apply (unfold is_lub_def is_ub_def) kleing@10496 259 apply blast kleing@10496 260 done kleing@10496 261 kleing@10496 262 lemma is_lub_bigger2 [iff]: berghofe@22271 263 "is_lub (r^** ) x y x = r^** y x" kleing@10496 264 apply (unfold is_lub_def is_ub_def) kleing@10496 265 apply blast nipkow@12542 266 done kleing@10496 267 kleing@10496 268 lemma extend_lub: berghofe@22271 269 "\ single_valuedP r; is_lub (r^** ) x y u; r x' x \ berghofe@22271 270 \ EX v. is_lub (r^** ) x' y v" kleing@10496 271 apply (unfold is_lub_def is_ub_def) berghofe@22271 272 apply (case_tac "r^** y x") berghofe@22271 273 apply (case_tac "r^** y x'") kleing@10496 274 apply blast berghofe@23757 275 apply (blast elim: converse_rtranclpE dest: single_valuedD) kleing@10496 276 apply (rule exI) kleing@10496 277 apply (rule conjI) berghofe@23757 278 apply (blast intro: converse_rtranclp_into_rtranclp dest: single_valuedD) berghofe@23757 279 apply (blast intro: rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp berghofe@23757 280 elim: converse_rtranclpE dest: single_valuedD) nipkow@12542 281 done kleing@10496 282 nipkow@10797 283 lemma single_valued_has_lubs [rule_format]: berghofe@22271 284 "\ single_valuedP r; r^** x u \ \ (!y. r^** y u \ berghofe@22271 285 (EX z. is_lub (r^** ) x y z))" berghofe@23757 286 apply (erule converse_rtranclp_induct) kleing@10496 287 apply clarify berghofe@23757 288 apply (erule converse_rtranclp_induct) kleing@10496 289 apply blast berghofe@23757 290 apply (blast intro: converse_rtranclp_into_rtranclp) kleing@10496 291 apply (blast intro: extend_lub) kleing@10496 292 done kleing@10496 293 kleing@10496 294 lemma some_lub_conv: berghofe@22271 295 "\ acyclicP r; is_lub (r^** ) x y u \ \ some_lub (r^** ) x y = u" kleing@10496 296 apply (unfold some_lub_def is_lub_def) kleing@10496 297 apply (rule someI2) kleing@10496 298 apply assumption berghofe@22271 299 apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl [to_pred]) nipkow@12542 300 done kleing@10496 301 kleing@10496 302 lemma is_lub_some_lub: berghofe@22271 303 "\ single_valuedP r; acyclicP r; r^** x u; r^** y u \ berghofe@22271 304 \ is_lub (r^** ) x y (some_lub (r^** ) x y)"; nipkow@10797 305 by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv) kleing@10496 306 nipkow@12542 307 subsection{*An executable lub-finder*} nipkow@12542 308 nipkow@12542 309 constdefs berghofe@22271 310 exec_lub :: "('a \ 'a \ bool) \ ('a \ 'a) \ 'a binop" berghofe@22271 311 "exec_lub r f x y == while (\z. \ r\<^sup>*\<^sup>* x z) f y" nipkow@12542 312 nipkow@12542 313 nipkow@12542 314 lemma acyclic_single_valued_finite: berghofe@22271 315 "\acyclicP r; single_valuedP r; r\<^sup>*\<^sup>* x y \ berghofe@23757 316 \ finite ({(x, y). r x y} \ {a. r\<^sup>*\<^sup>* x a} \ {b. r\<^sup>*\<^sup>* b y})" berghofe@23757 317 apply(erule converse_rtranclp_induct) nipkow@12542 318 apply(rule_tac B = "{}" in finite_subset) berghofe@22271 319 apply(simp only:acyclic_def [to_pred]) berghofe@23757 320 apply(blast intro:rtranclp_into_tranclp2 rtranclp_tranclp_tranclp) nipkow@12542 321 apply simp nipkow@12542 322 apply(rename_tac x x') berghofe@23757 323 apply(subgoal_tac "{(x, y). r x y} \ {a. r\<^sup>*\<^sup>* x a} \ {b. r\<^sup>*\<^sup>* b y} = berghofe@23757 324 insert (x,x') ({(x, y). r x y} \ {a. r\<^sup>*\<^sup>* x' a} \ {b. r\<^sup>*\<^sup>* b y})") nipkow@12542 325 apply simp berghofe@23757 326 apply(blast intro:converse_rtranclp_into_rtranclp berghofe@23757 327 elim:converse_rtranclpE dest:single_valuedD) nipkow@12542 328 done nipkow@12542 329 nipkow@12542 330 kleing@12773 331 lemma exec_lub_conv: berghofe@22271 332 "\ acyclicP r; !x y. r x y \ f x = y; is_lub (r\<^sup>*\<^sup>*) x y u \ \ kleing@12773 333 exec_lub r f x y = u"; nipkow@12542 334 apply(unfold exec_lub_def) berghofe@22271 335 apply(rule_tac P = "\z. r\<^sup>*\<^sup>* y z \ r\<^sup>*\<^sup>* z u" and berghofe@23757 336 r = "({(x, y). r x y} \ {(a,b). r\<^sup>*\<^sup>* y a \ r\<^sup>*\<^sup>* b u})^-1" in while_rule) nipkow@12542 337 apply(blast dest: is_lubD is_ubD) nipkow@12542 338 apply(erule conjE) berghofe@23757 339 apply(erule_tac z = u in converse_rtranclpE) nipkow@12542 340 apply(blast dest: is_lubD is_ubD) berghofe@23757 341 apply(blast dest: rtranclp.rtrancl_into_rtrancl) nipkow@12542 342 apply(rename_tac s) berghofe@22271 343 apply(subgoal_tac "is_ub (r\<^sup>*\<^sup>*) x y s") nipkow@12542 344 prefer 2; apply(simp add:is_ub_def) berghofe@22271 345 apply(subgoal_tac "r\<^sup>*\<^sup>* u s") nipkow@12542 346 prefer 2; apply(blast dest:is_lubD) berghofe@23757 347 apply(erule converse_rtranclpE) nipkow@12542 348 apply blast berghofe@22271 349 apply(simp only:acyclic_def [to_pred]) berghofe@23757 350 apply(blast intro:rtranclp_into_tranclp2 rtranclp_tranclp_tranclp) nipkow@12542 351 apply(rule finite_acyclic_wf) nipkow@12542 352 apply simp nipkow@12542 353 apply(erule acyclic_single_valued_finite) nipkow@12542 354 apply(blast intro:single_valuedI) nipkow@12542 355 apply(simp add:is_lub_def is_ub_def) nipkow@12542 356 apply simp nipkow@12542 357 apply(erule acyclic_subset) nipkow@12542 358 apply blast nipkow@12542 359 apply simp nipkow@12542 360 apply(erule conjE) berghofe@23757 361 apply(erule_tac z = u in converse_rtranclpE) nipkow@12542 362 apply(blast dest: is_lubD is_ubD) berghofe@22271 363 apply blast nipkow@12542 364 done nipkow@12542 365 kleing@12773 366 lemma is_lub_exec_lub: berghofe@22271 367 "\ single_valuedP r; acyclicP r; r^** x u; r^** y u; !x y. r x y \ f x = y \ berghofe@22271 368 \ is_lub (r^** ) x y (exec_lub r f x y)" kleing@12773 369 by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv) kleing@12773 370 kleing@10496 371 end