src/HOL/MicroJava/BV/Convert.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;
nipkow@8011
     1
(*  Title:      HOL/MicroJava/BV/Convert.thy
nipkow@8011
     2
    ID:         $Id$
kleing@9757
     3
    Author:     Cornelia Pusch and Gerwin Klein
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
kleing@9757
     5
*)
nipkow@8011
     6
kleing@9757
     7
header "Lifted Type Relations"
nipkow@8011
     8
kleing@9594
     9
theory Convert = JVMExec:
nipkow@8011
    10
kleing@9757
    11
text "The supertype relation lifted to type err, type lists and state types."
kleing@9757
    12
kleing@9757
    13
datatype 'a err = Err | Ok 'a
kleing@9757
    14
nipkow@8011
    15
types
kleing@9757
    16
 locvars_type = "ty err list"
kleing@9594
    17
 opstack_type = "ty list"
kleing@9594
    18
 state_type   = "opstack_type \<times> locvars_type"
nipkow@8011
    19
kleing@9757
    20
kleing@9757
    21
consts
kleing@9757
    22
  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
kleing@9757
    23
primrec
kleing@9757
    24
  "strict f Err    = Err"
kleing@9757
    25
  "strict f (Ok x) = f x"
kleing@9757
    26
kleing@9757
    27
consts
kleing@9757
    28
  opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
kleing@9757
    29
primrec
kleing@9757
    30
  "opt_map f None     = None"
kleing@9757
    31
  "opt_map f (Some x) = Some (f x)"
kleing@9757
    32
kleing@9757
    33
consts
kleing@9757
    34
  val :: "'a err \<Rightarrow> 'a"
kleing@9757
    35
primrec
kleing@9757
    36
  "val (Ok s) = s"
nipkow@8011
    37
kleing@9757
    38
  
kleing@9757
    39
constdefs
kleing@9757
    40
  (* lifts a relation to err with Err as top element *)
kleing@9757
    41
  lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
kleing@9594
    42
  "lift_top P a' a \<equiv> case a of 
kleing@9757
    43
                       Err  \<Rightarrow> True
kleing@9757
    44
                     | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
kleing@9757
    45
kleing@9757
    46
  (* lifts a relation to option with None as bottom element *)
kleing@9757
    47
  lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
kleing@9757
    48
  "lift_bottom P a' a \<equiv> case a' of 
kleing@9757
    49
                          None    \<Rightarrow> True 
kleing@9757
    50
                        | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
kleing@9757
    51
kleing@9757
    52
  sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
kleing@9757
    53
  "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
kleing@9757
    54
kleing@9757
    55
  sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
kleing@9757
    56
             ("_ \<turnstile> _ <=l _"  [71,71] 70)
kleing@9757
    57
  "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
kleing@9757
    58
kleing@9757
    59
  sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  
kleing@9757
    60
               ("_ \<turnstile> _ <=s _"  [71,71] 70)
kleing@9757
    61
  "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
kleing@9757
    62
kleing@9757
    63
  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
kleing@9757
    64
                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
kleing@9757
    65
  "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
kleing@9594
    66
kleing@9594
    67
kleing@9757
    68
lemma not_Err_eq [iff]:
kleing@9757
    69
  "(x \<noteq> Err) = (\<exists>a. x = Ok a)" 
kleing@9757
    70
  by (cases x) auto
kleing@9594
    71
kleing@9757
    72
lemma not_Some_eq [iff]:
kleing@9757
    73
  "(\<forall>y. x \<noteq> Ok y) = (x = Err)"
kleing@9757
    74
  by (cases x) auto  
kleing@9594
    75
kleing@9594
    76
kleing@9594
    77
lemma lift_top_refl [simp]:
kleing@9594
    78
  "[| !!x. P x x |] ==> lift_top P x x"
kleing@9757
    79
  by (simp add: lift_top_def split: err.splits)
kleing@9594
    80
kleing@9594
    81
lemma lift_top_trans [trans]:
kleing@9757
    82
  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] 
kleing@9757
    83
  ==> lift_top P x z"
kleing@9594
    84
proof -
kleing@9594
    85
  assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
kleing@9594
    86
  assume a: "lift_top P x y"
kleing@9594
    87
  assume b: "lift_top P y z"
