Renamed expand_const -> split_const.
authornipkow
Mon Apr 27 16:45:27 1998 +0200 (1998-04-27)
changeset 4831dae4d63a1318
parent 4830 bd73675adbed
child 4832 bc11b5b06f87
Renamed expand_const -> split_const.
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/AxClasses/Lattice/Order.ML
src/HOL/IOA/IOA.ML
src/HOL/IOA/Solve.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/PropLog.ML
src/HOL/Induct/SList.ML
src/HOL/Induct/Simult.ML
src/HOL/Integ/Integ.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Lambda.ML
src/HOL/W0/I.ML
src/HOL/W0/Maybe.ML
src/HOL/W0/W.ML
src/HOL/ex/set.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Mon Apr 27 16:45:11 1998 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Mon Apr 27 16:45:27 1998 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4  by (ALLGOALS 
     1.5      (asm_simp_tac 
     1.6       (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
     1.7 -			  pushes @ expand_ifs))));
     1.8 +			  pushes @ split_ifs))));
     1.9  (*Oops*)
    1.10  by (blast_tac (claset() addSDs [unique_session_keys]) 5);
    1.11  (*NS3, replay sub-case*) 
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Apr 27 16:45:11 1998 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Apr 27 16:45:27 1998 +0200
     2.3 @@ -320,7 +320,7 @@
     2.4  by (ALLGOALS
     2.5      (asm_simp_tac (simpset() addcongs [conj_cong] 
     2.6                               addsimps [analz_insert_eq, analz_insert_freshK]
     2.7 -                             addsimps (pushes@expand_ifs))));
     2.8 +                             addsimps (pushes@split_ifs))));
     2.9  (*Oops*)
    2.10  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    2.11  (*OR4*) 
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Apr 27 16:45:11 1998 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Apr 27 16:45:27 1998 +0200
     3.3 @@ -256,7 +256,7 @@
     3.4  by (ALLGOALS
     3.5      (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
     3.6                               addsimps [analz_insert_eq, analz_insert_freshK]
     3.7 -                             addsimps (pushes@expand_ifs))));
     3.8 +                             addsimps (pushes@split_ifs))));
     3.9  (*Oops*)
    3.10  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    3.11  (*OR4*) 
     4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Apr 27 16:45:11 1998 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Apr 27 16:45:27 1998 +0200
     4.3 @@ -222,7 +222,7 @@
     4.4  by (ALLGOALS
     4.5      (asm_simp_tac (simpset() addcongs [conj_cong] 
     4.6                               addsimps [analz_insert_eq, analz_insert_freshK]
     4.7 -                             addsimps (pushes@expand_ifs))));
     4.8 +                             addsimps (pushes@split_ifs))));
     4.9  (*Oops*)
    4.10  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    4.11  (*OR4*) 
     5.1 --- a/src/HOL/Auth/Recur.ML	Mon Apr 27 16:45:11 1998 +0200
     5.2 +++ b/src/HOL/Auth/Recur.ML	Mon Apr 27 16:45:27 1998 +0200
     5.3 @@ -409,7 +409,7 @@
     5.4  by (ALLGOALS (*6 seconds*)
     5.5      (asm_simp_tac 
     5.6       (analz_image_freshK_ss 
     5.7 -        addsimps expand_ifs
     5.8 +        addsimps split_ifs
     5.9  	addsimps 
    5.10            [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
    5.11  by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib])));
    5.12 @@ -438,7 +438,7 @@
    5.13  by analz_spies_tac;
    5.14  by (ALLGOALS
    5.15      (asm_simp_tac
    5.16 -     (simpset() addsimps (expand_ifs @
    5.17 +     (simpset() addsimps (split_ifs @
    5.18  			 [analz_insert_eq, analz_insert_freshK]))));
    5.19  (*RA4*)
    5.20  by (spy_analz_tac 5);
     6.1 --- a/src/HOL/Auth/TLS.ML	Mon Apr 27 16:45:11 1998 +0200
     6.2 +++ b/src/HOL/Auth/TLS.ML	Mon Apr 27 16:45:27 1998 +0200
     6.3 @@ -193,7 +193,7 @@
     6.4      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     6.5      ALLGOALS (asm_simp_tac 
     6.6                (simpset() addcongs [if_weak_cong]
     6.7 -                         addsimps (expand_ifs@pushes)))  THEN
     6.8 +                         addsimps (split_ifs@pushes)))  THEN
     6.9      (*Remove instances of pubK B:  the Spy already knows all public keys.
    6.10        Combining the two simplifier calls makes them run extremely slowly.*)
    6.11      ALLGOALS (asm_simp_tac 
    6.12 @@ -405,7 +405,7 @@
    6.13  by (REPEAT_FIRST (rtac analz_image_keys_lemma));
    6.14  by (ALLGOALS    (*18 seconds*)
    6.15      (asm_simp_tac (analz_image_keys_ss 
    6.16 -		   addsimps (expand_ifs@pushes)
    6.17 +		   addsimps (split_ifs@pushes)
    6.18  		   addsimps [range_sessionkeys_not_priK, 
    6.19                               analz_image_priK, certificate_def])));
    6.20  by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
     7.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Apr 27 16:45:11 1998 +0200
     7.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Apr 27 16:45:27 1998 +0200
     7.3 @@ -213,7 +213,7 @@
     7.4  by analz_spies_tac;
     7.5  by (ALLGOALS
     7.6      (asm_simp_tac 
     7.7 -     (simpset() addsimps (expand_ifs@pushes)
     7.8 +     (simpset() addsimps (split_ifs@pushes)
     7.9  	        addsimps [analz_insert_eq, analz_insert_freshK])));
    7.10  (*Oops*)
    7.11  by (blast_tac (claset() addDs [unique_session_keys]) 3);
    7.12 @@ -384,7 +384,7 @@
    7.13  by (ALLGOALS  (*12 seconds*)
    7.14      (asm_simp_tac 
    7.15       (analz_image_freshK_ss 
    7.16 -       addsimps expand_ifs
    7.17 +       addsimps split_ifs
    7.18         addsimps [all_conj_distrib, analz_image_freshK,
    7.19  		 KeyWithNonce_Says, KeyWithNonce_Notes,
    7.20  		 fresh_not_KeyWithNonce, 
    7.21 @@ -499,7 +499,7 @@
    7.22  by analz_spies_tac;
    7.23  by (ALLGOALS
    7.24      (asm_simp_tac 
    7.25 -     (simpset() addsimps (expand_ifs@pushes)
    7.26 +     (simpset() addsimps (split_ifs@pushes)
    7.27  	        addsimps [analz_insert_eq, analz_insert_freshK])));
    7.28  (*Prove YM3 by showing that no NB can also be an NA*)
    7.29  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
     8.1 --- a/src/HOL/Auth/Yahalom2.ML	Mon Apr 27 16:45:11 1998 +0200
     8.2 +++ b/src/HOL/Auth/Yahalom2.ML	Mon Apr 27 16:45:27 1998 +0200
     8.3 @@ -215,7 +215,7 @@
     8.4  by analz_spies_tac;
     8.5  by (ALLGOALS
     8.6      (asm_simp_tac 
     8.7 -     (simpset() addsimps expand_ifs
     8.8 +     (simpset() addsimps split_ifs
     8.9  	        addsimps [analz_insert_eq, analz_insert_freshK])));
    8.10  (*Oops*)
    8.11  by (blast_tac (claset() addDs [unique_session_keys]) 3);
     9.1 --- a/src/HOL/AxClasses/Lattice/Order.ML	Mon Apr 27 16:45:11 1998 +0200
     9.2 +++ b/src/HOL/AxClasses/Lattice/Order.ML	Mon Apr 27 16:45:27 1998 +0200
     9.3 @@ -115,7 +115,7 @@
     9.4  (** limits in linear orders **)
     9.5  
     9.6  goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
     9.7 -  by (stac expand_if 1);
     9.8 +  by (stac split_if 1);
     9.9    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
    9.10    (*case "x [= y"*)
    9.11      by (rtac le_refl 1);
    9.12 @@ -131,7 +131,7 @@
    9.13  qed "min_is_inf";
    9.14  
    9.15  goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
    9.16 -  by (stac expand_if 1);
    9.17 +  by (stac split_if 1);
    9.18    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
    9.19    (*case "x [= y"*)
    9.20      by (assume_tac 1);
    10.1 --- a/src/HOL/IOA/IOA.ML	Mon Apr 27 16:45:11 1998 +0200
    10.2 +++ b/src/HOL/IOA/IOA.ML	Mon Apr 27 16:45:27 1998 +0200
    10.3 @@ -32,7 +32,7 @@
    10.4    by (rtac ext 1);
    10.5    by (exhaust_tac "s(i)" 1);
    10.6    by (Asm_simp_tac 1);
    10.7 -  by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    10.8 +  by (Asm_simp_tac 1);
    10.9  qed "filter_oseq_idemp";
   10.10  
   10.11  goalw IOA.thy [mk_trace_def,filter_oseq_def]
   10.12 @@ -42,7 +42,7 @@
   10.13  \  (mk_trace A s n = Some(a)) =                                   \
   10.14  \   (s(n)=Some(a) & a : externals(asig_of(A)))";
   10.15    by (exhaust_tac "s(n)" 1);
   10.16 -  by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   10.17 +  by (ALLGOALS Asm_simp_tac);
   10.18    by (Fast_tac 1);
   10.19  qed "mk_trace_thm";
   10.20  
   10.21 @@ -138,8 +138,7 @@
   10.22  \     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
   10.23  \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
   10.24    by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
   10.25 -                            ioa_projections)
   10.26 -                  addsplits [expand_if]) 1);
   10.27 +                            ioa_projections)) 1);
   10.28  qed "trans_of_par4";
   10.29  
   10.30  goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
    11.1 --- a/src/HOL/IOA/Solve.ML	Mon Apr 27 16:45:11 1998 +0200
    11.2 +++ b/src/HOL/IOA/Solve.ML	Mon Apr 27 16:45:27 1998 +0200
    11.3 @@ -102,7 +102,7 @@
    11.4                  addsplits [split_option_case]) 1);
    11.5  qed"comp2_reachable";
    11.6  
    11.7 -Delsplits [expand_if];
    11.8 +Delsplits [split_if];
    11.9  
   11.10  (* Composition of possibility-mappings *)
   11.11  goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
   11.12 @@ -121,7 +121,7 @@
   11.13  by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
   11.14  by (simp_tac (simpset() addsimps [par_def]) 1);
   11.15  by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
   11.16 -by (stac expand_if 1);
   11.17 +by (stac split_if 1);
   11.18  by (rtac conjI 1);
   11.19  by (rtac impI 1); 
   11.20  by (etac disjE 1);
   11.21 @@ -142,7 +142,7 @@
   11.22  by (Asm_full_simp_tac 2);
   11.23  by (Fast_tac 2);
   11.24  by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
   11.25 -                 addsplits [expand_if]) 1);
   11.26 +                 addsplits [split_if]) 1);
   11.27  by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   11.28          asm_full_simp_tac(simpset() addsimps[comp1_reachable,
   11.29                                        comp2_reachable])1));
   11.30 @@ -176,7 +176,7 @@
   11.31  by (simp_tac (simpset() addsimps [rename_def]) 1);
   11.32  by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
   11.33  by Safe_tac;
   11.34 -by (stac expand_if 1);
   11.35 +by (stac split_if 1);
   11.36   by (rtac conjI 1);
   11.37   by (rtac impI 1);
   11.38   by (etac disjE 1);
   11.39 @@ -209,4 +209,4 @@
   11.40  by Auto_tac;
   11.41  qed"rename_through_pmap";
   11.42  
   11.43 -Addsplits [expand_if];
   11.44 +Addsplits [split_if];
    12.1 --- a/src/HOL/Induct/LList.ML	Mon Apr 27 16:45:11 1998 +0200
    12.2 +++ b/src/HOL/Induct/LList.ML	Mon Apr 27 16:45:27 1998 +0200
    12.3 @@ -6,13 +6,11 @@
    12.4  SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
    12.5  *)
    12.6  
    12.7 -open LList;
    12.8 -
    12.9  bind_thm ("UN1_I", UNIV_I RS UN_I);
   12.10  
   12.11  (** Simplification **)
   12.12  
   12.13 -simpset_ref() := simpset() addsplits [expand_split, expand_sum_case];
   12.14 +simpset_ref() := simpset() addsplits [split_split, split_sum_case];
   12.15  
   12.16  
   12.17  (*This justifies using llist in other recursive type definitions*)
   12.18 @@ -68,11 +66,11 @@
   12.19  
   12.20  (*UNUSED; obsolete?
   12.21  goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
   12.22 -by (simp_tac (simpset() addsplits [expand_split]) 1);
   12.23 +by (Simp_tac 1);
   12.24  qed "split_UN1";
   12.25  
   12.26  goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
   12.27 -by (simp_tac (simpset() addsplits [expand_sum_case]) 1);
   12.28 +by (Simp_tac 1);
   12.29  qed "sum_case2_UN1";
   12.30  *)
   12.31  
   12.32 @@ -318,7 +316,7 @@
   12.33  by (rename_tac "y" 1);
   12.34  by (stac prem1 1);
   12.35  by (stac prem2 1);
   12.36 -by (simp_tac (simpset() addsplits [expand_sum_case]) 1);
   12.37 +by (Simp_tac 1);
   12.38  by (strip_tac 1);
   12.39  by (res_inst_tac [("n", "n")] natE 1);
   12.40  by (rename_tac "m" 2);
   12.41 @@ -366,15 +364,15 @@
   12.42  by (rtac Rep_llist_inverse 1);
   12.43  qed "inj_Rep_llist";
   12.44  
   12.45 -goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
   12.46 -by (rtac inj_onto_inverseI 1);
   12.47 +goal LList.thy "inj_on Abs_llist (llist(range Leaf))";
   12.48 +by (rtac inj_on_inverseI 1);
   12.49  by (etac Abs_llist_inverse 1);
   12.50 -qed "inj_onto_Abs_llist";
   12.51 +qed "inj_on_Abs_llist";
   12.52  
   12.53  (** Distinctness of constructors **)
   12.54  
   12.55  goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil";
   12.56 -by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1);
   12.57 +by (rtac (CONS_not_NIL RS (inj_on_Abs_llist RS inj_on_contraD)) 1);
   12.58  by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
   12.59  qed "LCons_not_LNil";
   12.60  
   12.61 @@ -408,7 +406,7 @@
   12.62  (*For reasoning about abstract llist constructors*)
   12.63  
   12.64  AddIs ([Rep_llist]@llist.intrs);
   12.65 -AddSDs [inj_onto_Abs_llist RS inj_ontoD,
   12.66 +AddSDs [inj_on_Abs_llist RS inj_onD,
   12.67          inj_Rep_llist RS injD, Leaf_inject];
   12.68  
   12.69  goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
    13.1 --- a/src/HOL/Induct/PropLog.ML	Mon Apr 27 16:45:11 1998 +0200
    13.2 +++ b/src/HOL/Induct/PropLog.ML	Mon Apr 27 16:45:27 1998 +0200
    13.3 @@ -101,7 +101,7 @@
    13.4  
    13.5  (*This formulation is required for strong induction hypotheses*)
    13.6  goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)";
    13.7 -by (rtac (expand_if RS iffD2) 1);
    13.8 +by (rtac (split_if RS iffD2) 1);
    13.9  by (PropLog.pl.induct_tac "p" 1);
   13.10  by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
   13.11  by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
    14.1 --- a/src/HOL/Induct/SList.ML	Mon Apr 27 16:45:11 1998 +0200
    14.2 +++ b/src/HOL/Induct/SList.ML	Mon Apr 27 16:45:27 1998 +0200
    14.3 @@ -54,10 +54,10 @@
    14.4  by (rtac Rep_list_inverse 1);
    14.5  qed "inj_Rep_list";
    14.6  
    14.7 -goal SList.thy "inj_onto Abs_list (list(range Leaf))";
    14.8 -by (rtac inj_onto_inverseI 1);
    14.9 +goal SList.thy "inj_on Abs_list (list(range Leaf))";
   14.10 +by (rtac inj_on_inverseI 1);
   14.11  by (etac Abs_list_inverse 1);
   14.12 -qed "inj_onto_Abs_list";
   14.13 +qed "inj_on_Abs_list";
   14.14  
   14.15  (** Distinctness of constructors **)
   14.16  
   14.17 @@ -70,7 +70,7 @@
   14.18  val NIL_neq_CONS = sym RS CONS_neq_NIL;
   14.19  
   14.20  goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil";
   14.21 -by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1);
   14.22 +by (rtac (CONS_not_NIL RS (inj_on_Abs_list RS inj_on_contraD)) 1);
   14.23  by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
   14.24  qed "Cons_not_Nil";
   14.25  
   14.26 @@ -87,7 +87,7 @@
   14.27  
   14.28  AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
   14.29  
   14.30 -AddSDs [inj_onto_Abs_list RS inj_ontoD,
   14.31 +AddSDs [inj_on_Abs_list RS inj_onD,
   14.32          inj_Rep_list RS injD, Leaf_inject];
   14.33  
   14.34  goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
   14.35 @@ -346,7 +346,7 @@
   14.36  \                        (!y ys. xs=y#ys --> P(f y ys)))";
   14.37  by (list_ind_tac "xs" 1);
   14.38  by (ALLGOALS Asm_simp_tac);
   14.39 -qed "expand_list_case2";
   14.40 +qed "split_list_case2";
   14.41  
   14.42  
   14.43  (** Additional mapping lemmas **)
    15.1 --- a/src/HOL/Induct/Simult.ML	Mon Apr 27 16:45:11 1998 +0200
    15.2 +++ b/src/HOL/Induct/Simult.ML	Mon Apr 27 16:45:27 1998 +0200
    15.3 @@ -109,20 +109,20 @@
    15.4  by (rtac Rep_Tree_inverse 1);
    15.5  qed "inj_Rep_Tree";
    15.6  
    15.7 -goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)";
    15.8 -by (rtac inj_onto_inverseI 1);
    15.9 +goal Simult.thy "inj_on Abs_Tree (Part (TF(range Leaf)) In0)";
   15.10 +by (rtac inj_on_inverseI 1);
   15.11  by (etac Abs_Tree_inverse 1);
   15.12 -qed "inj_onto_Abs_Tree";
   15.13 +qed "inj_on_Abs_Tree";
   15.14  
   15.15  goal Simult.thy "inj(Rep_Forest)";
   15.16  by (rtac inj_inverseI 1);
   15.17  by (rtac Rep_Forest_inverse 1);
   15.18  qed "inj_Rep_Forest";
   15.19  
   15.20 -goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)";
   15.21 -by (rtac inj_onto_inverseI 1);
   15.22 +goal Simult.thy "inj_on Abs_Forest (Part (TF(range Leaf)) In1)";
   15.23 +by (rtac inj_on_inverseI 1);
   15.24  by (etac Abs_Forest_inverse 1);
   15.25 -qed "inj_onto_Abs_Forest";
   15.26 +qed "inj_on_Abs_Forest";
   15.27  
   15.28  (** Introduction rules for constructors **)
   15.29  
   15.30 @@ -199,8 +199,8 @@
   15.31                             TCONS_neq_FNIL, FNIL_neq_TCONS,
   15.32                             FCONS_neq_FNIL, FNIL_neq_FCONS,
   15.33                             TCONS_neq_FCONS, FCONS_neq_TCONS];
   15.34 -AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
   15.35 -                           inj_onto_Abs_Forest RS inj_ontoD,
   15.36 +AddSDs [inj_on_Abs_Tree RS inj_onD,
   15.37 +                           inj_on_Abs_Forest RS inj_onD,
   15.38                             inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
   15.39                             Leaf_inject];
   15.40  
    16.1 --- a/src/HOL/Integ/Integ.ML	Mon Apr 27 16:45:11 1998 +0200
    16.2 +++ b/src/HOL/Integ/Integ.ML	Mon Apr 27 16:45:27 1998 +0200
    16.3 @@ -79,12 +79,12 @@
    16.4  by (Fast_tac 1);
    16.5  qed "intrel_in_integ";
    16.6  
    16.7 -goal Integ.thy "inj_onto Abs_Integ Integ";
    16.8 -by (rtac inj_onto_inverseI 1);
    16.9 +goal Integ.thy "inj_on Abs_Integ Integ";
   16.10 +by (rtac inj_on_inverseI 1);
   16.11  by (etac Abs_Integ_inverse 1);
   16.12 -qed "inj_onto_Abs_Integ";
   16.13 +qed "inj_on_Abs_Integ";
   16.14  
   16.15 -Addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff,
   16.16 +Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
   16.17            intrel_iff, intrel_in_integ, Abs_Integ_inverse];
   16.18  
   16.19  goal Integ.thy "inj(Rep_Integ)";
   16.20 @@ -100,7 +100,7 @@
   16.21  goal Integ.thy "inj(znat)";
   16.22  by (rtac injI 1);
   16.23  by (rewtac znat_def);
   16.24 -by (dtac (inj_onto_Abs_Integ RS inj_ontoD) 1);
   16.25 +by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
   16.26  by (REPEAT (rtac intrel_in_integ 1));
   16.27  by (dtac eq_equiv_class 1);
   16.28  by (rtac equiv_intrel 1);
    17.1 --- a/src/HOL/Lambda/Eta.ML	Mon Apr 27 16:45:11 1998 +0200
    17.2 +++ b/src/HOL/Lambda/Eta.ML	Mon Apr 27 16:45:27 1998 +0200
    17.3 @@ -37,7 +37,7 @@
    17.4  by (dB.induct_tac "t" 1);
    17.5  by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
    17.6  by (Blast_tac 2);
    17.7 -by (simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
    17.8 +by (simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
    17.9  by (safe_tac HOL_cs);
   17.10  by (ALLGOALS trans_tac);
   17.11  qed "free_lift";
   17.12 @@ -50,7 +50,7 @@
   17.13  by (Blast_tac 2);
   17.14  by (asm_full_simp_tac (addsplit (simpset())) 2);
   17.15  by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
   17.16 -                      addsplits [expand_nat_case]) 1);
   17.17 +                      addsplits [split_nat_case]) 1);
   17.18  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   17.19  by (ALLGOALS trans_tac);
   17.20  qed "free_subst";
    18.1 --- a/src/HOL/Lambda/Lambda.ML	Mon Apr 27 16:45:11 1998 +0200
    18.2 +++ b/src/HOL/Lambda/Lambda.ML	Mon Apr 27 16:45:27 1998 +0200
    18.3 @@ -46,8 +46,8 @@
    18.4  (*** subst and lift ***)
    18.5  
    18.6  fun addsplit ss = ss addsimps [subst_Var]
    18.7 -                     delsplits [expand_if]
    18.8 -                     setloop (split_inside_tac [expand_if]);
    18.9 +                     delsplits [split_if]
   18.10 +                     setloop (split_inside_tac [split_if]);
   18.11  
   18.12  goal Lambda.thy "(Var k)[u/k] = u";
   18.13  by (asm_full_simp_tac(addsplit(simpset())) 1);
   18.14 @@ -76,7 +76,7 @@
   18.15  \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
   18.16  by (dB.induct_tac "t" 1);
   18.17  by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
   18.18 -                                addsplits [expand_nat_case]
   18.19 +                                addsplits [split_nat_case]
   18.20                                  addSolver cut_trans_tac)));
   18.21  by (safe_tac HOL_cs);
   18.22  by (ALLGOALS trans_tac);
   18.23 @@ -105,9 +105,9 @@
   18.24  by (dB.induct_tac "t" 1);
   18.25  by (ALLGOALS(asm_simp_tac
   18.26        (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
   18.27 -                 delsplits [expand_if]
   18.28 -                 addsplits [expand_nat_case]
   18.29 -                 addloop ("if",split_inside_tac[expand_if])
   18.30 +                 delsplits [split_if]
   18.31 +                 addsplits [split_nat_case]
   18.32 +                 addloop ("if",split_inside_tac[split_if])
   18.33                  addSolver cut_trans_tac)));
   18.34  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   18.35  by (ALLGOALS trans_tac);
    19.1 --- a/src/HOL/W0/I.ML	Mon Apr 27 16:45:11 1998 +0200
    19.2 +++ b/src/HOL/W0/I.ML	Mon Apr 27 16:45:27 1998 +0200
    19.3 @@ -16,10 +16,10 @@
    19.4  
    19.5    (* case Var n *)
    19.6    by (simp_tac (simpset() addsimps [app_subst_list]
    19.7 -      setloop (split_inside_tac [expand_if])) 1);
    19.8 +      setloop (split_inside_tac [split_if])) 1);
    19.9  
   19.10   (* case Abs e *)
   19.11 - by (asm_full_simp_tac (simpset() setloop (split_inside_tac [expand_bind])) 1);
   19.12 + by (asm_full_simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1);
   19.13   by (strip_tac 1);
   19.14   by (rtac conjI 1);
   19.15    by (strip_tac 1);
   19.16 @@ -37,7 +37,7 @@
   19.17                               less_imp_le,lessI]) 1);
   19.18  (** LEVEL 15 **)
   19.19  (* case App e1 e2 *)
   19.20 -by (simp_tac (simpset() setloop (split_inside_tac [expand_bind])) 1);
   19.21 +by (simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1);
   19.22  by (strip_tac 1);
   19.23  by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
   19.24  by (rtac conjI 1);
    20.1 --- a/src/HOL/W0/Maybe.ML	Mon Apr 27 16:45:11 1998 +0200
    20.2 +++ b/src/HOL/W0/Maybe.ML	Mon Apr 27 16:45:27 1998 +0200
    20.3 @@ -16,17 +16,17 @@
    20.4  
    20.5  Addsimps [bind_Ok,bind_Fail];
    20.6  
    20.7 -(* expansion of bind *)
    20.8 +(* case splitting of bind *)
    20.9  goal thy
   20.10    "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
   20.11 -by (maybe.induct_tac "res" 1);
   20.12 +by (induct_tac "res" 1);
   20.13  by (fast_tac (HOL_cs addss simpset()) 1);
   20.14  by (Asm_simp_tac 1);
   20.15 -qed "expand_bind";
   20.16 +qed "split_bind";
   20.17  
   20.18  goal Maybe.thy
   20.19    "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
   20.20 -by (simp_tac (simpset() addsplits [expand_bind]) 1);
   20.21 +by (simp_tac (simpset() addsplits [split_bind]) 1);
   20.22  qed "bind_eq_Fail";
   20.23  
   20.24  Addsimps [bind_eq_Fail];
    21.1 --- a/src/HOL/W0/W.ML	Mon Apr 27 16:45:11 1998 +0200
    21.2 +++ b/src/HOL/W0/W.ML	Mon Apr 27 16:45:27 1998 +0200
    21.3 @@ -17,12 +17,12 @@
    21.4  by (Asm_simp_tac 1);
    21.5  (* case Abs e *)
    21.6  by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
    21.7 -                        addsplits [expand_bind]) 1);
    21.8 +                        addsplits [split_bind]) 1);
    21.9  by (strip_tac 1);
   21.10  by (dtac sym 1);
   21.11  by (fast_tac (HOL_cs addss simpset()) 1);
   21.12  (* case App e1 e2 *)
   21.13 -by (simp_tac (simpset() addsplits [expand_bind]) 1);
   21.14 +by (simp_tac (simpset() addsplits [split_bind]) 1);
   21.15  by (strip_tac 1);
   21.16  by ( rename_tac "sa ta na sb tb nb sc" 1);
   21.17  by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
   21.18 @@ -47,10 +47,10 @@
   21.19  (* case Var(n) *)
   21.20  by (fast_tac (HOL_cs addss simpset()) 1);
   21.21  (* case Abs e *)
   21.22 -by (simp_tac (simpset() addsplits [expand_bind]) 1);
   21.23 +by (simp_tac (simpset() addsplits [split_bind]) 1);
   21.24  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   21.25  (* case App e1 e2 *)
   21.26 -by (simp_tac (simpset() addsplits [expand_bind]) 1);
   21.27 +by (simp_tac (simpset() addsplits [split_bind]) 1);
   21.28  by (strip_tac 1);
   21.29  by (rename_tac "s t na sa ta nb sb sc tb m" 1);
   21.30  by (eres_inst_tac [("x","a")] allE 1);
   21.31 @@ -94,7 +94,7 @@
   21.32          addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
   21.33  (* case Abs e *)
   21.34  by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
   21.35 -    addsplits [expand_bind]) 1);
   21.36 +    addsplits [split_bind]) 1);
   21.37  by (strip_tac 1);
   21.38  by (eres_inst_tac [("x","Suc n")] allE 1);
   21.39  by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
   21.40 @@ -102,7 +102,7 @@
   21.41                addsimps [new_tv_subst,new_tv_Suc_list])) 1);
   21.42  
   21.43  (* case App e1 e2 *)
   21.44 -by (simp_tac (simpset() addsplits [expand_bind]) 1);
   21.45 +by (simp_tac (simpset() addsplits [split_bind]) 1);
   21.46  by (strip_tac 1);
   21.47  by (rename_tac "s t na sa ta nb sb sc tb m" 1);
   21.48  by (eres_inst_tac [("x","n")] allE 1);
   21.49 @@ -162,7 +162,7 @@
   21.50  
   21.51  (* case Abs e *)
   21.52  by (asm_full_simp_tac (simpset() addsimps
   21.53 -    [free_tv_subst] addsplits [expand_bind]) 1);
   21.54 +    [free_tv_subst] addsplits [split_bind]) 1);
   21.55  by (strip_tac 1);
   21.56  by (rename_tac "s t na sa ta m v" 1);
   21.57  by (eres_inst_tac [("x","Suc n")] allE 1);
   21.58 @@ -176,7 +176,7 @@
   21.59                       addss (simpset() addsimps [less_Suc_eq])) 1);
   21.60  (** LEVEL 12 **)
   21.61  (* case App e1 e2 *)
   21.62 -by (simp_tac (simpset() addsplits [expand_bind]) 1);
   21.63 +by (simp_tac (simpset() addsplits [split_bind]) 1);
   21.64  by (strip_tac 1); 
   21.65  by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
   21.66  by (eres_inst_tac [("x","n")] allE 1);
   21.67 @@ -239,7 +239,7 @@
   21.68  by (eres_inst_tac [("x","t2")] allE 1);
   21.69  by (eres_inst_tac [("x","Suc n")] allE 1);
   21.70  by (fast_tac (HOL_cs addss (simpset() addcongs [conj_cong]
   21.71 -                            addsplits [expand_bind])) 1);
   21.72 +                            addsplits [split_bind])) 1);
   21.73  
   21.74  (** LEVEL 17 **)
   21.75  (* case App e1 e2 *)
   21.76 @@ -321,7 +321,7 @@
   21.77  by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2);
   21.78  by (Fast_tac 2);
   21.79  (** LEVEL 76 **)
   21.80 -by (asm_simp_tac (simpset() addsplits [expand_bind]) 1);
   21.81 +by (asm_simp_tac (simpset() addsplits [split_bind]) 1);
   21.82  by (safe_tac HOL_cs);
   21.83  by (dtac mgu_Ok 1);
   21.84  by ( fast_tac (HOL_cs addss simpset()) 1);
    22.1 --- a/src/HOL/ex/set.ML	Mon Apr 27 16:45:11 1998 +0200
    22.2 +++ b/src/HOL/ex/set.ML	Mon Apr 27 16:45:27 1998 +0200
    22.3 @@ -101,7 +101,7 @@
    22.4  qed "surj_if_then_else";
    22.5  
    22.6  val [injf,injg,compl,bij] = goal Lfp.thy
    22.7 -    "[| inj_onto f X;  inj_onto g (Compl X);  Compl(f``X) = g``Compl(X); \
    22.8 +    "[| inj_on f X;  inj_on g (Compl X);  Compl(f``X) = g``Compl(X); \
    22.9  \       bij = (%z. if z:X then f(z) else g(z)) |] ==> \
   22.10  \       inj(bij) & surj(bij)";
   22.11  val f_eq_gE = make_elim (compl RS disj_lemma);
   22.12 @@ -110,10 +110,10 @@
   22.13  by (rtac (compl RS surj_if_then_else) 2);
   22.14  by (rewtac inj_def);
   22.15  by (cut_facts_tac [injf,injg] 1);
   22.16 -by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]);
   22.17 -by (fast_tac (claset() addEs  [inj_ontoD, sym RS f_eq_gE]) 1);
   22.18 -by (stac expand_if 1);
   22.19 -by (fast_tac (claset() addEs  [inj_ontoD, f_eq_gE]) 1);
   22.20 +by (EVERY1 [rtac allI, rtac allI, stac split_if, rtac conjI, stac split_if]);
   22.21 +by (fast_tac (claset() addEs  [inj_onD, sym RS f_eq_gE]) 1);
   22.22 +by (stac split_if 1);
   22.23 +by (fast_tac (claset() addEs  [inj_onD, f_eq_gE]) 1);
   22.24  qed "bij_if_then_else";
   22.25  
   22.26  goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";
   22.27 @@ -129,7 +129,7 @@
   22.28  by (rtac exI 1);
   22.29  by (rtac bij_if_then_else 1);
   22.30  by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1,
   22.31 -           rtac (injg RS inj_onto_inv) 1]);
   22.32 +           rtac (injg RS inj_on_inv) 1]);
   22.33  by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
   22.34              etac imageE, etac ssubst, rtac rangeI]);
   22.35  by (EVERY1 [etac ssubst, stac double_complement,