# Theory Machines

Up to index of Isabelle/HOL/IMP

theory Machines
imports Natural
begin

    theory Machines imports Natural begin

    lemma rtrancl_eq: "R^* = Id ∪ (R O R^*)"
    by(fast intro:rtrancl.intros elim:rtranclE)

    lemma converse_rtrancl_eq: "R^* = Id ∪ (R^* O R)"
    by(subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)

    lemmas converse_rel_powE = rel_pow_E2

    lemma R_O_Rn_commute: "R O R^n = R^n O R"
    by(induct_tac n, simp, simp add: O_assoc[symmetric])

    lemma converse_in_rel_pow_eq:
    "((x,z) ∈ R^n) = (n=0 ∧ z=x ∨ (∃m y. n = Suc m ∧ (x,y) ∈ R ∧ (y,z) ∈ R^m))"
    apply(rule iffI)
     apply(blast elim:converse_rel_powE)
    apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
    done

    lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
    by(induct n, simp, simp add:O_assoc)

    lemma rel_pow_plusI: "[| (x,y) ∈ R^m; (y,z) ∈ R^n |] ==> (x,z) ∈ R^(m+n)"
    by(simp add:rel_pow_plus rel_compI)

    subsection "Instructions"

    text {* There are only three instructions: *}
    datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat

    types instrs = "instr list"

    subsection "M0 with PC"

    consts  exec01 :: "instr list => ((nat×state) × (nat×state))set"
    syntax
      "_exec01" :: "[instrs, nat,state, nat,state] => bool"
                   ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
      "_exec0s" :: "[instrs, nat,state, nat,state] => bool"
                   ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50)
      "_exec0n" :: "[instrs, nat,state, nat, nat,state] => bool"
                   ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50)

    syntax (xsymbols)
      "_exec01" :: "[instrs, nat,state, nat,state] => bool"
                   ("(_/ \<turnstile> (1⟨_,/_⟩)/ -1-> (1⟨_,/_⟩))" [50,0,0,0,0] 50)
      "_exec0s" :: "[instrs, nat,state, nat,state] => bool"
                   ("(_/ \<turnstile> (1⟨_,/_⟩)/ -*-> (1⟨_,/_⟩))" [50,0,0,0,0] 50)
      "_exec0n" :: "[instrs, nat,state, nat, nat,state] => bool"
                   ("(_/ \<turnstile> (1⟨_,/_⟩)/ -_-> (1⟨_,/_⟩))" [50,0,0,0,0] 50)

    syntax (HTML output)
      "_exec01" :: "[instrs, nat,state, nat,state] => bool"
                   ("(_/ |- (1⟨_,/_⟩)/ -1-> (1⟨_,/_⟩))" [50,0,0,0,0] 50)
      "_exec0s" :: "[instrs, nat,state, nat,state] => bool"
                   ("(_/ |- (1⟨_,/_⟩)/ -*-> (1⟨_,/_⟩))" [50,0,0,0,0] 50)
      "_exec0n" :: "[instrs, nat,state, nat, nat,state] => bool"
                   ("(_/ |- (1⟨_,/_⟩)/ -_-> (1⟨_,/_⟩))" [50,0,0,0,0] 50)

    translations
      "p \<turnstile> ⟨i,s⟩ -1-> ⟨j,t⟩" == "((i,s),j,t) : (exec01 p)"
      "p \<turnstile> ⟨i,s⟩ -*-> ⟨j,t⟩" == "((i,s),j,t) : (exec01 p)^*"
      "p \<turnstile> ⟨i,s⟩ -n-> ⟨j,t⟩" == "((i,s),j,t) : (exec01 p)^n"

    inductive "exec01 P"
    intros
    SET: "[| n<size P; P!n = SET x a |] ==> P \<turnstile> ⟨n,s⟩ -1-> ⟨Suc n,s[x\<mapsto> a s]⟩"
    JMPFT: "[| n<size P; P!n = JMPF b i;  b s |] ==> P \<turnstile> ⟨n,s⟩ -1-> ⟨Suc n,s⟩"
    JMPFF: "[| n<size P; P!n = JMPF b i; ¬b s; m=n+i+1; m ≤ size P |]
            ==> P \<turnstile> ⟨n,s⟩ -1-> ⟨m,s⟩"
    JMPB:  "[| n<size P; P!n = JMPB i; i ≤ n; j = n-i |] ==> P \<turnstile> ⟨n,s⟩ -1-> ⟨j,s⟩"

    subsection "M0 with lists"

    text {* We describe execution of programs in the machine by
      an operational (small step) semantics:
    *}

    types config = "instrs × instrs × state"

    consts  stepa1 :: "(config × config)set"

    syntax
      "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] => bool"
                   ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50)
      "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] => bool"
                   ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50)
      "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] => bool"
                   ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50)

    syntax (xsymbols)
      "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] => bool"
                   ("((1⟨_,/_,/_⟩)/ -1-> (1⟨_,/_,/_⟩))" 50)
      "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] => bool"
                   ("((1⟨_,/_,/_⟩)/ -*-> (1⟨_,/_,/_⟩))" 50)
      "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] => bool"
                   ("((1⟨_,/_,/_⟩)/ -_-> (1⟨_,/_,/_⟩))" 50)

    translations
      "⟨p,q,s⟩ -1-> ⟨p',q',t⟩" == "((p,q,s),p',q',t) : stepa1"
      "⟨p,q,s⟩ -*-> ⟨p',q',t⟩" == "((p,q,s),p',q',t) : (stepa1^*)"
      "⟨p,q,s⟩ -i-> ⟨p',q',t⟩" == "((p,q,s),p',q',t) : (stepa1^i)"

    inductive "stepa1"
    intros
      "⟨SET x a#p,q,s⟩ -1-> ⟨p,SET x a#q,s[x\<mapsto> a s]⟩"
      "b s ==> ⟨JMPF b i#p,q,s⟩ -1-> ⟨p,JMPF b i#q,s⟩"
      "[| ¬ b s; i ≤ size p |]
       ==> ⟨JMPF b i # p, q, s⟩ -1-> ⟨drop i p, rev(take i p) @ JMPF b i # q, s⟩"
      "i ≤ size q
       ==> ⟨JMPB i # p, q, s⟩ -1-> ⟨rev(take i q) @ JMPB i # p, drop i q, s⟩"

    inductive_cases execE: "((i#is,p,s),next) : stepa1"

    lemma exec_simp[simp]:
     "(⟨i#p,q,s⟩ -1-> ⟨p',q',t⟩) = (case i of
     SET x a => t = s[x\<mapsto> a s] ∧ p' = p ∧ q' = i#q |
     JMPF b n => t=s ∧ (if b s then p' = p ∧ q' = i#q
                else n ≤ size p ∧ p' = drop n p ∧ q' = rev(take n p) @ i # q) |
     JMPB n => n ≤ size q ∧ t=s ∧ p' = rev(take n q) @ i # p ∧ q' = drop n q)"
    apply(rule iffI)
    defer
    apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
    apply(erule execE)
    apply(simp_all)
    done

    lemma execn_simp[simp]:
    "(⟨i#p,q,s⟩ -n-> ⟨p'',q'',u⟩) =
     (n=0 ∧ p'' = i#p ∧ q'' = q ∧ u = s ∨
      ((∃m p' q' t. n = Suc m ∧
                    ⟨i#p,q,s⟩ -1-> ⟨p',q',t⟩ ∧ ⟨p',q',t⟩ -m-> ⟨p'',q'',u⟩)))"
    by(subst converse_in_rel_pow_eq, simp)

    lemma exec_star_simp[simp]: "(⟨i#p,q,s⟩ -*-> ⟨p'',q'',u⟩) =
     (p'' = i#p & q''=q & u=s |
     (∃p' q' t. ⟨i#p,q,s⟩ -1-> ⟨p',q',t⟩ ∧ ⟨p',q',t⟩ -*-> ⟨p'',q'',u⟩))"
    apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
    apply(blast)
    done

    declare nth_append[simp]

    lemma rev_revD: "rev xs = rev ys ==> xs = ys"
    by simp

    lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
    apply(rule iffI)
     apply(rule rev_revD, simp)
    apply fastsimp
    done

    lemma direction1:
     "⟨q,p,s⟩ -1-> ⟨q',p',t⟩ ==>
      rev p' @ q' = rev p @ q ∧ rev p @ q \<turnstile> ⟨size p,s⟩ -1-> ⟨size p',t⟩"
    apply(erule stepa1.induct)
       apply(simp add:exec01.SET)
      apply(fastsimp intro:exec01.JMPFT)
     apply simp
     apply(rule exec01.JMPFF)
         apply simp
        apply fastsimp
       apply simp
      apply simp
      apply arith
     apply simp
     apply arith
    apply(fastsimp simp add:exec01.JMPB)
    done
    (*
    lemma rev_take: "!!i. rev (take i xs) = drop (length xs - i) (rev xs)"
    apply(induct xs)
     apply simp_all
    apply(case_tac i)
    apply simp_all
    done

    lemma rev_drop: "!!i. rev (drop i xs) = take (length xs - i) (rev xs)"
    apply(induct xs)
     apply simp_all
    apply(case_tac i)
    apply simp_all
    done
    *)
    lemma direction2:
     "rpq \<turnstile> ⟨sp,s⟩ -1-> ⟨sp',t⟩ ==>
     ∀p q p' q'. rpq = rev p @ q & sp = size p & sp' = size p' -->
              rev p' @ q' = rev p @ q --> ⟨q,p,s⟩ -1-> ⟨q',p',t⟩"
    apply(erule exec01.induct)
       apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
       apply(drule sym)
       apply simp
       apply(rule rev_revD)
       apply simp
      apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
      apply(drule sym)
      apply simp
      apply(rule rev_revD)
      apply simp
     apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+
     apply(drule sym)
     apply simp
     apply(rule rev_revD)
     apply simp
    apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
    apply(drule sym)
    apply(simp add:rev_take)
    apply(rule rev_revD)
    apply(simp add:rev_drop)
    done

    theorem M_eqiv:
    "(⟨q,p,s⟩ -1-> ⟨q',p',t⟩) =
     (rev p' @ q' = rev p @ q ∧ rev p @ q \<turnstile> ⟨size p,s⟩ -1-> ⟨size p',t⟩)"
    by(fast dest:direction1 direction2)

    end

lemma rtrancl_eq:

      R* = Id ∪ (R O R*)

lemma converse_rtrancl_eq:

      R* = Id ∪ (R* O R)

lemmas converse_rel_powE:

      [| (x, z) ∈ R ^ n; [| n = 0; x = z |] ==> P;
         !!y m. [| n = Suc m; (x, y) ∈ R; (y, z) ∈ R ^ m |] ==> P |]
      ==> P

lemmas converse_rel_powE:

      [| (x, z) ∈ R ^ n; [| n = 0; x = z |] ==> P;
         !!y m. [| n = Suc m; (x, y) ∈ R; (y, z) ∈ R ^ m |] ==> P |]
      ==> P

lemma R_O_Rn_commute:

      R O R ^ n = R ^ n O R

lemma converse_in_rel_pow_eq:

      ((x, z) ∈ R ^ n) =
      (n = 0 ∧ z = x ∨ (∃m y. n = Suc m ∧ (x, y) ∈ R ∧ (y, z) ∈ R ^ m))

lemma rel_pow_plus:

      R ^ (m + n) = R ^ n O R ^ m

lemma rel_pow_plusI:

      [| (x, y) ∈ R ^ m; (y, z) ∈ R ^ n |] ==> (x, z) ∈ R ^ (m + n)

### Instructions

### M0 with PC

### M0 with lists

lemmas execE:

      [| ((i # is, p, s), next) ∈ stepa1;
         !!a x. [| next = (is, SET x a # p, s[x ::= a s]); i = SET x a |] ==> P;
         !!b i. [| b s; next = (is, JMPF b i # p, s); i = JMPF b i |] ==> P;
         !!b i. [| ¬ b s; i ≤ length is;
                   next = (drop i is, rev (take i is) @ JMPF b i # p, s);
                   i = JMPF b i |]
                ==> P;
         !!i. [| i ≤ length p; next = (rev (take i p) @ JMPB i # is, drop i p, s);
                 i = JMPB i |]
              ==> P |]
      ==> P

lemma exec_simp:

      (<i # p,q,s> -1-> <p',q',t>) =
      (case i of SET x a => t = s[x ::= a s] ∧ p' = p ∧ q' = i # q
       | JMPF b n =>
           t = s ∧
           (if b s then p' = p ∧ q' = i # q
            else n ≤ length p ∧ p' = drop n p ∧ q' = rev (take n p) @ i # q)
       | JMPB n => n ≤ length q ∧ t = s ∧ p' = rev (take n q) @ i # p ∧ q' = drop n q)

lemma execn_simp:

      (<i # p,q,s> -n-> <p'',q'',u>) =
      (n = 0 ∧ p'' = i # p ∧ q'' = q ∧ u = s ∨
       (∃m p' q' t.
           n = Suc m ∧ <i # p,q,s> -1-> <p',q',t> ∧ <p',q',t> -m-> <p'',q'',u>))

lemma exec_star_simp:

      (<i # p,q,s> -*-> <p'',q'',u>) =
      (p'' = i # p ∧ q'' = q ∧ u = s ∨
       (∃p' q' t. <i # p,q,s> -1-> <p',q',t> ∧ <p',q',t> -*-> <p'',q'',u>))

lemma rev_revD:

      rev xs = rev ys ==> xs = ys

lemma

      (rev xs @ rev ys = rev zs) = (ys @ xs = zs)

lemma direction1:

      <q,p,s> -1-> <q',p',t>
      ==> rev p' @ q' = rev p @ q ∧ rev p @ q |- ⟨length p,s⟩ -1-> ⟨length p',t⟩

lemma direction2:

      rpq |- ⟨sp,s⟩ -1-> ⟨sp',t⟩
      ==> ∀p q p' q'.
             rpq = rev p @ q ∧ sp = length p ∧ sp' = length p' -->
             rev p' @ q' = rev p @ q --> <q,p,s> -1-> <q',p',t>

theorem M_eqiv:

      (<q,p,s> -1-> <q',p',t>) =
      (rev p' @ q' = rev p @ q ∧ rev p @ q |- ⟨length p,s⟩ -1-> ⟨length p',t⟩)