# Theory Semilat

Up to index of Isabelle/HOL/MicroJava

theory Semilat
imports While_Combinator
begin

    (*  Title:      HOL/MicroJava/BV/Semilat.thy
        ID:         $Id: Semilat.thy,v 1.17 2005/06/17 14:13:08 haftmann Exp $
        Author:     Tobias Nipkow
        Copyright   2000 TUM

    Semilattices
    *)

    header {*
      \chapter{Bytecode Verifier}\label{cha:bv}
      \isaheader{Semilattices}
    *}

    theory Semilat imports While_Combinator begin

    types 'a ord    = "'a => 'a => bool"
          'a binop  = "'a => 'a => 'a"
          'a sl     = "'a set * 'a ord * 'a binop"

    consts
     "@lesub"   :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
     "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
    defs
    lesub_def:   "x <=_r y == r x y"
    lesssub_def: "x <_r y  == x <=_r y & x ~= y"

    syntax (xsymbols)
     "@lesub" :: "'a => 'a ord => 'a => bool" ("(_ /≤_ _)" [50, 1000, 51] 50)

    consts
     "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
    defs
    plussub_def: "x +_f y == f x y"

    syntax (xsymbols)
     "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+_ _)" [65, 1000, 66] 65)

    syntax (xsymbols)
     "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /\<squnion>_ _)" [65, 1000, 66] 65)

    constdefs
     ord :: "('a*'a)set => 'a ord"
    "ord r == %x y. (x,y):r"

     order :: "'a ord => bool"
    "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)"

     acc :: "'a ord => bool"
    "acc r == wf{(y,x) . x <_r y}"

     top :: "'a ord => 'a => bool"
    "top r T == !x. x <=_r T"

     closed :: "'a set => 'a binop => bool"
    "closed A f == !x:A. !y:A. x +_f y : A"

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

     is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
    "is_ub r x y u == (x,u):r & (y,u):r"

     is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
    "is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"

     some_lub :: "('a*'a)set => 'a => 'a => 'a"
    "some_lub r x y == SOME z. is_lub r x y z";

    locale (open) semilat =
      fixes A :: "'a set"
        and r :: "'a ord"
        and f :: "'a binop"
      assumes semilat: "semilat(A,r,f)"

    lemma order_refl [simp, intro]:
      "order r ==> x <=_r x";
      by (simp add: order_def)

    lemma order_antisym:
      "[| order r; x <=_r y; y <=_r x |] ==> x = y"
    apply (unfold order_def)
    apply (simp (no_asm_simp))
    done

    lemma order_trans:
       "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"
    apply (unfold order_def)
    apply blast
    done

    lemma order_less_irrefl [intro, simp]:
       "order r ==> ~ x <_r x"
    apply (unfold order_def lesssub_def)
    apply blast
    done

    lemma order_less_trans:
      "[| order r; x <_r y; y <_r z |] ==> x <_r z"
    apply (unfold order_def lesssub_def)
    apply blast
    done

    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)"
    apply (unfold semilat_def split_conv [THEN eq_reflection])
    apply (rule refl [THEN eq_reflection])
    done

    lemma (in semilat) orderI [simp, intro]:
      "order r"
      by (insert semilat) (simp add: semilat_Def)

    lemma (in semilat) closedI [simp, intro]:
      "closed A f"
      by (insert semilat) (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"
      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:
      "[| x:A; y:A |] ==> (x <=_r y) = (x +_f y = y)"
    apply (rule iffI)
     apply (blast intro: antisym_r refl_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 order_refl 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 |]
      ==> 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 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 (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)

    subsection{*An executable lub-finder*}

    constdefs
     exec_lub :: "('a * 'a) set => ('a => 'a) => 'a binop"
    "exec_lub r f x y == while (λz. (x,z) ∉ r*) f y"

    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 (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv)

    end

lemma order_refl:

      order r ==> x <=_r x

lemma order_antisym:

      [| order r; x <=_r y; y <=_r x |] ==> x = y

lemma order_trans:

      [| order r; x <=_r y; y <=_r z |] ==> x <=_r z

lemma order_less_irrefl:

      order r ==> ¬ x <_r x

lemma order_less_trans:

      [| order r; x <_r y; y <_r z |] ==> x <_r z

lemma topD:

      top r T ==> x <=_r T

lemma top_le_conv:

      [| order r; top r T |] ==> (T <=_r x) = (x = T)

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)

