src/HOL/IMP/Compiler2.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 62390 842917225d56
child 63540 f8652d0534fa
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@51259
     1
(* Author: Gerwin Klein *)
kleing@51259
     2
nipkow@52400
     3
theory Compiler2
kleing@43438
     4
imports Compiler
kleing@43438
     5
begin
kleing@43438
     6
kleing@56224
     7
text {*
kleing@56224
     8
The preservation of the source code semantics is already shown in the 
kleing@56224
     9
parent theory @{theory Compiler}. This here shows the second direction.
kleing@56224
    10
*}
kleing@56224
    11
nipkow@50061
    12
section {* Compiler Correctness, Reverse Direction *}
kleing@43438
    13
kleing@43438
    14
subsection {* Definitions *}
kleing@43438
    15
kleing@43438
    16
text {* Execution in @{term n} steps for simpler induction *}
kleing@43438
    17
primrec 
kleing@43438
    18
  exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" 
kleing@44000
    19
  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
kleing@43438
    20
where 
kleing@43438
    21
  "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
kleing@43438
    22
  "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
kleing@43438
    23
kleing@51259
    24
text {* The possible successor PCs of an instruction at position @{term n} *}
kleing@51705
    25
text_raw{*\snip{isuccsdef}{0}{1}{% *}
nipkow@53911
    26
definition isuccs :: "instr \<Rightarrow> int \<Rightarrow> int set" where
nipkow@53911
    27
"isuccs i n = (case i of
nipkow@53911
    28
  JMP j \<Rightarrow> {n + 1 + j} |
nipkow@53911
    29
  JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
nipkow@53911
    30
  JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
nipkow@53911
    31
  _ \<Rightarrow> {n +1})"
kleing@51705
    32
text_raw{*}%endsnip*}
kleing@43438
    33
kleing@51259
    34
text {* The possible successors PCs of an instruction list *}
nipkow@53911
    35
definition succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where
nipkow@53911
    36
"succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" 
kleing@43438
    37
kleing@51259
    38
text {* Possible exit PCs of a program *}
nipkow@53911
    39
definition exits :: "instr list \<Rightarrow> int set" where
nipkow@53911
    40
"exits P = succs P 0 - {0..< size P}"
kleing@43438
    41
kleing@43438
    42
  
kleing@43438
    43
subsection {* Basic properties of @{term exec_n} *}
kleing@43438
    44
kleing@43438
    45
lemma exec_n_exec:
kleing@43438
    46
  "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
nipkow@61147
    47
  by (induct n arbitrary: c) (auto intro: star.step)
kleing@43438
    48
kleing@43438
    49
lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
kleing@43438
    50
kleing@45218
    51
lemma exec_Suc:
kleing@44000
    52
  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
nipkow@44890
    53
  by (fastforce simp del: split_paired_Ex)
kleing@43438
    54
kleing@43438
    55
lemma exec_exec_n:
kleing@43438
    56
  "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
kleing@52915
    57
  by (induct rule: star.induct) (auto intro: exec_Suc)
kleing@43438
    58
    
kleing@43438
    59
lemma exec_eq_exec_n:
kleing@43438
    60
  "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')"
kleing@43438
    61
  by (blast intro: exec_exec_n exec_n_exec)
kleing@43438
    62
kleing@43438
    63
lemma exec_n_Nil [simp]:
kleing@43438
    64
  "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
kleing@52915
    65
  by (induct k) (auto simp: exec1_def)
kleing@43438
    66
kleing@44004
    67
lemma exec1_exec_n [intro!]:
kleing@43438
    68
  "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
