src/HOL/MicroJava/BV/JVMType.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 56073 29e308b56d23
child 58886 8a6cac7c7247
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*  Title:      HOL/MicroJava/BV/JVMType.thy
     2     Author:     Gerwin Klein
     3     Copyright   2000 TUM
     4 *)
     5 
     6 header {* \isaheader{The JVM Type System as Semilattice} *}
     7 
     8 theory JVMType
     9 imports JType
    10 begin
    11 
    12 type_synonym locvars_type = "ty err list"
    13 type_synonym opstack_type = "ty list"
    14 type_synonym state_type = "opstack_type \<times> locvars_type"
    15 type_synonym state = "state_type option err"    -- "for Kildall"
    16 type_synonym method_type = "state_type option list"   -- "for BVSpec"
    17 type_synonym class_type = "sig \<Rightarrow> method_type"
    18 type_synonym prog_type = "cname \<Rightarrow> class_type"
    19 
    20 
    21 definition stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl" where
    22   "stk_esl S maxs == upto_esl maxs (JType.esl S)"
    23 
    24 definition reg_sl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty err list sl" where
    25   "reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"
    26 
    27 definition sl :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state sl" where
    28   "sl S maxs maxr ==
    29   Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"
    30 
    31 definition states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state set" where
    32   "states S maxs maxr == fst(sl S maxs maxr)"
    33 
    34 definition le :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state ord" where
    35   "le S maxs maxr == fst(snd(sl S maxs maxr))"
    36 
    37 definition  sup :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state binop" where
    38   "sup S maxs maxr == snd(snd(sl S maxs maxr))"
    39 
    40 definition sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool"
    41                  ("_ |- _ <=o _" [71,71] 70) where 
    42   "sup_ty_opt G == Err.le (subtype G)"
    43 
    44 definition sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
    45               ("_ |- _ <=l _"  [71,71] 70) where
    46   "sup_loc G == Listn.le (sup_ty_opt G)"
    47 
    48 definition sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"   
    49                ("_ |- _ <=s _"  [71,71] 70) where
    50   "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
    51 
    52 definition sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
    53                    ("_ |- _ <=' _"  [71,71] 70) where
    54   "sup_state_opt G == Opt.le (sup_state G)"
    55 
    56 
    57 notation (xsymbols)
    58   sup_ty_opt  ("_ \<turnstile> _ <=o _" [71,71] 70) and
    59   sup_loc  ("_ \<turnstile> _ <=l _" [71,71] 70) and
    60   sup_state  ("_ \<turnstile> _ <=s _" [71,71] 70) and
    61   sup_state_opt  ("_ \<turnstile> _ <=' _" [71,71] 70)
    62                    
    63 
    64 lemma JVM_states_unfold: 
    65   "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
    66                                   list maxr (err(types S))))"
    67   apply (unfold states_def sl_def Opt.esl_def Err.sl_def
    68          stk_esl_def reg_sl_def Product.esl_def
    69          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def)
    70   by simp
    71 
    72 
    73 lemma JVM_le_unfold:
    74  "le S m n == 
    75   Err.le(Opt.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))" 
    76   apply (unfold le_def sl_def Opt.esl_def Err.sl_def
    77          stk_esl_def reg_sl_def Product.esl_def  
    78          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
    79   by simp
    80 
    81 lemma JVM_le_convert:
    82   "le G m n (OK t1) (OK t2) = G \<turnstile> t1 <=' t2"
    83   by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def 
    84                 sup_state_def sup_loc_def sup_ty_opt_def)
    85 
    86 lemma JVM_le_Err_conv:
    87   "le G m n = Err.le (sup_state_opt G)"
    88   by (unfold sup_state_opt_def sup_state_def sup_loc_def  
    89              sup_ty_opt_def JVM_le_unfold) simp
    90 
    91 lemma zip_map [rule_format]:
    92   "\<forall>a. length a = length b \<longrightarrow> 
    93   zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
    94   apply (induct b) 
    95    apply simp
    96   apply clarsimp
    97   apply (case_tac aa)
    98   apply simp_all
    99   done
   100 
   101 lemma [simp]: "Err.le r (OK a) (OK b) = r a b"
   102   by (simp add: Err.le_def lesub_def)
   103 
   104 lemma stk_convert:
   105   "Listn.le (subtype G) a b = G \<turnstile> map OK a <=l map OK b"
   106 proof 
   107   assume "Listn.le (subtype G) a b"
   108 
   109   hence le: "list_all2 (subtype G) a b"
   110     by (unfold Listn.le_def lesub_def)
   111   
   112   { fix x' y'
   113     assume "length a = length b"
   114            "(x',y') \<in> set (zip (map OK a) (map OK b))"
   115     then
   116     obtain x y where OK:
   117       "x' = OK x" "y' = OK y" "(x,y) \<in> set (zip a b)"
   118       by (auto simp add: zip_map)
   119     with le
   120     have "subtype G x y"
   121       by (simp add: list_all2_iff Ball_def)
   122     with OK
   123     have "G \<turnstile> x' <=o y'"
   124       by (simp add: sup_ty_opt_def)
   125   }
   126   
   127   with le
   128   show "G \<turnstile> map OK a <=l map OK b"
   129     by (unfold sup_loc_def Listn.le_def lesub_def list_all2_iff) auto
   130 next
   131   assume "G \<turnstile> map OK a <=l map OK b"
   132 
   133   thus "Listn.le (subtype G) a b"
   134     apply (unfold sup_loc_def list_all2_iff Listn.le_def lesub_def)
   135     apply (clarsimp simp add: zip_map)
   136     apply (drule bspec, assumption)
   137     apply (auto simp add: sup_ty_opt_def subtype_def)
   138     done
   139 qed
   140 
   141 
   142 lemma sup_state_conv:
   143   "(G \<turnstile> s1 <=s s2) == 
   144   (G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)"
   145   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def split_beta)
   146 
   147 
   148 lemma subtype_refl [simp]:
   149   "subtype G t t"
   150   by (simp add: subtype_def)
   151 
   152 theorem sup_ty_opt_refl [simp]:
   153   "G \<turnstile> t <=o t"
   154   by (simp add: sup_ty_opt_def Err.le_def lesub_def split: err.split)
   155 
   156 lemma le_list_refl2 [simp]: 
   157   "(\<And>xs. r xs xs) \<Longrightarrow> Listn.le r xs xs"
   158   by (induct xs, auto simp add: Listn.le_def lesub_def)
   159 
   160 theorem sup_loc_refl [simp]:
   161   "G \<turnstile> t <=l t"
   162   by (simp add: sup_loc_def)
   163 
   164 theorem sup_state_refl [simp]:
   165   "G \<turnstile> s <=s s"
   166   by (auto simp add: sup_state_def Product.le_def lesub_def)
   167 
   168 theorem sup_state_opt_refl [simp]:
   169   "G \<turnstile> s <=' s"
   170   by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
   171   
   172 
   173 theorem anyConvErr [simp]:
   174   "(G \<turnstile> Err <=o any) = (any = Err)"
   175   by (simp add: sup_ty_opt_def Err.le_def split: err.split)
   176 
   177 theorem OKanyConvOK [simp]:
   178   "(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq> ty)"
   179   by (simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def)
   180 
   181 theorem sup_ty_opt_OK:
   182   "G \<turnstile> a <=o (OK b) \<Longrightarrow> \<exists> x. a = OK x"
   183   by (clarsimp simp add: sup_ty_opt_def Err.le_def split: err.splits)
   184 
   185 lemma widen_PrimT_conv1 [simp]:
   186   "\<lbrakk> G \<turnstile> S \<preceq> T; S = PrimT x\<rbrakk> \<Longrightarrow> T = PrimT x"
   187   by (auto elim: widen.cases)
   188 
   189 theorem sup_PTS_eq:
   190   "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
   191   by (auto simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def 
   192               split: err.splits)
   193 
   194 theorem sup_loc_Nil [iff]:
   195   "(G \<turnstile> [] <=l XT) = (XT=[])"
   196   by (simp add: sup_loc_def Listn.le_def)
   197 
   198 theorem sup_loc_Cons [iff]:
   199   "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))"
   200   by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons1)
   201 
   202 theorem sup_loc_Cons2:
   203   "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
   204   by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons2)
   205 
   206 lemma sup_state_Cons:
   207   "(G \<turnstile> (x#xt, a) <=s (y#yt, b)) = 
   208    ((G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt,b)))"
   209   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def)
   210 
   211 
   212 theorem sup_loc_length:
   213   "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
   214 proof -
   215   assume G: "G \<turnstile> a <=l b"
   216   have "\<forall>b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
   217     by (induct a, auto)
   218   with G
   219   show ?thesis by blast
   220 qed
   221 
   222 theorem sup_loc_nth:
   223   "\<lbrakk> G \<turnstile> a <=l b; n < length a \<rbrakk> \<Longrightarrow> G \<turnstile> (a!n) <=o (b!n)"
   224 proof -
   225   assume a: "G \<turnstile> a <=l b" "n < length a"
   226   have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
   227     (is "?P a")
   228   proof (induct a)
   229     show "?P []" by simp
   230     
   231     fix x xs assume IH: "?P xs"
   232 
   233     show "?P (x#xs)"
   234     proof (intro strip)
   235       fix n b
   236       assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)"
   237       with IH
   238       show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)"
   239         by (cases n) auto
   240     qed
   241   qed
   242   with a
   243   show ?thesis by blast
   244 qed
   245 
   246 theorem all_nth_sup_loc:
   247   "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) 
   248   \<longrightarrow> (G \<turnstile> a <=l b)" (is "?P a")
   249 proof (induct a)
   250   show "?P []" by simp
   251 
   252   fix l ls assume IH: "?P ls"
   253   
   254   show "?P (l#ls)"
   255   proof (intro strip)
   256     fix b
   257     assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
   258     assume l: "length (l#ls) = length b"
   259     
   260     then obtain b' bs where b: "b = b'#bs"
   261       by (cases b) (simp, simp add: neq_Nil_conv)
   262 
   263     with f
   264     have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
   265       by auto
   266 
   267     with f b l IH
   268     show "G \<turnstile> (l # ls) <=l b"
   269       by auto
   270   qed
   271 qed
   272 
   273 
   274 theorem sup_loc_append:
   275   "length a = length b \<Longrightarrow> 
   276    (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
   277 proof -
   278   assume l: "length a = length b"
   279 
   280   have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
   281             (G \<turnstile> x <=l y))" (is "?P a") 
   282   proof (induct a)
   283     show "?P []" by simp
   284     
   285     fix l ls assume IH: "?P ls"    
   286     show "?P (l#ls)" 
   287     proof (intro strip)
   288       fix b
   289       assume "length (l#ls) = length (b::ty err list)"
   290       with IH
   291       show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
   292         by (cases b) auto
   293     qed
   294   qed
   295   with l
   296   show ?thesis by blast
   297 qed
   298 
   299 theorem sup_loc_rev [simp]:
   300   "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)"
   301 proof -
   302   have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a")
   303   proof (induct a)
   304     show "?P []" by simp
   305 
   306     fix l ls assume IH: "?P ls"
   307 
   308     { 
   309       fix b
   310       have "?Q (l#ls) b"
   311       proof (cases b)
   312         case Nil
   313         thus ?thesis by (auto dest: sup_loc_length)
   314       next
   315         case (Cons a list)
   316         show ?thesis
   317         proof
   318           assume "G \<turnstile> (l # ls) <=l b"
   319           thus "G \<turnstile> rev (l # ls) <=l rev b"
   320             by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append)
   321         next
   322           assume "G \<turnstile> rev (l # ls) <=l rev b"
   323           hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])"
   324             by (simp add: Cons)          
   325           
   326           hence "length (rev ls) = length (rev list)"
   327             by (auto dest: sup_loc_length)
   328 
   329           from this G
   330           obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a"
   331             by (simp add: sup_loc_append)
   332 
   333           thus "G \<turnstile> (l # ls) <=l b"
   334             by (simp add: Cons IH)
   335         qed
   336       qed    
   337     }
   338     thus "?P (l#ls)" by blast
   339   qed
   340 
   341   thus ?thesis by blast
   342 qed
   343 
   344 
   345 theorem sup_loc_update [rule_format]:
   346   "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
   347           (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
   348 proof (induct x)
   349   show "?P []" by simp
   350 
   351   fix l ls assume IH: "?P ls"
   352   show "?P (l#ls)"
   353   proof (intro strip)
   354     fix n y
   355     assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y"
   356     with IH
   357     show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]"
   358       by (cases n) (auto simp add: sup_loc_Cons2 list_all2_Cons1)
   359   qed
   360 qed
   361 
   362 
   363 theorem sup_state_length [simp]:
   364   "G \<turnstile> s2 <=s s1 \<Longrightarrow> 
   365    length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
   366   by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def)
   367 
   368 theorem sup_state_append_snd:
   369   "length a = length b \<Longrightarrow> 
   370   (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
   371   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
   372 
   373 theorem sup_state_append_fst:
   374   "length a = length b \<Longrightarrow> 
   375   (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
   376   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
   377 
   378 theorem sup_state_Cons1:
   379   "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
   380    (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
   381   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def)
   382 
   383 theorem sup_state_Cons2:
   384   "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
   385    (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
   386   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_Cons2)
   387 
   388 theorem sup_state_ignore_fst:  
   389   "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
   390   by (simp add: sup_state_def lesub_def Product.le_def)
   391 
   392 theorem sup_state_rev_fst:
   393   "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
   394 proof -
   395   have m: "\<And>f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
   396   show ?thesis by (simp add: m sup_state_def stk_convert lesub_def Product.le_def)
   397 qed
   398   
   399 
   400 lemma sup_state_opt_None_any [iff]:
   401   "(G \<turnstile> None <=' any) = True"
   402   by (simp add: sup_state_opt_def Opt.le_def split: option.split)
   403 
   404 lemma sup_state_opt_any_None [iff]:
   405   "(G \<turnstile> any <=' None) = (any = None)"
   406   by (simp add: sup_state_opt_def Opt.le_def split: option.split)
   407 
   408 lemma sup_state_opt_Some_Some [iff]:
   409   "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)"
   410   by (simp add: sup_state_opt_def Opt.le_def lesub_def del: split_paired_Ex)
   411 
   412 lemma sup_state_opt_any_Some [iff]:
   413   "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)"
   414   by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
   415 
   416 lemma sup_state_opt_Some_any:
   417   "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))"
   418   by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split)
   419 
   420 
   421 theorem sup_ty_opt_trans [trans]:
   422   "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
   423   by (auto intro: widen_trans 
   424            simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def 
   425            split: err.splits)
   426 
   427 theorem sup_loc_trans [trans]:
   428   "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
   429 proof -
   430   assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
   431  
   432   hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
   433   proof (intro strip)
   434     fix n 
   435     assume n: "n < length a"
   436     with G(1)
   437     have "G \<turnstile> (a!n) <=o (b!n)"
   438       by (rule sup_loc_nth)
   439     also 
   440     from n G
   441     have "G \<turnstile> \<dots> <=o (c!n)"
   442       by - (rule sup_loc_nth, auto dest: sup_loc_length)
   443     finally
   444     show "G \<turnstile> (a!n) <=o (c!n)" .
   445   qed
   446 
   447   with G
   448   show ?thesis 
   449     by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) 
   450 qed
   451   
   452 
   453 theorem sup_state_trans [trans]:
   454   "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
   455   by (auto intro: sup_loc_trans simp add: sup_state_def stk_convert Product.le_def lesub_def)
   456 
   457 theorem sup_state_opt_trans [trans]:
   458   "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
   459   by (auto intro: sup_state_trans 
   460            simp add: sup_state_opt_def Opt.le_def lesub_def 
   461            split: option.splits)
   462 
   463 end