src/HOL/IMP/Machines.thy
author krauss
Mon Jul 27 21:47:41 2009 +0200 (2009-07-27 ago)
changeset 32235 8f9b8d14fc9f
parent 31970 ccaadfcf6941
child 42174 d0be2722ce9f
permissions -rw-r--r--
"more standard" argument order of relation composition (op O)
haftmann@30952
     1
theory Machines
haftmann@30952
     2
imports Natural
haftmann@30952
     3
begin
nipkow@13095
     4
nipkow@13095
     5
lemma converse_in_rel_pow_eq:
haftmann@30952
     6
  "((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
     7
apply(rule iffI)
krauss@31969
     8
 apply(blast elim:rel_pow_E2)
krauss@32235
     9
apply (auto simp: rel_pow_commute[symmetric])
nipkow@13095
    10
done
nipkow@13095
    11
nipkow@13095
    12
subsection "Instructions"
nipkow@13095
    13
nipkow@13095
    14
text {* There are only three instructions: *}
nipkow@13675
    15
datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat
nipkow@13095
    16
nipkow@13095
    17
types instrs = "instr list"
nipkow@13095
    18
nipkow@13095
    19
subsection "M0 with PC"
nipkow@13095
    20
berghofe@23746
    21
inductive_set
berghofe@23746
    22
  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
berghofe@23746
    23
  and exec01' :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
berghofe@23746
    24
    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
berghofe@23746
    25
  for P :: "instr list"
berghofe@23746
    26
where
berghofe@23746
    27
  "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)"
berghofe@23746
    28
| 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>"
berghofe@23746
    29
| 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>"
berghofe@23746
    30
| JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
berghofe@23746
    31
        \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
berghofe@23746
    32
| 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
    33
berghofe@23746
    34
abbreviation
berghofe@23746
    35
  exec0s :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
berghofe@23746
    36
    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
berghofe@23746
    37
  "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^*"
kleing@14565
    38
berghofe@23746
    39
abbreviation
berghofe@23746
    40
  exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
berghofe@23746
    41
    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
haftmann@30952
    42
  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^^n"
nipkow@13095
    43
nipkow@13095
    44
subsection "M0 with lists"
nipkow@13095
    45
nipkow@13095
    46
text {* We describe execution of programs in the machine by
nipkow@13095
    47
  an operational (small step) semantics:
nipkow@13095
    48
*}
nipkow@13095
    49
nipkow@13095
    50
types config = "instrs \<times> instrs \<times> state"
nipkow@13095
    51
nipkow@13095
    52
berghofe@23746
    53
inductive_set
berghofe@23746
    54
  stepa1 :: "(config \<times> config)set"
berghofe@23746
    55
  and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
berghofe@23746
    56
    ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
berghofe@23746
    57
where
berghofe@23746
    58
  "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : stepa1"
berghofe@23746
    59
| "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>"
berghofe@23746
    60
| "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
berghofe@23746
    61
| "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
nipkow@13095
    62
   \<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>"
berghofe@23746
    63
| "i \<le> size q
nipkow@13095
    64
   \<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
    65
berghofe@23746
    66
abbreviation
berghofe@23746
    67
  stepa :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
berghofe@23746
    68
    ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)  where
berghofe@23746
    69
  "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^*)"
berghofe@23746
    70
berghofe@23746
    71
abbreviation
berghofe@23746
    72
  stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
berghofe@23746
    73
    ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
haftmann@30952
    74
  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^^i)"
berghofe@23746
    75
berghofe@23746
    76
inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1"
nipkow@13095
    77
nipkow@13095
    78
lemma exec_simp[simp]:
nipkow@13095
    79
 "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of
nipkow@13675
    80
 SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q |
nipkow@13095
    81
 JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q
nipkow@13095
    82
            else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) |
nipkow@13095
    83
 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
    84
apply(rule iffI)
nipkow@13095
    85
defer
nipkow@13095
    86
apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
nipkow@13095
    87
apply(erule execE)
nipkow@13095
    88
apply(simp_all)
nipkow@13095
    89
done
nipkow@13095
    90
nipkow@13095
    91
lemma execn_simp[simp]:
nipkow@13095
    92
