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