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