lemma orderI:

      semilat (A, r, f) ==> order r

lemma closedI:

      semilat (A, r, f) ==> closed A f

lemma closedD:

      [| closed A f; x ∈ A; y ∈ A |] ==> x +_f y ∈ A

lemma closed_UNIV:

      closed UNIV f

lemma closed_f:

      [| semilat (A, r, f); x ∈ A; y ∈ A |] ==> x +_f y ∈ A

lemma refl_r:

      semilat (A, r, f) ==> x <=_r x

lemma antisym_r:

      [| semilat (A, r, f); x <=_r y; y <=_r x |] ==> x = y

lemma trans_r:

      [| semilat (A, r, f); x <=_r y; y <=_r z |] ==> x <=_r z

lemma ub1:

      [| semilat (A, r, f); x ∈ A; y ∈ A |] ==> x <=_r x +_f y

lemma ub2:

      [| semilat (A, r, f); x ∈ A; y ∈ A |] ==> y <=_r x +_f y

lemma lub:

      [| semilat (A, r, f); x <=_r z; y <=_r z; x ∈ A; y ∈ A; z ∈ A |]
      ==> x +_f y <=_r z

lemma plus_le_conv:

      [| semilat (A, r, f); x ∈ A; y ∈ A; z ∈ A |]
      ==> (x +_f y <=_r z) = (x <=_r z ∧ y <=_r z)

lemma le_iff_plus_unchanged:

      [| semilat (A, r, f); x ∈ A; y ∈ A |] ==> (x <=_r y) = (x +_f y = y)

lemma le_iff_plus_unchanged2:

      [| semilat (A, r, f); x ∈ A; y ∈ A |] ==> (x <=_r y) = (y +_f x = y)

lemma plus_assoc:

      [| semilat (A, r, f); a ∈ A; b ∈ A; c ∈ A |] ==> a +_f (b +_f c) = a +_f b +_f c

lemma plus_com_lemma:

      [| semilat (A, r, f); a ∈ A; b ∈ A |] ==> a +_f b <=_r b +_f a

lemma plus_commutative:

      [| semilat (A, r, f); a ∈ A; b ∈ A |] ==> a +_f b = b +_f a

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)

lemma is_ubI:

      [| (x, u) ∈ r; (y, u) ∈ r |] ==> is_ub r x y u

lemma is_ubD:

      is_ub r x y u ==> (x, u) ∈ r ∧ (y, u) ∈ r

lemma is_lub_bigger1:

      is_lub (r*) x y y = ((x, y) ∈ r*)

lemma is_lub_bigger2:

      is_lub (r*) x y x = ((y, x) ∈ r*)

lemma extend_lub:

      [| single_valued r; is_lub (r*) x y u; (x', x) ∈ r |] ==> ∃v. is_lub (r*) x' y v

lemma single_valued_has_lubs:

      [| single_valued r; (x, u) ∈ r*; (y, u) ∈ r* |] ==> Ex (is_lub (r*) x y)

lemma some_lub_conv:

      [| acyclic r; is_lub (r*) x y u |] ==> some_lub (r*) x y = u

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)

### An executable lub-finder

lemma acyclic_single_valued_finite:

      [| acyclic r; single_valued r; (x, y) ∈ r* |]
      ==> finite (r ∩ {a. (x, a) ∈ r*} × {b. (b, y) ∈ r*})

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

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)