src/HOL/IMP/ASM.thy
author nipkow
Tue, 20 Sep 2011 05:48:23 +0200
changeset 45015 fdac1e9880eb
parent 44036 d03f9f28d01d
child 45222 6eab55bab82f
permissions -rw-r--r--
Updated IMP to use new induction method
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     1
header "Arithmetic Stack Machine and Compilation"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     2
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     3
theory ASM imports AExp begin
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     4
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     5
subsection "Arithmetic Stack Machine"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     6
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     7
datatype ainstr = LOADI val | LOAD string | ADD
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     8
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     9
type_synonym stack = "val list"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    10
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    11
abbreviation "hd2 xs == hd(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    12
abbreviation "tl2 xs == tl(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    13
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    14
text{* \noindent Abbreviations are transparent: they are unfolded after
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    15
parsing and folded back again before printing. Internally, they do not
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    16
exist. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    17
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    18
fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    19
"aexec1 (LOADI n) _ stk  =  n # stk" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    20
"aexec1 (LOAD n) s stk  =  s(n) # stk" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    21
"aexec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    22
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    23
fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    24
"aexec [] _ stk = stk" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    25
"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    26
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    27
value "aexec [LOADI 5, LOAD ''y'', ADD]
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43158
diff changeset
    28
 <''x'' := 42, ''y'' := 43> [50]"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    29
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    30
lemma aexec_append[simp]:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    31
  "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44036
diff changeset
    32
apply(induction is1 arbitrary: stk)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    33
apply (auto)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    34
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    35
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    36
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    37
subsection "Compilation"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    38
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    39
fun acomp :: "aexp \<Rightarrow> ainstr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    40
"acomp (N n) = [LOADI n]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    41
"acomp (V x) = [LOAD x]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    42
"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    43
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    44
value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    45
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    46
theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44036
diff changeset
    47
apply(induction a arbitrary: stk)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    48
apply (auto)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    49
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    50
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    51
end