kleing@9594
    88
kleing@9757
    89
  { assume "z = Err" 
kleing@9594
    90
    hence ?thesis by (simp add: lift_top_def)
kleing@9594
    91
  } note z_none = this
kleing@9594
    92
kleing@9757
    93
  { assume "x = Err"
kleing@9594
    94
    with a b
kleing@9594
    95
    have ?thesis
kleing@9757
    96
      by (simp add: lift_top_def split: err.splits)
kleing@9594
    97
  } note x_none = this
kleing@9594
    98
  
kleing@9594
    99
  { fix r t
kleing@9757
   100
    assume x: "x = Ok r" and z: "z = Ok t"    
kleing@9594
   101
    with a b
kleing@9757
   102
    obtain s where y: "y = Ok s" 
kleing@9757
   103
      by (simp add: lift_top_def split: err.splits)
kleing@9594
   104
    
kleing@9594
   105
    from a x y
kleing@9594
   106
    have "P r s" by (simp add: lift_top_def)
kleing@9594
   107
    also
kleing@9594
   108
    from b y z
kleing@9594
   109
    have "P s t" by (simp add: lift_top_def)
kleing@9594
   110
    finally 
kleing@9594
   111
    have "P r t" .
kleing@9594
   112
kleing@9594
   113
    with x z
kleing@9594
   114
    have ?thesis by (simp add: lift_top_def)
kleing@9594
   115
  } 
kleing@9594
   116
kleing@9594
   117
  with x_none z_none
kleing@9594
   118
  show ?thesis by blast
kleing@9594
   119
qed
kleing@9594
   120
kleing@9757
   121
lemma lift_top_Err_any [simp]:
kleing@9757
   122
  "lift_top P Err any = (any = Err)"
kleing@9757
   123
  by (simp add: lift_top_def split: err.splits)
kleing@9757
   124
kleing@9757
   125
lemma lift_top_Ok_Ok [simp]:
kleing@9757
   126
  "lift_top P (Ok a) (Ok b) = P a b"
kleing@9757
   127
  by (simp add: lift_top_def split: err.splits)
kleing@9757
   128
kleing@9757
   129
lemma lift_top_any_Ok [simp]:
kleing@9757
   130
  "lift_top P any (Ok b) = (\<exists>a. any = Ok a \<and> P a b)"
kleing@9757
   131
  by (simp add: lift_top_def split: err.splits)
kleing@9757
   132
kleing@9757
   133
lemma lift_top_Ok_any:
kleing@9757
   134
  "lift_top P (Ok a) any = (any = Err \<or> (\<exists>b. any = Ok b \<and> P a b))"
kleing@9757
   135
  by (simp add: lift_top_def split: err.splits)
kleing@9594
   136
kleing@9757
   137
kleing@9757
   138
lemma lift_bottom_refl [simp]:
kleing@9757
   139
  "[| !!x. P x x |] ==> lift_bottom P x x"
kleing@9757
   140
  by (simp add: lift_bottom_def split: option.splits)
kleing@9757
   141
kleing@9757
   142
lemma lift_bottom_trans [trans]:
kleing@9757
   143
  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |]
kleing@9757
   144
  ==> lift_bottom P x z"
kleing@9757
   145
proof -
kleing@9757
   146
  assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
kleing@9757
   147
  assume a: "lift_bottom P x y"
kleing@9757
   148
  assume b: "lift_bottom P y z"
kleing@9757
   149
kleing@9757
   150
  { assume "x = None" 
kleing@9757
   151
    hence ?thesis by (simp add: lift_bottom_def)
kleing@9757
   152
  } note z_none = this
kleing@9594
   153
kleing@9757
   154
  { assume "z = None"
kleing@9757
   155
    with a b
kleing@9757
   156
    have ?thesis
kleing@9757
   157
      by (simp add: lift_bottom_def split: option.splits)
kleing@9757
   158
  } note x_none = this
kleing@9757
   159
  
