kleing@12516: (*  Title:      HOL/MicroJava/BV/JVM.thy
kleing@10812:     ID:         $Id$
kleing@10812:     Author:     Gerwin Klein
kleing@10812:     Copyright   2000 TUM
kleing@10812: 
kleing@10812: *)
kleing@10812: 
kleing@12516: header "The JVM Type System as Semilattice"
kleing@10812: 
kleing@10812: theory JVMType = Opt + Product + Listn + JType:
kleing@10812: 
kleing@10812: types
kleing@10812:   locvars_type = "ty err list"
kleing@10812:   opstack_type = "ty list"
kleing@10812:   state_type   = "opstack_type \<times> locvars_type"
kleing@12516:   state        = "state_type option err"    -- "for Kildall"
kleing@12516:   method_type  = "state_type option list"   -- "for BVSpec"
kleing@10812:   class_type   = "sig => method_type"
kleing@10812:   prog_type    = "cname => class_type"
kleing@10812: 
kleing@10812: 
kleing@10812: constdefs
kleing@10812:   stk_esl :: "'c prog => nat => ty list esl"
kleing@10812:   "stk_esl S maxs == upto_esl maxs (JType.esl S)"
kleing@10812: 
kleing@10812:   reg_sl :: "'c prog => nat => ty err list sl"
kleing@10812:   "reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"
kleing@10812: 
kleing@10812:   sl :: "'c prog => nat => nat => state sl"
kleing@10812:   "sl S maxs maxr ==
kleing@10812:   Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"
kleing@10812: 
kleing@10812: constdefs
kleing@10812:   states :: "'c prog => nat => nat => state set"
kleing@10812:   "states S maxs maxr == fst(sl S maxs maxr)"
kleing@10812: 
kleing@10812:   le :: "'c prog => nat => nat => state ord"
kleing@10812:   "le S maxs maxr == fst(snd(sl S maxs maxr))"
kleing@10812: 
kleing@10812:   sup :: "'c prog => nat => nat => state binop"
kleing@10812:   "sup S maxs maxr == snd(snd(sl S maxs maxr))"
kleing@10812: 
kleing@10812: 
kleing@10812: constdefs
kleing@10812:   sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
oheimb@11372:                  ("_ |- _ <=o _" [71,71] 70)
kleing@10812:   "sup_ty_opt G == Err.le (subtype G)"
kleing@10812: 
kleing@10812:   sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
oheimb@11372:               ("_ |- _ <=l _"  [71,71] 70)
kleing@10812:   "sup_loc G == Listn.le (sup_ty_opt G)"
kleing@10812: 
kleing@12516:   sup_state :: "['code prog,state_type,state_type] => bool"   
oheimb@11372:                ("_ |- _ <=s _"  [71,71] 70)
kleing@10812:   "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
kleing@10812: 
kleing@10812:   sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
oheimb@11372:                    ("_ |- _ <=' _"  [71,71] 70)
kleing@10812:   "sup_state_opt G == Opt.le (sup_state G)"
kleing@10812: 
kleing@10812: 
oheimb@11372: syntax (xsymbols)
kleing@10812:   sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
oheimb@11372:                    ("_ \<turnstile> _ <=o _" [71,71] 70)
kleing@10812:   sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
oheimb@11372:                    ("_ \<turnstile> _ <=l _" [71,71] 70)
kleing@12516:   sup_state     :: "['code prog,state_type,state_type] => bool" 
oheimb@11372:                    ("_ \<turnstile> _ <=s _" [71,71] 70)
kleing@10812:   sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
oheimb@11372:                    ("_ \<turnstile> _ <=' _" [71,71] 70)
kleing@10812:                    
kleing@10812: 
kleing@10812: lemma JVM_states_unfold: 
kleing@10812:   "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
kleing@10812:                                   list maxr (err(types S))))"
kleing@10812:   apply (unfold states_def sl_def Opt.esl_def Err.sl_def
kleing@10812:          stk_esl_def reg_sl_def Product.esl_def
kleing@10812:          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def)
kleing@10812:   by simp
kleing@10812: 
kleing@10812: 
kleing@10812: lemma JVM_le_unfold:
kleing@10812:  "le S m n == 
kleing@10812:   Err.le(Opt.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))" 
kleing@10812:   apply (unfold le_def sl_def Opt.esl_def Err.sl_def
kleing@10812:          stk_esl_def reg_sl_def Product.esl_def  
kleing@10812:          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
kleing@10812:   by simp
kleing@10812: 
kleing@10812: lemma JVM_le_convert:
kleing@10812:   "le G m n (OK t1) (OK t2) = G \<turnstile> t1 <=' t2"
kleing@10812:   by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def 
kleing@10812:                 sup_state_def sup_loc_def sup_ty_opt_def)
kleing@10812: 
kleing@10812: lemma JVM_le_Err_conv:
kleing@10812:   "le G m n = Err.le (sup_state_opt G)"
kleing@10812:   by (unfold sup_state_opt_def sup_state_def sup_loc_def  
kleing@10812:              sup_ty_opt_def JVM_le_unfold) simp
kleing@10812: 
kleing@10812: lemma zip_map [rule_format]:
kleing@12516:   "\<forall>a. length a = length b --> 
kleing@12516:   zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
kleing@10812:   apply (induct b) 
kleing@10812:    apply simp
kleing@10812:   apply clarsimp
kleing@10812:   apply (case_tac aa)
kleing@10812:   apply simp+
kleing@10812:   done
kleing@10812: 
kleing@10812: lemma [simp]: "Err.le r (OK a) (OK b) = r a b"
kleing@10812:   by (simp add: Err.le_def lesub_def)
kleing@10812: 
kleing@10812: lemma stk_convert:
kleing@10812:   "Listn.le (subtype G) a b = G \<turnstile> map OK a <=l map OK b"
kleing@10812: proof 
kleing@10812:   assume "Listn.le (subtype G) a b"
kleing@10812: 
kleing@10812:   hence le: "list_all2 (subtype G) a b"
kleing@10812:     by (unfold Listn.le_def lesub_def)
kleing@10812:   
kleing@10812:   { fix x' y'
kleing@10812:     assume "length a = length b"
kleing@10812:            "(x',y') \<in> set (zip (map OK a) (map OK b))"
kleing@10812:     then
kleing@10812:     obtain x y where OK:
kleing@10812:       "x' = OK x" "y' = OK y" "(x,y) \<in> set (zip a b)"
kleing@10812:       by (auto simp add: zip_map)
kleing@10812:     with le
kleing@10812:     have "subtype G x y"
kleing@10812:       by (simp add: list_all2_def Ball_def)
kleing@10812:     with OK
kleing@10812:     have "G \<turnstile> x' <=o y'"
kleing@10812:       by (simp add: sup_ty_opt_def)
kleing@10812:   }
kleing@10812:   
kleing@10812:   with le
kleing@10812:   show "G \<turnstile> map OK a <=l map OK b"
kleing@10812:     by (unfold sup_loc_def Listn.le_def lesub_def list_all2_def) auto
kleing@10812: next
kleing@10812:   assume "G \<turnstile> map OK a <=l map OK b"
kleing@10812: 
kleing@10812:   thus "Listn.le (subtype G) a b"
kleing@10812:     apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def)
kleing@10812:     apply (clarsimp simp add: zip_map)
kleing@10812:     apply (drule bspec, assumption)
kleing@10812:     apply (auto simp add: sup_ty_opt_def subtype_def)
kleing@10812:     done
kleing@10812: qed
kleing@10812: 
kleing@10812: 
kleing@10812: lemma sup_state_conv:
kleing@12516:   "(G \<turnstile> s1 <=s s2) == 
kleing@12516:   (G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)"
kleing@10812:   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def split_beta)
kleing@10812: 
kleing@10812: 
kleing@10812: lemma subtype_refl [simp]:
kleing@10812:   "subtype G t t"
kleing@10812:   by (simp add: subtype_def)
kleing@10812: 
kleing@10812: theorem sup_ty_opt_refl [simp]:
kleing@10812:   "G \<turnstile> t <=o t"
kleing@10812:   by (simp add: sup_ty_opt_def Err.le_def lesub_def split: err.split)
kleing@10812: 
kleing@10812: lemma le_list_refl2 [simp]: 
kleing@10812:   "(\<And>xs. r xs xs) \<Longrightarrow> Listn.le r xs xs"
kleing@10812:   by (induct xs, auto simp add: Listn.le_def lesub_def)
kleing@10812: 
kleing@10812: theorem sup_loc_refl [simp]:
kleing@10812:   "G \<turnstile> t <=l t"
kleing@10812:   by (simp add: sup_loc_def)
kleing@10812: 
kleing@10812: theorem sup_state_refl [simp]:
kleing@10812:   "G \<turnstile> s <=s s"
kleing@10812:   by (auto simp add: sup_state_def Product.le_def lesub_def)
kleing@10812: 
kleing@10812: theorem sup_state_opt_refl [simp]:
kleing@10812:   "G \<turnstile> s <=' s"
kleing@10812:   by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
kleing@10812:   
kleing@10812: 
kleing@10812: theorem anyConvErr [simp]:
kleing@10812:   "(G \<turnstile> Err <=o any) = (any = Err)"
kleing@10812:   by (simp add: sup_ty_opt_def Err.le_def split: err.split)
kleing@10812: 
kleing@10812: theorem OKanyConvOK [simp]:
kleing@10812:   "(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq> ty)"
kleing@10812:   by (simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def)
kleing@10812: 
kleing@10812: theorem sup_ty_opt_OK:
kleing@10812:   "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x"
kleing@10812:   by (clarsimp simp add: sup_ty_opt_def Err.le_def split: err.splits)
kleing@10812: 
kleing@10812: lemma widen_PrimT_conv1 [simp]:
kleing@10812:   "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
kleing@10812:   by (auto elim: widen.elims)
kleing@10812: 
kleing@10812: theorem sup_PTS_eq:
kleing@10812:   "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
kleing@10812:   by (auto simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def 
kleing@10812:               split: err.splits)
kleing@10812: 
kleing@10812: theorem sup_loc_Nil [iff]:
kleing@10812:   "(G \<turnstile> [] <=l XT) = (XT=[])"
kleing@10812:   by (simp add: sup_loc_def Listn.le_def)
kleing@10812: 
kleing@10812: theorem sup_loc_Cons [iff]:
kleing@10812:   "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))"
kleing@10812:   by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons1)
kleing@10812: 
kleing@10812: theorem sup_loc_Cons2:
kleing@10812:   "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
kleing@10812:   by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons2)
kleing@10812: 
kleing@10812: 
kleing@10812: theorem sup_loc_length:
kleing@10812:   "G \<turnstile> a <=l b ==> length a = length b"
kleing@10812: proof -
kleing@10812:   assume G: "G \<turnstile> a <=l b"
kleing@10812:   have "\<forall>b. (G \<turnstile> a <=l b) --> length a = length b"
kleing@10812:     by (induct a, auto)
kleing@10812:   with G
kleing@10812:   show ?thesis by blast
kleing@10812: qed
kleing@10812: 
kleing@10812: theorem sup_loc_nth:
kleing@10812:   "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
kleing@10812: proof -
kleing@10812:   assume a: "G \<turnstile> a <=l b" "n < length a"
kleing@10812:   have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))"
kleing@10812:     (is "?P a")
kleing@10812:   proof (induct a)
kleing@10812:     show "?P []" by simp
kleing@10812:     
kleing@10812:     fix x xs assume IH: "?P xs"
kleing@10812: 
kleing@10812:     show "?P (x#xs)"
kleing@10812:     proof (intro strip)
kleing@10812:       fix n b
kleing@10812:       assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)"
kleing@10812:       with IH
kleing@10812:       show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)"
kleing@10812:         by - (cases n, auto)
kleing@10812:     qed
kleing@10812:   qed
kleing@10812:   with a
kleing@10812:   show ?thesis by blast
kleing@10812: qed
kleing@10812: 
kleing@10812: theorem all_nth_sup_loc:
kleing@10812:   "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) 
kleing@10812:   --> (G \<turnstile> a <=l b)" (is "?P a")
kleing@10812: proof (induct a)
kleing@10812:   show "?P []" by simp
kleing@10812: 
kleing@10812:   fix l ls assume IH: "?P ls"
kleing@10812:   
kleing@10812:   show "?P (l#ls)"
kleing@10812:   proof (intro strip)
kleing@10812:     fix b
kleing@10812:     assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
kleing@10812:     assume l: "length (l#ls) = length b"
kleing@10812:     
kleing@10812:     then obtain b' bs where b: "b = b'#bs"
kleing@10812:       by - (cases b, simp, simp add: neq_Nil_conv, rule that)
kleing@10812: 
kleing@10812:     with f
kleing@10812:     have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))"
kleing@10812:       by auto
kleing@10812: 
kleing@10812:     with f b l IH
kleing@10812:     show "G \<turnstile> (l # ls) <=l b"
kleing@10812:       by auto
kleing@10812:   qed
kleing@10812: qed
kleing@10812: 
kleing@10812: 
kleing@10812: theorem sup_loc_append:
kleing@10812:   "length a = length b ==> 
kleing@10812:    (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
kleing@10812: proof -
kleing@10812:   assume l: "length a = length b"
kleing@10812: 
kleing@10812:   have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
kleing@10812:             (G \<turnstile> x <=l y))" (is "?P a") 
kleing@10812:   proof (induct a)
kleing@10812:     show "?P []" by simp
kleing@10812:     
kleing@10812:     fix l ls assume IH: "?P ls"    
kleing@10812:     show "?P (l#ls)" 
kleing@10812:     proof (intro strip)
kleing@10812:       fix b
kleing@10812:       assume "length (l#ls) = length (b::ty err list)"
kleing@10812:       with IH
kleing@10812:       show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
kleing@10812:         by - (cases b, auto)
kleing@10812:     qed
kleing@10812:   qed
kleing@10812:   with l
kleing@10812:   show ?thesis by blast
kleing@10812: qed
kleing@10812: 
kleing@10812: theorem sup_loc_rev [simp]:
kleing@10812:   "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)"
kleing@10812: proof -
kleing@10812:   have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a")
kleing@10812:   proof (induct a)
kleing@10812:     show "?P []" by simp
kleing@10812: 
kleing@10812:     fix l ls assume IH: "?P ls"
kleing@10812: 
kleing@10812:     { 
kleing@10812:       fix b
kleing@10812:       have "?Q (l#ls) b"
kleing@10812:       proof (cases (open) b)
kleing@10812:         case Nil
kleing@10812:         thus ?thesis by (auto dest: sup_loc_length)
kleing@10812:       next
kleing@10812:         case Cons 
kleing@10812:         show ?thesis
kleing@10812:         proof
kleing@10812:           assume "G \<turnstile> (l # ls) <=l b"
kleing@10812:           thus "G \<turnstile> rev (l # ls) <=l rev b"
kleing@10812:             by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append)
kleing@10812:         next
kleing@10812:           assume "G \<turnstile> rev (l # ls) <=l rev b"
kleing@10812:           hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])"
kleing@10812:             by (simp add: Cons)          
kleing@10812:           
kleing@10812:           hence "length (rev ls) = length (rev list)"
kleing@10812:             by (auto dest: sup_loc_length)
kleing@10812: 
kleing@10812:           from this G
kleing@10812:           obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a"
kleing@10812:             by (simp add: sup_loc_append)
kleing@10812: 
kleing@10812:           thus "G \<turnstile> (l # ls) <=l b"
kleing@10812:             by (simp add: Cons IH)
kleing@10812:         qed
kleing@10812:       qed    
kleing@10812:     }
kleing@10812:     thus "?P (l#ls)" by blast
kleing@10812:   qed
kleing@10812: 
kleing@10812:   thus ?thesis by blast
kleing@10812: qed
kleing@10812: 
kleing@10812: 
kleing@10812: theorem sup_loc_update [rule_format]:
kleing@10812:   "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> 
kleing@10812:           (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
kleing@10812: proof (induct x)
kleing@10812:   show "?P []" by simp
kleing@10812: 
kleing@10812:   fix l ls assume IH: "?P ls"
kleing@10812:   show "?P (l#ls)"
kleing@10812:   proof (intro strip)
kleing@10812:     fix n y
kleing@10812:     assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y"
kleing@10812:     with IH
kleing@10812:     show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]"
kleing@10812:       by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1)
kleing@10812:   qed
kleing@10812: qed
kleing@10812: 
kleing@10812: 
kleing@10812: theorem sup_state_length [simp]:
kleing@10812:   "G \<turnstile> s2 <=s s1 ==> 
kleing@10812:    length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
kleing@10812:   by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def);
kleing@10812: 
kleing@10812: theorem sup_state_append_snd:
kleing@10812:   "length a = length b ==> 
kleing@10812:   (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
kleing@10812:   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
kleing@10812: 
kleing@10812: theorem sup_state_append_fst:
kleing@10812:   "length a = length b ==> 
kleing@10812:   (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
kleing@10812:   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
kleing@10812: 
kleing@10812: theorem sup_state_Cons1:
kleing@10812:   "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
kleing@10812:    (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
kleing@10812:   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons)
kleing@10812: 
kleing@10812: theorem sup_state_Cons2:
kleing@10812:   "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
kleing@10812:    (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
kleing@10812:   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons sup_loc_Cons2)
kleing@10812: 
kleing@10812: theorem sup_state_ignore_fst:  
kleing@10812:   "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)"
kleing@10812:   by (simp add: sup_state_def lesub_def Product.le_def)
kleing@10812: 
kleing@10812: theorem sup_state_rev_fst:
kleing@10812:   "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
kleing@10812: proof -
kleing@10812:   have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
kleing@10812:   show ?thesis by (simp add: m sup_state_def stk_convert lesub_def Product.le_def)
kleing@10812: qed
kleing@10812:   
kleing@10812: 
kleing@10812: lemma sup_state_opt_None_any [iff]:
kleing@10812:   "(G \<turnstile> None <=' any) = True"
kleing@10812:   by (simp add: sup_state_opt_def Opt.le_def split: option.split)
kleing@10812: 
kleing@10812: lemma sup_state_opt_any_None [iff]:
kleing@10812:   "(G \<turnstile> any <=' None) = (any = None)"
kleing@10812:   by (simp add: sup_state_opt_def Opt.le_def split: option.split)
kleing@10812: 
kleing@10812: lemma sup_state_opt_Some_Some [iff]:
kleing@10812:   "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)"
kleing@10812:   by (simp add: sup_state_opt_def Opt.le_def lesub_def del: split_paired_Ex)
kleing@10812: 
kleing@10812: lemma sup_state_opt_any_Some [iff]:
kleing@10812:   "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)"
kleing@10812:   by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
kleing@10812: 
kleing@10812: lemma sup_state_opt_Some_any:
kleing@10812:   "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))"
kleing@10812:   by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
kleing@10812: 
kleing@10812: 
kleing@10812: theorem sup_ty_opt_trans [trans]:
kleing@10812:   "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c"
kleing@10812:   by (auto intro: widen_trans 
kleing@10812:            simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def 
kleing@10812:            split: err.splits)
kleing@10812: 
kleing@10812: theorem sup_loc_trans [trans]:
kleing@10812:   "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c"
kleing@10812: proof -
kleing@10812:   assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
kleing@10812:  
kleing@10812:   hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))"
kleing@10812:   proof (intro strip)
kleing@10812:     fix n 
kleing@10812:     assume n: "n < length a"
kleing@10812:     with G
kleing@10812:     have "G \<turnstile> (a!n) <=o (b!n)"
kleing@10812:       by - (rule sup_loc_nth)
kleing@10812:     also 
kleing@10812:     from n G
kleing@10812:     have "G \<turnstile> ... <=o (c!n)"
kleing@10812:       by - (rule sup_loc_nth, auto dest: sup_loc_length)
kleing@10812:     finally
kleing@10812:     show "G \<turnstile> (a!n) <=o (c!n)" .
kleing@10812:   qed
kleing@10812: 
kleing@10812:   with G
kleing@10812:   show ?thesis 
kleing@10812:     by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) 
kleing@10812: qed
kleing@10812:   
kleing@10812: 
kleing@10812: theorem sup_state_trans [trans]:
kleing@10812:   "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c"
kleing@10812:   by (auto intro: sup_loc_trans simp add: sup_state_def stk_convert Product.le_def lesub_def)
kleing@10812: 
kleing@10812: theorem sup_state_opt_trans [trans]:
kleing@10812:   "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c"
kleing@10812:   by (auto intro: sup_state_trans 
kleing@10812:            simp add: sup_state_opt_def Opt.le_def lesub_def 
kleing@10812:            split: option.splits)
kleing@10812: 
kleing@10812: end