Theory JType

Up to index of Isabelle/HOL/jsr

theory JType = WellForm + SetSemilat:
(*  Title:      HOL/MicroJava/BV/JType.thy
    ID:         $Id: JType.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

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

theory JType = WellForm + SetSemilat:

consts
  boundedRA :: "nat × ty \<Rightarrow> bool"
recdef boundedRA "{}"
  "boundedRA (mpc,RA pc) = (pc < mpc)"
  "boundedRA v = True"

constdefs
  init_tys :: "'c prog \<Rightarrow> nat \<Rightarrow> init_ty set"
  "init_tys G maxpc \<equiv> {Init T      |T. is_type G T \<and> boundedRA (maxpc+1,T)} \<union> 
                      {UnInit C pc |C pc. is_class G C \<and> pc < maxpc} \<union> 
                      {PartInit C  |C. is_class G C}"

  init_le :: "'c prog \<Rightarrow> init_ty ord" ("_ |- _ <=i _" [71,71,71] 70)
  "G |- a <=i b \<equiv> case a of 
                    Init t1 \<Rightarrow> (case b of Init t2 \<Rightarrow> G \<turnstile> t1 \<preceq> t2
                                       | UnInit c n \<Rightarrow> False
                                       | PartInit c \<Rightarrow> False)
                  | UnInit c1 n1 \<Rightarrow> a = b
                  | PartInit c1 \<Rightarrow> a = b"



lemma boundedRA_def2:
  "boundedRA (mpc, T) = 
  ((\<exists>pc. T = RA pc \<and> pc < mpc) \<or> 
   T \<in> RefT ` UNIV \<or> 
   T \<in> PrimT ` {Void,Integer,Boolean})"
  apply (cases T)
  apply auto
  apply (case_tac prim_ty)
  apply auto
  done


lemma finite_classes:
  "finite {C. is_class G C}"
proof -
  have "{C. is_class G C} = dom (map_of G)"
    by (auto simp add: is_class_def class_def dom_def)
  thus ?thesis by (simp add: finite_dom_map_of)
qed


lemma finite_init_tys: "finite (init_tys G mpc)"
proof -
  note finite_classes [simp, intro]
  note finite_imageI [simp,intro]

  have "{T. is_type G T \<and> boundedRA (mpc+1,T)} = 
        {Class C|C. is_class G C} \<union> {NT} \<union> 
        PrimT ` {Void,Integer,Boolean} \<union> {RA pc|pc. pc < mpc+1}"
    by (auto simp add: boundedRA_def2 split: ref_ty.splits)
  moreover 
  have "{Class C|C. is_class G C} = RefT ` ClassT ` {C. is_class G C}" by auto
  hence "finite {Class C|C. is_class G C}" by simp
  moreover
  have "\<forall>n. {RA pc|pc. pc < Suc n} = {RA n} \<union> {RA pc|pc. pc < n}" by auto
  hence "finite {RA pc|pc. pc < mpc+1}" by (induct mpc) auto
  ultimately
  have "finite {T. is_type G T \<and> boundedRA (mpc+1, T)}" by simp
  moreover
  have "{Init T|T. is_type G T \<and> boundedRA (mpc+1, T)} = 
        Init ` {T. is_type G T \<and> boundedRA (mpc+1, T)}" by auto
  ultimately
  have "finite {Init T|T. is_type G T \<and> boundedRA (mpc+1, T)}" by simp
  moreover {
    have "\<forall>n. {pc. pc < Suc n} = {n} \<union> {pc. pc < n}" by auto
    hence "finite {pc. pc < mpc}" by (induct mpc) auto      
    moreover
    have "{UnInit C pc |C pc. is_class G C \<and> pc < mpc} = 
          (\<lambda>(C,pc). UnInit C pc) ` ({C. is_class G C} × {pc. pc < mpc})"
      by auto
    ultimately
    have "finite {UnInit C pc |C pc. is_class G C \<and> pc < mpc}" by simp
  }
  moreover 
  have "{PartInit C |C. is_class G C} = PartInit ` {C. is_class G C}" by auto
  hence "finite {PartInit C |C. is_class G C}" by simp 
  ultimately
  show ?thesis by (unfold init_tys_def) auto
qed

lemma acc_JType: "acc (op \<subseteq>) (Pow (init_tys G mpc))" 
  by (rule acc_set [OF finite_init_tys])
  

syntax (xsymbols) 
  init_le :: "['code prog,init_ty,init_ty] \<Rightarrow> bool" ("_ \<turnstile> _ \<preceq>i _" [71,71,71] 70)

lemma le_Init_Init [iff]:
  "G \<turnstile> Init t1 \<preceq>i Init t2 = G \<turnstile> t1 \<preceq> t2"
  by (unfold init_le_def) simp

lemma le_Init_UnInit [iff]:
  "init_le G (Init t) (UnInit c n) = False"
  by (unfold init_le_def) simp

lemma le_UnInit_Init [iff]:
  "init_le G (UnInit c n) (Init t) = False"
  by (unfold init_le_def) simp

lemma le_UnInit_UnInit [iff]:
  "init_le G (UnInit c1 n1) (UnInit c2 n2) = (c1 = c2 \<and> n1 = n2)"
  by (unfold init_le_def) simp

lemma init_le_Init:
  "(G \<turnstile> Init t \<preceq>i x) = (\<exists>t'. x = Init t' \<and> G \<turnstile> t \<preceq> t')"
  by (simp add: init_le_def split: init_ty.splits)

lemma init_le_Init2:
  "(G \<turnstile> x \<preceq>i (Init t')) = (\<exists>t. x = Init t \<and> G \<turnstile> t \<preceq> t')"
  by (cases x, auto simp add: init_le_def)

lemma init_le_UnInit [iff]:
  "(G \<turnstile> UnInit C pc \<preceq>i x) = (x = UnInit C pc)"
  by (cases x, auto simp add: init_le_def)

lemma init_le_UnInit2 [iff]:
  "(G \<turnstile> T \<preceq>i (UnInit C pc)) = (T = UnInit C pc)"
  by (cases T, auto simp add: init_le_def)

lemma init_le_PartInit [iff]:
  "(G \<turnstile> PartInit C \<preceq>i x) = (x = PartInit C)"
  by (cases x, auto simp add: init_le_def)

lemma init_le_PartInit2 [iff]:
  "G \<turnstile> x \<preceq>i PartInit C = (x = PartInit C)"
  by (cases x, auto simp add: init_le_def)

lemma init_refl [iff]: "init_le G x x"
  by (auto simp add: init_le_def split: init_ty.split)

lemma init_trans [trans]: 
  "\<lbrakk> init_le G a b; init_le G b c \<rbrakk> \<Longrightarrow> init_le G a c" 
  by (auto intro: widen_trans 
           simp add: init_le_def split: init_ty.splits)


end

lemma boundedRA_def2:

  boundedRA (mpc, T) =
  ((EX pc. T = RA pc & pc < mpc) |
   T : range RefT | T : PrimT ` {Void, Integer, Boolean})

lemma finite_classes:

  finite (Collect (is_class G))

lemma finite_init_tys:

  finite (init_tys G mpc)

lemma acc_JType:

  acc op <= (Pow (init_tys G mpc))

lemma le_Init_Init:

  G |- Init t1 <=i Init t2 = G |- t1 <= t2

lemma le_Init_UnInit:

  G |- Init t <=i UnInit c n = False

lemma le_UnInit_Init:

  G |- UnInit c n <=i Init t = False

lemma le_UnInit_UnInit:

  G |- UnInit c1 n1 <=i UnInit c2 n2 = (c1 = c2 & n1 = n2)

lemma init_le_Init:

  G |- Init t <=i x = (EX t'. x = Init t' & G |- t <= t')

lemma init_le_Init2:

  G |- x <=i Init t' = (EX t. x = Init t & G |- t <= t')

lemma init_le_UnInit:

  G |- UnInit C pc <=i x = (x = UnInit C pc)

lemma init_le_UnInit2:

  G |- T <=i UnInit C pc = (T = UnInit C pc)

lemma init_le_PartInit:

  G |- PartInit C <=i x = (x = PartInit C)

lemma init_le_PartInit2:

  G |- x <=i PartInit C = (x = PartInit C)

lemma init_refl:

  G |- x <=i x

lemma init_trans:

  [| G |- a <=i b; G |- b <=i c |] ==> G |- a <=i c