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)
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〉)