kleing@43438
    69
  by (cases c') simp
kleing@43438
    70
kleing@43438
    71
kleing@43438
    72
subsection {* Concrete symbolic execution steps *}
kleing@43438
    73
kleing@43438
    74
lemma exec_n_step:
kleing@43438
    75
  "n \<noteq> n' \<Longrightarrow> 
kleing@43438
    76
  P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') = 
kleing@43438
    77
  (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)"
kleing@43438
    78
  by (cases k) auto
kleing@43438
    79
kleing@43438
    80
lemma exec1_end:
kleing@51259
    81
  "size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
kleing@52915
    82
  by (auto simp: exec1_def)
kleing@43438
    83
kleing@43438
    84
lemma exec_n_end:
kleing@51259
    85
  "size P <= (n::int) \<Longrightarrow> 
kleing@43438
    86
  P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
kleing@43438
    87
  by (cases k) (auto simp: exec1_end)
kleing@43438
    88
kleing@43438
    89
lemmas exec_n_simps = exec_n_step exec_n_end
kleing@43438
    90
kleing@43438
    91
kleing@43438
    92
subsection {* Basic properties of @{term succs} *}
kleing@43438
    93
kleing@43438
    94
lemma succs_simps [simp]: 
kleing@43438
    95
  "succs [ADD] n = {n + 1}"
kleing@43438
    96
  "succs [LOADI v] n = {n + 1}"
kleing@43438
    97
  "succs [LOAD x] n = {n + 1}"
kleing@43438
    98
  "succs [STORE x] n = {n + 1}"
kleing@43438
    99
  "succs [JMP i] n = {n + 1 + i}"
kleing@45322
   100
  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
kleing@45322
   101
  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
kleing@43438
   102
  by (auto simp: succs_def isuccs_def)
kleing@43438
   103
kleing@43438
   104
lemma succs_empty [iff]: "succs [] n = {}"
kleing@43438
   105
  by (simp add: succs_def)
kleing@43438
   106
kleing@43438
   107
lemma succs_Cons:
kleing@43438
   108
  "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
kleing@43438
   109
proof 
kleing@51259
   110
  let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)"
kleing@43438
   111
  { fix p assume "p \<in> succs (x#xs) n"
kleing@51259
   112
    then obtain i::int where isuccs: "?isuccs p (x#xs) n i"
kleing@43438
   113
      unfolding succs_def by auto     
kleing@43438
   114
    have "p \<in> ?x \<union> ?xs" 
kleing@43438
   115
    proof cases
kleing@43438
   116
      assume "i = 0" with isuccs show ?thesis by simp
kleing@43438
   117
    next
kleing@43438
   118
      assume "i \<noteq> 0" 
kleing@43438
   119
      with isuccs 
kleing@43438
   120
      have "?isuccs p xs (1+n) (i - 1)" by auto
kleing@43438
   121
      hence "p \<in> ?xs" unfolding succs_def by blast
kleing@43438
   122
      thus ?thesis .. 
kleing@43438
   123
    qed
kleing@43438
   124
  } 
kleing@43438
   125
  thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..
kleing@43438
   126
  
kleing@43438
   127
  { fix p assume "p \<in> ?x \<or> p \<in> ?xs"
kleing@43438
   128
    hence "p \<in> succs (x#xs) n"
kleing@43438
   129
    proof
nipkow@44890
   130
      assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def)
kleing@43438
   131
    next
kleing@43438
   132
      assume "p \<in> ?xs"
kleing@43438
   133
      then obtain i where "?isuccs p xs (1+n) i"
kleing@43438
   134
        unfolding succs_def by auto
kleing@43438
   135
      hence "?isuccs p (x#xs) n (1+i)"
kleing@43438
   136
        by (simp add: algebra_simps)
kleing@43438
   137
      thus ?thesis unfolding succs_def by blast
kleing@43438
   138
    qed
kleing@43438
   139
  }  
kleing@43438
   140
  thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast
kleing@43438
   141
qed
kleing@43438
   142
kleing@43438
   143
lemma succs_iexec1:
kleing@51259
   144
  assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P"
kleing@44004
   145
  shows "fst c' \<in> succs P 0"
nipkow@50060
   146
  using assms by (auto simp: succs_def isuccs_def split: instr.split)
kleing@43438
   147
kleing@43438
   148
lemma succs_shift:
kleing@43438
   149
  "(p - n \<in> succs P 0) = (p \<in> succs P n)" 
nipkow@44890
   150
  by (fastforce simp: succs_def isuccs_def split: instr.split)
kleing@43438
   151
  
kleing@43438
   152
lemma inj_op_plus [simp]:
kleing@43438
   153
  "inj (op + (i::int))"
kleing@43438
   154
  by (metis add_minus_cancel inj_on_inverseI)
kleing@43438
   155
kleing@43438
   156
lemma succs_set_shift [simp]:
kleing@43438
   157
  "op + i ` succs xs 0 = succs xs i"
kleing@43438
   158
  by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)
kleing@43438
   159
kleing@43438
   160
lemma succs_append [simp]:
kleing@51259
   161
  "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)"
kleing@43438
   162
  by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)
kleing@43438
   163
kleing@43438
   164
kleing@43438
   165
lemma exits_append [simp]:
kleing@51259
   166
  "exits (xs @ ys) = exits xs \<union> (op + (size xs)) ` exits ys - 