kleing@9757
   160
  { fix r t
kleing@9757
   161
    assume x: "x = Some r" and z: "z = Some t"    
kleing@9757
   162
    with a b
kleing@9757
   163
    obtain s where y: "y = Some s" 
kleing@9757
   164
      by (simp add: lift_bottom_def split: option.splits)
kleing@9757
   165
    
kleing@9757
   166
    from a x y
kleing@9757
   167
    have "P r s" by (simp add: lift_bottom_def)
kleing@9757
   168
    also
kleing@9757
   169
    from b y z
kleing@9757
   170
    have "P s t" by (simp add: lift_bottom_def)
kleing@9757
   171
    finally 
kleing@9757
   172
    have "P r t" .
kleing@9594
   173
kleing@9757
   174
    with x z
kleing@9757
   175
    have ?thesis by (simp add: lift_bottom_def)
kleing@9757
   176
  } 
kleing@9757
   177
kleing@9757
   178
  with x_none z_none
kleing@9757
   179
  show ?thesis by blast
kleing@9757
   180
qed
kleing@9757
   181
kleing@9757
   182
lemma lift_bottom_any_None [simp]:
kleing@9757
   183
  "lift_bottom P any None = (any = None)"
kleing@9757
   184
  by (simp add: lift_bottom_def split: option.splits)
kleing@9757
   185
kleing@9757
   186
lemma lift_bottom_Some_Some [simp]:
kleing@9757
   187
  "lift_bottom P (Some a) (Some b) = P a b"
kleing@9757
   188
  by (simp add: lift_bottom_def split: option.splits)
kleing@9757
   189
kleing@9757
   190
lemma lift_bottom_any_Some [simp]:
kleing@9757
   191
  "lift_bottom P (Some a) any = (\<exists>b. any = Some b \<and> P a b)"
kleing@9757
   192
  by (simp add: lift_bottom_def split: option.splits)
kleing@9757
   193
kleing@9757
   194
lemma lift_bottom_Some_any:
kleing@9757
   195
  "lift_bottom P any (Some b) = (any = None \<or> (\<exists>a. any = Some a \<and> P a b))"
kleing@9757
   196
  by (simp add: lift_bottom_def split: option.splits)
kleing@9594
   197
kleing@9594
   198
kleing@9594
   199
kleing@9594
   200
theorem sup_ty_opt_refl [simp]:
kleing@9594
   201
  "G \<turnstile> t <=o t"
kleing@9594
   202
  by (simp add: sup_ty_opt_def)
kleing@9594
   203
kleing@9594
   204
theorem sup_loc_refl [simp]:
kleing@9594
   205
  "G \<turnstile> t <=l t"
kleing@9594
   206
  by (induct t, auto simp add: sup_loc_def)
kleing@9594
   207
kleing@9594
   208
theorem sup_state_refl [simp]:
kleing@9594
   209
  "G \<turnstile> s <=s s"
kleing@9594
   210
  by (simp add: sup_state_def)
kleing@9594
   211
kleing@9757
   212
theorem sup_state_opt_refl [simp]:
kleing@9757
   213
  "G \<turnstile> s <=' s"
kleing@9757
   214
  by (simp add: sup_state_opt_def)
kleing@9594
   215
kleing@9594
   216
kleing@9757
   217
theorem anyConvErr [simp]:
kleing@9757
   218
  "(G \<turnstile> Err <=o any) = (any = Err)"
kleing@9594
   219
  by (simp add: sup_ty_opt_def)
kleing@9594
   220
kleing@9757
   221
theorem OkanyConvOk [simp]:
kleing@9757
   222
  "(G \<turnstile> (Ok ty') <=o (Ok ty)) = (G \<turnstile> ty' \<preceq> ty)"
kleing@9594
   223
  by (simp add: sup_ty_opt_def)
kleing@9594
   224
kleing@9757
   225
theorem sup_ty_opt_Ok:
kleing@9757
   226
  "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> x. a = Ok x"
kleing@9594
   227
  by (clarsimp simp add: sup_ty_opt_def)
kleing@9594
   228
kleing@9594
   229
lemma widen_PrimT_conv1 [simp]:
kleing@9594
   230
  "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
kleing@9594
   231
  by (auto elim: widen.elims)
kleing@9594
   232
kleing@9594
   233
theorem sup_PTS_eq:
kleing@9757
   234
  "(G \<turnstile> Ok (PrimT p) <=o X) = (X=Err \<or> X = Ok (PrimT p))"
kleing@9757
   235
  by (auto simp add: sup_ty_opt_def lift_top_Ok_any)
