src/HOL/Bali/Trans.thy
changeset 37956 ee939247b2fb
parent 37597 a02ea93e88c6
child 40945 b8703f63bfb2
     1.1 --- a/src/HOL/Bali/Trans.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -9,12 +9,13 @@
     1.4  
     1.5  theory Trans imports Evaln begin
     1.6  
     1.7 -definition groundVar :: "var \<Rightarrow> bool" where
     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 -                 | InsInitV c v \<Rightarrow> False)"
    1.13 +definition
    1.14 +  groundVar :: "var \<Rightarrow> bool" where
    1.15 +  "groundVar v \<longleftrightarrow> (case v of
    1.16 +                     LVar ln \<Rightarrow> True
    1.17 +                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
    1.18 +                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
    1.19 +                   | InsInitV c v \<Rightarrow> False)"
    1.20  
    1.21  lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
    1.22    assumes ground: "groundVar v" and
    1.23 @@ -34,14 +35,15 @@
    1.24      done
    1.25  qed
    1.26  
    1.27 -definition groundExprs :: "expr list \<Rightarrow> bool" where
    1.28 -  "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
    1.29 +definition
    1.30 +  groundExprs :: "expr list \<Rightarrow> bool"
    1.31 +  where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
    1.32    
    1.33 -primrec the_val:: "expr \<Rightarrow> val" where
    1.34 -  "the_val (Lit v) = v"
    1.35 +primrec the_val:: "expr \<Rightarrow> val"
    1.36 +  where "the_val (Lit v) = v"
    1.37  
    1.38  primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
    1.39 -  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
    1.40 +  "the_var G s (LVar ln) = (lvar ln (store s),s)"
    1.41  | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
    1.42  | the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
    1.43