kleing@51259
   167
                     {0..<size xs + size ys}" 
kleing@43438
   168
  by (auto simp: exits_def image_set_diff)
kleing@43438
   169
  
kleing@43438
   170
lemma exits_single:
kleing@43438
   171
  "exits [x] = isuccs x 0 - {0}"
kleing@43438
   172
  by (auto simp: exits_def succs_def)
kleing@43438
   173
  
kleing@43438
   174
lemma exits_Cons:
kleing@43438
   175
  "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs - 
kleing@51259
   176
                     {0..<1 + size xs}" 
kleing@43438
   177
  using exits_append [of "[x]" xs]
kleing@43438
   178
  by (simp add: exits_single)
kleing@43438
   179
kleing@43438
   180
lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)
kleing@43438
   181
kleing@43438
   182
lemma exits_simps [simp]:
kleing@43438
   183
  "exits [ADD] = {1}"
kleing@43438
   184
  "exits [LOADI v] = {1}"
kleing@43438
   185
  "exits [LOAD x] = {1}"
kleing@43438
   186
  "exits [STORE x] = {1}"
kleing@43438
   187
  "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
kleing@45322
   188
  "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}"
kleing@45322
   189
  "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}"
kleing@43438
   190
  by (auto simp: exits_def)
kleing@43438
   191
kleing@43438
   192
lemma acomp_succs [simp]:
kleing@51259
   193
  "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
kleing@43438
   194
  by (induct a arbitrary: n) auto
kleing@43438
   195
kleing@43438
   196
lemma acomp_size:
kleing@51259
   197
  "(1::int) \<le> size (acomp a)"
kleing@43438
   198
  by (induct a) auto
kleing@43438
   199
kleing@44010
   200
lemma acomp_exits [simp]:
kleing@51259
   201
  "exits (acomp a) = {size (acomp a)}"
kleing@43438
   202
  by (auto simp: exits_def acomp_size)
kleing@43438
   203
kleing@43438
   204
lemma bcomp_succs:
kleing@43438
   205
  "0 \<le> i \<Longrightarrow>
nipkow@53880
   206
  succs (bcomp b f i) n \<subseteq> {n .. n + size (bcomp b f i)}
nipkow@53880
   207
                           \<union> {n + i + size (bcomp b f i)}" 
nipkow@53880
   208
proof (induction b arbitrary: f i n)
kleing@43438
   209
  case (And b1 b2)
kleing@43438
   210
  from And.prems
kleing@43438
   211
  show ?case 
nipkow@53880
   212
    by (cases f)
nipkow@45015
   213
       (auto dest: And.IH(1) [THEN subsetD, rotated] 
nipkow@45015
   214
                   And.IH(2) [THEN subsetD, rotated])
kleing@43438
   215
qed auto
kleing@43438
   216
kleing@43438
   217
lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
kleing@43438
   218
kleing@43438
   219
lemma bcomp_exits:
kleing@51259
   220
  fixes i :: int
kleing@51259
   221
  shows
kleing@43438
   222
  "0 \<le> i \<Longrightarrow>
nipkow@53880
   223
  exits (bcomp b f i) \<subseteq> {size (bcomp b f i), i + size (bcomp b f i)}" 
kleing@43438
   224
  by (auto simp: exits_def)
kleing@43438
   225
  
kleing@43438
   226
lemma bcomp_exitsD [dest!]:
nipkow@53880
   227
  "p \<in> exits (bcomp b f i) \<Longrightarrow> 0 \<le> i \<Longrightarrow> 
nipkow@53880
   228
  p = size (bcomp b f i) \<or> p = i + size (bcomp b f i)"
kleing@43438
   229
  using bcomp_exits by auto
kleing@43438
   230
kleing@43438
   231
lemma ccomp_succs:
kleing@51259
   232
  "succs (ccomp c) n \<subseteq> {n..n + size (ccomp c)}"
nipkow@45015
   233
proof (induction c arbitrary: n)
kleing@43438
   234
  case SKIP thus ?case by simp
kleing@43438
   235
next
kleing@43438
   236
  case Assign thus ?case by simp
kleing@43438
   237
next
nipkow@47818
   238
  case (Seq c1 c2)
nipkow@47818
   239
  from Seq.prems
kleing@43438
   240
  show ?case 
nipkow@47818
   241
    by (fastforce dest: Seq.IH [THEN subsetD])
