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