src/HOL/MicroJava/BV/Convert.thy

re-shaped and re-ordered conversion relations

(*  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>_ <=o _")
 "G \\<turnstile> a' <=o 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> _ <=l _"  [71,71] 70)
 "G \\<turnstile> LT <=l LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t <=o t')"


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

end