diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Machines.thy --- a/src/HOL/IMP/Machines.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Machines.thy Wed Jul 11 11:14:51 2007 +0200 @@ -36,43 +36,28 @@ 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" - ("(_/ \ (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) +inductive_set + exec01 :: "instr list \ ((nat\state) \ (nat\state))set" + and exec01' :: "[instrs, nat,state, nat,state] \ bool" + ("(_/ \ (1\_,/_\)/ -1\ (1\_,/_\))" [50,0,0,0,0] 50) + for P :: "instr list" +where + "p \ \i,s\ -1\ \j,t\ == ((i,s),j,t) : (exec01 p)" +| SET: "\ n \ P \ \n,s\ -1\ \Suc n,s[x\ a s]\" +| JMPFT: "\ n \ P \ \n,s\ -1\ \Suc n,s\" +| JMPFF: "\ nb s; m=n+i+1; m \ size P \ + \ P \ \n,s\ -1\ \m,s\" +| JMPB: "\ n n; j = n-i \ \ P \ \n,s\ -1\ \j,s\" -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) +abbreviation + exec0s :: "[instrs, nat,state, nat,state] \ bool" + ("(_/ \ (1\_,/_\)/ -*\ (1\_,/_\))" [50,0,0,0,0] 50) where + "p \ \i,s\ -*\ \j,t\ == ((i,s),j,t) : (exec01 p)^*" -translations - "p \ \i,s\ -1\ \j,t\" == "((i,s),j,t) : (exec01 p)" - "p \ \i,s\ -*\ \j,t\" == "((i,s),j,t) : (exec01 p)^*" - "p \ \i,s\ -n\ \j,t\" == "((i,s),j,t) : (exec01 p)^n" - -inductive "exec01 P" -intros -SET: "\ n \ P \ \n,s\ -1\ \Suc n,s[x\ a s]\" -JMPFT: "\ n \ P \ \n,s\ -1\ \Suc n,s\" -JMPFF: "\ nb s; m=n+i+1; m \ size P \ - \ P \ \n,s\ -1\ \m,s\" -JMPB: "\ n n; j = n-i \ \ P \ \n,s\ -1\ \j,s\" +abbreviation + exec0n :: "[instrs, nat,state, nat, nat,state] \ bool" + ("(_/ \ (1\_,/_\)/ -_\ (1\_,/_\))" [50,0,0,0,0] 50) where + "p \ \i,s\ -n\ \j,t\ == ((i,s),j,t) : (exec01 p)^n" subsection "M0 with lists" @@ -82,40 +67,31 @@ 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\ a s]\" - "b s \ \JMPF b i#p,q,s\ -1\ \p,JMPF b i#q,s\" - "\ \ b s; i \ size p \ +inductive_set + stepa1 :: "(config \ config)set" + and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \ bool" + ("((1\_,/_,/_\)/ -1\ (1\_,/_,/_\))" 50) +where + "\p,q,s\ -1\ \p',q',t\ == ((p,q,s),p',q',t) : stepa1" +| "\SET x a#p,q,s\ -1\ \p,SET x a#q,s[x\ 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 +| "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" +abbreviation + stepa :: "[instrs,instrs,state, instrs,instrs,state] \ bool" + ("((1\_,/_,/_\)/ -*\ (1\_,/_,/_\))" 50) where + "\p,q,s\ -*\ \p',q',t\ == ((p,q,s),p',q',t) : (stepa1^*)" + +abbreviation + stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \ bool" + ("((1\_,/_,/_\)/ -_\ (1\_,/_,/_\))" 50) where + "\p,q,s\ -i\ \p',q',t\ == ((p,q,s),p',q',t) : (stepa1^i)" + +inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1" lemma exec_simp[simp]: "(\i#p,q,s\ -1\ \p',q',t\) = (case i of