src/HOL/MicroJava/BV/Convert.thy

*** empty log message ***

(*  Title:      HOL/MicroJava/BV/Convert.thy
    ID:         $Id$
    Author:     Cornelia Pusch
    Copyright   1999 Technische Universitaet Muenchen

The supertype relation lifted to type options, type lists and state types.
*)

Convert = JVMExec + 

types
 locvars_type = ty option list
 opstack_type = ty list
 state_type   = "opstack_type \\<times> locvars_type"

constdefs

 sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ >= _")
 "G \\<turnstile> a >= a' \\<equiv>
    case a of
      None \\<Rightarrow> True
    | Some t  \\<Rightarrow>  case a' of 
		     None \\<Rightarrow> False
		   | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t" 

 sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool"	  ("_ \\<turnstile> _ >>= _"  [71,71] 70)
 "G \\<turnstile> LT >>= LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t >= t')"


 sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool"	  ("_ \\<turnstile> _ >>>= _"  [71,71] 70)
 "G \\<turnstile> s >>>= s' \\<equiv> G \\<turnstile> map Some (fst s) >>= map Some (fst s') \\<and> G \\<turnstile> snd s >>= snd s'"

end