Theory JVM_SemiType

Up to index of Isabelle/HOL/Jinja

theory JVM_SemiType = SemiType: 
(*  Title:      HOL/MicroJava/BV/JVM.thy
    ID:         $Id: JVM_SemiType.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Gerwin Klein
    Copyright   2000 TUM

*)

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

theory JVM_SemiType = SemiType:

types tyl = "ty err list"
types tys = "ty list"
types tyi = "tys × tyl"
types tyi' = "tyi option"
types tym = "tyi' list"
types tyP = "mname => cname => tym"


constdefs
  stk_esl :: "'c prog => nat => tys esl"
  "stk_esl P mxs ≡ upto_esl mxs (SemiType.esl P)"

  loc_sl :: "'c prog => nat => tyl sl"
  "loc_sl P mxl ≡ Listn.sl mxl (Err.sl (SemiType.esl P))"

  sl :: "'c prog => nat => nat => tyi' err sl"
  "sl P mxs mxl ≡
  Err.sl(Opt.esl(Product.esl (stk_esl P mxs) (Err.esl(loc_sl P mxl))))"


constdefs
  states :: "'c prog => nat => nat => tyi' err set"
  "states P mxs mxl ≡ fst(sl P mxs mxl)"

  le :: "'c prog => nat => nat => tyi' err ord"
  "le P mxs mxl ≡ fst(snd(sl P mxs mxl))"

  sup :: "'c prog => nat => nat => tyi' err binop"
  "sup P mxs mxl ≡ snd(snd(sl P mxs mxl))"


constdefs
  sup_ty_opt :: "['c prog,ty err,ty err] => bool" 
                 ("_ |- _ <=T _" [71,71,71] 70)
  "sup_ty_opt P ≡ Err.le (subtype P)"

  sup_state :: "['c prog,tyi,tyi] => bool"   
                 ("_ |- _ <=i _"  [71,71,71] 70)
  "sup_state P ≡ Product.le (Listn.le (subtype P)) (Listn.le (sup_ty_opt P))"

  sup_state_opt :: "['c prog,tyi',tyi'] => bool" 
                 ("_ |- _ <=' _"  [71,71,71] 70)
  "sup_state_opt P ≡ Opt.le (sup_state P)"

syntax
  sup_loc :: "['c prog,tyl,tyl] => bool" 
                 ("_ |- _ [<=T] _"  [71,71,71] 70)


syntax (xsymbols)
  sup_ty_opt    :: "['c prog, ty err, ty err] => bool" 
                   ("_ \<turnstile> _ ≤\<top> _" [71,71,71] 70)
  sup_loc       :: "['c prog, tyl, tyl] => bool"
                   ("_ \<turnstile> _ [≤\<top>] _"  [71,71,71] 70)
  sup_state     :: "['c prog, tyi, tyi] => bool" 
                   ("_ \<turnstile> _ ≤i _" [71,71,71] 70)
  sup_state_opt :: "['c prog, tyi', tyi'] => bool"
                   ("_ \<turnstile> _ ≤' _" [71,71,71] 70)

translations
  "P \<turnstile> LT [≤\<top>] LT'" == "list_all2 (sup_ty_opt P) LT LT'"


section "Unfolding"

lemma JVM_states_unfold: 
  "states P mxs mxl ≡ err(opt((Union {list n (types P) |n. n <= mxs}) <*>
                                 list mxl (err(types P))))"
(*<*)
  apply (unfold states_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
  apply simp
  done
(*>*)

lemma JVM_le_unfold:
 "le P m n ≡ 
  Err.le(Opt.le(Product.le(Listn.le(subtype P))(Listn.le(Err.le(subtype P)))))" 
(*<*)
  apply (unfold le_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def  
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def) 
  apply simp
  done
(*>*)
    
lemma sl_def2:
  "JVM_SemiType.sl P mxs mxl ≡ 
  (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)"
(*<*) by (unfold JVM_SemiType.sup_def states_def JVM_SemiType.le_def) simp (*>*)


lemma JVM_le_conv:
  "le P m n (OK t1) (OK t2) = P \<turnstile> t1 ≤' t2"
(*<*) by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def  
                sup_state_def sup_ty_opt_def) (*>*)

lemma JVM_le_Err_conv:
  "le P m n = Err.le (sup_state_opt P)"
(*<*) by (unfold sup_state_opt_def sup_state_def  
             sup_ty_opt_def JVM_le_unfold) simp (*>*)

lemma err_le_unfold [iff]: 
  "Err.le r (OK a) (OK b) = r a b"
(*<*) by (simp add: Err.le_def lesub_def) (*>*)
  

section {* Semilattice *}

lemma order_sup_state_opt [intro, simp]: 
  "wf_prog wf_mb P ==> order (sup_state_opt P)"   
(*<*) by (unfold sup_state_opt_def sup_state_def sup_ty_opt_def) blast (*>*)

lemma semilat_JVM [intro?]:
  "wf_prog wf_mb P ==> semilat (JVM_SemiType.sl P mxs mxl)"
