adapted case_tac/induct_tac;
authorwenzelm
Mon Jun 09 17:07:08 2008 +0200 (2008-06-09 ago)
changeset 27095c1c27955d7dd
parent 27094 2cf13a72e170
child 27096 d4145c286bd1
adapted case_tac/induct_tac;
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOLCF/Tools/domain/domain_theorems.ML
     1.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Sun Jun 08 14:31:06 2008 +0200
     1.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Mon Jun 09 17:07:08 2008 +0200
     1.3 @@ -1207,7 +1207,7 @@
     1.4  --{* 34 subgoals left *}
     1.5  apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     1.6  apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     1.7 -apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
     1.8 +apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
     1.9  apply(simp_all add:Graph10)
    1.10  --{* 47 subgoals left *}
    1.11  apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
     2.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Sun Jun 08 14:31:06 2008 +0200
     2.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon Jun 09 17:07:08 2008 +0200
     2.3 @@ -196,7 +196,7 @@
     2.4  apply fastsimp
     2.5  --{* 5 subgoals left *}
     2.6  prefer 5
     2.7 -apply(tactic {* ALLGOALS (case_tac "j=k") *})
     2.8 +apply(case_tac [!] "j=k")
     2.9  --{* 10 subgoals left *}
    2.10  apply simp_all
    2.11  apply(erule_tac x=k in allE)
    2.12 @@ -502,8 +502,8 @@
    2.13  
    2.14  lemma Example2_lemma2_aux2: 
    2.15    "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
    2.16 -apply(induct j)
    2.17 - apply (simp_all cong:setsum_cong)
    2.18 +apply(induct j) 
    2.19 + apply simp_all
    2.20  done
    2.21  
    2.22  lemma Example2_lemma2: 
     3.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun Jun 08 14:31:06 2008 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Jun 09 17:07:08 2008 +0200
     3.3 @@ -94,7 +94,7 @@
     3.4                val stmnt2 = HOLogic.mk_Trueprop
     3.5                    (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
     3.6  
     3.7 -              val proof2 = fn _ => EVERY [case_tac "y" 1,
     3.8 +              val proof2 = fn _ => EVERY [DatatypePackage.case_tac "y" 1,
     3.9                                            asm_simp_tac (HOL_basic_ss addsimps simp1) 1,
    3.10                                            rtac @{thm exI} 1,
    3.11                                            rtac @{thm refl} 1]
     4.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Jun 08 14:31:06 2008 +0200
     4.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Jun 09 17:07:08 2008 +0200
     4.3 @@ -96,7 +96,7 @@
     4.4    in pg'' thy defs t tacs end;
     4.5  
     4.6  fun case_UU_tac rews i v =
     4.7 -  case_tac (v^"=UU") i THEN
     4.8 +  DatatypePackage.case_tac (v^"=UU") i THEN
     4.9    asm_simp_tac (HOLCF_ss addsimps rews) i;
    4.10  
    4.11  val chain_tac =
    4.12 @@ -647,7 +647,7 @@
    4.13        fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
    4.14        val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
    4.15        val tacs = [
    4.16 -        induct_tac "n" 1,
    4.17 +        DatatypePackage.induct_tac "n" 1,
    4.18          simp_tac iterate_Cprod_ss 1,
    4.19          asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
    4.20      in pg copy_take_defs goal tacs end;
    4.21 @@ -678,7 +678,7 @@
    4.22        fun eq_tacs ((dn, _), cons) = map con_tac cons;
    4.23        val tacs =
    4.24          simp_tac iterate_Cprod_ss 1 ::
    4.25 -        induct_tac "n" 1 ::
    4.26 +        DatatypePackage.induct_tac "n" 1 ::
    4.27          simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
    4.28          asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
    4.29          TRY (safe_tac HOL_cs) ::
    4.30 @@ -750,7 +750,7 @@
    4.31            val tacs1 = [
    4.32              quant_tac 1,
    4.33              simp_tac HOL_ss 1,
    4.34 -            induct_tac "n" 1,
    4.35 +            DatatypePackage.induct_tac "n" 1,
    4.36              simp_tac (take_ss addsimps prems) 1,
    4.37              TRY (safe_tac HOL_cs)];
    4.38            fun arg_tac arg =
    4.39 @@ -845,7 +845,7 @@
    4.40                maps con_tacs cons;
    4.41              val tacs =
    4.42                rtac allI 1 ::
    4.43 -              induct_tac "n" 1 ::
    4.44 +              DatatypePackage.induct_tac "n" 1 ::
    4.45                simp_tac take_ss 1 ::
    4.46                TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
    4.47                flat (mapn foo_tacs 1 (conss ~~ cases));
    4.48 @@ -938,7 +938,7 @@
    4.49          REPEAT (CHANGED (asm_simp_tac take_ss 1))];
    4.50        val tacs = [
    4.51          rtac impI 1,
    4.52 -        induct_tac "n" 1,
    4.53 +        DatatypePackage.induct_tac "n" 1,
    4.54          simp_tac take_ss 1,
    4.55          safe_tac HOL_cs] @
    4.56          flat (mapn x_tacs 0 xs);