Adapted to changes in cases method.
authorberghofe
Sat Jan 30 17:03:46 2010 +0100 (2010-01-30)
changeset 3499081e8fdfeb849
parent 34989 b5c6e59e2cd7
child 34991 1adaefa63c5a
Adapted to changes in cases method.
src/HOL/Bali/DeclConcepts.thy
src/HOL/IMP/Transition.thy
src/HOL/Lambda/Eta.thy
src/HOL/Nominal/Examples/Pattern.thy
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sat Jan 30 17:01:01 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sat Jan 30 17:03:46 2010 +0100
     1.3 @@ -915,23 +915,15 @@
     1.4      assume "G \<turnstile> m member_of C"
     1.5      then show "n=m"
     1.6      proof (cases)
     1.7 -      case (Immediate m' _)
     1.8 -      with eqid 
     1.9 -      have "m=m'"
    1.10 -           "memberid n = memberid m" 
    1.11 -           "G\<turnstile> mbr m declared_in C" 
    1.12 -           "declclass m = C"
    1.13 -        by auto
    1.14 -      with member_n   
    1.15 +      case Immediate
    1.16 +      with eqid member_n
    1.17        show ?thesis
    1.18          by (cases n, cases m) 
    1.19             (auto simp add: declared_in_def 
    1.20                             cdeclaredmethd_def cdeclaredfield_def
    1.21                      split: memberdecl.splits)
    1.22      next
    1.23 -      case (Inherited m' _ _)
    1.24 -      then have "G\<turnstile> memberid m undeclared_in C"
    1.25 -        by simp
    1.26 +      case Inherited
    1.27        with eqid member_n
    1.28        show ?thesis
    1.29          by (cases n) (auto dest: declared_not_undeclared)
    1.30 @@ -1656,10 +1648,7 @@
    1.31      from member_of
    1.32      show "?Methd C"
    1.33      proof (cases)
    1.34 -      case (Immediate membr Ca)
    1.35 -      then have "Ca=C" "membr = method sig m" and 
    1.36 -                "G\<turnstile>Methd sig m declared_in C" "declclass m = C"
    1.37 -        by (cases m,auto)
    1.38 +      case Immediate
    1.39        with clsC 
    1.40        have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m"
    1.41          by (cases m)
    1.42 @@ -1669,13 +1658,12 @@
    1.43        show ?thesis
    1.44          by (simp add: methd_rec)
    1.45      next
    1.46 -      case (Inherited membr Ca S)
    1.47 +      case (Inherited S)
    1.48        with clsC
    1.49 -      have eq_Ca_C: "Ca=C" and
    1.50 -            undecl: "G\<turnstile>mid sig undeclared_in C" and
    1.51 +      have  undecl: "G\<turnstile>mid sig undeclared_in C" and
    1.52               super: "G \<turnstile>Methd sig m member_of (super c)"
    1.53          by (auto dest: subcls1D)
    1.54 -      from eq_Ca_C clsC undecl 
    1.55 +      from clsC undecl 
    1.56        have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = None"
    1.57          by (auto simp add: undeclared_in_def cdeclaredmethd_def
    1.58                      intro: table_of_mapconst_NoneI)
     2.1 --- a/src/HOL/IMP/Transition.thy	Sat Jan 30 17:01:01 2010 +0100
     2.2 +++ b/src/HOL/IMP/Transition.thy	Sat Jan 30 17:03:46 2010 +0100
     2.3 @@ -205,20 +205,16 @@
     2.4      (is "\<exists>i j s'. ?Q i j s'")
     2.5    proof (cases set: evalc1)
     2.6      case Semi1
     2.7 -    then obtain s' where
     2.8 -        "co = Some c2" and "s''' = s'" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
     2.9 -      by auto
    2.10 -    with 1 n have "?Q 1 n s'" by simp
    2.11 +    from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n
    2.12 +    have "?Q 1 n s'''" by simp
    2.13      thus ?thesis by blast
    2.14    next
    2.15 -    case Semi2
    2.16 -    then obtain c1' s' where
    2.17 -        "co = Some (c1'; c2)" "s''' = s'" and
    2.18 -        c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
    2.19 -      by auto
    2.20 -    with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
    2.21 +    case (Semi2 c1')
    2.22 +    note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>`
    2.23 +    with `co = Some (c1'; c2)` and n
    2.24 +    have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
    2.25      with Suc.hyps obtain i j s0 where
    2.26 -        c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
    2.27 +        c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
    2.28          c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
    2.29          i:   "n = i+j"
    2.30        by fast
    2.31 @@ -228,7 +224,7 @@
    2.32      with c2 i
    2.33      have "?Q (i+1) j s0" by simp
    2.34      thus ?thesis by blast
    2.35 -  qed auto -- "the remaining cases cannot occur"
    2.36 +  qed
    2.37  qed
    2.38  
    2.39  
     3.1 --- a/src/HOL/Lambda/Eta.thy	Sat Jan 30 17:01:01 2010 +0100
     3.2 +++ b/src/HOL/Lambda/Eta.thy	Sat Jan 30 17:03:46 2010 +0100
     3.3 @@ -273,13 +273,13 @@
     3.4        by (rule eta_case)
     3.5      with eta show ?thesis by simp
     3.6    next
     3.7 -    case (abs r u)
     3.8 -    hence "r \<rightarrow>\<^sub>\<eta> s'" by simp
     3.9 -    then obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
    3.10 +    case (abs r)
    3.11 +    from `r \<rightarrow>\<^sub>\<eta> s'`
    3.12 +    obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
    3.13      from r have "Abs r => Abs t'" ..
    3.14      moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs)
    3.15      ultimately show ?thesis using abs by simp iprover
    3.16 -  qed simp_all
    3.17 +  qed
    3.18  next
    3.19    case (app u u' t t')
    3.20    from `s \<rightarrow>\<^sub>\<eta> u \<degree> t` show ?case
    3.21 @@ -291,20 +291,20 @@
    3.22        by (rule eta_case)
    3.23      with eta show ?thesis by simp
    3.24    next
    3.25 -    case (appL s' t'' u'')
    3.26 -    hence "s' \<rightarrow>\<^sub>\<eta> u" by simp
    3.27 -    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
    3.28 +    case (appL s')
    3.29 +    from `s' \<rightarrow>\<^sub>\<eta> u`
    3.30 +    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
    3.31      from s' and app have "s' \<degree> t => r \<degree> t'" by simp
    3.32      moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL)
    3.33      ultimately show ?thesis using appL by simp iprover
    3.34    next
    3.35 -    case (appR s' t'' u'')
    3.36 -    hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
    3.37 -    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
    3.38 +    case (appR s')
    3.39 +    from `s' \<rightarrow>\<^sub>\<eta> t`
    3.40 +    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
    3.41      from s' and app have "u \<degree> s' => u' \<degree> r" by simp
    3.42      moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR)
    3.43      ultimately show ?thesis using appR by simp iprover
    3.44 -  qed simp
    3.45 +  qed
    3.46  next
    3.47    case (beta u u' t t')
    3.48    from `s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t` show ?case
    3.49 @@ -316,9 +316,8 @@
    3.50        by (rule eta_case)
    3.51      with eta show ?thesis by simp
    3.52    next
    3.53 -    case (appL s' t'' u'')
    3.54 -    hence "s' \<rightarrow>\<^sub>\<eta> Abs u" by simp
    3.55 -    thus ?thesis
    3.56 +    case (appL s')
    3.57 +    from `s' \<rightarrow>\<^sub>\<eta> Abs u` show ?thesis
    3.58      proof cases
    3.59        case (eta s'' dummy)
    3.60        have "Abs (lift u 1) = lift (Abs u) 0" by simp
    3.61 @@ -332,23 +331,23 @@
    3.62        with s have "s => u'[t'/0]" by simp
    3.63        thus ?thesis by iprover
    3.64      next
    3.65 -      case (abs r r')
    3.66 -      hence "r \<rightarrow>\<^sub>\<eta> u" by simp
    3.67 -      then obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
    3.68 +      case (abs r)
    3.69 +      from `r \<rightarrow>\<^sub>\<eta> u`
    3.70 +      obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
    3.71        from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp
    3.72        moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
    3.73          by (rule rtrancl_eta_subst')
    3.74        ultimately show ?thesis using abs and appL by simp iprover
    3.75 -    qed simp_all
    3.76 +    qed
    3.77    next
    3.78 -    case (appR s' t'' u'')
    3.79 -    hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
    3.80 -    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
    3.81 +    case (appR s')
    3.82 +    from `s' \<rightarrow>\<^sub>\<eta> t`
    3.83 +    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
    3.84      from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp
    3.85      moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
    3.86        by (rule rtrancl_eta_subst'')
    3.87      ultimately show ?thesis using appR by simp iprover
    3.88 -  qed simp
    3.89 +  qed
    3.90  qed
    3.91  
    3.92  theorem eta_postponement':
     4.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Sat Jan 30 17:01:01 2010 +0100
     4.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Sat Jan 30 17:03:46 2010 +0100
     4.3 @@ -575,13 +575,13 @@
     4.4    and R: "\<And>U. S = T \<rightarrow> U \<Longrightarrow> (x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> P"
     4.5    shows P using ty
     4.6  proof cases
     4.7 -  case (Abs x' T' \<Gamma>' t' U)
     4.8 +  case (Abs x' T' t' U)
     4.9    obtain y::name where y: "y \<sharp> (x, \<Gamma>, \<lambda>x':T'. t')"
    4.10      by (rule exists_fresh) (auto intro: fin_supp)
    4.11    from `(\<lambda>x:T. t) = (\<lambda>x':T'. t')` [symmetric]
    4.12    have x: "x \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
    4.13    have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
    4.14 -  from `(x', T') # \<Gamma>' \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>'"
    4.15 +  from `(x', T') # \<Gamma> \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>"
    4.16      by (auto dest: valid_typing)
    4.17    have "(\<lambda>x:T. t) = (\<lambda>x':T'. t')" by fact
    4.18    also from x x' y have "\<dots> = [(x, y)] \<bullet> [(x', y)] \<bullet> (\<lambda>x':T'. t')"
    4.19 @@ -592,10 +592,10 @@
    4.20    then have T: "T = T'" and t: "[(x, y)] \<bullet> [(x', y)] \<bullet> t' = t"
    4.21      by (simp_all add: trm.inject alpha)
    4.22    from Abs T have "S = T \<rightarrow> U" by simp
    4.23 -  moreover from `(x', T') # \<Gamma>' \<turnstile> t' : U`
    4.24 -  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma>' \<turnstile> t' : U)"
    4.25 +  moreover from `(x', T') # \<Gamma> \<turnstile> t' : U`
    4.26 +  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma> \<turnstile> t' : U)"
    4.27      by (simp add: perm_bool)
    4.28 -  with T t y `\<Gamma> = \<Gamma>'` x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
    4.29 +  with T t y x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
    4.30      by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
    4.31    ultimately show ?thesis by (rule R)
    4.32  qed simp_all
    4.33 @@ -764,7 +764,7 @@
    4.34    and R: "\<And>T \<Delta>. \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> P"
    4.35    shows P using ty
    4.36  proof cases
    4.37 -  case (Let p' t' \<Gamma>' T \<Delta> u' U')
    4.38 +  case (Let p' t' T \<Delta> u')
    4.39    then have "(supp \<Delta>::name set) \<sharp>* \<Gamma>"
    4.40      by (auto intro: valid_typing valid_app_freshs)
    4.41    with Let have "(supp p'::name set) \<sharp>* \<Gamma>"
    4.42 @@ -776,7 +776,7 @@
    4.43    moreover from Let have "pat_type p = pat_type p'"
    4.44      by (simp add: trm.inject)
    4.45    moreover note distinct
    4.46 -  moreover from `\<Delta> @ \<Gamma>' \<turnstile> u' : U'` have "valid (\<Delta> @ \<Gamma>')"
    4.47 +  moreover from `\<Delta> @ \<Gamma> \<turnstile> u' : U` have "valid (\<Delta> @ \<Gamma>)"
    4.48      by (rule valid_typing)
    4.49    then have "valid \<Delta>" by (rule valid_appD)
    4.50    with `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "distinct (pat_vars p')"