kleing@43438
   242
next
kleing@43438
   243
  case (If b c1 c2)
kleing@43438
   244
  from If.prems
kleing@43438
   245
  show ?case
nipkow@45015
   246
    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
kleing@43438
   247
next
kleing@43438
   248
  case (While b c)
kleing@43438
   249
  from While.prems
nipkow@45015
   250
  show ?case by (auto dest!: While.IH [THEN subsetD])
kleing@43438
   251
qed
kleing@43438
   252
kleing@43438
   253
lemma ccomp_exits:
kleing@51259
   254
  "exits (ccomp c) \<subseteq> {size (ccomp c)}"
kleing@43438
   255
  using ccomp_succs [of c 0] by (auto simp: exits_def)
kleing@43438
   256
kleing@43438
   257
lemma ccomp_exitsD [dest!]:
kleing@51259
   258
  "p \<in> exits (ccomp c) \<Longrightarrow> p = size (ccomp c)"
kleing@43438
   259
  using ccomp_exits by auto
kleing@43438
   260
kleing@43438
   261
kleing@43438
   262
subsection {* Splitting up machine executions *}
kleing@43438
   263
kleing@43438
   264
lemma exec1_split:
kleing@51259
   265
  fixes i j :: int
kleing@51259
   266
  shows
kleing@51259
   267
  "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow> 
kleing@51259
   268
  c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
kleing@52915
   269
  by (auto split: instr.splits simp: exec1_def)
kleing@43438
   270
kleing@43438
   271
lemma exec_n_split:
kleing@51259
   272
  fixes i j :: int
kleing@51259
   273
  assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')"
kleing@51259
   274
          "0 \<le> i" "i < size c" 
kleing@51259
   275
          "j \<notin> {size P ..< size P + size c}"
kleing@51259
   276
  shows "\<exists>s'' (i'::int) k m. 
kleing@43438
   277
                   c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
kleing@43438
   278
                   i' \<in> exits c \<and> 
kleing@51259
   279
                   P @ c @ P' \<turnstile> (size P + i', s'') \<rightarrow>^m (j, s') \<and>
kleing@43438
   280
                   n = k + m" 
nipkow@45015
   281
using assms proof (induction n arbitrary: i j s)
kleing@43438
   282
  case 0
kleing@43438
   283
  thus ?case by simp
kleing@43438
   284
next
kleing@43438
   285
  case (Suc n)
kleing@51259
   286
  have i: "0 \<le> i" "i < size c" by fact+
kleing@43438
   287
  from Suc.prems
kleing@51259
   288
  have j: "\<not> (size P \<le> j \<and> j < size P + size c)" by simp
kleing@43438
   289
  from Suc.prems 
kleing@43438
   290
  obtain i0 s0 where
kleing@51259
   291
    step: "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (i0,s0)" and
kleing@43438
   292
    rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')"
kleing@43438
   293
    by clarsimp
kleing@43438
   294
kleing@43438
   295
  from step i
kleing@51259
   296
  have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - size P, s0)" by (rule exec1_split)
kleing@43438
   297
kleing@51259
   298
  have "i0 = size P + (i0 - size P) " by simp
kleing@51259
   299
  then obtain j0::int where j0: "i0 = size P + j0"  ..
kleing@43438
   300
kleing@43438
   301
  note split_paired_Ex [simp del]
kleing@43438
   302
kleing@51259
   303
  { assume "j0 \<in> {0 ..< size c}"
kleing@43438
   304
    with j0 j rest c
kleing@43438
   305
    have ?case
nipkow@45015
   306
      by (fastforce dest!: Suc.IH intro!: exec_Suc)
kleing@43438
   307
  } moreover {
kleing@51259
   308
    assume "j0 \<notin> {0 ..< size c}"
kleing@43438
   309
    moreover
kleing@43438
   310
    from c j0 have "j0 \<in> succs c 0"
kleing@52915
   311
      by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
kleing@43438
   312
    ultimately
kleing@43438
   313
    have "j0 \<in> exits c" by (simp add: exits_def)
kleing@43438
   314
    with c j0 rest
nipkow@44890
   315
    have ?case by fastforce
kleing@43438
   316
  }
kleing@43438
   317
  ultimately
kleing@43438
   318
  show ?case by cases
kleing@43438
   319
qed
kleing@43438
   320
kleing@43438
   321
lemma exec_n_drop_right:
kleing@51259
   322
  fixes j :: int
