Theory JVMType

Up to index of Isabelle/HOL/jsr

(*  Title:      HOL/MicroJava/BV/JVM.thy
    ID:         $Id: JVMType.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2000 TUM
*)

header {* \isaheader{The JVM Type System as Semilattice} *}

theory JVMType = Product + Listn + JType:

types
  locvars_type = "init_ty err list"
  opstack_type = "init_ty list"
  state_type   = "opstack_type × locvars_type"
  state_bool   = "state_type × bool"

  address_type = "state_bool set"
  state        = "address_type err"    -- "for Kildall"
  method_type  = "address_type list"   -- "for BVSpec"

  class_type   = "sig \<Rightarrow> method_type"
  prog_type    = "cname \<Rightarrow> class_type"

constdefs
  address_types :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> address_type"
  "address_types G maxs maxr maxpc \<equiv> 
  ((Union {list n (init_tys G maxpc) |n. n \<le> maxs}) × list maxr (err (init_tys G maxpc))) × {True,False}"

  states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state set"
  "states G maxs maxr maxpc \<equiv> err (Pow (address_types G maxs maxr maxpc))"

  sl :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state sl"
  "sl G maxs maxr maxpc \<equiv> SetSemilat.sl (address_types G maxs maxr maxpc)"


constdefs
  le :: "state ord"
  "le \<equiv> Err.le (op \<subseteq>)"

  sup :: "state binop"
  "sup \<equiv> lift2 (\<lambda>x y. OK (x \<union> y))"


lemma sl_def2:
  "sl G mxs mxr mpc \<equiv> (states G mxs mxr mpc, le, sup)"
  by (unfold sl_def SetSemilat.sl_def Err.sl_def 
             Err.esl_def sup_def states_def le_def) simp

lemma states_def2: 
  "states G mxs mxr mpc \<equiv> fst (sl G mxs mxr mpc)"
  by (unfold sl_def2) simp

lemma le_def2: 
  "le \<equiv> fst (snd (sl G mxs mxr mpc))"
  by (unfold sl_def2) simp

lemma sup_def2: 
  "sup \<equiv> snd (snd (sl G mxs mxr mpc))"
  by (unfold sl_def2) simp


lemma finite_list [intro!]:
  assumes A: "finite A"
  shows "finite (list n A)"
proof (induct n)
  have "list 0 A = {[]}" by auto
  thus "finite (list 0 A)" by simp
next
  fix n assume "finite (list n A)"
  moreover
  have "list (Suc n) A = split Cons ` (A × list n A)"
    by (unfold list_def) (auto simp add: length_Suc_conv)
  ultimately
  show "finite (list (Suc n) A)" using A
    by (auto intro: finite_imageI)
qed

lemma finite_Union [intro!]:
  "finite X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> finite x) \<Longrightarrow> finite (Union X)"
  by (simp add: Union_def)

lemma finite_count [intro!,simp]:
  "finite {f x|x. x \<le> (n::nat)}"
proof (induct n)
  show "finite {f x |x. x \<le> 0}" by simp
next
  fix n assume "finite {f x |x. x \<le> n}"
  moreover
  have "{f x |x. x \<le> Suc n} = {f (Suc n)} \<union> {f x |x. x \<le> n}" 
  proof
    show "{f (Suc n)} \<union> {f x |x. x \<le> n} \<subseteq> {f x |x. x \<le> Suc n}" by auto
    { fix y assume "y \<in> {f x |x. x \<le> Suc n}"
      then obtain x where y: "y = f x" and "x \<le> Suc n" by auto
      hence "x \<le> n \<or> x = Suc n" by auto
      with y have "y \<in> {f (Suc n)} \<union> {f x |x. x \<le> n}" by auto
     } 
     thus "{f x |x. x \<le> Suc n} \<subseteq> {f (Suc n)} \<union> {f x |x. x \<le> n}" ..
   qed
   ultimately
   show "finite {f x |x. x \<le> Suc n}" by simp
qed

lemma finite_Union_list [intro!]:
  "finite A \<Longrightarrow> finite (Union {list n A|n. n \<le> m})"
  by auto

lemma finite_productI [intro!]:
  "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A × B)"
  by (erule finite_induct) auto

lemma finite_err [iff]:
  "finite (err A) = finite A"
proof -
  have "err A = insert Err (OK`A)" by (unfold err_def) auto
  moreover have "inj_on OK A" by (unfold inj_on_def) auto
  ultimately show ?thesis by (auto intro: finite_imageI dest: finite_imageD)
qed
    
lemma semilat_JVM: "semilat (sl G mxs mxr mpc)"  
  by (unfold sl_def) (rule semilat_set)

lemma finite_address_types: "finite (address_types G mxs mxr mpc)"
  apply (insert finite_init_tys [of G mpc])
  apply (unfold address_types_def)
  apply auto
  done
  
lemma acc_JVM: "acc le (states G mxs mxr mpc)"
  apply (unfold states_def le_def)
  apply (rule acc_err)
  apply (rule acc_set)
  apply (rule finite_address_types)
  done

end

lemma sl_def2:

  JVMType.sl G mxs mxr mpc == (states G mxs mxr mpc, JVMType.le, JVMType.sup)

lemma states_def2:

  states G mxs mxr mpc == fst (JVMType.sl G mxs mxr mpc)

lemma le_def2:

  JVMType.le == fst (snd (JVMType.sl G mxs mxr mpc))

lemma sup_def2:

  JVMType.sup == snd (snd (JVMType.sl G mxs mxr mpc))

lemma

  finite A ==> finite (list n A)

lemma finite_Union:

  [| finite X; !!x. x : X ==> finite x |] ==> finite (Union X)

lemma finite_count:

  finite {f x |x. x <= n}

lemma finite_Union_list:

  finite A ==> finite (Union {list n A |n. n <= m})

lemma finite_productI:

  [| finite A; finite B |] ==> finite (A <*> B)

lemma finite_err:

  finite (err A) = finite A

lemma semilat_JVM:

  semilat (JVMType.sl G mxs mxr mpc)

lemma finite_address_types:

  finite (address_types G mxs mxr mpc)

lemma acc_JVM:

  acc JVMType.le (states G mxs mxr mpc)