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