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