src/HOL/MicroJava/BV/StepMono.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/MicroJava/BV/StepMono.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4     Copyright   2000 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* Monotonicity of step and app *}
     8 
     9 theory StepMono = Step:
    10 
    11 
    12 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
    13   by (auto elim: widen.elims)
    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)
    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 zs)" "(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)
    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\<in>set (zip a b). x \<in> widen G) = (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 
    80       have  "n' \<le> length ls" by simp 
    81       hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
    82       thus ?thesis
    83       proof elim
    84         fix a b 
    85         assume "ls = a @ b" "length a = n'"
    86         with s
    87         have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
    88         thus ?thesis by blast
    89       qed
    90     qed
    91   qed
    92 qed
    93 
    94 
    95 
    96 lemma rev_append_cons:
    97 "\<lbrakk>n < length x\<rbrakk> \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
    98 proof -
    99   assume n: "n < length x"
   100   hence "n \<le> length x" by simp
   101   hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
   102   thus ?thesis
   103   proof elim
   104     fix r d assume x: "x = r@d" "length r = n"
   105     with n
   106     have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
   107     
   108     thus ?thesis 
   109     proof elim
   110       fix b c 
   111       assume "d = b#c"
   112       with x
   113       have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
   114       thus ?thesis by blast
   115     qed
   116   qed
   117 qed
   118 
   119 
   120 lemma app_mono: 
   121 "\<lbrakk>G \<turnstile> s <=' s'; app i G rT s'\<rbrakk> \<Longrightarrow> app i G rT s";
   122 proof -
   123 
   124   { fix s1 s2
   125     assume G:   "G \<turnstile> s2 <=s s1"
   126     assume app: "app i G rT (Some s1)"
   127 
   128     have "app i G rT (Some s2)"
   129     proof (cases (open) i)
   130       case Load
   131     
   132       from G
   133       have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
   134       
   135       from G Load app
   136       have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
   137       
   138       with G Load app l
   139       show ?thesis by clarsimp (drule sup_loc_some, simp+)
   140     next
   141       case Store
   142       with G app
   143       show ?thesis
   144         by - (cases s2,
   145               auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def)
   146     next
   147       case Bipush
   148       thus ?thesis by simp 
   149     next
   150       case Aconst_null
   151       thus ?thesis by simp
   152     next
   153       case New
   154       with app
   155       show ?thesis by simp
   156     next
   157       case Getfield
   158       with app G
   159       show ?thesis
   160         by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
   161     next
   162       case Putfield
   163       
   164       with app 
   165       obtain vT oT ST LT b
   166         where s1: "s1 = (vT # oT # ST, LT)" and
   167                   "field (G, cname) vname = Some (cname, b)" 
   168                   "is_class G cname" and
   169               oT: "G\<turnstile> oT\<preceq> (Class cname)" and
   170               vT: "G\<turnstile> vT\<preceq> b"
   171         by simp (elim exE conjE, rule that) 
   172       moreover
   173       from s1 G
   174       obtain vT' oT' ST' LT'
   175         where s2:  "s2 = (vT' # oT' # ST', LT')" and
   176               oT': "G\<turnstile> oT' \<preceq> oT" and
   177               vT': "G\<turnstile> vT' \<preceq> vT"
   178         by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
   179       moreover
   180       from vT' vT
   181       have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
   182       moreover
   183       from oT' oT
   184       have "G\<turnstile> oT' \<preceq> (Class cname)" by (rule widen_trans)
   185       ultimately
   186       show ?thesis
   187         by (auto simp add: Putfield)
   188     next
   189       case Checkcast
   190       with app G
   191       show ?thesis 
   192         by - (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2)
   193     next
   194       case Return
   195       with app G
   196       show ?thesis
   197         by - (cases s2, auto simp add: sup_state_Cons2, rule widen_trans)
   198     next
   199       case Pop
   200       with app G
   201       show ?thesis
   202         by - (cases s2, clarsimp simp add: sup_state_Cons2)
   203     next
   204       case Dup
   205       with app G
   206       show ?thesis
   207         by - (cases s2, clarsimp simp add: sup_state_Cons2)
   208     next
   209       case Dup_x1
   210       with app G
   211       show ?thesis
   212         by - (cases s2, clarsimp simp add: sup_state_Cons2)
   213     next
   214       case Dup_x2
   215       with app G
   216       show ?thesis
   217         by - (cases s2, clarsimp simp add: sup_state_Cons2)
   218     next
   219       case Swap
   220       with app G
   221       show ?thesis
   222         by - (cases s2, clarsimp simp add: sup_state_Cons2)
   223     next
   224       case IAdd
   225       with app G
   226       show ?thesis
   227         by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
   228     next
   229       case Goto 
   230       with app
   231       show ?thesis by simp
   232     next
   233       case Ifcmpeq
   234       with app G
   235       show ?thesis
   236         by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
   237     next
   238       case Invoke
   239       
   240       with app
   241       obtain apTs X ST LT mD' rT' b' where
   242         s1: "s1 = (rev apTs @ X # ST, LT)" and
   243         l:  "length apTs = length list" and
   244         C:  "G \<turnstile> X \<preceq> Class cname" and
   245         w:  "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
   246         m:  "method (G, cname) (mname, list) = Some (mD', rT', b')"
   247         by (simp, elim exE conjE) (rule that)
   248 
   249       obtain apTs' X' ST' LT' where
   250         s2: "s2 = (rev apTs' @ X' # ST', LT')" and
   251         l': "length apTs' = length list"
   252       proof -
   253         from l s1 G 
   254         have "length list < length (fst s2)" 
   255           by (simp add: sup_state_length)
   256         hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
   257           by (rule rev_append_cons [rule_format])
   258         thus ?thesis
   259           by -  (cases s2, elim exE conjE, simp, rule that) 
   260       qed
   261 
   262       from l l'
   263       have "length (rev apTs') = length (rev apTs)" by simp
   264     
   265       from this s1 s2 G 
   266       obtain
   267         G': "G \<turnstile> (apTs',LT') <=s (apTs,LT)" and
   268         X : "G \<turnstile>  X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)"
   269         by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1)
   270         
   271       with C
   272       have C': "G \<turnstile> X' \<preceq> Class cname"
   273         by - (rule widen_trans, auto)
   274     
   275       from G'
   276       have "G \<turnstile> map Ok apTs' <=l map Ok apTs"
   277         by (simp add: sup_state_def)
   278       also
   279       from l w
   280       have "G \<turnstile> map Ok apTs <=l map Ok list" 
   281         by (simp add: all_widen_is_sup_loc)
   282       finally
   283       have "G \<turnstile> map Ok apTs' <=l map Ok list" .
   284 
   285       with l'
   286       have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
   287         by (simp add: all_widen_is_sup_loc)
   288 
   289       from Invoke s2 l' w' C' m
   290       show ?thesis 
   291         by simp blast
   292     qed
   293   } note mono_Some = this
   294 
   295   assume "G \<turnstile> s <=' s'" "app i G rT s'"
   296   
   297   thus ?thesis 
   298     by - (cases s, cases s', auto simp add: mono_Some)
   299 qed
   300     
   301 lemmas [simp del] = split_paired_Ex
   302 lemmas [simp] = step_def
   303 
   304 lemma step_mono_Some:
   305 "[| succs i pc \<noteq> []; app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
   306   G \<turnstile> the (step i G (Some s1)) <=s the (step i G (Some s2))"
   307 proof (cases s1, cases s2) 
   308   fix a1 b1 a2 b2
   309   assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
   310   assume succs: "succs i pc \<noteq> []"
   311   assume app2: "app i G rT (Some s2)"
   312   assume G: "G \<turnstile> s1 <=s s2"
   313 
   314   hence "G \<turnstile> Some s1 <=' Some s2" 
   315     by simp
   316   from this app2
   317   have app1: "app i G rT (Some s1)" by (rule app_mono)
   318   
   319   have "step i G (Some s1) \<noteq> None \<and> step i G (Some s2) \<noteq> None"
   320     by simp
   321   then 
   322   obtain a1' b1' a2' b2'
   323     where step: "step i G (Some s1) = Some (a1',b1')" 
   324                 "step i G (Some s2) = Some (a2',b2')"
   325     by (auto simp del: step_def simp add: s)
   326 
   327   have "G \<turnstile> (a1',b1') <=s (a2',b2')"
   328   proof (cases (open) i)
   329     case Load
   330 
   331     with s app1
   332     obtain y where
   333        y:  "nat < length b1" "b1 ! nat = Ok y" by clarsimp
   334 
   335     from Load s app2
   336     obtain y' where
   337        y': "nat < length b2" "b2 ! nat = Ok y'" by clarsimp
   338 
   339     from G s 
   340     have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def)
   341 
   342     with y y'
   343     have "G \<turnstile> y \<preceq> y'" 
   344       by - (drule sup_loc_some, simp+)
   345     
   346     with Load G y y' s step app1 app2 
   347     show ?thesis by (clarsimp simp add: sup_state_def)
   348   next
   349     case Store
   350     with G s step app1 app2
   351     show ?thesis
   352       by (clarsimp simp add: sup_state_def sup_loc_update)
   353   next
   354     case Bipush
   355     with G s step app1 app2
   356     show ?thesis
   357       by (clarsimp simp add: sup_state_Cons1)
   358   next
   359     case New
   360     with G s step app1 app2
   361     show ?thesis
   362       by (clarsimp simp add: sup_state_Cons1)
   363   next
   364     case Aconst_null
   365     with G s step app1 app2
   366     show ?thesis
   367       by (clarsimp simp add: sup_state_Cons1)
   368   next
   369     case Getfield
   370     with G s step app1 app2
   371     show ?thesis
   372       by (clarsimp simp add: sup_state_Cons1)
   373   next
   374     case Putfield
   375     with G s step app1 app2
   376     show ?thesis
   377       by (clarsimp simp add: sup_state_Cons1)
   378   next
   379     case Checkcast
   380     with G s step app1 app2
   381     show ?thesis
   382       by (clarsimp simp add: sup_state_Cons1)
   383   next
   384     case Invoke
   385 
   386     with s app1
   387     obtain a X ST where
   388       s1: "s1 = (a @ X # ST, b1)" and
   389       l:  "length a = length list"
   390       by (simp, elim exE conjE, simp)
   391 
   392     from Invoke s app2
   393     obtain a' X' ST' where
   394       s2: "s2 = (a' @ X' # ST', b2)" and
   395       l': "length a' = length list"
   396       by (simp, elim exE conjE, simp)
   397 
   398     from l l'
   399     have lr: "length a = length a'" by simp
   400       
   401     from lr G s s1 s2 
   402     have "G \<turnstile> (ST, b1) <=s (ST', b2)"
   403       by (simp add: sup_state_append_fst sup_state_Cons1)
   404     
   405     moreover
   406     
   407     from Invoke G s step app1 app2
   408     have "b1 = b1' \<and> b2 = b2'" by simp
   409 
   410     ultimately 
   411 
   412     have "G \<turnstile> (ST, b1') <=s (ST', b2')" by simp
   413 
   414     with Invoke G s step app1 app2 s1 s2 l l'
   415     show ?thesis 
   416       by (clarsimp simp add: sup_state_def)
   417   next
   418     case Return
   419     with succs have "False" by simp
   420     thus ?thesis by blast
   421   next
   422     case Pop
   423     with G s step app1 app2
   424     show ?thesis
   425       by (clarsimp simp add: sup_state_Cons1)
   426   next
   427     case Dup
   428     with G s step app1 app2
   429     show ?thesis
   430       by (clarsimp simp add: sup_state_Cons1)
   431   next
   432     case Dup_x1
   433     with G s step app1 app2
   434     show ?thesis
   435       by (clarsimp simp add: sup_state_Cons1)
   436   next 
   437     case Dup_x2
   438     with G s step app1 app2
   439     show ?thesis
   440       by (clarsimp simp add: sup_state_Cons1)
   441   next
   442     case Swap
   443     with G s step app1 app2
   444     show ?thesis
   445       by (clarsimp simp add: sup_state_Cons1)
   446   next
   447     case IAdd
   448     with G s step app1 app2
   449     show ?thesis
   450       by (clarsimp simp add: sup_state_Cons1)
   451   next
   452     case Goto
   453     with G s step app1 app2
   454     show ?thesis by simp
   455   next
   456     case Ifcmpeq
   457     with G s step app1 app2
   458     show ?thesis
   459       by (clarsimp simp add: sup_state_Cons1)   
   460   qed
   461 
   462   with step
   463   show ?thesis by auto  
   464 qed
   465 
   466 lemma step_mono:
   467   "[| succs i pc \<noteq> []; app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
   468   G \<turnstile> step i G s1 <=' step i G s2"
   469   by (cases s1, cases s2, auto dest: step_mono_Some)
   470 
   471 lemmas [simp del] = step_def
   472 
   473 end
   474