10 |
10 |
11 |
11 |
12 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where |
12 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where |
13 "aval (N i) s = Some i" | |
13 "aval (N i) s = Some i" | |
14 "aval (V x) s = s x" | |
14 "aval (V x) s = s x" | |
15 "aval (Plus a\<^isub>1 a\<^isub>2) s = |
15 "aval (Plus a\<^sub>1 a\<^sub>2) s = |
16 (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of |
16 (case (aval a\<^sub>1 s, aval a\<^sub>2 s) of |
17 (Some i\<^isub>1,Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1+i\<^isub>2) | _ \<Rightarrow> None)" |
17 (Some i\<^sub>1,Some i\<^sub>2) \<Rightarrow> Some(i\<^sub>1+i\<^sub>2) | _ \<Rightarrow> None)" |
18 |
18 |
19 |
19 |
20 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where |
20 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where |
21 "bval (Bc v) s = Some v" | |
21 "bval (Bc v) s = Some v" | |
22 "bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" | |
22 "bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" | |
23 "bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of |
23 "bval (And b\<^sub>1 b\<^sub>2) s = (case (bval b\<^sub>1 s, bval b\<^sub>2 s) of |
24 (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" | |
24 (Some bv\<^sub>1, Some bv\<^sub>2) \<Rightarrow> Some(bv\<^sub>1 & bv\<^sub>2) | _ \<Rightarrow> None)" | |
25 "bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of |
25 "bval (Less a\<^sub>1 a\<^sub>2) s = (case (aval a\<^sub>1 s, aval a\<^sub>2 s) of |
26 (Some i\<^isub>1, Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1 < i\<^isub>2) | _ \<Rightarrow> None)" |
26 (Some i\<^sub>1, Some i\<^sub>2) \<Rightarrow> Some(i\<^sub>1 < i\<^sub>2) | _ \<Rightarrow> None)" |
27 |
27 |
28 |
28 |
29 lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i" |
29 lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i" |
30 by (induct a) auto |
30 by (induct a) auto |
31 |
31 |