(* Title: HOL/MicroJava/DFA/Semilat.thy
Author: Tobias Nipkow
Copyright 2000 TUM
*)
chapter \<open>Bytecode Verifier \label{cha:bv}\<close>
section \<open>Semilattices\<close>
theory Semilat
imports Main "HOL-Library.While_Combinator"
begin
type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
definition lesub :: "'a \ 'a ord \ 'a \ bool"
where "lesub x r y \ r x y"
definition lesssub :: "'a \ 'a ord \ 'a \ bool"
where "lesssub x r y \ lesub x r y \ x \ y"
definition plussub :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c"
where "plussub x f y = f x y"
notation (ASCII)
"lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and
"lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and
"plussub" ("(_ /+'__ _)" [65, 1000, 66] 65)
notation
"lesub" ("(_ /\\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"lesssub" ("(_ /\\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"plussub" ("(_ /\\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
(* allow \<sub> instead of \<bsub>..\<esub> *)
abbreviation (input)
lesub1 :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50)
where "x \\<^sub>r y == x \\<^bsub>r\<^esub> y"
abbreviation (input)
lesssub1 :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50)
where "x \\<^sub>r y == x \\<^bsub>r\<^esub> y"
abbreviation (input)
plussub1 :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /\\<^sub>_ _)" [65, 1000, 66] 65)
where "x \\<^sub>f y == x \\<^bsub>f\<^esub> 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 \\<^sub>r x) \ (\x y. x \\<^sub>r y \ y \\<^sub>r x \ x=y) \ (\x y z. x \\<^sub>r y \ y \\<^sub>r z \ x \\<^sub>r z)"
definition top :: "'a ord \ 'a \ bool" where
"top r T \ \x. x \\<^sub>r T"
definition acc :: "'a ord \ bool" where
"acc r \ wf {(y,x). x \\<^sub>r y}"
definition closed :: "'a set \ 'a binop \ bool" where
"closed A f \ \x\A. \y\A. x \\<^sub>f y \ A"
definition semilat :: "'a sl \ bool" where
"semilat \ \(A,r,f). order r \ closed A f \
(\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
(\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
(\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>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 \\<^sub>r x"
(*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)
lemma order_antisym: "\ order r; x \\<^sub>r y; y \\<^sub>r x \ \ x = y"
(*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)
lemma order_trans: "\ order r; x \\<^sub>r y; y \\<^sub>r z \ \ x \\<^sub>r z"
(*<*) by (unfold order_def) blast (*>*)
lemma order_less_irrefl [intro, simp]: "order r \ \ x \\<^sub>r x"
(*<*) by (unfold order_def lesssub_def) blast (*>*)
lemma order_less_trans: "\ order r; x \\<^sub>r y; y \\<^sub>r z \ \ x \\<^sub>r z"
(*<*) by (unfold order_def lesssub_def) blast (*>*)
lemma topD [simp, intro]: "top r T \ x \\<^sub>r T"
(*<*) by (simp add: top_def) (*>*)
lemma top_le_conv [simp]: "\ order r; top r T \ \ (T \\<^sub>r x) = (x = T)"
(*<*) by (blast intro: order_antisym) (*>*)
lemma semilat_Def:
"semilat(A,r,f) \ order r \ closed A f \
(\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
(\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
(\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>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 \\<^sub>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 \\<^sub>f y \ A"
(*<*) by (simp add: closedD [OF closedI]) (*>*)
lemma (in Semilat) refl_r [intro, simp]: "x \\<^sub>r x" by simp
lemma (in Semilat) antisym_r [intro?]: "\ x \\<^sub>r y; y \\<^sub>r x \ \ x = y"
(*<*) by (rule order_antisym) auto (*>*)
lemma (in Semilat) trans_r [trans, intro?]: "\x \\<^sub>r y; y \\<^sub>r z\ \ x \\<^sub>r z"
(*<*) by (auto intro: order_trans) (*>*)
lemma (in Semilat) ub1 [simp, intro?]: "\ x \ A; y \ A \ \ x \\<^sub>r x \\<^sub>f y"
(*<*) using semilat by (simp add: semilat_Def) (*>*)
lemma (in Semilat) ub2 [simp, intro?]: "\ x \ A; y \ A \ \ y \\<^sub>r x \\<^sub>f y"
(*<*) using semilat by (simp add: semilat_Def) (*>*)
lemma (in Semilat) lub [simp, intro?]:
"\ x \\<^sub>r z; y \\<^sub>r z; x \ A; y \ A; z \ A \ \ x \\<^sub>f y \\<^sub>r z"
(*<*) using semilat by (simp add: semilat_Def) (*>*)
lemma (in Semilat) plus_le_conv [simp]:
"\ x \ A; y \ A; z \ A \ \ (x \\<^sub>f y \\<^sub>r z) = (x \\<^sub>r z \ y \\<^sub>r z)"
(*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*)
lemma (in Semilat) le_iff_plus_unchanged: "\ x \ A; y \ A \ \ (x \\<^sub>r y) = (x \\<^sub>f y = y)"
(*<*)
apply (rule iffI)
apply (blast intro: antisym_r lub ub2)
apply (erule subst)
apply simp
done
(*>*)
lemma (in Semilat) le_iff_plus_unchanged2: "\ x \ A; y \ A \ \ (x \\<^sub>r y) = (y \\<^sub>f x = y)"
(*<*)
apply (rule iffI)
apply (blast intro: order_antisym lub 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 \\<^sub>f (b \\<^sub>f c) = a \\<^sub>f b \\<^sub>f c"
(*<*)
proof -
from a b have ab: "a \\<^sub>f b \ A" ..
from this c have abc: "(a \\<^sub>f b) \\<^sub>f c \ A" ..
from b c have bc: "b \\<^sub>f c \ A" ..
from a this have abc': "a \\<^sub>f (b \\<^sub>f c) \ A" ..
show ?thesis
proof
show "a \\<^sub>f (b \\<^sub>f c) \\<^sub>r (a \\<^sub>f b) \\<^sub>f c"
proof -
from a b have "a \\<^sub>r a \\<^sub>f b" ..
also from ab c have "\ \\<^sub>r \ \\<^sub>f c" ..
finally have "a<": "a \\<^sub>r (a \\<^sub>f b) \\<^sub>f c" .
from a b have "b \\<^sub>r a \\<^sub>f b" ..
also from ab c have "\ \\<^sub>r \ \\<^sub>f c" ..
finally have "b<": "b \\<^sub>r (a \\<^sub>f b) \\<^sub>f c" .
from ab c have "c<": "c \\<^sub>r (a \\<^sub>f b) \\<^sub>f c" ..
from "b<" "c<" b c abc have "b \\<^sub>f c \\<^sub>r (a \\<^sub>f b) \\<^sub>f c" ..
from "a<" this a bc abc show ?thesis ..
qed
show "(a \\<^sub>f b) \\<^sub>f c \\<^sub>r a \\<^sub>f (b \\<^sub>f c)"
proof -
from b c have "b \\<^sub>r b \\<^sub>f c" ..
also from a bc have "\ \\<^sub>r a \\<^sub>f \" ..
finally have "b<": "b \\<^sub>r a \\<^sub>f (b \\<^sub>f c)" .
from b c have "c \\<^sub>r b \\<^sub>f c" ..
also from a bc have "\ \\<^sub>r a \\<^sub>f \" ..
finally have "c<": "c \\<^sub>r a \\<^sub>f (b \\<^sub>f c)" .
from a bc have "a<": "a \\<^sub>r a \\<^sub>f (b \\<^sub>f c)" ..
from "a<" "b<" a b abc' have "a \\<^sub>f b \\<^sub>r a \\<^sub>f (b \\<^sub>f c)" ..
from this "c<" ab c abc' show ?thesis ..
qed
qed
qed
(*>*)
lemma (in Semilat) plus_com_lemma:
"\a \ A; b \ A\ \ a \\<^sub>f b \\<^sub>r b \\<^sub>f a"
(*<*)
proof -
assume a: "a \ A" and b: "b \ A"
from b a have "a \\<^sub>r b \\<^sub>f a" ..
moreover from b a have "b \\<^sub>r b \\<^sub>f a" ..
moreover note a b
moreover from b a have "b \\<^sub>f a \ A" ..
ultimately show ?thesis ..
qed
(*>*)
lemma (in Semilat) plus_commutative:
"\a \ A; b \ A\ \ a \\<^sub>f b = b \\<^sub>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\<^sup>*) x y y = ((x,y)\r\<^sup>*)"
(*<*)
apply (unfold is_lub_def is_ub_def)
apply blast
done
(*>*)
lemma is_lub_bigger2 [iff]:
"is_lub (r\<^sup>*) x y x = ((y,x)\r\<^sup>*)"
(*<*)
apply (unfold is_lub_def is_ub_def)
apply blast
done
(*>*)
lemma extend_lub:
"\ single_valued r; is_lub (r\<^sup>*) x y u; (x',x) \ r \
\<Longrightarrow> \<exists>v. is_lub (r\<^sup>*) x' y v"
(*<*)
apply (unfold is_lub_def is_ub_def)
apply (case_tac "(y,x) \ r\<^sup>*")
apply (case_tac "(y,x') \ r\<^sup>*")
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\<^sup>*\ \ (\y. (y,u) \ r\<^sup>* \
(\<exists>z. is_lub (r\<^sup>*) 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\<^sup>*) x y u\ \ some_lub (r\<^sup>*) 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\<^sup>*; (y,u)\r\<^sup>*\
\<Longrightarrow> is_lub (r\<^sup>*) x y (some_lub (r\<^sup>*) x y)"
(*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
subsection\<open>An executable lub-finder\<close>
definition exec_lub :: "('a * 'a) set \ ('a \ 'a) \ 'a binop" where
"exec_lub r f x y \ while (\z. (x,z) \ r\<^sup>*) 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\<^sup>*\
\<Longrightarrow> finite (r \<inter> {a. (x, a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})"
(*<*)
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\<^sup>*} \ {b. (b,y) \ r\<^sup>*} =
insert (x,x') (r \ {a. (x', a) \ r\<^sup>*} \ {b. (b, y) \ r\<^sup>*})")
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\<^sup>*) x y u \ \
exec_lub r f x y = u"
(*<*)
apply(unfold exec_lub_def)
apply(rule_tac P = "\z. (y,z) \ r\<^sup>* \ (z,u) \ r\<^sup>*" and
r = "(r \ {(a,b). (y,a) \ r\<^sup>* \ (b,u) \ r\<^sup>*})\" 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\<^sup>*) x y s")
prefer 2 apply(simp add:is_ub_def)
apply(subgoal_tac "(u, s) \ r\<^sup>*")
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\<^sup>*; (y,u)\r\<^sup>*; \x y. (x,y) \ r \ f x = y \
\<Longrightarrow> is_lub (r\<^sup>*) x y (exec_lub r f x y)"
(*<*) by (fastforce dest: single_valued_has_lubs simp add: exec_lub_conv) (*>*)
end
¤ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
