src/HOL/Bali/Trans.thy
changeset 37597 a02ea93e88c6
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/Trans.thy	Mon Jun 28 15:32:08 2010 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Mon Jun 28 15:32:13 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  theory Trans imports Evaln begin
     1.5  
     1.6  definition groundVar :: "var \<Rightarrow> bool" where
     1.7 -"groundVar v \<equiv> (case v of
     1.8 +"groundVar v \<longleftrightarrow> (case v of
     1.9                     LVar ln \<Rightarrow> True
    1.10                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
    1.11                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
    1.12 @@ -35,19 +35,15 @@
    1.13  qed
    1.14  
    1.15  definition groundExprs :: "expr list \<Rightarrow> bool" where
    1.16 -"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
    1.17 +  "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
    1.18    
    1.19 -consts the_val:: "expr \<Rightarrow> val"
    1.20 -primrec
    1.21 -"the_val (Lit v) = v"
    1.22 +primrec the_val:: "expr \<Rightarrow> val" where
    1.23 +  "the_val (Lit v) = v"
    1.24  
    1.25 -consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
    1.26 -primrec
    1.27 -"the_var G s (LVar ln)                    =(lvar ln (store s),s)"
    1.28 -the_var_FVar_def:
    1.29 -"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
    1.30 -the_var_AVar_def:
    1.31 -"the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
    1.32 +primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
    1.33 +  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
    1.34 +| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
    1.35 +| the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
    1.36  
    1.37  lemma the_var_FVar_simp[simp]:
    1.38  "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"