7 PRELIMINARY!!!!!!!! |
7 PRELIMINARY!!!!!!!! |
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 |
13 "groundVar v \<longleftrightarrow> (case v of |
13 groundVar :: "var \<Rightarrow> bool" where |
14 LVar ln \<Rightarrow> True |
14 "groundVar v \<longleftrightarrow> (case v of |
15 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a |
15 LVar ln \<Rightarrow> True |
16 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i |
16 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a |
17 | InsInitV c v \<Rightarrow> False)" |
17 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i |
|
18 | InsInitV c v \<Rightarrow> False)" |
18 |
19 |
19 lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]: |
20 lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]: |
20 assumes ground: "groundVar v" and |
21 assumes ground: "groundVar v" and |
21 LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and |
22 LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and |
22 FVar: "\<And> accC statDeclC stat a fn. |
23 FVar: "\<And> accC statDeclC stat a fn. |
32 apply (simp add: groundVar_def,blast) |
33 apply (simp add: groundVar_def,blast) |
33 apply (simp add: groundVar_def) |
34 apply (simp add: groundVar_def) |
34 done |
35 done |
35 qed |
36 qed |
36 |
37 |
37 definition groundExprs :: "expr list \<Rightarrow> bool" where |
38 definition |
38 "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)" |
39 groundExprs :: "expr list \<Rightarrow> bool" |
|
40 where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)" |
39 |
41 |
40 primrec the_val:: "expr \<Rightarrow> val" where |
42 primrec the_val:: "expr \<Rightarrow> val" |
41 "the_val (Lit v) = v" |
43 where "the_val (Lit v) = v" |
42 |
44 |
43 primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where |
45 primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where |
44 "the_var G s (LVar ln) =(lvar ln (store s),s)" |
46 "the_var G s (LVar ln) = (lvar ln (store s),s)" |
45 | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" |
47 | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" |
46 | the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" |
48 | the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" |
47 |
49 |
48 lemma the_var_FVar_simp[simp]: |
50 lemma the_var_FVar_simp[simp]: |
49 "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" |
51 "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" |