src/HOL/IMP/Machines.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 18372 2bffdf62fe7f
permissions -rw-r--r--
Constant "If" is now local
haftmann@16417
     1
theory Machines imports Natural begin
nipkow@13095
     2
nipkow@13095
     3
lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
nipkow@13095
     4
by(fast intro:rtrancl.intros elim:rtranclE)
nipkow@13095
     5
nipkow@13095
     6
lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
nipkow@13095
     7
by(subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
nipkow@13095
     8
nipkow@13095
     9
lemmas converse_rel_powE = rel_pow_E2
nipkow@13095
    10
nipkow@13095
    11
lemma R_O_Rn_commute: "R O R^n = R^n O R"
nipkow@13095
    12
by(induct_tac n, simp, simp add: O_assoc[symmetric])
nipkow@13095
    13
nipkow@13095
    14
lemma converse_in_rel_pow_eq:
nipkow@13095
    15
"((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
nipkow@13095
    16
apply(rule iffI)
nipkow@13095
    17
 apply(blast elim:converse_rel_powE)
nipkow@13095
    18
apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
nipkow@13095
    19
done
nipkow@13095
    20
nipkow@13095
    21
lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
nipkow@13095
    22
by(induct n, simp, simp add:O_assoc)
nipkow@13095
    23
nipkow@13095
    24
lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
nipkow@13095
    25
by(simp add:rel_pow_plus rel_compI)
nipkow@13095
    26
nipkow@13095
    27
subsection "Instructions"
nipkow@13095
    28
nipkow@13095
    29
text {* There are only three instructions: *}
nipkow@13675
    30
datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat
nipkow@13095
    31
nipkow@13095
    32
types instrs = "instr list"
nipkow@13095
    33
nipkow@13095
    34
subsection "M0 with PC"
nipkow@13095
    35
nipkow@13675
    36
consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set" 
nipkow@13095
    37
syntax
nipkow@13095
    38
  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
nipkow@13095
    39
               ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
nipkow@13095
    40
  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
nipkow@13095
    41
               ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50)
nipkow@13095
    42
  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
nipkow@13095
    43
               ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50)
nipkow@13095
    44
nipkow@13095
    45
syntax (xsymbols)
nipkow@13095
    46
  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
nipkow@13095
    47
               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
nipkow@13095
    48
  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
nipkow@13095
    49
               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
nipkow@13095
    50
  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
nipkow@13095
    51
               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
nipkow@13095
    52
kleing@14565
    53
syntax (HTML output)
kleing@14565
    54
  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
kleing@14565
    55
               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
kleing@14565
    56
  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
kleing@14565
    57
               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
kleing@14565
    58
  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
kleing@14565
    59
               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
kleing@14565
    60
nipkow@13095
    61
translations  
nipkow@13095
    62
  "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
nipkow@13095
    63
  "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
nipkow@13095
    64
  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n"
nipkow@13095
    65
nipkow@13095
    66
inductive "exec01 P"
nipkow@13095
    67
intros
nipkow@13675
    68
SET: "\<lbrakk> n<size P; P!n = SET x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>"
nipkow@13095
    69
JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>"
nipkow@13095
    70
JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
nipkow@13095
    71
        \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
nipkow@13095
    72
JMPB:  "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>"
nipkow@13095
    73
nipkow@13095
    74
subsection "M0 with lists"
nipkow@13095
    75
nipkow@13095
    76
text {* We describe execution of programs in the machine by
nipkow@13095
    77
  an operational (small step) semantics:
nipkow@13095
    78
*}
nipkow@13095
    79
nipkow@13095
    80
types config = "instrs \<times> instrs \<times> state"
nipkow@13095
    81
nipkow@13095
    82
consts  stepa1 :: "(config \<times> config)set"
nipkow@13095
    83
nipkow@13095
    84
syntax
nipkow@13095
    85
  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
nipkow@13095
    86
               ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50)
nipkow@13095
    87
  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
nipkow@13095
    88
               ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50)
nipkow@13095
    89
  "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] \<Rightarrow> bool"
nipkow@13095
    90
               ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50)
nipkow@13095
    91
nipkow@13095
    92
syntax (xsymbols)
nipkow@13095
    93
  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
nipkow@13095
    94
               ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
nipkow@13095
    95
  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
nipkow@13095
    96
               ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
nipkow@13095
    97
  "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
nipkow@13095
    98
               ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
nipkow@13095
    99
nipkow@13095
   100
translations  
nipkow@13095
   101
  "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1"
nipkow@13095
   102
  "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)"
nipkow@13095
   103
  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)"
nipkow@13095
   104
nipkow@13095
   105
nipkow@13095
   106
inductive "stepa1"
nipkow@13095
   107
intros
nipkow@13675
   108
  "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>"
nipkow@13095
   109
  "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
nipkow@13095
   110
  "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
nipkow@13095
   111
   \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>"
nipkow@13095
   112
  "i \<le> size q
nipkow@13095
   113
   \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>"
nipkow@13095
   114
nipkow@13095
   115
inductive_cases execE: "((i#is,p,s),next) : stepa1"
nipkow@13095
   116
nipkow@13095
   117
