38 STORE string | |
38 STORE string | |
39 JMP int | |
39 JMP int | |
40 JMPFLESS int | |
40 JMPFLESS int | |
41 JMPFGE int |
41 JMPFGE int |
42 |
42 |
43 (* reads slightly nicer *) |
|
44 abbreviation |
|
45 "JMPB i == JMP (-i)" |
|
46 |
|
47 type_synonym stack = "val list" |
43 type_synonym stack = "val list" |
48 type_synonym config = "int\<times>state\<times>stack" |
44 type_synonym config = "int\<times>state\<times>stack" |
49 |
45 |
50 abbreviation "hd2 xs == hd(tl xs)" |
46 abbreviation "hd2 xs == hd(tl xs)" |
51 abbreviation "tl2 xs == tl(tl xs)" |
47 abbreviation "tl2 xs == tl(tl xs)" |
52 |
48 |
53 inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
49 inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
54 ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50) |
50 ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60) |
55 where |
51 where |
56 "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" | |
52 "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" | |
57 "LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" | |
53 "LOAD x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" | |
58 "ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" | |
54 "ADD \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" | |
59 "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" | |
55 "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" | |
64 code_pred iexec1 . |
60 code_pred iexec1 . |
65 |
61 |
66 declare iexec1.intros |
62 declare iexec1.intros |
67 |
63 |
68 definition |
64 definition |
69 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) |
65 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) |
70 where |
66 where |
71 "P \<turnstile> c \<rightarrow> c' = |
67 "P \<turnstile> c \<rightarrow> c' = |
72 (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)" |
68 (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)" |
73 |
69 |
74 declare exec1_def [simp] |
70 declare exec1_def [simp] |
75 |
71 |
76 lemma exec1I [intro, code_pred_intro]: |
72 lemma exec1I [intro, code_pred_intro]: |
77 "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" |
73 assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P" |
78 by simp |
74 shows "P \<turnstile> (i,s,stk) \<rightarrow> c'" |
|
75 using assms by simp |
79 |
76 |
80 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) |
77 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) |
81 where |
78 where |
82 refl: "P \<turnstile> c \<rightarrow>* c" | |
79 refl: "P \<turnstile> c \<rightarrow>* c" | |
83 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
80 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
243 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = |
240 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = |
244 (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1) |
241 (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1) |
245 in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" | |
242 in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" | |
246 "ccomp (WHILE b DO c) = |
243 "ccomp (WHILE b DO c) = |
247 (let cc = ccomp c; cb = bcomp b False (isize cc + 1) |
244 (let cc = ccomp c; cb = bcomp b False (isize cc + 1) |
248 in cb @ cc @ [JMPB (isize cb + isize cc + 1)])" |
245 in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])" |
|
246 |
249 |
247 |
250 value "ccomp |
248 value "ccomp |
251 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) |
249 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) |
252 ELSE ''v'' ::= V ''u'')" |
250 ELSE ''v'' ::= V ''u'')" |
253 |
251 |