kleing@9594
   236
kleing@9594
   237
kleing@9594
   238
kleing@9594
   239
theorem sup_loc_Nil [iff]:
kleing@9594
   240
  "(G \<turnstile> [] <=l XT) = (XT=[])"
kleing@9594
   241
  by (simp add: sup_loc_def)
kleing@9594
   242
kleing@9594
   243
theorem sup_loc_Cons [iff]:
kleing@9594
   244
  "(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@9594
   245
  by (simp add: sup_loc_def list_all2_Cons1)
kleing@9594
   246
kleing@9594
   247
theorem sup_loc_Cons2:
kleing@9757
   248
  "(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@9594
   249
  by (simp add: sup_loc_def list_all2_Cons2)
kleing@9594
   250
kleing@9594
   251
kleing@9594
   252
theorem sup_loc_length:
kleing@9594
   253
  "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
kleing@9594
   254
proof -
kleing@9594
   255
  assume G: "G \<turnstile> a <=l b"
kleing@9594
   256
  have "\<forall> b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
kleing@9594
   257
    by (induct a, auto)
kleing@9594
   258
  with G
kleing@9594
   259
  show ?thesis by blast
kleing@9594
   260
qed
kleing@9594
   261
kleing@9594
   262
theorem sup_loc_nth:
kleing@9594
   263
  "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
kleing@9594
   264
proof -
kleing@9594
   265
  assume a: "G \<turnstile> a <=l b" "n < length a"
kleing@9594
   266
  have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
kleing@9594
   267
    (is "?P a")
kleing@9594
   268
  proof (induct a)
kleing@9594
   269
    show "?P []" by simp
kleing@9594
   270
    
kleing@9594
   271
    fix x xs assume IH: "?P xs"
kleing@9594
   272
kleing@9594
   273
    show "?P (x#xs)"
kleing@9594
   274
    proof (intro strip)
kleing@9594
   275
      fix n b
kleing@9594
   276
      assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)"
kleing@9594
   277
      with IH
kleing@9594
   278
      show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)"
kleing@9594
   279
        by - (cases n, auto)
kleing@9594
   280
    qed
kleing@9594
   281
  qed
kleing@9594
   282
  with a
kleing@9594
   283
  show ?thesis by blast
kleing@9594
   284
qed
kleing@9594
   285
kleing@9594
   286
kleing@9594
   287
theorem all_nth_sup_loc:
kleing@9757
   288
  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> 
kleing@9757
   289
       (G \<turnstile> a <=l b)" (is "?P a")
kleing@9594
   290
proof (induct a)
kleing@9594
   291
  show "?P []" by simp
nipkow@8011
   292
kleing@9594
   293
  fix l ls assume IH: "?P ls"
kleing@9594
   294
  
kleing@9594
   295
  show "?P (l#ls)"
kleing@9594
   296
  proof (intro strip)
kleing@9594
   297
    fix b
kleing@9594
   298
    assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
kleing@9594
   299
    assume l: "length (l#ls) = length b"
kleing@9594
   300
    
kleing@9594
   301
    then obtain b' bs where b: "b = b'#bs"
kleing@9594
   302
      by - (cases b, simp, simp add: neq_Nil_conv, rule that)
kleing@9594
   303
kleing@9594
   304
    with f
kleing@9594
   305
    have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
kleing@9594
   306
      by auto
kleing@9594
   307
kleing@9594
   308
    with f b l IH
kleing@9594
   309
    show "G \<turnstile> (l # ls) <=l b"
kleing@9594
   310
      by auto
kleing@9594
   311
  qed
kleing@9594
   312
qed
kleing@9594
   313
kleing@9594
   314
kleing@9594
   315
theorem sup_loc_append:
kleing@9757
   316
  "length a = length b ==> 
kleing@9757
   317
   (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
kleing@9594
   318
proof -
kleing@9594
   319
  assume l: "length a = length b"
kleing@9594
   320
kleing@9757
   321
  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
kleing@9757
   322
            (G \<turnstile> x <=l y))" (is "?P a") 
kleing@9594
   323
  proof (induct a)
kleing@9594
   324
    show "?P []" by simp
kleing@9594
   325
    