lemma exec_simp[simp]:
nipkow@13095
   118
 "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of
nipkow@13675
   119
 SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q |
nipkow@13095
   120
 JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q
nipkow@13095
   121
            else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) |
nipkow@13095
   122
 JMPB n \<Rightarrow> n \<le> size q \<and> t=s \<and> p' = rev(take n q) @ i # p \<and> q' = drop n q)"
nipkow@13095
   123
apply(rule iffI)
nipkow@13095
   124
defer
nipkow@13095
   125
apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
nipkow@13095
   126
apply(erule execE)
nipkow@13095
   127
apply(simp_all)
nipkow@13095
   128
done
nipkow@13095
   129
nipkow@13095
   130
lemma execn_simp[simp]:
nipkow@13095
   131
"(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) =
nipkow@13095
   132
 (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or>
nipkow@13095
   133
  ((\<exists>m p' q' t. n = Suc m \<and>
nipkow@13095
   134
                \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -m\<rightarrow> \<langle>p'',q'',u\<rangle>)))"
nipkow@13095
   135
by(subst converse_in_rel_pow_eq, simp)
nipkow@13095
   136
nipkow@13095
   137
nipkow@13095
   138
lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) =
nipkow@13095
   139
 (p'' = i#p & q''=q & u=s |
nipkow@13095
   140
 (\<exists>p' q' t. \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>))"
nipkow@13095
   141
apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
nipkow@13095
   142
apply(blast)
nipkow@13095
   143
done
nipkow@13095
   144
nipkow@13095
   145
declare nth_append[simp]
nipkow@13095
   146
nipkow@13095
   147
lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys"
nipkow@13095
   148
by simp
nipkow@13095
   149
nipkow@13095
   150
lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
nipkow@13095
   151
apply(rule iffI)
nipkow@13095
   152
 apply(rule rev_revD, simp)
nipkow@13095
   153
apply fastsimp
nipkow@13095
   154
done
nipkow@13095
   155
nipkow@13095
   156
lemma direction1:
nipkow@13095
   157
 "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
nipkow@13095
   158
  rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
nipkow@13095
   159
apply(erule stepa1.induct)
nipkow@13675
   160
   apply(simp add:exec01.SET)
nipkow@13095
   161
  apply(fastsimp intro:exec01.JMPFT)
nipkow@13095
   162
 apply simp
nipkow@13095
   163
 apply(rule exec01.JMPFF)
nipkow@13095
   164
     apply simp
nipkow@13095
   165
    apply fastsimp
nipkow@13095
   166
   apply simp
nipkow@13095
   167
  apply simp
nipkow@13095
   168
  apply arith
nipkow@13095
   169
 apply simp
nipkow@13095
   170
 apply arith
nipkow@13095
   171
apply(fastsimp simp add:exec01.JMPB)
nipkow@13095
   172
done
nipkow@13098
   173
(*
nipkow@13098
   174
lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
nipkow@13095
   175
apply(induct xs)
nipkow@13095
   176
 apply simp_all
nipkow@13095
   177
apply(case_tac i)
nipkow@13095
   178
apply simp_all
nipkow@13095
   179
done
nipkow@13095
   180
nipkow@13098
   181
lemma rev_drop: "\<And>i. rev (drop i xs) = take (length xs - i) (rev xs)"
nipkow@13098
   182
apply(induct xs)
nipkow@13098
   183
 apply simp_all
nipkow@13098
   184
apply(case_tac i)
nipkow@13098
   185
apply simp_all
nipkow@13098
   186
done
nipkow@13098
   187
*)
nipkow@13095
   188
lemma direction2:
nipkow@13095
   189
 "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
nipkow@13095
   190
 \<forall>p q p' q'. rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
nipkow@13095
   191
          rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
nipkow@13095
   192
apply(erule exec01.induct)
nipkow@13098
   193
   apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
nipkow@13095
   194
   apply(drule sym)
nipkow@13095
   195
   apply simp
nipkow@13095
   196
   apply(rule rev_revD)
nipkow@13095
   197
   apply simp
nipkow@13098
   198
  apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
nipkow@13095
   199
  apply(drule sym)
nipkow@13095
   200
  apply simp
nipkow@13095
   201
  apply(rule rev_revD)
nipkow@13095
   202
  apply simp
berghofe@13612
   203
 apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+
nipkow@13095
   204
 apply(drule sym)
nipkow@13095
   205
 apply simp
nipkow@13095
   206
 apply(rule rev_revD)
nipkow@13095
   207
 apply simp
nipkow@13098
   208
apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
nipkow@13095
   209
apply(drule sym)
nipkow@13098
   210
apply(simp add:rev_take)
nipkow@13095
   211
apply(rule rev_revD)
nipkow@13098
   212
apply(simp add:rev_drop)
nipkow@13095
   213
done
nipkow@13095
   214
nipkow@13095
   215
nipkow@13095
   216
theorem M_eqiv:
nipkow@13095
   217
"(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
nipkow@13095
   218
 (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
nipkow@13095
   219
by(fast dest:direction1 direction2)
nipkow@13095
   220
nipkow@13095
   221
end