Theory JVM_SemiType

(*  Title:      HOL/MicroJava/BV/JVM.thy
    Author:     Gerwin Klein
    Copyright   2000 TUM

*)

section ‹ The JVM Type System as Semilattice ›

theory JVM_SemiType imports SemiType begin

type_synonym ty⇩l = "ty err list"
type_synonym ty⇩s = "ty list"
type_synonym ty⇩i = "ty⇩s × ty⇩l"
type_synonym ty⇩i' = "ty⇩i option"
type_synonym ty⇩m = "ty⇩i' list"
type_synonym ty⇩P = "mname ⇒ cname ⇒ ty⇩m"


definition stk_esl :: "'c prog ⇒ nat ⇒ ty⇩s esl"
where
  "stk_esl P mxs ≡ upto_esl mxs (SemiType.esl P)"

definition loc_sl :: "'c prog ⇒ nat ⇒ ty⇩l sl"
where
  "loc_sl P mxl ≡ Listn.sl mxl (Err.sl (SemiType.esl P))"

definition sl :: "'c prog ⇒ nat ⇒ nat ⇒ ty⇩i' err sl"
where
  "sl P mxs mxl ≡
  Err.sl(Opt.esl(Product.esl (stk_esl P mxs) (Err.esl(loc_sl P mxl))))"


definition states :: "'c prog ⇒ nat ⇒ nat ⇒ ty⇩i' err set"
where "states P mxs mxl ≡ fst(sl P mxs mxl)"

definition le :: "'c prog ⇒ nat ⇒ nat ⇒ ty⇩i' err ord"
where
  "le P mxs mxl ≡ fst(snd(sl P mxs mxl))"

definition sup :: "'c prog ⇒ nat ⇒ nat ⇒ ty⇩i' err binop"
where
  "sup P mxs mxl ≡ snd(snd(sl P mxs mxl))"


definition sup_ty_opt :: "['c prog,ty err,ty err] ⇒ bool" 
    (‹_ ⊢ _ ≤⇩⊤ _› [71,71,71] 70)
where
  "sup_ty_opt P ≡ Err.le (subtype P)"

definition sup_state :: "['c prog,ty⇩i,ty⇩i] ⇒ bool"   
    (‹_ ⊢ _ ≤⇩i _› [71,71,71] 70)
where
  "sup_state P ≡ Product.le (Listn.le (subtype P)) (Listn.le (sup_ty_opt P))"

definition sup_state_opt :: "['c prog,ty⇩i',ty⇩i'] ⇒ bool" 
    (‹_ ⊢ _ ≤'' _› [71,71,71] 70)
where
  "sup_state_opt P ≡ Opt.le (sup_state P)"

abbreviation
  sup_loc :: "['c prog,ty⇩l,ty⇩l] ⇒ bool"  (‹_ ⊢ _ [≤⇩⊤] _›  [71,71,71] 70)
  where "P ⊢ LT [≤⇩⊤] LT' ≡ list_all2 (sup_ty_opt P) LT LT'"

notation (ASCII)
  sup_ty_opt  (‹_ |- _ <=T _› [71,71,71] 70) and
  sup_state  (‹_ |- _ <=i _›  [71,71,71] 70) and
  sup_state_opt  (‹_ |- _ <=' _›  [71,71,71] 70) and
  sup_loc  (‹_ |- _ [<=T] _›  [71,71,71] 70)


subsection "Unfolding"

lemma JVM_states_unfold: 
  "states P mxs mxl ≡ err(opt((Union {nlists n (types P) |n. n <= mxs}) ×
                                 nlists mxl (err(types P))))"
(*<*)
  by (simp add: 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)
(*>*)

lemma JVM_le_unfold:
 "le P m n ≡ 
  Err.le(Opt.le(Product.le(Listn.le(subtype P))(Listn.le(Err.le(subtype P)))))" 
(*<*)
  by (simp add: 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)
(*>*)
    
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 ⊢ 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) (*>*)
  

subsection ‹ Semilattice ›
lemma order_sup_state_opt' [intro, simp]:
  "wf_prog wf_mb P ⟹ 
      order (sup_state_opt P) (opt ((⋃ {nlists n (types P) |n. n ≤ mxs} ) × nlists (Suc (length Ts + mxl⇩0)) (err (types P))))"   
