header {*
\chapter{Bytecode Verifier}\label{cha:bv}
\isaheader{Semilattices}
*}
theory Semilat
imports Main "~~/src/HOL/Library/While_Combinator"
begin
type_synonym 'a ord = "'a => 'a => bool"
type_synonym 'a binop = "'a => 'a => 'a"
type_synonym 'a sl = "'a set × 'a ord × 'a binop"
consts
"lesub" :: "'a => 'a ord => 'a => bool"
"lesssub" :: "'a => 'a ord => 'a => bool"
"plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c"
notation
"lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and
"lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and
"plussub" ("(_ /+'__ _)" [65, 1000, 66] 65)
notation (xsymbols)
"lesub" ("(_ /\<sqsubseteq>⇘_⇙ _)" [50, 0, 51] 50) and
"lesssub" ("(_ /\<sqsubset>⇘_⇙ _)" [50, 0, 51] 50) and
"plussub" ("(_ /\<squnion>⇘_⇙ _)" [65, 0, 66] 65)
abbreviation (input)
lesub1 :: "'a => 'a ord => 'a => bool" ("(_ /\<sqsubseteq>⇩_ _)" [50, 1000, 51] 50)
where "x \<sqsubseteq>⇩r y == x \<sqsubseteq>⇘r⇙ y"
abbreviation (input)
lesssub1 :: "'a => 'a ord => 'a => bool" ("(_ /\<sqsubset>⇩_ _)" [50, 1000, 51] 50)
where "x \<sqsubset>⇩r y == x \<sqsubset>⇘r⇙ y"
abbreviation (input)
plussub1 :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /\<squnion>⇩_ _)" [65, 1000, 66] 65)
where "x \<squnion>⇩f y == x \<squnion>⇘f⇙ y"
defs
lesub_def: "x \<sqsubseteq>⇩r y ≡ r x y"
lesssub_def: "x \<sqsubset>⇩r y ≡ x \<sqsubseteq>⇩r y ∧ x ≠ y"
plussub_def: "x \<squnion>⇩f y ≡ f x y"
definition ord :: "('a × 'a) set => 'a ord"
where
"ord r = (λx y. (x,y) ∈ r)"
definition order :: "'a ord => bool"
where
"order r <-> (∀x. x \<sqsubseteq>⇩r x) ∧ (∀x y. x \<sqsubseteq>⇩r y ∧ y \<sqsubseteq>⇩r x --> x=y) ∧ (∀x y z. x \<sqsubseteq>⇩r y ∧ y \<sqsubseteq>⇩r z --> x \<sqsubseteq>⇩r z)"
definition top :: "'a ord => 'a => bool"
where
"top r T <-> (∀x. x \<sqsubseteq>⇩r T)"
definition acc :: "'a ord => bool"
where
"acc r <-> wf {(y,x). x \<sqsubset>⇩r y}"
definition closed :: "'a set => 'a binop => bool"
where
"closed A f <-> (∀x∈A. ∀y∈A. x \<squnion>⇩f y ∈ A)"
definition semilat :: "'a sl => bool"
where
"semilat = (λ(A,r,f). order r ∧ closed A f ∧
(∀x∈A. ∀y∈A. x \<sqsubseteq>⇩r x \<squnion>⇩f y) ∧
(∀x∈A. ∀y∈A. y \<sqsubseteq>⇩r x \<squnion>⇩f y) ∧
(∀x∈A. ∀y∈A. ∀z∈A. x \<sqsubseteq>⇩r z ∧ y \<sqsubseteq>⇩r z --> x \<squnion>⇩f y \<sqsubseteq>⇩r z))"
definition is_ub :: "('a × 'a) set => 'a => 'a => 'a => bool"
where
"is_ub r x y u <-> (x,u)∈r ∧ (y,u)∈r"
definition is_lub :: "('a × 'a) set => 'a => 'a => 'a => bool"
where
"is_lub r x y u <-> is_ub r x y u ∧ (∀z. is_ub r x y z --> (u,z)∈r)"
definition some_lub :: "('a × 'a) set => 'a => 'a => 'a"
where
"some_lub r x y = (SOME z. is_lub r x y z)"
locale Semilat =
fixes A :: "'a set"
fixes r :: "'a ord"
fixes f :: "'a binop"
assumes semilat: "semilat (A, r, f)"
lemma order_refl [simp, intro]: "order r ==> x \<sqsubseteq>⇩r x"
by (unfold order_def) (simp (no_asm_simp))
lemma order_antisym: "[| order r; x \<sqsubseteq>⇩r y; y \<sqsubseteq>⇩r x |] ==> x = y"
by (unfold order_def) (simp (no_asm_simp))
lemma order_trans: "[| order r; x \<sqsubseteq>⇩r y; y \<sqsubseteq>⇩r z |] ==> x \<sqsubseteq>⇩r z"
by (unfold order_def) blast
lemma order_less_irrefl [intro, simp]: "order r ==> ¬ x \<sqsubset>⇩r x"
by (unfold order_def lesssub_def) blast
lemma order_less_trans: "[| order r; x \<sqsubset>⇩r y; y \<sqsubset>⇩r z |] ==> x \<sqsubset>⇩r z"
by (unfold order_def lesssub_def) blast
lemma topD [simp, intro]: "top r T ==> x \<sqsubseteq>⇩r T"
by (simp add: top_def)
lemma top_le_conv [simp]: "[| order r; top r T |] ==> (T \<sqsubseteq>⇩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 \<sqsubseteq>⇩r x \<squnion>⇩f y) ∧
(∀x∈A. ∀y∈A. y \<sqsubseteq>⇩r x \<squnion>⇩f y) ∧
(∀x∈A. ∀y∈A. ∀z∈A. x \<sqsubseteq>⇩r z ∧ y \<sqsubseteq>⇩r z --> x \<squnion>⇩f y \<sqsubseteq>⇩r z)"
by (unfold semilat_def) clarsimp
lemma (in Semilat) orderI [simp, intro]: "order r"
using semilat by (simp add: semilat_Def)
lemma (in Semilat) closedI [simp, intro]: "closed A f"
using semilat by (simp add: semilat_Def)
lemma closedD: "[| closed A f; x∈A; y∈A |] ==> x \<squnion>⇩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 \<squnion>⇩f y ∈ A"
by (simp add: closedD [OF closedI])
lemma (in Semilat) refl_r [intro, simp]: "x \<sqsubseteq>⇩r x" by simp
lemma (in Semilat) antisym_r [intro?]: "[| x \<sqsubseteq>⇩r y; y \<sqsubseteq>⇩r x |] ==> x = y"
by (rule order_antisym) auto
lemma (in Semilat) trans_r [trans, intro?]: "[|x \<sqsubseteq>⇩r y; y \<sqsubseteq>⇩r z|] ==> x \<sqsubseteq>⇩r z"
by (auto intro: order_trans)
lemma (in Semilat) ub1 [simp, intro?]: "[| x ∈ A; y ∈ A |] ==> x \<sqsubseteq>⇩r x \<squnion>⇩f y"
by (insert semilat) (unfold semilat_Def, simp)
lemma (in Semilat) ub2 [simp, intro?]: "[| x ∈ A; y ∈ A |] ==> y \<sqsubseteq>⇩r x \<squnion>⇩f y"
by (insert semilat) (unfold semilat_Def, simp)
lemma (in Semilat) lub [simp, intro?]:
"[| x \<sqsubseteq>⇩r z; y \<sqsubseteq>⇩r z; x ∈ A; y ∈ A; z ∈ A |] ==> x \<squnion>⇩f y \<sqsubseteq>⇩r z"
by (insert semilat) (unfold semilat_Def, simp)
lemma (in Semilat) plus_le_conv [simp]:
"[| x ∈ A; y ∈ A; z ∈ A |] ==> (x \<squnion>⇩f y \<sqsubseteq>⇩r z) = (x \<sqsubseteq>⇩r z ∧ y \<sqsubseteq>⇩r z)"
by (blast intro: ub1 ub2 lub order_trans)
lemma (in Semilat) le_iff_plus_unchanged:
assumes "x ∈ A" and "y ∈ A"
shows "x \<sqsubseteq>⇩r y <-> x \<squnion>⇩f y = y" (is "?P <-> ?Q")
proof
assume ?P
with assms show ?Q by (blast intro: antisym_r lub ub2)
next
assume ?Q
then have "y = x \<squnion>⇘f⇙ y" by simp
moreover from assms have "x \<sqsubseteq>⇘r⇙ x \<squnion>⇘f⇙ y" by simp
ultimately show ?P by simp
qed
lemma (in Semilat) le_iff_plus_unchanged2:
assumes "x ∈ A" and "y ∈ A"
shows "x \<sqsubseteq>⇩r y <-> y \<squnion>⇩f x = y" (is "?P <-> ?Q")
proof
assume ?P
with assms show ?Q by (blast intro: antisym_r lub ub1)
next
assume ?Q
then have "y = y \<squnion>⇘f⇙ x" by simp
moreover from assms have "x \<sqsubseteq>⇘r⇙ y \<squnion>⇘f⇙ x" by simp
ultimately show ?P by simp
qed
lemma (in Semilat) plus_assoc [simp]:
assumes a: "a ∈ A" and b: "b ∈ A" and c: "c ∈ A"
shows "a \<squnion>⇩f (b \<squnion>⇩f c) = a \<squnion>⇩f b \<squnion>⇩f c"
proof -
from a b have ab: "a \<squnion>⇩f b ∈ A" ..
from this c have abc: "(a \<squnion>⇩f b) \<squnion>⇩f c ∈ A" ..
from b c have bc: "b \<squnion>⇩f c ∈ A" ..
from a this have abc': "a \<squnion>⇩f (b \<squnion>⇩f c) ∈ A" ..
show ?thesis
proof
show "a \<squnion>⇩f (b \<squnion>⇩f c) \<sqsubseteq>⇩r (a \<squnion>⇩f b) \<squnion>⇩f c"
proof -
from a b have "a \<sqsubseteq>⇩r a \<squnion>⇩f b" ..
also from ab c have "… \<sqsubseteq>⇩r … \<squnion>⇩f c" ..
finally have "a<": "a \<sqsubseteq>⇩r (a \<squnion>⇩f b) \<squnion>⇩f c" .
from a b have "b \<sqsubseteq>⇩r a \<squnion>⇩f b" ..
also from ab c have "… \<sqsubseteq>⇩r … \<squnion>⇩f c" ..
finally have "b<": "b \<sqsubseteq>⇩r (a \<squnion>⇩f b) \<squnion>⇩f c" .
from ab c have "c<": "c \<sqsubseteq>⇩r (a \<squnion>⇩f b) \<squnion>⇩f c" ..
from "b<" "c<" b c abc have "b \<squnion>⇩f c \<sqsubseteq>⇩r (a \<squnion>⇩f b) \<squnion>⇩f c" ..
from "a<" this a bc abc show ?thesis ..
qed
show "(a \<squnion>⇩f b) \<squnion>⇩f c \<sqsubseteq>⇩r a \<squnion>⇩f (b \<squnion>⇩f c)"
proof -
from b c have "b \<sqsubseteq>⇩r b \<squnion>⇩f c" ..
also from a bc have "… \<sqsubseteq>⇩r a \<squnion>⇩f …" ..
finally have "b<": "b \<sqsubseteq>⇩r a \<squnion>⇩f (b \<squnion>⇩f c)" .
from b c have "c \<sqsubseteq>⇩r b \<squnion>⇩f c" ..
also from a bc have "… \<sqsubseteq>⇩r a \<squnion>⇩f …" ..
finally have "c<": "c \<sqsubseteq>⇩r a \<squnion>⇩f (b \<squnion>⇩f c)" .
from a bc have "a<": "a \<sqsubseteq>⇩r a \<squnion>⇩f (b \<squnion>⇩f c)" ..
from "a<" "b<" a b abc' have "a \<squnion>⇩f b \<sqsubseteq>⇩r a \<squnion>⇩f (b \<squnion>⇩f c)" ..
from this "c<" ab c abc' show ?thesis ..
qed
qed
qed
lemma (in Semilat) plus_com_lemma:
"[|a ∈ A; b ∈ A|] ==> a \<squnion>⇩f b \<sqsubseteq>⇩r b \<squnion>⇩f a"
proof -
assume a: "a ∈ A" and b: "b ∈ A"
from b a have "a \<sqsubseteq>⇩r b \<squnion>⇩f a" ..
moreover from b a have "b \<sqsubseteq>⇩r b \<squnion>⇩f a" ..
moreover note a b
moreover from b a have "b \<squnion>⇩f a ∈ A" ..
ultimately show ?thesis ..
qed
lemma (in Semilat) plus_commutative:
"[|a ∈ A; b ∈ A|] ==> a \<squnion>⇩f b = b \<squnion>⇩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 (unfold is_lub_def)
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 (fastforce dest: single_valued_has_lubs simp add: some_lub_conv)
subsection{*An executable lub-finder*}
definition exec_lub :: "('a * 'a) set => ('a => 'a) => 'a binop"
where
"exec_lub r f x y = while (λz. (x,z) ∉ r⇧*) f y"
lemma exec_lub_refl: "exec_lub r f T T = T"
by (simp add: exec_lub_def while_unfold)
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 (fastforce dest: single_valued_has_lubs simp add: exec_lub_conv)
end