src/HOL/IMP/Machines.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 32235 8f9b8d14fc9f
child 42174 d0be2722ce9f
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     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