kleing@9594
   326
    fix l ls assume IH: "?P ls"    
kleing@9594
   327
    show "?P (l#ls)" 
kleing@9594
   328
    proof (intro strip)
kleing@9594
   329
      fix b
kleing@9757
   330
      assume "length (l#ls) = length (b::ty err list)"
kleing@9594
   331
      with IH
kleing@9594
   332
      show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
kleing@9594
   333
        by - (cases b, auto)
kleing@9594
   334
    qed
kleing@9594
   335
  qed
kleing@9594
   336
  with l
kleing@9594
   337
  show ?thesis by blast
kleing@9594
   338
qed
kleing@9594
   339
kleing@9594
   340
theorem sup_loc_rev [simp]:
kleing@9594
   341
  "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)"
kleing@9594
   342
proof -
kleing@9594
   343
  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@9594
   344
  proof (induct a)
kleing@9594
   345
    show "?P []" by simp
kleing@9594
   346
kleing@9594
   347
    fix l ls assume IH: "?P ls"
kleing@9594
   348
kleing@9594
   349
    { 
kleing@9594
   350
      fix b
kleing@9594
   351
      have "?Q (l#ls) b"
wenzelm@9664
   352
      proof (cases (open) b)
kleing@9594
   353
        case Nil
kleing@9594
   354
        thus ?thesis by (auto dest: sup_loc_length)
kleing@9594
   355
      next
kleing@9594
   356
        case Cons 
kleing@9594
   357
        show ?thesis
kleing@9594
   358
        proof
kleing@9594
   359
          assume "G \<turnstile> (l # ls) <=l b"
kleing@9594
   360
          thus "G \<turnstile> rev (l # ls) <=l rev b"
kleing@9594
   361
            by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append)
kleing@9594
   362
        next
kleing@9594
   363
          assume "G \<turnstile> rev (l # ls) <=l rev b"
kleing@9594
   364
          hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])"
kleing@9594
   365
            by (simp add: Cons)          
kleing@9594
   366
          
kleing@9594
   367
          hence "length (rev ls) = length (rev list)"
kleing@9594
   368
            by (auto dest: sup_loc_length)
kleing@9594
   369
kleing@9594
   370
          from this G
kleing@9594
   371
          obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a"
kleing@9594
   372
            by (simp add: sup_loc_append)
kleing@9594
   373
kleing@9594
   374
          thus "G \<turnstile> (l # ls) <=l b"
kleing@9594
   375
            by (simp add: Cons IH)
kleing@9594
   376
        qed
kleing@9594
   377
      qed    
kleing@9594
   378
    }
kleing@9594
   379
    thus "?P (l#ls)" by blast
kleing@9594
   380
  qed
nipkow@8011
   381
kleing@9594
   382
  thus ?thesis by blast
kleing@9594
   383
qed
kleing@9594
   384
kleing@9594
   385
wenzelm@9941
   386
theorem sup_loc_update [rule_format]:
kleing@9757
   387
  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
kleing@9757
   388
          (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
kleing@9594
   389
proof (induct x)
kleing@9594
   390
  show "?P []" by simp
kleing@9594
   391
kleing@9594
   392
  fix l ls assume IH: "?P ls"
kleing@9594
   393
  show "?P (l#ls)"
kleing@9594
   394
  proof (intro strip)
kleing@9594
   395
    fix n y
kleing@9594
   396
    assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y"
kleing@9594
   397
    with IH
kleing@9594
   398
    show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]"
kleing@9594
   399
      by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1)
kleing@9594
   400
  qed
kleing@9594
   401
qed
kleing@9594
   402
kleing@9594
   403
kleing@9594
   404
theorem sup_state_length [simp]:
kleing@9757
   405
  "G \<turnstile> s2 <=s s1 ==> 
kleing@9757
   406
   length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
kleing@9594
   407
  by (auto dest: sup_loc_length simp add: sup_state_def);
kleing@9594
   408
kleing@9594
   409
theorem sup_state_append_snd:
kleing@9757
   410
  "length a = length b ==> 