(*<*) 
  unfolding sup_state_opt_def sup_state_def sup_ty_opt_def   
  by (blast intro:order_le_prodI) ―‹ use Listn.thy.order_listI2  ›
(*<*) 
lemma order_sup_state_opt'' [intro, simp]:
  "wf_prog wf_mb P ⟹ 
      order (sup_state_opt P) (opt ((⋃ {nlists n (types P) |n. n ≤ mxs} ) × nlists ((length Ts + mxl⇩0)) (err (types P))))"   
(*<*) 
  unfolding sup_state_opt_def sup_state_def sup_ty_opt_def   
  by (blast intro:order_le_prodI) ―‹ use Listn.thy.order_listI2  ›
(*<*)
(*
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)"
(*<*)
  unfolding 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
(*>*)

subsection ‹ Widening with @{text "⊤"} ›

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

lemma sup_ty_opt_refl [iff]: "P ⊢ T ≤⇩⊤ T"
(*<*)
  unfolding sup_ty_opt_def
  by (metis le_err_refl lesub_def subtype_refl)
(*>*)

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

lemma any_Err [iff]: "P ⊢ T ≤⇩⊤ Err"
(*<*) by (unfold sup_ty_opt_def) (rule le_Err [simplified lesub_def]) (*>*)

lemma OK_OK_conv [iff]:
  "P ⊢ OK T ≤⇩⊤ OK T' = P ⊢ T ≤ T'"
(*<*) by (simp add: sup_ty_opt_def fun_of_def) (*>*)

lemma any_OK_conv [iff]:
  "P ⊢ X ≤⇩⊤ OK T' = (∃T. X = OK T ∧ P ⊢ T ≤ T')"
(*<*)
  unfolding sup_ty_opt_def 
  by (rule le_OK_conv [simplified lesub_def])
(*>*)

lemma OK_any_conv:
 "P ⊢ OK T ≤⇩⊤ X = (X = Err ∨ (∃T'. X = OK T' ∧ P ⊢ T ≤ T'))"
(*<*)
  unfolding sup_ty_opt_def 
  by (rule OK_le_conv [simplified lesub_def])
(*>*)

lemma sup_ty_opt_trans [intro?, trans]:
  "⟦P ⊢ a ≤⇩⊤ b; P ⊢ b ≤⇩⊤ c⟧ ⟹ P ⊢ a ≤⇩⊤ c"
(*<*) by (auto intro: widen_trans  
           simp add: sup_ty_opt_def Err.le_def lesub_def fun_of_def
           split: err.splits) (*>*)


subsection "Stack and Registers"

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

lemma sup_loc_refl [iff]: "P ⊢ LT [≤⇩⊤] LT"
(*<*) by (rule list_all2_refl) simp (*>*)

lemmas sup_loc_Cons1 [iff] = list_all2_Cons1 [of "sup_ty_opt P"] for P

lemma sup_loc_def:
  "P ⊢ LT [≤⇩⊤] LT' ≡ Listn.le (sup_ty_opt P) LT LT'"
(*<*) by (simp add: Listn.le_def lesub_def) (*>*)

lemma sup_loc_widens_conv [iff]:
  "P ⊢ map OK Ts [≤⇩⊤] map OK Ts' = P ⊢ Ts [≤] Ts'"
(*<*)
  by (simp add: list_all2_map1 list_all2_map2)
(*>*)


lemma sup_loc_trans [intro?, trans]:
  "⟦P ⊢ a [≤⇩⊤] b; P ⊢ b [≤⇩⊤] c⟧ ⟹ P ⊢ a [≤⇩⊤] c"
(*<*) by (rule list_all2_trans, rule sup_ty_opt_trans) (*>*)


subsection "State Type"

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

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

lemma sup_state_trans [intro?, trans]:
  "⟦P ⊢ a ≤⇩i b; P ⊢ b ≤⇩i c⟧ ⟹ P ⊢ a ≤⇩i c"
(*<*) by (auto intro: sup_loc_trans widens_trans simp add: sup_state_conv2) (*>*)


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

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

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

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

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

lemma sup_state_opt_trans [intro?, trans]:
  "⟦P ⊢ a ≤' b; P ⊢ b ≤' c⟧ ⟹ P ⊢ a ≤' c"
