src/HOL/IMP/Machines.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 18372 2bffdf62fe7f
child 20217 25b068a99d2b
permissions -rw-r--r--
adaptions to codegen_package
     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.intros 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 consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
    40 syntax
    41   "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    42                ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
    43   "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    44                ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50)
    45   "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    46                ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50)
    47 
    48 syntax (xsymbols)
    49   "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    50                ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    51   "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    52                ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    53   "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    54                ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    55 
    56 syntax (HTML output)
    57   "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    58                ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    59   "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    60                ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    61   "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    62                ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    63 
    64 translations
    65   "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
    66   "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
    67   "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n"
    68 
    69 inductive "exec01 P"
    70 intros
    71 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>"
    72 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>"
    73 JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
    74         \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
    75 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>"
    76 
    77 subsection "M0 with lists"
    78 
    79 text {* We describe execution of programs in the machine by
    80   an operational (small step) semantics:
    81 *}
    82 
    83 types config = "instrs \<times> instrs \<times> state"
    84 
    85 consts  stepa1 :: "(config \<times> config)set"
    86 
    87 syntax
    88   "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    89                ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50)
    90   "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    91                ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50)
    92   "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] \<Rightarrow> bool"
    93                ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50)
    94 
    95 syntax (xsymbols)
    96   "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    97                ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
    98   "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
    99                ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
   100   "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
   101                ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
   102 
   103 translations
   104   "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1"
   105   "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)"
   106   "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)"
   107 
   108 
   109 inductive "stepa1"
   110 intros
   111   "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>"
   112   "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
   113   "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
   114    \<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>"
   115   "i \<le> size q
   116    \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>"
   117 
   118 inductive_cases execE: "((i#is,p,s),next) : stepa1"
   119 
   120 lemma exec_simp[simp]:
   121  "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of
   122  SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q |
   123  JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q
   124             else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) |
   125  JMPB n \<Rightarrow> n \<le> size q \<and> t=s \<and> p' = rev(take n q) @ i # p \<and> q' = drop n q)"
   126 apply(rule iffI)
   127 defer
   128 apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
   129 apply(erule execE)
   130 apply(simp_all)
   131 done
   132 
   133 lemma execn_simp[simp]:
   134 "(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) =
   135  (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or>
   136   ((\<exists>m p' q' t. n = Suc m \<and>
   137                 \<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>)))"
   138 by(subst converse_in_rel_pow_eq, simp)
   139 
   140 
   141 lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) =
   142  (p'' = i#p & q''=q & u=s |
   143  (\<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>))"
   144 apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
   145 apply(blast)
   146 done
   147 
   148 declare nth_append[simp]
   149 
   150 lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys"
   151 by simp
   152 
   153 lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
   154 apply(rule iffI)
   155  apply(rule rev_revD, simp)
   156 apply fastsimp
   157 done
   158 
   159 lemma direction1:
   160  "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
   161   rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
   162 apply(induct set: stepa1)
   163    apply(simp add:exec01.SET)
   164   apply(fastsimp intro:exec01.JMPFT)
   165  apply simp
   166  apply(rule exec01.JMPFF)
   167      apply simp
   168     apply fastsimp
   169    apply simp
   170   apply simp
   171   apply arith
   172  apply simp
   173  apply arith
   174 apply(fastsimp simp add:exec01.JMPB)
   175 done
   176 (*
   177 lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
   178 apply(induct xs)
   179  apply simp_all
   180 apply(case_tac i)
   181 apply simp_all
   182 done
   183 
   184 lemma rev_drop: "\<And>i. rev (drop i xs) = take (length xs - i) (rev xs)"
   185 apply(induct xs)
   186  apply simp_all
   187 apply(case_tac i)
   188 apply simp_all
   189 done
   190 *)
   191 lemma direction2:
   192  "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
   193   rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
   194           rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
   195 apply(induct fixing: p q p' q' set: exec01)
   196    apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
   197    apply(drule sym)
   198    apply simp
   199    apply(rule rev_revD)
   200    apply simp
   201   apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
   202   apply(drule sym)
   203   apply simp
   204   apply(rule rev_revD)
   205   apply simp
   206  apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+
   207  apply(drule sym)
   208  apply simp
   209  apply(rule rev_revD)
   210  apply simp
   211 apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
   212 apply(drule sym)
   213 apply(simp add:rev_take)
   214 apply(rule rev_revD)
   215 apply(simp add:rev_drop)
   216 done
   217 
   218 
   219 theorem M_eqiv:
   220 "(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
   221  (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
   222   by (blast dest: direction1 direction2)
   223 
   224 end