kleing@9757
   411
  (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@9594
   412
  by (auto simp add: sup_state_def sup_loc_append)
kleing@9594
   413
kleing@9594
   414
theorem sup_state_append_fst:
kleing@9757
   415
  "length a = length b ==> 
kleing@9757
   416
  (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@9594
   417
  by (auto simp add: sup_state_def sup_loc_append)
kleing@9594
   418
kleing@9594
   419
theorem sup_state_Cons1:
kleing@9757
   420
  "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
kleing@9757
   421
   (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
kleing@9594
   422
  by (auto simp add: sup_state_def map_eq_Cons)
kleing@9594
   423
kleing@9594
   424
theorem sup_state_Cons2:
kleing@9757
   425
  "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
kleing@9757
   426
   (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
kleing@9594
   427
  by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
kleing@9594
   428
kleing@9594
   429
theorem sup_state_ignore_fst:  
kleing@9594
   430
  "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
kleing@9594
   431
  by (simp add: sup_state_def)
kleing@9594
   432
kleing@9594
   433
theorem sup_state_rev_fst:
kleing@9594
   434
  "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
kleing@9594
   435
proof -
kleing@9594
   436
  have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
kleing@9594
   437
  show ?thesis by (simp add: m sup_state_def)
kleing@9594
   438
qed
kleing@9594
   439
  
kleing@9757
   440
kleing@9757
   441
lemma sup_state_opt_None_any [iff]:
kleing@9757
   442
  "(G \<turnstile> None <=' any) = True"
kleing@9757
   443
  by (simp add: sup_state_opt_def lift_bottom_def)
kleing@9757
   444
kleing@9757
   445
lemma sup_state_opt_any_None [iff]:
kleing@9757
   446
  "(G \<turnstile> any <=' None) = (any = None)"
kleing@9757
   447
  by (simp add: sup_state_opt_def)
kleing@9757
   448
kleing@9757
   449
lemma sup_state_opt_Some_Some [iff]:
kleing@9757
   450
  "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)"
kleing@9757
   451
  by (simp add: sup_state_opt_def del: split_paired_Ex)
kleing@9757
   452
kleing@9757
   453
lemma sup_state_opt_any_Some [iff]:
kleing@9757
   454
  "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)"
kleing@9757
   455
  by (simp add: sup_state_opt_def)
kleing@9757
   456
kleing@9757
   457
lemma sup_state_opt_Some_any:
kleing@9757
   458
  "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))"
kleing@9757
   459
  by (simp add: sup_state_opt_def lift_bottom_Some_any)
kleing@9757
   460
kleing@9757
   461
kleing@9594
   462
theorem sup_ty_opt_trans [trans]:
kleing@9594
   463
  "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
kleing@9594
   464
  by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
kleing@9594
   465
kleing@9594
   466
theorem sup_loc_trans [trans]:
kleing@9594
   467
  "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
kleing@9594
   468
proof -
kleing@9594
   469
  assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
kleing@9594
   470
 
kleing@9594
   471
  hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
kleing@9594
   472
  proof (intro strip)
kleing@9594
   473
    fix n 
kleing@9594
   474
    assume n: "n < length a"
kleing@9594
   475
    with G
kleing@9594
   476
    have "G \<turnstile> (a!n) <=o (b!n)"
kleing@9594
   477
      by - (rule sup_loc_nth)
kleing@9594
   478
    also 
kleing@9594
   479
    from n G
kleing@9594
   480
    have "G \<turnstile> ... <=o (c!n)"
kleing@9594
   481
      by - (rule sup_loc_nth, auto dest: sup_loc_length)
kleing@9594
   482
    finally
kleing@9594
   483
    show "G \<turnstile> (a!n) <=o (c!n)" .
kleing@9594
   484
  qed
kleing@9594
   485
kleing@9594
   486
  with G
kleing@9594
   487
  show ?thesis 
wenzelm@9941
   488
    by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) 
kleing@9594
   489
qed
kleing@9594
   490
  
kleing@9594
   491
kleing@9594
   492
theorem sup_state_trans [trans]:
kleing@9594
   493
  "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
kleing@9594
   494
  by (auto intro: sup_loc_trans simp add: sup_state_def)
nipkow@8011
   495
kleing@9757
   496
theorem sup_state_opt_trans [trans]:
kleing@9757
   497
  "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
kleing@9757
   498
  by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
kleing@9757
   499
kleing@9757
   500
nipkow@8011
   501
end