case_split_tac (works without context);
authorwenzelm
Tue Jun 10 16:43:14 2008 +0200 (2008-06-10)
changeset 2711797e9dae57284
parent 27116 56617a7b68c5
child 27118 9a26c0d7a47a
case_split_tac (works without context);
src/HOL/MicroJava/Comp/Index.thy
src/HOL/Nominal/Examples/Class.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
     1.1 --- a/src/HOL/MicroJava/Comp/Index.thy	Tue Jun 10 16:43:07 2008 +0200
     1.2 +++ b/src/HOL/MicroJava/Comp/Index.thy	Tue Jun 10 16:43:14 2008 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    \<Longrightarrow> (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) = 
     1.5       the (loc x)"
     1.6  apply (simp only: index_def gjmb_plns_def)
     1.7 -apply (case_tac "(gmb G C S)")
     1.8 +apply (case_tac "gmb G C S" rule: prod.exhaust)
     1.9  apply (simp add: galldefs del: set_append map_append)
    1.10  apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
    1.11  apply (intro strip)
    1.12 @@ -74,7 +74,7 @@
    1.13    locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
    1.14            locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
    1.15  apply (simp only: locvars_xstate_def locvars_locals_def index_def)
    1.16 -apply (case_tac "(gmb G C S)", simp)
    1.17 +apply (case_tac "gmb G C S" rule: prod.exhaust, simp)
    1.18  apply (case_tac b, simp)
    1.19  apply (rule conjI)
    1.20  apply (simp add: gl_def)
     2.1 --- a/src/HOL/Nominal/Examples/Class.thy	Tue Jun 10 16:43:07 2008 +0200
     2.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Tue Jun 10 16:43:14 2008 +0200
     2.3 @@ -16599,7 +16599,7 @@
     2.4               \<Longrightarrow> P (x1,x2,x3)"  
     2.5   shows "P (x1,x2,x3)"
     2.6  apply(rule_tac my_wf_induct_triple[OF a])
     2.7 -apply(case_tac x)
     2.8 +apply(case_tac x rule: prod.exhaust)
     2.9  apply(simp)
    2.10  apply(case_tac b)
    2.11  apply(simp)
     3.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Jun 10 16:43:07 2008 +0200
     3.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Jun 10 16:43:14 2008 +0200
     3.3 @@ -763,12 +763,11 @@
     3.4  *)
     3.5  ML {*
     3.6  fun split_idle_tac ss simps i =
     3.7 -    EVERY [TRY (rtac @{thm actionI} i),
     3.8 -           DatatypePackage.case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
     3.9 -           rewrite_goals_tac @{thms action_rews},
    3.10 -           forward_tac [temp_use @{thm Step1_4_7}] i,
    3.11 -           asm_full_simp_tac (ss addsimps simps) i
    3.12 -          ]
    3.13 +  TRY (rtac @{thm actionI} i) THEN
    3.14 +  case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
    3.15 +  rewrite_goals_tac @{thms action_rews} THEN
    3.16 +  forward_tac [temp_use @{thm Step1_4_7}] i THEN
    3.17 +  asm_full_simp_tac (ss addsimps simps) i
    3.18  *}
    3.19  (* ----------------------------------------------------------------------
    3.20     Combine steps 1.2 and 1.4 to prove that the implementation satisfies