Quelle  Semilat.thy

(*  Title:      HOL/MicroJava/DFA/Semilat.thy
  Author: Tobias Nipkow
  Copyright 2000 TUM
*)

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"
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