kleing@51259
   323
  assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<size c}"
kleing@44004
   324
  shows "\<exists>s'' i' k m. 
kleing@44004
   325
          (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
kleing@44004
   326
           else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
kleing@44004
   327
           i' \<in> exits c) \<and> 
kleing@44004
   328
           c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
kleing@44004
   329
           n = k + m"
kleing@44004
   330
  using assms
kleing@43438
   331
  by (cases "c = []")
kleing@43438
   332
     (auto dest: exec_n_split [where P="[]", simplified])
kleing@43438
   333
  
kleing@43438
   334
kleing@43438
   335
text {*
kleing@43438
   336
  Dropping the left context of a potentially incomplete execution of @{term c}.
kleing@43438
   337
*}
kleing@43438
   338
kleing@43438
   339
lemma exec1_drop_left:
kleing@51259
   340
  fixes i n :: int
kleing@51259
   341
  assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "size P1 \<le> i"
kleing@51259
   342
  shows "P2 \<turnstile> (i - size P1, s, stk) \<rightarrow> (n - size P1, s', stk')"
kleing@43438
   343
proof -
kleing@51259
   344
  have "i = size P1 + (i - size P1)" by simp 
kleing@51259
   345
  then obtain i' :: int where "i = size P1 + i'" ..
kleing@43438
   346
  moreover
kleing@51259
   347
  have "n = size P1 + (n - size P1)" by simp 
kleing@51259
   348
  then obtain n' :: int where "n = size P1 + n'" ..
kleing@43438
   349
  ultimately 
kleing@52915
   350
  show ?thesis using assms 
kleing@52915
   351
    by (clarsimp simp: exec1_def simp del: iexec.simps)
kleing@43438
   352
qed
kleing@43438
   353
kleing@43438
   354
lemma exec_n_drop_left:
kleing@51259
   355
  fixes i n :: int
kleing@44004
   356
  assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
kleing@51259
   357
          "size P \<le> i" "exits P' \<subseteq> {0..}"
kleing@51259
   358
  shows "P' \<turnstile> (i - size P, s, stk) \<rightarrow>^k (n - size P, s', stk')"
nipkow@45015
   359
using assms proof (induction k arbitrary: i s stk)
kleing@43438
   360
  case 0 thus ?case by simp
kleing@43438
   361
next
kleing@43438
   362
  case (Suc k)
kleing@43438
   363
  from Suc.prems
kleing@43438
   364
  obtain i' s'' stk'' where
kleing@43438
   365
    step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and
kleing@43438
   366
    rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
kleing@53356
   367
    by auto
kleing@51259
   368
  from step `size P \<le> i`
kleing@51259
   369
  have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
kleing@43438
   370
    by (rule exec1_drop_left)
kleing@45218
   371
  moreover
kleing@51259
   372
  then have "i' - size P \<in> succs P' 0"
kleing@52915
   373
    by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
kleing@43438
   374
  with `exits P' \<subseteq> {0..}`
kleing@51259
   375
  have "size P \<le> i'" by (auto simp: exits_def)
kleing@43438
   376
  from rest this `exits P' \<subseteq> {0..}`     
kleing@51259
   377
  have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
nipkow@45015
   378
    by (rule Suc.IH)
kleing@45218
   379
  ultimately
kleing@45218
   380
  show ?case by auto
kleing@43438
   381
qed
kleing@43438
   382
kleing@43438
   383
lemmas exec_n_drop_Cons = 
wenzelm@45605
   384
  exec_n_drop_left [where P="[instr]", simplified] for instr
kleing@43438
   385
kleing@43438
   386
definition
kleing@51259
   387
  "closed P \<longleftrightarrow> exits P \<subseteq> {size P}" 
kleing@43438
   388
kleing@43438
   389
lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
kleing@43438
   390
  using ccomp_exits by (auto simp: closed_def)
kleing@43438
   391
kleing@43438
   392
lemma acomp_closed [simp, intro!]: "closed (acomp c)"
kleing@43438
   393
  by (simp add: closed_def)
kleing@43438
   394
kleing@43438
   395
lemma exec_n_split_full:
kleing@51259
   396
  fixes j :: int
kleing@43438
   397
  assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')"
kleing@51259
   398
  assumes P: "size P \<le> j" 
kleing@43438
   399
  assumes closed: "closed P"
kleing@43438
   400
  assumes exits: "exits P' \<subseteq> {0..}"
kleing@51259
   401
  shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'') \<and> 