(*<*)
  apply (unfold JVM_SemiType.sl_def stk_esl_def loc_sl_def)  
  apply (blast intro: err_semilat_Product_esl err_semilat_upto_esl 
                      Listn_sl err_semilat_JType_esl)
  done
(*>*)

lemma acc_JVM [intro]:
  "wf_prog wf_mb P ==> acc (JVM_SemiType.le P mxs mxl)"
(*<*) by (unfold JVM_le_unfold) blast (*>*)


section {* Widening with @{text "\<top>"} *}

lemma subtype_refl[iff]: "subtype P t t" (*<*) by (simp add: fun_of_def) (*>*)

lemma sup_ty_opt_refl [iff]: "P \<turnstile> T ≤\<top> T"
(*<*)
  apply (unfold sup_ty_opt_def)
  apply (fold lesub_def)
  apply (rule le_err_refl)
  apply (simp add: lesub_def)
  done
(*>*)

lemma Err_any_conv [iff]: "P \<turnstile> Err ≤\<top> T = (T = Err)"
(*<*) by (unfold sup_ty_opt_def) (rule Err_le_conv [simplified lesub_def]) (*>*)

lemma any_Err [iff]: "P \<turnstile> T ≤\<top> Err"
(*<*) by (unfold sup_ty_opt_def) (rule le_Err [simplified lesub_def]) (*>*)

lemma OK_OK_conv [iff]:
  "P \<turnstile> OK T ≤\<top> OK T' = P \<turnstile> T ≤ T'"
(*<*) by (simp add: sup_ty_opt_def fun_of_def) (*>*)

lemma any_OK_conv [iff]:
  "P \<turnstile> X ≤\<top> OK T' = (∃T. X = OK T ∧ P \<turnstile> T ≤ T')"
(*<*)
  apply (unfold sup_ty_opt_def) 
  apply (unfold fun_of_def)
  apply (rule le_OK_conv [simplified lesub_def])
  done  
(*>*)

lemma OK_any_conv:
 "P \<turnstile> OK T ≤\<top> X = (X = Err ∨ (∃T'. X = OK T' ∧ P \<turnstile> T ≤ T'))"
(*<*)
  apply (unfold sup_ty_opt_def) 
  apply (unfold fun_of_def)
  apply (rule OK_le_conv [simplified lesub_def])
  done
(*>*)

lemma sup_ty_opt_trans [intro?, trans]:
  "[|P \<turnstile> a ≤\<top> b; P \<turnstile> b ≤\<top> c|] ==> P \<turnstile> a ≤\<top> c"
(*<*) by (auto intro: widen_trans  
           simp add: sup_ty_opt_def Err.le_def lesub_def fun_of_def
           split: err.splits) (*>*)


section "Stack and Registers"

lemma stk_convert:
  "P \<turnstile> ST [≤] ST' = Listn.le (subtype P) ST ST'"
(*<*) by (simp add: Listn.le_def lesub_def) (*>*)

lemma sup_loc_refl [iff]: "P \<turnstile> LT [≤\<top>] LT"
(*<*) by (rule list_all2_refl) simp (*>*)

lemmas sup_loc_Cons1 [iff] = list_all2_Cons1 [of "sup_ty_opt P", standard]

lemma sup_loc_def:
  "P \<turnstile> LT [≤\<top>] LT' ≡ Listn.le (sup_ty_opt P) LT LT'"
(*<*) by (unfold Listn.le_def lesub_def) (*>*)

lemma sup_loc_widens_conv [iff]:
  "P \<turnstile> map OK Ts [≤\<top>] map OK Ts' = P \<turnstile> Ts [≤] Ts'"
(*<*)
  apply (simp add: list_all2_map1 list_all2_map2)
  apply (fold fun_of_def)
  apply (rule refl)
  done 
(*>*)


lemma sup_loc_trans [intro?, trans]:
  "[|P \<turnstile> a [≤\<top>] b; P \<turnstile> b [≤\<top>] c|] ==> P \<turnstile> a [≤\<top>] c"
(*<*) by (rule list_all2_trans, rule sup_ty_opt_trans) (*>*)


section "State Type"

lemma sup_state_conv [iff]:
  "P \<turnstile> (ST,LT) ≤i (ST',LT') = (P \<turnstile> ST [≤] ST' ∧ P \<turnstile> LT [≤\<top>] LT')"
(*<*) by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_def) (*>*)
  
lemma sup_state_conv2:
  "P \<turnstile> s1 ≤i s2 = (P \<turnstile> fst s1 [≤] fst s2 ∧ P \<turnstile> snd s1 [≤\<top>] snd s2)"
(*<*) by (cases s1, cases s2) simp (*>*)

lemma sup_state_refl [iff]: "P \<turnstile> s ≤i s"
(*<*) by (auto simp add: sup_state_conv2) (*>*)

lemma sup_state_trans [intro?, trans]:
  "[|P \<turnstile> a ≤i b; P \<turnstile> b ≤i c|] ==> P \<turnstile> a ≤i c"
(*<*) by (auto intro: sup_loc_trans widens_trans simp add: sup_state_conv2) (*>*)


lemma sup_state_opt_None_any [iff]:
  "P \<turnstile> None ≤' s"
