8 *) |
8 *) |
9 |
9 |
10 theory Trans imports Evaln begin |
10 theory Trans imports Evaln begin |
11 |
11 |
12 definition groundVar :: "var \<Rightarrow> bool" where |
12 definition groundVar :: "var \<Rightarrow> bool" where |
13 "groundVar v \<equiv> (case v of |
13 "groundVar v \<longleftrightarrow> (case v of |
14 LVar ln \<Rightarrow> True |
14 LVar ln \<Rightarrow> True |
15 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a |
15 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a |
16 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i |
16 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i |
17 | InsInitV c v \<Rightarrow> False)" |
17 | InsInitV c v \<Rightarrow> False)" |
18 |
18 |
33 apply (simp add: groundVar_def) |
33 apply (simp add: groundVar_def) |
34 done |
34 done |
35 qed |
35 qed |
36 |
36 |
37 definition groundExprs :: "expr list \<Rightarrow> bool" where |
37 definition groundExprs :: "expr list \<Rightarrow> bool" where |
38 "groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es" |
38 "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)" |
39 |
39 |
40 consts the_val:: "expr \<Rightarrow> val" |
40 primrec the_val:: "expr \<Rightarrow> val" where |
41 primrec |
41 "the_val (Lit v) = v" |
42 "the_val (Lit v) = v" |
42 |
43 |
43 primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where |
44 consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" |
44 "the_var G s (LVar ln) =(lvar ln (store s),s)" |
45 primrec |
45 | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" |
46 "the_var G s (LVar ln) =(lvar ln (store s),s)" |
46 | the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" |
47 the_var_FVar_def: |
|
48 "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" |
|
49 the_var_AVar_def: |
|
50 "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" |
|
51 |
47 |
52 lemma the_var_FVar_simp[simp]: |
48 lemma the_var_FVar_simp[simp]: |
53 "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" |
49 "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" |
54 by (simp) |
50 by (simp) |
55 declare the_var_FVar_def [simp del] |
51 declare the_var_FVar_def [simp del] |