kleing@51259
   402
                           P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - size P, s', stk')"
kleing@43438
   403
proof (cases "P")
kleing@43438
   404
  case Nil with exec
nipkow@44890
   405
  show ?thesis by fastforce
kleing@43438
   406
next
kleing@43438
   407
  case Cons
kleing@51259
   408
  hence "0 < size P" by simp
kleing@43438
   409
  with exec P closed
kleing@43438
   410
  obtain k1 k2 s'' stk'' where
kleing@51259
   411
    1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'')" and
kleing@51259
   412
    2: "P @ P' \<turnstile> (size P,s'',stk'') \<rightarrow>^k2 (j, s', stk')"
kleing@43438
   413
    by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] 
kleing@43438
   414
             simp: closed_def)
kleing@43438
   415
  moreover
kleing@51259
   416
  have "j = size P + (j - size P)" by simp
kleing@51259
   417
  then obtain j0 :: int where "j = size P + j0" ..
kleing@43438
   418
  ultimately
kleing@43438
   419
  show ?thesis using exits
nipkow@44890
   420
    by (fastforce dest: exec_n_drop_left)
kleing@43438
   421
qed
kleing@43438
   422
kleing@43438
   423
kleing@43438
   424
subsection {* Correctness theorem *}
kleing@43438
   425
kleing@43438
   426
lemma acomp_neq_Nil [simp]:
kleing@43438
   427
  "acomp a \<noteq> []"
kleing@43438
   428
  by (induct a) auto
kleing@43438
   429
kleing@43438
   430
lemma acomp_exec_n [dest!]:
kleing@51259
   431
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a),s',stk') \<Longrightarrow> 
kleing@43438
   432
  s' = s \<and> stk' = aval a s#stk"
nipkow@45015
   433
proof (induction a arbitrary: n s' stk stk')
kleing@43438
   434
  case (Plus a1 a2)
kleing@51259
   435
  let ?sz = "size (acomp a1) + (size (acomp a2) + 1)"
kleing@43438
   436
  from Plus.prems
kleing@43438
   437
  have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')" 
kleing@43438
   438
    by (simp add: algebra_simps)
kleing@43438
   439
      
kleing@43438
   440
  then obtain n1 s1 stk1 n2 s2 stk2 n3 where 
kleing@51259
   441
    "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)"
kleing@51259
   442
    "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)" 
kleing@43438
   443
       "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
kleing@43438
   444
    by (auto dest!: exec_n_split_full)
kleing@43438
   445
kleing@52915
   446
  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def)
kleing@52915
   447
qed (auto simp: exec_n_simps exec1_def)
kleing@43438
   448
kleing@43438
   449
lemma bcomp_split:
kleing@51259
   450
  fixes i j :: int
nipkow@53880
   451
  assumes "bcomp b f i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" 
nipkow@53880
   452
          "j \<notin> {0..<size (bcomp b f i)}" "0 \<le> i"
kleing@51259
   453
  shows "\<exists>s'' stk'' (i'::int) k m. 
nipkow@53880
   454
           bcomp b f i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
nipkow@53880
   455
           (i' = size (bcomp b f i) \<or> i' = i + size (bcomp b f i)) \<and>
nipkow@53880
   456
           bcomp b f i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
kleing@43438
   457
           n = k + m"
nipkow@53880
   458
  using assms by (cases "bcomp b f i = []") (fastforce dest!: exec_n_drop_right)+
kleing@43438
   459
kleing@43438
   460
lemma bcomp_exec_n [dest]:
kleing@51259
   461
  fixes i j :: int
nipkow@53880
   462
  assumes "bcomp b f j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
nipkow@53880
   463
          "size (bcomp b f j) \<le> i" "0 \<le> j"
nipkow@53880
   464
  shows "i = size(bcomp b f j) + (if f = bval b s then j else 0) \<and>
kleing@44004
   465
         s' = s \<and> stk' = stk"
nipkow@53880
   466
using assms proof (induction b arbitrary: f j i n s' stk')
nipkow@45200
   467
  case Bc thus ?case 
nipkow@62390
   468
    by (simp split: if_split_asm add: exec_n_simps exec1_def)
kleing@43438
   469
next
kleing@43438
   470
  case (Not b) 
kleing@43438
   471
  from Not.prems show ?case
nipkow@45015
   472
    by (fastforce dest!: Not.IH) 
kleing@43438
   473
next
kleing@43438
   474
  case (And b1 b2)
