Theory Semilat

theory Semilat
imports While_Combinator
(*  Title:      HOL/MicroJava/DFA/Semilat.thy
Author:     Tobias Nipkow
*)

chapter ‹Bytecode Verifier \label{cha:bv}›

section ‹Semilattices›

theory Semilat
imports Main "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"

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"  ("(_ /⊑⇘_⇙ _)" [50, 0, 51] 50) and
"lesssub"  ("(_ /⊏⇘_⇙ _)" [50, 0, 51] 50) and
"plussub"  ("(_ /⊔⇘_⇙ _)" [65, 0, 66] 65)

(* allow \<sub> instead of \<bsub>..\<esub> *)
abbreviation (input)
lesub1 :: "'a ⇒ 'a ord ⇒ 'a ⇒ bool" ("(_ /⊑⇩_ _)" [50, 1000, 51] 50)
where "x ⊑⇩r y == x ⊑⇘r⇙ y"

abbreviation (input)
lesssub1 :: "'a ⇒ 'a ord ⇒ 'a ⇒ bool" ("(_ /⊏⇩_ _)" [50, 1000, 51] 50)
where "x ⊏⇩r y == x ⊏⇘r⇙ y"

abbreviation (input)
plussub1 :: "'a ⇒ ('a ⇒ 'b ⇒ 'c) ⇒ 'b ⇒ 'c" ("(_ /⊔⇩_ _)" [65, 1000, 66] 65)
where "x ⊔⇩f y == x ⊔⇘f⇙ 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 ⊑⇩r x) ∧ (∀x y. x ⊑⇩r y ∧ y ⊑⇩r x ⟶ x=y) ∧ (∀x y z. x ⊑⇩r y ∧ y ⊑⇩r z ⟶ x ⊑⇩r z)"

definition top :: "'a ord ⇒ 'a ⇒ bool" where
"top r T ≡ ∀x. x ⊑⇩r T"

definition acc :: "'a ord ⇒ bool" where
"acc r ≡ wf {(y,x). x ⊏⇩r y}"

definition closed :: "'a set ⇒ 'a binop ⇒ bool" where
"closed A f ≡ ∀x∈A. ∀y∈A. x ⊔⇩f y ∈ A"

definition semilat :: "'a sl ⇒ bool" where
"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)"

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 ⊑⇩r x"
(*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)

lemma order_antisym: "⟦ order r; x ⊑⇩r y; y ⊑⇩r x ⟧ ⟹ x = y"
(*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)

lemma order_trans: "⟦ order r; x ⊑⇩r y; y ⊑⇩r z ⟧ ⟹ x ⊑⇩r z"
(*<*) by (unfold order_def) blast (*>*)

lemma order_less_irrefl [intro, simp]: "order r ⟹ ¬ x ⊏⇩r x"
(*<*) by (unfold order_def lesssub_def) blast (*>*)

lemma order_less_trans: "⟦ order r; x ⊏⇩r y; y ⊏⇩r z ⟧ ⟹ x ⊏⇩r z"
(*<*) by (unfold order_def lesssub_def) blast (*>*)

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)"
(*<*) 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 ⊔⇩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"
(*<*) using semilat by (simp add: semilat_Def) (*>*)

lemma (in Semilat) ub2 [simp, intro?]: "⟦ x ∈ A; y ∈ A ⟧ ⟹ y ⊑⇩r x ⊔⇩f y"
(*<*) using semilat by (simp add: semilat_Def) (*>*)

lemma (in Semilat) lub [simp, intro?]:
"⟦ x ⊑⇩r z; y ⊑⇩r z; x ∈ A; y ∈ A; z ∈ A ⟧ ⟹ x ⊔⇩f y ⊑⇩r z"
(*<*) using semilat by (simp add: semilat_Def) (*>*)

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 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 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 ⟧
⟹ ∃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⇧* ⟶
(∃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 (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"

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⇧*})¯" 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")
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
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