39 subsection "Syntax of Commands" |
39 subsection "Syntax of Commands" |
40 (* a copy of Com.thy - keep in sync! *) |
40 (* a copy of Com.thy - keep in sync! *) |
41 |
41 |
42 datatype |
42 datatype |
43 com = SKIP |
43 com = SKIP |
44 | Assign vname aexp ("_ ::= _" [1000, 61] 61) |
44 | Assign vname aexp ("_ ::= _" [1000, 61] 61) |
45 | Semi com com ("_; _" [60, 61] 60) |
45 | Seq com com ("_; _" [60, 61] 60) |
46 | If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61) |
46 | If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61) |
47 | While bexp com ("WHILE _ DO _" [0, 61] 61) |
47 | While bexp com ("WHILE _ DO _" [0, 61] 61) |
48 |
48 |
49 |
49 |
50 subsection "Small-Step Semantics of Commands" |
50 subsection "Small-Step Semantics of Commands" |
52 inductive |
52 inductive |
53 small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
53 small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
54 where |
54 where |
55 Assign: "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" | |
55 Assign: "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" | |
56 |
56 |
57 Semi1: "(SKIP;c,s) \<rightarrow> (c,s)" | |
57 Seq1: "(SKIP;c,s) \<rightarrow> (c,s)" | |
58 Semi2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" | |
58 Seq2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" | |
59 |
59 |
60 IfTrue: "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" | |
60 IfTrue: "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" | |
61 IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" | |
61 IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" | |
62 |
62 |
63 While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
63 While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
91 Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2" |
91 Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2" |
92 |
92 |
93 inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where |
93 inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where |
94 Skip_ty: "\<Gamma> \<turnstile> SKIP" | |
94 Skip_ty: "\<Gamma> \<turnstile> SKIP" | |
95 Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" | |
95 Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" | |
96 Semi_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" | |
96 Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" | |
97 If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" | |
97 If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" | |
98 While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c" |
98 While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c" |
99 |
99 |
100 inductive_cases [elim!]: |
100 inductive_cases [elim!]: |
101 "\<Gamma> \<turnstile> x ::= a" "\<Gamma> \<turnstile> c1;c2" |
101 "\<Gamma> \<turnstile> x ::= a" "\<Gamma> \<turnstile> c1;c2" |
162 case Skip_ty thus ?case by simp |
162 case Skip_ty thus ?case by simp |
163 next |
163 next |
164 case Assign_ty |
164 case Assign_ty |
165 thus ?case by (metis Assign aprogress) |
165 thus ?case by (metis Assign aprogress) |
166 next |
166 next |
167 case Semi_ty thus ?case by simp (metis Semi1 Semi2) |
167 case Seq_ty thus ?case by simp (metis Seq1 Seq2) |
168 next |
168 next |
169 case (If_ty \<Gamma> b c1 c2) |
169 case (If_ty \<Gamma> b c1 c2) |
170 then obtain bv where "tbval b s bv" by (metis bprogress) |
170 then obtain bv where "tbval b s bv" by (metis bprogress) |
171 show ?case |
171 show ?case |
172 proof(cases bv) |
172 proof(cases bv) |