src/HOL/Bali/Trans.thy
changeset 47176 568fdc70e565
parent 40945 b8703f63bfb2
child 56073 29e308b56d23
     1.1 --- a/src/HOL/Bali/Trans.thy	Wed Mar 28 11:46:14 2012 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Wed Mar 28 12:08:08 2012 +0200
     1.3 @@ -17,23 +17,18 @@
     1.4                     | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
     1.5                     | InsInitV c v \<Rightarrow> False)"
     1.6  
     1.7 -lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
     1.8 -  assumes ground: "groundVar v" and
     1.9 -          LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
    1.10 -          FVar: "\<And> accC statDeclC stat a fn. 
    1.11 -                    \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
    1.12 -          AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
    1.13 -  shows "P"
    1.14 -proof -
    1.15 -  from ground LVar FVar AVar
    1.16 -  show ?thesis
    1.17 -    apply (cases v)
    1.18 -    apply (simp add: groundVar_def)
    1.19 -    apply (simp add: groundVar_def,blast)
    1.20 -    apply (simp add: groundVar_def,blast)
    1.21 -    apply (simp add: groundVar_def)
    1.22 -    done
    1.23 -qed
    1.24 +lemma groundVar_cases:
    1.25 +  assumes ground: "groundVar v"
    1.26 +  obtains (LVar) ln where "v=LVar ln"
    1.27 +    | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
    1.28 +    | (AVar) a i where "v=(Lit a).[Lit i]"
    1.29 +  using ground LVar FVar AVar
    1.30 +  apply (cases v)
    1.31 +  apply (simp add: groundVar_def)
    1.32 +  apply (simp add: groundVar_def,blast)
    1.33 +  apply (simp add: groundVar_def,blast)
    1.34 +  apply (simp add: groundVar_def)
    1.35 +  done
    1.36  
    1.37  definition
    1.38    groundExprs :: "expr list \<Rightarrow> bool"