"(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) =
nipkow@13095
    93
 (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or>
nipkow@13095
    94
  ((\<exists>m p' q' t. n = Suc m \<and>
nipkow@13095
    95
                \<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
    96
by(subst converse_in_rel_pow_eq, simp)
nipkow@13095
    97
nipkow@13095
    98
nipkow@13095
    99
lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) =
nipkow@13095
   100
 (p'' = i#p & q''=q & u=s |
nipkow@13095
   101
 (\<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
   102
apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
nipkow@13095
   103
apply(blast)
nipkow@13095
   104
done
nipkow@13095
   105
nipkow@13095
   106
declare nth_append[simp]
nipkow@13095
   107
nipkow@13095
   108
lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys"
nipkow@13095
   109
by simp
nipkow@13095
   110
nipkow@13095
   111
lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
nipkow@13095
   112
apply(rule iffI)
nipkow@13095
   113
 apply(rule rev_revD, simp)
nipkow@13095
   114
apply fastsimp
nipkow@13095
   115
done
nipkow@13095
   116
nipkow@13095
   117
lemma direction1:
nipkow@13095
   118
 "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
nipkow@13095
   119
  rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
wenzelm@18372
   120
apply(induct set: stepa1)
nipkow@13675
   121
   apply(simp add:exec01.SET)
nipkow@13095
   122
  apply(fastsimp intro:exec01.JMPFT)
nipkow@13095
   123
 apply simp
nipkow@13095
   124
 apply(rule exec01.JMPFF)
nipkow@13095
   125
     apply simp
nipkow@13095
   126
    apply fastsimp
nipkow@13095
   127
   apply simp
nipkow@13095
   128
  apply simp
nipkow@13095
   129
 apply simp
nipkow@13095
   130
apply(fastsimp simp add:exec01.JMPB)
nipkow@13095
   131
done
webertj@20217
   132
nipkow@13098
   133
(*
nipkow@13098
   134
lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
nipkow@13095
   135
apply(induct xs)
nipkow@13095
   136
 apply simp_all
nipkow@13095
   137
apply(case_tac i)
nipkow@13095
   138
apply simp_all
nipkow@13095
   139
done
nipkow@13095
   140
nipkow@13098
   141
lemma rev_drop: "\<And>i. rev (drop i xs) = take (length xs - i) (rev xs)"
nipkow@13098
   142
apply(induct xs)
nipkow@13098
   143
 apply simp_all
nipkow@13098
   144
apply(case_tac i)
nipkow@13098
   145
apply simp_all
nipkow@13098
   146
done
nipkow@13098
   147
*)
webertj@20217
   148
nipkow@13095
   149
lemma direction2:
nipkow@13095
   150
 "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
wenzelm@18372
   151
  rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
nipkow@13095
   152
          rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
wenzelm@20503
   153
apply(induct arbitrary: p q p' q' set: exec01)
nipkow@13098
   154
   apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
nipkow@13095
   155
   apply(drule sym)
nipkow@13095
   156
   apply simp
nipkow@13095
   157
   apply(rule rev_revD)
nipkow@13095
   158
   apply simp
nipkow@13098
   159
  apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
nipkow@13095
   160
  apply(drule sym)
nipkow@13095
   161
  apply simp
nipkow@13095
   162
  apply(rule rev_revD)
nipkow@13095
   163
  apply simp
berghofe@13612
   164
 apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+
nipkow@13095
   165
 apply(drule sym)
nipkow@13095
   166
 apply simp
nipkow@13095
   167
 apply(rule rev_revD)
nipkow@13095
   168
 apply simp
nipkow@13098
   169
apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
nipkow@13095
   170
apply(drule sym)
nipkow@13098
   171
apply(simp add:rev_take)
nipkow@13095
   172
apply(rule rev_revD)
nipkow@13098
   173
apply(simp add:rev_drop)
nipkow@13095
   174
done
nipkow@13095
   175
nipkow@13095
   176
nipkow@13095
   177
theorem M_eqiv:
nipkow@13095
   178
"(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
nipkow@13095
   179
 (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
wenzelm@18372
   180
  by (blast dest: direction1 direction2)
nipkow@13095
   181
nipkow@13095
   182
end