(*<*)
  unfolding sup_state_opt_def Opt.le_def lesub_def
  by (simp add: option.case_eq_if sup_state_trans)
(*>*)


lemma sup_state_opt_err  : "(Err.le (sup_state_opt P)) s s"
  unfolding JVM_le_unfold Product.le_def Opt.le_def Err.le_def lesssub_def lesub_def Listn.le_def
  by (auto split: err.splits)

lemma Cons_less_Conss1 [simp]:
  "x#xs [⊏⇘subtype P⇙] y#ys = (x ⊏⇘subtype P⇙ y ∧ xs [⊑⇘subtype P⇙] ys ∨ x = y ∧ xs [⊏⇘subtype P⇙] ys)"
  unfolding lesssub_def
  by (metis Cons_le_Cons lesub_def list.inject subtype_refl) 

lemma Cons_less_Conss2 [simp]:
  "x#xs [⊏⇘Err.le (subtype P)⇙] y#ys = (x ⊏⇘Err.le (subtype P)⇙ y ∧ xs [⊑⇘Err.le (subtype P)⇙] ys ∨ x = y ∧ xs [⊏⇘Err.le (subtype P)⇙] ys)"
  unfolding lesssub_def
  by (metis Cons_le_Cons le_err_refl lesub_def list.inject subtype_refl) 

lemma acc_le_listI1 [intro!]:
  " acc (subtype P) ⟹ acc (Listn.le (subtype P))"
  (*<*) 
  unfolding acc_def
  apply (subgoal_tac
      "wf(UN n. {(ys,xs). size xs = n ∧ size ys = n ∧ xs <_(Listn.le (subtype P)) ys})")
   apply (erule wf_subset)

   apply (blast intro: lesssub_lengthD)
  apply (rule wf_UN)
   prefer 2
  apply force
  apply (rename_tac n)
  apply (induct_tac n)
   apply (simp add: lesssub_def cong: conj_cong)
  apply (rename_tac k)
  apply (simp add: wf_eq_minimal)
  apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
  apply clarify
  apply (rename_tac M m)
  apply (case_tac "∃x xs. size xs = k ∧ x#xs ∈ M")
   prefer 2
   apply blast
  apply (erule_tac x = "{a. ∃xs. size xs = k ∧ a#xs:M}" in allE)
  apply (erule impE)
   apply blast
  apply (thin_tac "∃x xs. P x xs" for P)
  apply clarify
  apply (rename_tac maxA xs)
  apply (erule_tac x = "{ys. size ys = size xs ∧ maxA#ys ∈ M}" in allE)
  apply (erule impE)
   apply blast
  apply clarify
  using Cons_less_Conss1 by blast

lemma acc_le_listI2 [intro!]:
  " acc (Err.le (subtype P)) ⟹ acc (Listn.le (Err.le (subtype P)))"
  (*<*) 
  unfolding acc_def
  apply (subgoal_tac
      "wf(UN n. {(ys,xs). size xs = n ∧ size ys = n ∧ xs <_(Listn.le (Err.le (subtype P))) ys})")
   apply (erule wf_subset)

   apply (blast intro: lesssub_lengthD)
  apply (rule wf_UN)
   prefer 2
   apply force
  apply (rename_tac n)
  apply (induct_tac n)
   apply (simp add: lesssub_def cong: conj_cong)
  apply (rename_tac k)
  apply (simp add: wf_eq_minimal)
  apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
  apply clarify
  apply (rename_tac M m)
  apply (case_tac "∃x xs. size xs = k ∧ x#xs ∈ M")
   prefer 2
   apply blast
  apply (erule_tac x = "{a. ∃xs. size xs = k ∧ a#xs:M}" in allE)
  apply (erule impE)
   apply blast
  apply (thin_tac "∃x xs. P x xs" for P)
  apply clarify
  apply (rename_tac maxA xs)
  apply (erule_tac x = "{ys. size ys = size xs ∧ maxA#ys ∈ M}" in allE)
  apply (erule impE)
   apply blast
  apply clarify
  using Cons_less_Conss2 by blast

lemma acc_JVM [intro]:
  "wf_prog wf_mb P ⟹ acc (JVM_SemiType.le P mxs mxl)"
(*<*) by (unfold JVM_le_unfold) blast (*>*)  ―‹ use acc_listI1, acc_listI2 ›

end