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