src/HOL/MicroJava/BV/EffectMono.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23467 d1b97708d5eb
child 25362 8d06e11a01d1
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/BV/EffMono.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4     Copyright   2000 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{Monotonicity of eff and app} *}
     8 
     9 theory EffectMono imports Effect begin
    10 
    11 
    12 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
    13   by (auto elim: widen.cases)
    14 
    15 
    16 lemma sup_loc_some [rule_format]:
    17 "\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow> 
    18   (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
    19 proof (induct (open) ?P b)
    20   show "?P []" by simp
    21 
    22   case Cons
    23   show "?P (a#list)" 
    24   proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def)
    25     fix z zs n
    26     assume * : 
    27       "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" 
    28       "n < Suc (length list)" "(z # zs) ! n = OK t"
    29 
    30     show "(\<exists>t. (a # list) ! n = OK t) \<and> G \<turnstile>(a # list) ! n <=o OK t" 
    31     proof (cases n) 
    32       case 0
    33       with * show ?thesis by (simp add: sup_ty_opt_OK)
    34     next
    35       case Suc
    36       with Cons *
    37       show ?thesis by (simp add: sup_loc_def Listn.le_def lesub_def) 
    38     qed
    39   qed 
    40 qed
    41    
    42 
    43 lemma all_widen_is_sup_loc:
    44 "\<forall>b. length a = length b \<longrightarrow> 
    45      (\<forall>(x, y)\<in>set (zip a b). G \<turnstile> x \<preceq> y) = (G \<turnstile> (map OK a) <=l (map OK b))" 
    46  (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
    47 proof (induct "a")
    48   show "?P []" by simp
    49 
    50   fix l ls assume Cons: "?P ls"
    51 
    52   show "?P (l#ls)" 
    53   proof (intro allI impI)
    54     fix b 
    55     assume "length (l # ls) = length (b::ty list)" 
    56     with Cons
    57     show "?Q (l # ls) b" by - (cases b, auto)
    58   qed
    59 qed
    60  
    61 
    62 lemma append_length_n [rule_format]: 
    63 "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
    64 proof (induct (open) ?P x)
    65   show "?P []" by simp
    66 
    67   fix l ls assume Cons: "?P ls"
    68 
    69   show "?P (l#ls)"
    70   proof (intro allI impI)
    71     fix n
    72     assume l: "n \<le> length (l # ls)"
    73 
    74     show "\<exists>a b. l # ls = a @ b \<and> length a = n" 
    75     proof (cases n)
    76       assume "n=0" thus ?thesis by simp
    77     next
    78       fix n' assume s: "n = Suc n'"
    79       with l have  "n' \<le> length ls" by simp
    80       hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
    81       then obtain a b where "ls = a @ b" "length a = n'" by iprover
    82       with s have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
    83       thus ?thesis by blast
    84     qed
    85   qed
    86 qed
    87 
    88 lemma rev_append_cons:
    89 "n < length x \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
    90 proof -
    91   assume n: "n < length x"
    92   hence "n \<le> length x" by simp
    93   hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
    94   then obtain r d where x: "x = r@d" "length r = n" by iprover
    95   with n have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
    96   then obtain b c where "d = b#c" by iprover
    97   with x have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
    98   thus ?thesis by blast
    99 qed
   100 
   101 lemma sup_loc_length_map:
   102   "G \<turnstile> map f a <=l map g b \<Longrightarrow> length a = length b"
   103 proof -
   104   assume "G \<turnstile> map f a <=l map g b"
   105   hence "length (map f a) = length (map g b)" by (rule sup_loc_length)
   106   thus ?thesis by simp
   107 qed
   108 
   109 lemmas [iff] = not_Err_eq
   110 
   111 lemma app_mono: 
   112 "\<lbrakk>G \<turnstile> s <=' s'; app i G m rT pc et s'\<rbrakk> \<Longrightarrow> app i G m rT pc et s"
   113 proof -
   114 
   115   { fix s1 s2
   116     assume G:   "G \<turnstile> s2 <=s s1"
   117     assume app: "app i G m rT pc et (Some s1)"
   118 
   119     note [simp] = sup_loc_length sup_loc_length_map
   120 
   121     have "app i G m rT pc et (Some s2)"
   122     proof (cases (open) i)
   123       case Load
   124     
   125       from G Load app
   126       have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_conv)
   127       
   128       with G Load app show ?thesis 
   129         by (cases s2) (auto simp add: sup_state_conv dest: sup_loc_some)
   130     next
   131       case Store
   132       with G app show ?thesis
   133         by (cases s2, auto simp add: sup_loc_Cons2 sup_state_conv)
   134     next
   135       case LitPush
   136       with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
   137     next
   138       case New
   139       with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
   140     next
   141       case Getfield
   142       with app G show ?thesis
   143         by (cases s2) (clarsimp simp add: sup_state_Cons2, rule widen_trans) 
   144     next
   145       case Putfield
   146       
   147       with app 
   148       obtain vT oT ST LT b
   149         where s1: "s1 = (vT # oT # ST, LT)" and
   150                   "field (G, cname) vname = Some (cname, b)" 
   151                   "is_class G cname" and
   152               oT: "G\<turnstile> oT\<preceq> (Class cname)" and
   153               vT: "G\<turnstile> vT\<preceq> b" and
   154               xc: "Ball (set (match G NullPointer pc et)) (is_class G)"
   155         by force
   156       moreover
   157       from s1 G
   158       obtain vT' oT' ST' LT'
   159         where s2:  "s2 = (vT' # oT' # ST', LT')" and
   160               oT': "G\<turnstile> oT' \<preceq> oT" and
   161               vT': "G\<turnstile> vT' \<preceq> vT"
   162         by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
   163       moreover
   164       from vT' vT
   165       have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
   166       moreover
   167       from oT' oT
   168       have "G\<turnstile> oT' \<preceq> (Class cname)" by (rule widen_trans)
   169       ultimately
   170       show ?thesis by (auto simp add: Putfield xc)
   171     next
   172       case Checkcast
   173       with app G show ?thesis 
   174         by (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2)
   175     next
   176       case Return
   177       with app G show ?thesis
   178         by (cases s2) (auto simp add: sup_state_Cons2, rule widen_trans)
   179     next
   180       case Pop
   181       with app G show ?thesis
   182         by (cases s2, clarsimp simp add: sup_state_Cons2)
   183     next
   184       case Dup
   185       with app G show ?thesis
   186         by (cases s2, clarsimp simp add: sup_state_Cons2,
   187             auto dest: sup_state_length)
   188     next
   189       case Dup_x1
   190       with app G show ?thesis
   191         by (cases s2, clarsimp simp add: sup_state_Cons2, 
   192             auto dest: sup_state_length)
   193     next
   194       case Dup_x2
   195       with app G show ?thesis
   196         by (cases s2, clarsimp simp add: sup_state_Cons2,
   197             auto dest: sup_state_length)
   198     next
   199       case Swap
   200       with app G show ?thesis
   201         by (cases s2, clarsimp simp add: sup_state_Cons2)
   202     next
   203       case IAdd
   204       with app G show ?thesis
   205         by (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
   206     next
   207       case Goto 
   208       with app show ?thesis by simp
   209     next
   210       case Ifcmpeq
   211       with app G show ?thesis
   212         by (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
   213     next
   214       case Invoke
   215       
   216       with app
   217       obtain apTs X ST LT mD' rT' b' where
   218         s1: "s1 = (rev apTs @ X # ST, LT)" and
   219         l:  "length apTs = length list" and
   220         c:  "is_class G cname" and
   221         C:  "G \<turnstile> X \<preceq> Class cname" and
   222         w:  "\<forall>(x, y) \<in> set (zip apTs list). G \<turnstile> x \<preceq> y" and
   223         m:  "method (G, cname) (mname, list) = Some (mD', rT', b')" and
   224         x:  "\<forall>C \<in> set (match_any G pc et). is_class G C"
   225         by (simp del: not_None_eq, elim exE conjE) (rule that)
   226 
   227       obtain apTs' X' ST' LT' where
   228         s2: "s2 = (rev apTs' @ X' # ST', LT')" and
   229         l': "length apTs' = length list"
   230       proof -
   231         from l s1 G 
   232         have "length list < length (fst s2)" 
   233           by simp
   234         hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
   235           by (rule rev_append_cons [rule_format])
   236         thus ?thesis
   237           by -  (cases s2, elim exE conjE, simp, rule that) 
   238       qed
   239 
   240       from l l'
   241       have "length (rev apTs') = length (rev apTs)" by simp
   242     
   243       from this s1 s2 G 
   244       obtain
   245         G': "G \<turnstile> (apTs',LT') <=s (apTs,LT)" and
   246         X : "G \<turnstile>  X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)"
   247         by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1)
   248         
   249       with C
   250       have C': "G \<turnstile> X' \<preceq> Class cname"
   251         by - (rule widen_trans, auto)
   252     
   253       from G'
   254       have "G \<turnstile> map OK apTs' <=l map OK apTs"
   255         by (simp add: sup_state_conv)
   256       also
   257       from l w
   258       have "G \<turnstile> map OK apTs <=l map OK list" 
   259         by (simp add: all_widen_is_sup_loc)
   260       finally
   261       have "G \<turnstile> map OK apTs' <=l map OK list" .
   262 
   263       with l'
   264       have w': "\<forall>(x, y) \<in> set (zip apTs' list). G \<turnstile> x \<preceq> y"
   265         by (simp add: all_widen_is_sup_loc)
   266 
   267       from Invoke s2 l' w' C' m c x
   268       show ?thesis
   269         by (simp del: split_paired_Ex) blast
   270     next
   271       case Throw
   272       with app G show ?thesis
   273         by (cases s2, clarsimp simp add: sup_state_Cons2 widen_RefT2)
   274     qed
   275   } note this [simp]
   276 
   277   assume "G \<turnstile> s <=' s'" "app i G m rT pc et s'"
   278   thus ?thesis by (cases s, cases s', auto)
   279 qed
   280     
   281 lemmas [simp del] = split_paired_Ex
   282 
   283 lemma eff'_mono:
   284 "\<lbrakk> app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 \<rbrakk> \<Longrightarrow>
   285   G \<turnstile> eff' (i,G,s1) <=s eff' (i,G,s2)"
   286 proof (cases s1, cases s2)
   287   fix a1 b1 a2 b2
   288   assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
   289   assume app2: "app i G m rT pc et (Some s2)"
   290   assume G: "G \<turnstile> s1 <=s s2"
   291   
   292   note [simp] = eff_def
   293 
   294   with G have "G \<turnstile> (Some s1) <=' (Some s2)" by simp
   295   from this app2
   296   have app1: "app i G m rT pc et (Some s1)" by (rule app_mono)
   297 
   298   show ?thesis
   299   proof (cases (open) i)
   300     case Load
   301 
   302     with s app1
   303     obtain y where
   304        y:  "nat < length b1" "b1 ! nat = OK y" by clarsimp
   305 
   306     from Load s app2
   307     obtain y' where
   308        y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp
   309 
   310     from G s 
   311     have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_conv)
   312 
   313     with y y'
   314     have "G \<turnstile> y \<preceq> y'" 
   315       by - (drule sup_loc_some, simp+)
   316     
   317     with Load G y y' s app1 app2 
   318     show ?thesis by (clarsimp simp add: sup_state_conv)
   319   next
   320     case Store
   321     with G s app1 app2
   322     show ?thesis
   323       by (clarsimp simp add: sup_state_conv sup_loc_update)
   324   next
   325     case LitPush
   326     with G s app1 app2
   327     show ?thesis
   328       by (clarsimp simp add: sup_state_Cons1)
   329   next
   330     case New
   331     with G s app1 app2
   332     show ?thesis
   333       by (clarsimp simp add: sup_state_Cons1)
   334   next
   335     case Getfield
   336     with G s app1 app2
   337     show ?thesis
   338       by (clarsimp simp add: sup_state_Cons1)
   339   next
   340     case Putfield
   341     with G s app1 app2
   342     show ?thesis
   343       by (clarsimp simp add: sup_state_Cons1)
   344   next
   345     case Checkcast
   346     with G s app1 app2
   347     show ?thesis
   348       by (clarsimp simp add: sup_state_Cons1)
   349   next
   350     case Invoke
   351 
   352     with s app1
   353     obtain a X ST where
   354       s1: "s1 = (a @ X # ST, b1)" and
   355       l:  "length a = length list"
   356       by (simp, elim exE conjE, simp (no_asm_simp))
   357 
   358     from Invoke s app2
   359     obtain a' X' ST' where
   360       s2: "s2 = (a' @ X' # ST', b2)" and
   361       l': "length a' = length list"
   362       by (simp, elim exE conjE, simp (no_asm_simp))
   363 
   364     from l l'
   365     have lr: "length a = length a'" by simp
   366       
   367     from lr G s1 s2 
   368     have "G \<turnstile> (ST, b1) <=s (ST', b2)"
   369       by (simp add: sup_state_append_fst sup_state_Cons1)
   370     
   371     moreover
   372 
   373     obtain b1' b2' where eff':
   374       "b1' = snd (eff' (i,G,s1))" 
   375       "b2' = snd (eff' (i,G,s2))" by simp
   376 
   377     from Invoke G s eff' app1 app2
   378     obtain "b1 = b1'" "b2 = b2'" by simp
   379 
   380     ultimately 
   381 
   382     have "G \<turnstile> (ST, b1') <=s (ST', b2')" by simp
   383 
   384     with Invoke G s app1 app2 eff' s1 s2 l l'
   385     show ?thesis 
   386       by (clarsimp simp add: sup_state_conv)
   387   next
   388     case Return 
   389     with G
   390     show ?thesis
   391       by simp
   392   next
   393     case Pop
   394     with G s app1 app2
   395     show ?thesis
   396       by (clarsimp simp add: sup_state_Cons1)
   397   next
   398     case Dup
   399     with G s app1 app2
   400     show ?thesis
   401       by (clarsimp simp add: sup_state_Cons1)
   402   next
   403     case Dup_x1
   404     with G s app1 app2
   405     show ?thesis
   406       by (clarsimp simp add: sup_state_Cons1)
   407   next 
   408     case Dup_x2
   409     with G s app1 app2
   410     show ?thesis
   411       by (clarsimp simp add: sup_state_Cons1)
   412   next
   413     case Swap
   414     with G s app1 app2
   415     show ?thesis
   416       by (clarsimp simp add: sup_state_Cons1)
   417   next
   418     case IAdd
   419     with G s app1 app2
   420     show ?thesis
   421       by (clarsimp simp add: sup_state_Cons1)
   422   next
   423     case Goto
   424     with G s app1 app2
   425     show ?thesis by simp
   426   next
   427     case Ifcmpeq
   428     with G s app1 app2
   429     show ?thesis
   430       by (clarsimp simp add: sup_state_Cons1)
   431   next 
   432     case Throw
   433     with G
   434     show ?thesis
   435       by simp
   436   qed
   437 qed
   438 
   439 lemmas [iff del] = not_Err_eq
   440 
   441 end