kleing@43438
   475
  
nipkow@53880
   476
  let ?b2 = "bcomp b2 f j" 
nipkow@53880
   477
  let ?m  = "if f then size ?b2 else size ?b2 + j"
kleing@43438
   478
  let ?b1 = "bcomp b1 False ?m" 
kleing@43438
   479
nipkow@53880
   480
  have j: "size (bcomp (And b1 b2) f j) \<le> i" "0 \<le> j" by fact+
kleing@43438
   481
  
kleing@43438
   482
  from And.prems
kleing@51259
   483
  obtain s'' stk'' and i'::int and k m where 
kleing@43438
   484
    b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')"
kleing@51259
   485
        "i' = size ?b1 \<or> i' = ?m + size ?b1" and
kleing@51259
   486
    b2: "?b2 \<turnstile> (i' - size ?b1, s'', stk'') \<rightarrow>^m (i - size ?b1, s', stk')"
kleing@43438
   487
    by (auto dest!: bcomp_split dest: exec_n_drop_left)
kleing@43438
   488
  from b1 j
kleing@51259
   489
  have "i' = size ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
nipkow@45015
   490
    by (auto dest!: And.IH)
kleing@43438
   491
  with b2 j
kleing@43438
   492
  show ?case 
nipkow@62390
   493
    by (fastforce dest!: And.IH simp: exec_n_end split: if_split_asm)
kleing@43438
   494
next
kleing@43438
   495
  case Less
kleing@52915
   496
  thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *) 
kleing@43438
   497
qed
kleing@43438
   498
kleing@43438
   499
lemma ccomp_empty [elim!]:
kleing@43438
   500
  "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
kleing@43438
   501
  by (induct c) auto
kleing@43438
   502
kleing@44070
   503
declare assign_simp [simp]
kleing@43438
   504
kleing@43438
   505
