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