# Theory SemilatAlg

Up to index of Isabelle/HOL/MicroJava

theory SemilatAlg
imports Typing_Framework Product
begin

    (*  Title:      HOL/MicroJava/BV/SemilatAlg.thy
        ID:         $Id: SemilatAlg.thy,v 1.6 2005/06/17 14:13:08 haftmann Exp $
        Author:     Gerwin Klein
        Copyright   2002 Technische Universitaet Muenchen
    *)

    header {* \isaheader{More on Semilattices} *}

    theory SemilatAlg imports Typing_Framework Product begin

    constdefs
      lesubstep_type :: "(nat × 's) list => 's ord => (nat × 's) list => bool"
                        ("(_ /<=|_| _)" [50, 0, 51] 50)
      "x <=|r| y ≡ ∀(p,s) ∈ set x. ∃s'. (p,s') ∈ set y ∧ s <=_r s'"

    consts
     "@plusplussub" :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
    primrec
      "[] ++_f y = y"
      "(x#xs) ++_f y = xs ++_f (x +_f y)"

    constdefs
     bounded :: "'s step_type => nat => bool"
    "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"

     pres_type :: "'s step_type => nat => 's set => bool"
    "pres_type step n A == ∀s∈A. ∀p<n. ∀(q,s')∈set (step p s). s' ∈ A"

     mono :: "'s ord => 's step_type => nat => 's set => bool"
    "mono r step n A ==
     ∀s p t. s ∈ A ∧ p < n ∧ s <=_r t --> step p s <=|r| step p t"

    lemma pres_typeD:
      "[| pres_type step n A; s∈A; p<n; (q,s')∈set (step p s) |] ==> s' ∈ A"
      by (unfold pres_type_def, blast)

    lemma monoD:
      "[| mono r step n A; p < n; s∈A; s <=_r t |] ==> step p s <=|r| step p t"
      by (unfold mono_def, blast)

    lemma boundedD:
      "[| bounded step n; p < n; (q,t) : set (step p xs) |] ==> q < n"
      by (unfold bounded_def, blast)

    lemma lesubstep_type_refl [simp, intro]:
      "(!!x. x <=_r x) ==> x <=|r| x"
      by (unfold lesubstep_type_def) auto

    lemma lesub_step_typeD:
      "a <=|r| b ==> (x,y) ∈ set a ==> ∃y'. (x, y') ∈ set b ∧ y <=_r y'"
      by (unfold lesubstep_type_def) blast

    lemma list_update_le_listI [rule_format]:
      "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->
       x <=_r ys!p --> semilat(A,r,f) --> x∈A -->
       xs[p := x +_f xs!p] <=[r] ys"
      apply (unfold Listn.le_def lesub_def semilat_def)
      apply (simp add: list_all2_conv_all_nth nth_list_update)
      done

    lemma plusplus_closed: includes semilat shows
      "!!y. [| set x ⊆ A; y ∈ A|] ==> x ++_f y ∈ A"
    proof (induct x)
      show "!!y. y ∈ A ==> [] ++_f y ∈ A" by simp
      fix y x xs
      assume y: "y ∈ A" and xs: "set (x#xs) ⊆ A"
      assume IH: "!!y. [| set xs ⊆ A; y ∈ A|] ==> xs ++_f y ∈ A"
      from xs obtain x: "x ∈ A" and "set xs ⊆ A" by simp
      from x y have "(x +_f y) ∈ A" ..
      with xs have "xs ++_f (x +_f y) ∈ A" by - (rule IH)
      thus "(x#xs) ++_f y ∈ A" by simp
    qed

    lemma (in semilat) pp_ub2:
     "!!y. [| set x ⊆ A; y ∈ A|] ==> y <=_r x ++_f y"
    proof (induct x)
      from semilat show "!!y. y <=_r [] ++_f y" by simp

      fix y a l
      assume y:  "y ∈ A"
      assume "set (a#l) ⊆ A"
      then obtain a: "a ∈ A" and x: "set l ⊆ A" by simp
      assume "!!y. [|set l ⊆ A; y ∈ A|] ==> y <=_r l ++_f y"
      hence IH: "!!y. y ∈ A ==> y <=_r l ++_f y" .

      from a y have "y <=_r a +_f y" ..
      also from a y have "a +_f y ∈ A" ..
      hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
      finally have "y <=_r l ++_f (a +_f y)" .
      thus "y <=_r (a#l) ++_f y" by simp
    qed

    lemma (in semilat) pp_ub1:
    shows "!!y. [|set ls ⊆ A; y ∈ A; x ∈ set ls|] ==> x <=_r ls ++_f y"
    proof (induct ls)
      show "!!y. x ∈ set [] ==> x <=_r [] ++_f y" by simp

      fix y s ls
      assume "set (s#ls) ⊆ A"
      then obtain s: "s ∈ A" and ls: "set ls ⊆ A" by simp
      assume y: "y ∈ A"

      assume
        "!!y. [|set ls ⊆ A; y ∈ A; x ∈ set ls|] ==> x <=_r ls ++_f y"
      hence IH: "!!y. x ∈ set ls ==> y ∈ A ==> x <=_r ls ++_f y" .

      assume "x ∈ set (s#ls)"
      then obtain xls: "x = s ∨ x ∈ set ls" by simp
      moreover {
        assume xs: "x = s"
        from s y have "s <=_r s +_f y" ..
        also from s y have "s +_f y ∈ A" ..
        with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)
        finally have "s <=_r ls ++_f (s +_f y)" .
        with xs have "x <=_r ls ++_f (s +_f y)" by simp
      }
      moreover {
        assume "x ∈ set ls"
        hence "!!y. y ∈ A ==> x <=_r ls ++_f y" by (rule IH)
        moreover from s y have "s +_f y ∈ A" ..
        ultimately have "x <=_r ls ++_f (s +_f y)" .
      }
      ultimately
      have "x <=_r ls ++_f (s +_f y)" by blast
      thus "x <=_r (s#ls) ++_f y" by simp
    qed

    lemma (in semilat) pp_lub:
      assumes "z ∈ A"
      shows
      "!!y. y ∈ A ==> set xs ⊆ A ==> ∀x ∈ set xs. x <=_r z ==> y <=_r z ==> xs ++_f y <=_r z"
    proof (induct xs)
      fix y assume "y <=_r z" thus "[] ++_f y <=_r z" by simp
    next
      fix y l ls assume y: "y ∈ A" and "set (l#ls) ⊆ A"
      then obtain l: "l ∈ A" and ls: "set ls ⊆ A" by auto
      assume "∀x ∈ set (l#ls). x <=_r z"
      then obtain "l <=_r z" and lsz: "∀x ∈ set ls. x <=_r z" by auto
      assume "y <=_r z" have "l +_f y <=_r z" ..
      moreover
      from l y have "l +_f y ∈ A" ..
      moreover
      assume "!!y. y ∈ A ==> set ls ⊆ A ==> ∀x ∈ set ls. x <=_r z ==> y <=_r z
              ==> ls ++_f y <=_r z"
      ultimately
      have "ls ++_f (l +_f y) <=_r z" using ls lsz by -
      thus "(l#ls) ++_f y <=_r z" by simp
    qed

    lemma ub1': includes semilat
    shows "[|∀(p,s) ∈ set S. s ∈ A; y ∈ A; (a,b) ∈ set S|]
      ==> b <=_r map snd [(p', t')∈S. p' = a] ++_f y"
    proof -
      let "b <=_r ?map ++_f y" = ?thesis

      assume "y ∈ A"
      moreover
      assume "∀(p,s) ∈ set S. s ∈ A"
      hence "set ?map ⊆ A" by auto
      moreover
      assume "(a,b) ∈ set S"
      hence "b ∈ set ?map" by (induct S, auto)
      ultimately
      show ?thesis by - (rule pp_ub1)
    qed

    lemma plusplus_empty:
      "∀s'. (q, s') ∈ set S --> s' +_f ss ! q = ss ! q ==>
       (map snd [(p', t')∈ S. p' = q] ++_f ss ! q) = ss ! q"
    apply (induct S)
    apply auto
    done

    end

lemma pres_typeD:

      [| pres_type step n A; s ∈ A; p < n; (q, s') ∈ set (step p s) |] ==> s' ∈ A

lemma monoD:

      [| SemilatAlg.mono r step n A; p < n; s ∈ A; s <=_r t |]
      ==> step p s <=|r| step p t

lemma boundedD:

      [| bounded step n; p < n; (q, t) ∈ set (step p xs) |] ==> q < n

lemma lesubstep_type_refl:

      (!!x. x <=_r x) ==> x <=|r| x

lemma lesub_step_typeD:

      [| a <=|r| b; (x, y) ∈ set a |] ==> ∃y'. (x, y') ∈ set b ∧ y <=_r y'

lemma list_update_le_listI:

      [| set xs ⊆ A; set ys ⊆ A; xs <=[r] ys; p < length xs; x <=_r ys ! p;
         semilat (A, r, f); x ∈ A |]
      ==> xs[p := x +_f xs ! p] <=[r] ys

lemma plusplus_closed:

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

lemma pp_ub2:

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

lemma pp_ub1:

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

lemma pp_lub:

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

lemma ub1':

      [| semilat (A, r, f); ∀(p, s)∈set S. s ∈ A; y ∈ A; (a, b) ∈ set S |]
      ==> b <=_r map snd [(p', t')∈S . p' = a] ++_f y

lemma plusplus_empty:

      ∀s'. (q, s') ∈ set S --> s' +_f ss ! q = ss ! q
      ==> map snd [(p', t')∈S . p' = q] ++_f ss ! q = ss ! q