Theory Semilat

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

Semilattices.
*)

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 ⊑⇘ry"

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

abbreviation (input)
  plussub1 :: "'a  ('a  'b  'c)  'b  'c" ("(_ /⊔⇩_ _)" [65, 1000, 66] 65)
  where "x ⊔⇩f y == x ⊔⇘fy"

definition ord :: "('a × 'a) set  'a ord"
where
  "ord r = (λx y. (x,y)  r)"

definition order :: "'a ord  'a set  bool"
where
  "order r A  (xA. x ⊑⇩r x)  (xA. yA. x ⊑⇩r y  y ⊑⇩r x  x=y)  (xA.  yA. zA. 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  (xA. yA. x ⊔⇩f y  A)"

definition semilat :: "'a sl  bool"
where
  "semilat = (λ(A,r,f). order r A  closed A f  
                       (xA. yA. x ⊑⇩r x ⊔⇩f y) 
                       (xA. yA. y ⊑⇩r x ⊔⇩f y) 
                       (xA. yA. zA. 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 A  x  A  x ⊑⇩r x"
  (*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)

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

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

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

lemma order_less_trans: " order r A; x ⊏⇩r y; y ⊏⇩r z; x  A; y  A; z  A   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 A; top r T; x  A; T  A  (T ⊑⇩r x) = (x = T)"
  (*<*) by (blast intro: order_antisym) (*>*)

lemma semilat_Def:
"semilat(A,r,f)  order r A  closed A f  
                 (xA. yA. x ⊑⇩r x ⊔⇩f y)  
                 (xA. yA. y ⊑⇩r x ⊔⇩f y)  
                 (xA. yA. zA. x ⊑⇩r z  y ⊑⇩r z  x ⊔⇩f y ⊑⇩r z)"
  (*<*) by (unfold semilat_def) clarsimp (*>*)

lemma (in Semilat) orderI [simp, intro]: "order r A"
  (*<*) 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; xA; yA   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  A  x ⊑⇩r x" by auto

lemma (in Semilat) antisym_r [intro?]: " x ⊑⇩r y; y ⊑⇩r x; x  A; y  A   x = y"
  (*<*) by (rule order_antisym) auto (*>*)

lemma (in Semilat) trans_r [trans, intro?]: "x ⊑⇩r y; y ⊑⇩r z; x  A; y  A; z  A   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:
  assumes "x  A" and "y  A"
  shows "x ⊑⇩r y  x ⊔⇩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 ⊔⇘fy" by simp
  moreover from assms have "x ⊑⇘rx ⊔⇘fy" by simp
  ultimately show ?P by simp
qed
(*>*)

lemma (in Semilat) le_iff_plus_unchanged2:
  assumes "x  A" and "y  A"
  shows "x ⊑⇩r y  y ⊔⇩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 ⊔⇘fx" by simp
  moreover from assms have "x ⊑⇘ry ⊔⇘fx" 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 ⊔⇩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 1: "a ⊑⇩r a ⊔⇩f b" .. 
      from ab c have 2: " ⊑⇩r  ⊔⇩f c" ..
      with 1  have "a<": "a ⊑⇩r (a ⊔⇩f b) ⊔⇩f c" using a ab abc by (rule trans_r)
      from a b have 11: "b ⊑⇩r a ⊔⇩f b" ..
      hence "b<": "b ⊑⇩r (a ⊔⇩f b) ⊔⇩f c" using 2 b ab abc by (rule trans_r)
      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 3:"b ⊑⇩r b ⊔⇩f c" .. 
      from a bc have bc_abc: " ⊑⇩r a ⊔⇩f " ..
      with 3 have "b<": "b ⊑⇩r a ⊔⇩f (b ⊔⇩f c)"using b bc abc' by (rule trans_r)
      from b c have 4: "c ⊑⇩r b ⊔⇩f c" ..      
      hence "c<": "c ⊑⇩r a ⊔⇩f (b ⊔⇩f c)"using bc_abc c bc abc' by (rule trans_r)
      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
  next
    show "a ⊔⇘f(b ⊔⇘fc)  A" using abc' by auto
  next
    show "a ⊔⇘fb ⊔⇘fc  A" using abc by auto
  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 (simp only: some_lub_def is_lub_def)
apply (rule someI2)
 apply (simp only: is_lub_def)
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