lemma ccomp_exec_n:
kleing@51259
   506
  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (size(ccomp c),t,stk')
kleing@43438
   507
  \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
nipkow@45015
   508
proof (induction c arbitrary: s t stk stk' n)
kleing@43438
   509
  case SKIP
kleing@43438
   510
  thus ?case by auto
kleing@43438
   511
next
kleing@43438
   512
  case (Assign x a)
kleing@43438
   513
  thus ?case
kleing@52915
   514
    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps exec1_def)
kleing@43438
   515
next
nipkow@47818
   516
  case (Seq c1 c2)
nipkow@44890
   517
  thus ?case by (fastforce dest!: exec_n_split_full)
kleing@43438
   518
next
kleing@43438
   519
  case (If b c1 c2)
nipkow@45015
   520
  note If.IH [dest!]
kleing@43438
   521
kleing@43438
   522
  let ?if = "IF b THEN c1 ELSE c2"
kleing@43438
   523
  let ?cs = "ccomp ?if"
kleing@51259
   524
  let ?bcomp = "bcomp b False (size (ccomp c1) + 1)"
kleing@43438
   525
  
kleing@51259
   526
  from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (size ?cs,t,stk')`
kleing@51259
   527
  obtain i' :: int and k m s'' stk'' where
kleing@51259
   528
    cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (size ?cs,t,stk')" and
kleing@43438
   529
        "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')" 
kleing@51259
   530
        "i' = size ?bcomp \<or> i' = size ?bcomp + size (ccomp c1) + 1"
kleing@43438
   531
    by (auto dest!: bcomp_split)
kleing@43438
   532
kleing@43438
   533
  hence i':
kleing@43438
   534
    "s''=s" "stk'' = stk" 
kleing@51259
   535
    "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)"
kleing@43438
   536
    by auto
kleing@43438
   537
  
kleing@43438
   538
  with cs have cs':
kleing@51259
   539
    "ccomp c1@JMP (size (ccomp c2))#ccomp c2 \<turnstile> 
kleing@51259
   540
       (if bval b s then 0 else size (ccomp c1)+1, s, stk) \<rightarrow>^m
kleing@51259
   541
       (1 + size (ccomp c1) + size (ccomp c2), t, stk')"
nipkow@44890
   542
    by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
kleing@43438
   543
     
kleing@43438
   544
  show ?case
kleing@43438
   545
  proof (cases "bval b s")
kleing@43438
   546
    case True with cs'
kleing@43438
   547
    show ?thesis
kleing@43438
   548
      by simp
nipkow@44890
   549
         (fastforce dest: exec_n_drop_right 
nipkow@62390
   550
                   split: if_split_asm
kleing@52915
   551
                   simp: exec_n_simps exec1_def)
kleing@43438
   552
  next
kleing@43438
   553
    case False with cs'
kleing@43438
   554
    show ?thesis
kleing@43438
   555
      by (auto dest!: exec_n_drop_Cons exec_n_drop_left 
kleing@43438
   556
               simp: exits_Cons isuccs_def)
kleing@43438
   557
  qed
kleing@43438
   558
next
kleing@43438
   559
  case (While b c)
kleing@43438
   560
kleing@43438
   561
  from While.prems
kleing@43438
   562
  show ?case
nipkow@45015
   563
  proof (induction n arbitrary: s rule: nat_less_induct)
kleing@43438
   564
    case (1 n)
kleing@43438
   565
    
kleing@43438
   566
    { assume "\<not> bval b s"
kleing@43438
   567
      with "1.prems"
kleing@43438
   568
      have ?case
kleing@43438
   569
        by simp
nipkow@53880
   570
           (fastforce dest!: bcomp_exec_n bcomp_split simp: exec_n_simps)
kleing@43438
   571
    } moreover {
kleing@43438
   572
      assume b: "bval b s"
kleing@43438
   573
      let ?c0 = "WHILE b DO c"
kleing@43438
   574
      let ?cs = "ccomp ?c0"
kleing@51259
   575
      let ?bs = "bcomp b False (size (ccomp c) + 1)"
kleing@51259
   576
      let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]"
kleing@43438
   577
      
kleing@43438
   578
      from "1.prems" b
kleing@43438
   579
      obtain k where
kleing@51259
   580
        cs: "?cs \<turnstile> (size ?bs, s, stk) \<rightarrow>^k (size ?cs, t, stk')" and
kleing@43438
   581
        k:  "k \<le> n"
nipkow@44890
   582
        by (fastforce dest!: bcomp_split)
kleing@43438
   583
      
kleing@43438
   584
      have ?case
kleing@43438
   585
      proof cases
kleing@43438
   586
        assume "ccomp c = []"
kleing@43438
   587
        with cs k
kleing@43438
   588
        obtain m where
kleing@51259
   589
          "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')"
kleing@43438
   590
          "m < n"
kleing@52915
   591
          by (auto simp: exec_n_step [where k=k] exec1_def)
nipkow@45015
   592
        with "1.IH"
kleing@43438
   593
        show ?case by blast
kleing@43438
   594
      next
kleing@43438
   595
        assume "ccomp c \<noteq> []"
kleing@43438
   596
        with cs
kleing@43438
   597
        obtain m m' s'' stk'' where
kleing@51259
   598
          c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (size (ccomp c), s'', stk'')" and 
kleing@51259
   599
          rest: "?cs \<turnstile> (size ?bs + size (ccomp c), s'', stk'') \<rightarrow>^m 
kleing@51259
   600
                       (size ?cs, t, stk')" and
kleing@43438
   601
          m: "k = m + m'"
kleing@43438
   602
          by (auto dest: exec_n_split [where i=0, simplified])
kleing@43438
   603
        from c
kleing@43438
   604
        have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
nipkow@45015
   605
          by (auto dest!: While.IH)
kleing@43438
   606
        moreover
kleing@43438
   607
        from rest m k stk
kleing@43438
   608
        obtain k' where
kleing@51259
   609
          "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')"
kleing@43438
   610
          "k' < n"
kleing@52915
   611
          by (auto simp: exec_n_step [where k=m] exec1_def)
nipkow@45015
   612
        with "1.IH"
kleing@43438
   613
        have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
kleing@43438
   614
        ultimately
kleing@43438
   615
        show ?case using b by blast
kleing@43438
   616
      qed
kleing@43438
   617
    }
kleing@43438
   618
    ultimately show ?case by cases
kleing@43438
   619
  qed
kleing@43438
   620
qed
kleing@43438
   621
kleing@43438
   622
theorem ccomp_exec:
kleing@51259
   623
  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t"
kleing@43438
   624
  by (auto dest: exec_exec_n ccomp_exec_n)
kleing@43438
   625
kleing@43438
   626
corollary ccomp_sound:
kleing@51259
   627
  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)  \<longleftrightarrow>  (c,s) \<Rightarrow> t"
kleing@43438
   628
  by (blast intro!: ccomp_exec ccomp_bigstep)
kleing@43438
   629
kleing@43438
   630
end