(* Title: HOL/MicroJava/BV/Semilat.thy ID: $Id: Semilat.thy,v 1.17 2005/06/17 14:13:08 haftmann Exp $ Author: Tobias Nipkow Copyright 2000 TUM Semilattices *) header {* \chapter{Bytecode Verifier}\label{cha:bv} \isaheader{Semilattices} *} theory Semilat imports While_Combinator begin types 'a ord = "'a => 'a => bool" 'a binop = "'a => 'a => 'a" 'a sl = "'a set * 'a ord * 'a binop" consts "@lesub" :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50) "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50) defs lesub_def: "x <=_r y == r x y" lesssub_def: "x <_r y == x <=_r y & x ~= y" syntax (xsymbols) "@lesub" :: "'a => 'a ord => 'a => bool" ("(_ /≤_ _)" [50, 1000, 51] 50) consts "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65) defs plussub_def: "x +_f y == f x y" syntax (xsymbols) "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+_ _)" [65, 1000, 66] 65) syntax (xsymbols) "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /\<squnion>_ _)" [65, 1000, 66] 65) constdefs ord :: "('a*'a)set => 'a ord" "ord r == %x y. (x,y):r" order :: "'a ord => bool" "order r == (!x. x <=_r x) & (!x y. x <=_r y & y <=_r x --> x=y) & (!x y z. x <=_r y & y <=_r z --> x <=_r z)" acc :: "'a ord => bool" "acc r == wf{(y,x) . x <_r y}" top :: "'a ord => 'a => bool" "top r T == !x. x <=_r T" closed :: "'a set => 'a binop => bool" "closed A f == !x:A. !y:A. x +_f y : A" semilat :: "'a sl => bool" "semilat == %(A,r,f). order r & closed A f & (!x:A. !y:A. x <=_r x +_f y) & (!x:A. !y:A. y <=_r x +_f y) & (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)" is_ub :: "('a*'a)set => 'a => 'a => 'a => bool" "is_ub r x y u == (x,u):r & (y,u):r" is_lub :: "('a*'a)set => 'a => 'a => 'a => bool" "is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)" some_lub :: "('a*'a)set => 'a => 'a => 'a" "some_lub r x y == SOME z. is_lub r x y z"; locale (open) semilat = fixes A :: "'a set" and r :: "'a ord" and f :: "'a binop" assumes semilat: "semilat(A,r,f)" lemma order_refl [simp, intro]: "order r ==> x <=_r x"; by (simp add: order_def) lemma order_antisym: "[| order r; x <=_r y; y <=_r x |] ==> x = y" apply (unfold order_def) apply (simp (no_asm_simp)) done lemma order_trans: "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z" apply (unfold order_def) apply blast done lemma order_less_irrefl [intro, simp]: "order r ==> ~ x <_r x" apply (unfold order_def lesssub_def) apply blast done lemma order_less_trans: "[| order r; x <_r y; y <_r z |] ==> x <_r z" apply (unfold order_def lesssub_def) apply blast done lemma topD [simp, intro]: "top r T ==> x <=_r T" by (simp add: top_def) lemma top_le_conv [simp]: "[| order r; top r T |] ==> (T <=_r x) = (x = T)" by (blast intro: order_antisym) lemma semilat_Def: "semilat(A,r,f) == order r & closed A f & (!x:A. !y:A. x <=_r x +_f y) & (!x:A. !y:A. y <=_r x +_f y) & (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)" apply (unfold semilat_def split_conv [THEN eq_reflection]) apply (rule refl [THEN eq_reflection]) done lemma (in semilat) orderI [simp, intro]: "order r" by (insert semilat) (simp add: semilat_Def) lemma (in semilat) closedI [simp, intro]: "closed A f" by (insert semilat) (simp add: semilat_Def) lemma closedD: "[| closed A f; x:A; y:A |] ==> x +_f y : A" by (unfold closed_def) blast lemma closed_UNIV [simp]: "closed UNIV f" by (simp add: closed_def) lemma (in semilat) closed_f [simp, intro]: "[|x:A; y:A|] ==> x +_f y : A" by (simp add: closedD [OF closedI]) lemma (in semilat) refl_r [intro, simp]: "x <=_r x" by simp lemma (in semilat) antisym_r [intro?]: "[| x <=_r y; y <=_r x |] ==> x = y" by (rule order_antisym) auto lemma (in semilat) trans_r [trans, intro?]: "[|x <=_r y; y <=_r z|] ==> x <=_r z" by (auto intro: order_trans) lemma (in semilat) ub1 [simp, intro?]: "[| x:A; y:A |] ==> x <=_r x +_f y" by (insert semilat) (unfold semilat_Def, simp) lemma (in semilat) ub2 [simp, intro?]: "[| x:A; y:A |] ==> y <=_r x +_f y" by (insert semilat) (unfold semilat_Def, simp) lemma (in semilat) lub [simp, intro?]: "[| x <=_r z; y <=_r z; x:A; y:A; z:A |] ==> x +_f y <=_r z"; by (insert semilat) (unfold semilat_Def, simp) lemma (in semilat) plus_le_conv [simp]: "[| x:A; y:A; z:A |] ==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)" by (blast intro: ub1 ub2 lub order_trans) lemma (in semilat) le_iff_plus_unchanged: "[| x:A; y:A |] ==> (x <=_r y) = (x +_f y = y)" apply (rule iffI) apply (blast intro: antisym_r refl_r lub ub2) apply (erule subst) apply simp done lemma (in semilat) le_iff_plus_unchanged2: "[| x:A; y:A |] ==> (x <=_r y) = (y +_f x = y)" apply (rule iffI) apply (blast intro: order_antisym lub order_refl ub1) apply (erule subst) apply simp done lemma (in semilat) plus_assoc [simp]: assumes a: "a ∈ A" and b: "b ∈ A" and c: "c ∈ A" shows "a +_f (b +_f c) = a +_f b +_f c" proof - from a b have ab: "a +_f b ∈ A" .. from this c have abc: "(a +_f b) +_f c ∈ A" .. from b c have bc: "b +_f c ∈ A" .. from a this have abc': "a +_f (b +_f c) ∈ A" .. show ?thesis proof show "a +_f (b +_f c) <=_r (a +_f b) +_f c" proof - from a b have "a <=_r a +_f b" .. also from ab c have "… <=_r … +_f c" .. finally have "a<": "a <=_r (a +_f b) +_f c" . from a b have "b <=_r a +_f b" .. also from ab c have "… <=_r … +_f c" .. finally have "b<": "b <=_r (a +_f b) +_f c" . from ab c have "c<": "c <=_r (a +_f b) +_f c" .. from "b<" "c<" b c abc have "b +_f c <=_r (a +_f b) +_f c" .. from "a<" this a bc abc show ?thesis .. qed show "(a +_f b) +_f c <=_r a +_f (b +_f c)" proof - from b c have "b <=_r b +_f c" .. also from a bc have "… <=_r a +_f …" .. finally have "b<": "b <=_r a +_f (b +_f c)" . from b c have "c <=_r b +_f c" .. also from a bc have "… <=_r a +_f …" .. finally have "c<": "c <=_r a +_f (b +_f c)" . from a bc have "a<": "a <=_r a +_f (b +_f c)" .. from "a<" "b<" a b abc' have "a +_f b <=_r a +_f (b +_f c)" .. from this "c<" ab c abc' show ?thesis .. qed qed qed lemma (in semilat) plus_com_lemma: "[|a ∈ A; b ∈ A|] ==> a +_f b <=_r b +_f a" proof - assume a: "a ∈ A" and b: "b ∈ A" from b a have "a <=_r b +_f a" .. moreover from b a have "b <=_r b +_f a" .. moreover note a b moreover from b a have "b +_f a ∈ A" .. ultimately show ?thesis .. qed lemma (in semilat) plus_commutative: "[|a ∈ A; b ∈ A|] ==> a +_f b = b +_f a" by(blast intro: order_antisym plus_com_lemma) lemma is_lubD: "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)" by (simp add: is_lub_def) lemma is_ubI: "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u" by (simp add: is_ub_def) lemma is_ubD: "is_ub r x y u ==> (x,u) : r & (y,u) : r" by (simp add: is_ub_def) lemma is_lub_bigger1 [iff]: "is_lub (r^* ) x y y = ((x,y):r^* )" apply (unfold is_lub_def is_ub_def) apply blast done lemma is_lub_bigger2 [iff]: "is_lub (r^* ) x y x = ((y,x):r^* )" apply (unfold is_lub_def is_ub_def) apply blast done lemma extend_lub: "[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |] ==> EX v. is_lub (r^* ) x' y v" apply (unfold is_lub_def is_ub_def) apply (case_tac "(y,x) : r^*") apply (case_tac "(y,x') : r^*") apply blast apply (blast elim: converse_rtranclE dest: single_valuedD) apply (rule exI) apply (rule conjI) apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD) apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl elim: converse_rtranclE dest: single_valuedD) done lemma single_valued_has_lubs [rule_format]: "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> (EX z. is_lub (r^* ) x y z))" apply (erule converse_rtrancl_induct) apply clarify apply (erule converse_rtrancl_induct) apply blast apply (blast intro: converse_rtrancl_into_rtrancl) apply (blast intro: extend_lub) done lemma some_lub_conv: "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u" apply (unfold some_lub_def is_lub_def) apply (rule someI2) apply assumption apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl) done lemma is_lub_some_lub: "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> is_lub (r^* ) x y (some_lub (r^* ) x y)"; by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv) subsection{*An executable lub-finder*} constdefs exec_lub :: "('a * 'a) set => ('a => 'a) => 'a binop" "exec_lub r f x y == while (λz. (x,z) ∉ r*) f y" lemma acyclic_single_valued_finite: "[|acyclic r; single_valued r; (x,y) ∈ r*|] ==> finite (r ∩ {a. (x, a) ∈ r*} × {b. (b, y) ∈ r*})" apply(erule converse_rtrancl_induct) apply(rule_tac B = "{}" in finite_subset) apply(simp only:acyclic_def) apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) apply simp apply(rename_tac x x') apply(subgoal_tac "r ∩ {a. (x,a) ∈ r*} × {b. (b,y) ∈ r*} = insert (x,x') (r ∩ {a. (x', a) ∈ r*} × {b. (b, y) ∈ r*})") apply simp apply(blast intro:converse_rtrancl_into_rtrancl elim:converse_rtranclE dest:single_valuedD) done lemma exec_lub_conv: "[| acyclic r; !x y. (x,y) ∈ r --> f x = y; is_lub (r*) x y u |] ==> exec_lub r f x y = u"; apply(unfold exec_lub_def) apply(rule_tac P = "λz. (y,z) ∈ r* ∧ (z,u) ∈ r*" and r = "(r ∩ {(a,b). (y,a) ∈ r* ∧ (b,u) ∈ r*})^-1" in while_rule) apply(blast dest: is_lubD is_ubD) apply(erule conjE) apply(erule_tac z = u in converse_rtranclE) apply(blast dest: is_lubD is_ubD) apply(blast dest:rtrancl_into_rtrancl) apply(rename_tac s) apply(subgoal_tac "is_ub (r*) x y s") prefer 2; apply(simp add:is_ub_def) apply(subgoal_tac "(u, s) ∈ r*") prefer 2; apply(blast dest:is_lubD) apply(erule converse_rtranclE) apply blast apply(simp only:acyclic_def) apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) apply(rule finite_acyclic_wf) apply simp apply(erule acyclic_single_valued_finite) apply(blast intro:single_valuedI) apply(simp add:is_lub_def is_ub_def) apply simp apply(erule acyclic_subset) apply blast apply simp apply(erule conjE) apply(erule_tac z = u in converse_rtranclE) apply(blast dest: is_lubD is_ubD) apply(blast dest:rtrancl_into_rtrancl) done lemma is_lub_exec_lub: "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; !x y. (x,y) ∈ r --> f x = y |] ==> is_lub (r^* ) x y (exec_lub r f x y)" by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv) end
lemma order_refl:
order r ==> x <=_r x
lemma order_antisym:
[| order r; x <=_r y; y <=_r x |] ==> x = y
lemma order_trans:
[| order r; x <=_r y; y <=_r z |] ==> x <=_r z
lemma order_less_irrefl:
order r ==> ¬ x <_r x
lemma order_less_trans:
[| order r; x <_r y; y <_r z |] ==> x <_r z
lemma topD:
top r T ==> x <=_r T
lemma top_le_conv:
[| order r; top r T |] ==> (T <=_r x) = (x = T)
lemma semilat_Def:
semilat (A, r, f) == order r ∧ closed A f ∧ (∀x∈A. ∀y∈A. x <=_r x +_f y) ∧ (∀x∈A. ∀y∈A. y <=_r x +_f y) ∧ (∀x∈A. ∀y∈A. ∀z∈A. x <=_r z ∧ y <=_r z --> x +_f y <=_r z)
lemma orderI:
semilat (A, r, f) ==> order r
lemma closedI:
semilat (A, r, f) ==> closed A f
lemma closedD:
[| closed A f; x ∈ A; y ∈ A |] ==> x +_f y ∈ A
lemma closed_UNIV:
closed UNIV f
lemma closed_f:
[| semilat (A, r, f); x ∈ A; y ∈ A |] ==> x +_f y ∈ A
lemma refl_r:
semilat (A, r, f) ==> x <=_r x
lemma antisym_r:
[| semilat (A, r, f); x <=_r y; y <=_r x |] ==> x = y
lemma trans_r:
[| semilat (A, r, f); x <=_r y; y <=_r z |] ==> x <=_r z
lemma ub1:
[| semilat (A, r, f); x ∈ A; y ∈ A |] ==> x <=_r x +_f y
lemma ub2:
[| semilat (A, r, f); x ∈ A; y ∈ A |] ==> y <=_r x +_f y
lemma lub:
[| semilat (A, r, f); x <=_r z; y <=_r z; x ∈ A; y ∈ A; z ∈ A |] ==> x +_f y <=_r z
lemma plus_le_conv:
[| semilat (A, r, f); x ∈ A; y ∈ A; z ∈ A |] ==> (x +_f y <=_r z) = (x <=_r z ∧ y <=_r z)
lemma le_iff_plus_unchanged:
[| semilat (A, r, f); x ∈ A; y ∈ A |] ==> (x <=_r y) = (x +_f y = y)
lemma le_iff_plus_unchanged2:
[| semilat (A, r, f); x ∈ A; y ∈ A |] ==> (x <=_r y) = (y +_f x = y)
lemma plus_assoc:
[| semilat (A, r, f); a ∈ A; b ∈ A; c ∈ A |] ==> a +_f (b +_f c) = a +_f b +_f c
lemma plus_com_lemma:
[| semilat (A, r, f); a ∈ A; b ∈ A |] ==> a +_f b <=_r b +_f a
lemma plus_commutative:
[| semilat (A, r, f); a ∈ A; b ∈ A |] ==> a +_f b = b +_f a
lemma is_lubD:
is_lub r x y u ==> is_ub r x y u ∧ (∀z. is_ub r x y z --> (u, z) ∈ r)
lemma is_ubI:
[| (x, u) ∈ r; (y, u) ∈ r |] ==> is_ub r x y u
lemma is_ubD:
is_ub r x y u ==> (x, u) ∈ r ∧ (y, u) ∈ r
lemma is_lub_bigger1:
is_lub (r*) x y y = ((x, y) ∈ r*)
lemma is_lub_bigger2:
is_lub (r*) x y x = ((y, x) ∈ r*)
lemma extend_lub:
[| single_valued r; is_lub (r*) x y u; (x', x) ∈ r |] ==> ∃v. is_lub (r*) x' y v
lemma single_valued_has_lubs:
[| single_valued r; (x, u) ∈ r*; (y, u) ∈ r* |] ==> Ex (is_lub (r*) x y)
lemma some_lub_conv:
[| acyclic r; is_lub (r*) x y u |] ==> some_lub (r*) x y = u
lemma is_lub_some_lub:
[| single_valued r; acyclic r; (x, u) ∈ r*; (y, u) ∈ r* |] ==> is_lub (r*) x y (some_lub (r*) x y)
lemma acyclic_single_valued_finite:
[| acyclic r; single_valued r; (x, y) ∈ r* |] ==> finite (r ∩ {a. (x, a) ∈ r*} × {b. (b, y) ∈ r*})
lemma exec_lub_conv:
[| acyclic r; ∀x y. (x, y) ∈ r --> f x = y; is_lub (r*) x y u |] ==> exec_lub r f x y = u
lemma is_lub_exec_lub:
[| single_valued r; acyclic r; (x, u) ∈ r*; (y, u) ∈ r*; ∀x y. (x, y) ∈ r --> f x = y |] ==> is_lub (r*) x y (exec_lub r f x y)