(*<*) by (simp add: sup_state_opt_def Opt.le_def) (*>*)

lemma sup_state_opt_any_None [iff]:
  "P \<turnstile> s ≤' None = (s = None)"
(*<*) by (simp add: sup_state_opt_def Opt.le_def) (*>*)

lemma sup_state_opt_Some_Some [iff]:
  "P \<turnstile> Some a ≤' Some b = P \<turnstile> a ≤i b"  
(*<*) by (simp add: sup_state_opt_def Opt.le_def lesub_def) (*>*)

lemma sup_state_opt_any_Some:
  "P \<turnstile> (Some s) ≤' X = (∃s'. X = Some s' ∧ P \<turnstile> s ≤i s')"
(*<*) by (simp add: sup_state_opt_def Opt.le_def lesub_def) (*>*)

lemma sup_state_opt_refl [iff]: "P \<turnstile> s ≤' s"
(*<*) by (simp add: sup_state_opt_def Opt.le_def lesub_def) (*>*)

lemma sup_state_opt_trans [intro?, trans]:
  "[|P \<turnstile> a ≤' b; P \<turnstile> b ≤' c|] ==> P \<turnstile> a ≤' c"
(*<*)
  apply (unfold sup_state_opt_def Opt.le_def lesub_def)
  apply (simp del: split_paired_All)
  apply (rule sup_state_trans, assumption+)
  done
(*>*)

end

Unfolding

lemma JVM_states_unfold: 

  states P mxs mxl ==
  err (opt (Union {list n (types P) |n. n <= mxs} <*> list mxl (err (types P))))

lemma JVM_le_unfold: 

  JVM_SemiType.le P m n ==
  Err.le
   (Opt.le (Product.le (Listn.le (subtype P)) (Listn.le (Err.le (subtype P)))))

lemma sl_def2: 

  JVM_SemiType.sl P mxs mxl ==
  (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)

lemma JVM_le_conv: 

  JVM_SemiType.le P m n (OK t1) (OK t2) = P |- t1 <=' t2

lemma JVM_le_Err_conv: 

  JVM_SemiType.le P m n = Err.le (sup_state_opt P)

lemma err_le_unfold: 

  Err.le r (OK a) (OK b) = r a b

Semilattice

lemma order_sup_state_opt: 

  wf_prog wf_mb P ==> order (sup_state_opt P)

lemma semilat_JVM: 

  wf_prog wf_mb P ==> semilat (JVM_SemiType.sl P mxs mxl)

lemma acc_JVM: 

  wf_prog wf_mb P ==> acc (JVM_SemiType.le P mxs mxl)

Widening with @{text "\<top>"}

lemma subtype_refl: 

  (subtype P) t t

lemma sup_ty_opt_refl: 

  P |- T <=T T

lemma Err_any_conv: 

  P |- Err <=T T = (T = Err)

lemma any_Err: 

  P |- T <=T Err

lemma OK_OK_conv: 

  P |- OK T <=T OK T' = widen P T T'

lemma any_OK_conv: 

  P |- X <=T OK T' = (EX T. X = OK T & widen P T T')

lemma OK_any_conv: 

  P |- OK T <=T X = (X = Err | (EX T'. X = OK T' & widen P T T'))

lemma sup_ty_opt_trans: 

  [| P |- a <=T b; P |- b <=T c |] ==> P |- a <=T c

Stack and Registers

lemma stk_convert: 

  widens P ST ST' = Listn.le (subtype P) ST ST'

lemma sup_loc_refl: 

  P |- LT [<=T] LT

lemmas sup_loc_Cons1: 

  P |- (x # xs) [<=T] ys =
  (EX z zs. ys = z # zs & P |- x <=T z & P |- xs [<=T] zs)

lemma sup_loc_def: 

  P |- LT [<=T] LT' == Listn.le (sup_ty_opt P) LT LT'

lemma sup_loc_widens_conv: 

  P |- map OK Ts [<=T] map OK Ts' = widens P Ts Ts'

lemma sup_loc_trans: 

  [| P |- a [<=T] b; P |- b [<=T] c |] ==> P |- a [<=T] c

State Type

lemma sup_state_conv: 

  P |- (ST, LT) <=i (ST', LT') = (widens P ST ST' & P |- LT [<=T] LT')

lemma sup_state_conv2: 

  P |- s1 <=i s2 = (widens P (fst s1) (fst s2) & P |- snd s1 [<=T] snd s2)

lemma sup_state_refl: 

  P |- s <=i s

lemma sup_state_trans: 

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

lemma sup_state_opt_None_any: 

  P |- None <=' s

lemma sup_state_opt_any_None: 

  P |- s <=' None = (s = None)

lemma sup_state_opt_Some_Some: 

  P |- ⌊a⌋ <=' ⌊b⌋ = P |- a <=i b

lemma sup_state_opt_any_Some: 

  P |- ⌊s⌋ <=' X = (EX s'. X = ⌊s'⌋ & P |- s <=i s')

lemma sup_state_opt_refl: 

  P |- s <=' s

lemma sup_state_opt_trans: 

  [| P |- a <=' b; P |- b <=' c |] ==> P |- a <=' c