# HG changeset patch # User nipkow # Date 893688327 -7200 # Node ID dae4d63a1318f6498e6a76d28c29af1c7d902a57 # Parent bd73675adbed4fd136807a68a045120fd198503b Renamed expand_const -> split_const. diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Mon Apr 27 16:45:27 1998 +0200 @@ -265,7 +265,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ - pushes @ expand_ifs)))); + pushes @ split_ifs)))); (*Oops*) by (blast_tac (claset() addSDs [unique_session_keys]) 5); (*NS3, replay sub-case*) diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Mon Apr 27 16:45:27 1998 +0200 @@ -320,7 +320,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong] addsimps [analz_insert_eq, analz_insert_freshK] - addsimps (pushes@expand_ifs)))); + addsimps (pushes@split_ifs)))); (*Oops*) by (blast_tac (claset() addSDs [unique_session_keys]) 4); (*OR4*) diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.ML Mon Apr 27 16:45:27 1998 +0200 @@ -256,7 +256,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] addsimps [analz_insert_eq, analz_insert_freshK] - addsimps (pushes@expand_ifs)))); + addsimps (pushes@split_ifs)))); (*Oops*) by (blast_tac (claset() addSDs [unique_session_keys]) 4); (*OR4*) diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Mon Apr 27 16:45:27 1998 +0200 @@ -222,7 +222,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong] addsimps [analz_insert_eq, analz_insert_freshK] - addsimps (pushes@expand_ifs)))); + addsimps (pushes@split_ifs)))); (*Oops*) by (blast_tac (claset() addSDs [unique_session_keys]) 4); (*OR4*) diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/Recur.ML Mon Apr 27 16:45:27 1998 +0200 @@ -409,7 +409,7 @@ by (ALLGOALS (*6 seconds*) (asm_simp_tac (analz_image_freshK_ss - addsimps expand_ifs + addsimps split_ifs addsimps [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib]))); @@ -438,7 +438,7 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (simpset() addsimps (expand_ifs @ + (simpset() addsimps (split_ifs @ [analz_insert_eq, analz_insert_freshK])))); (*RA4*) by (spy_analz_tac 5); diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/TLS.ML Mon Apr 27 16:45:27 1998 +0200 @@ -193,7 +193,7 @@ ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*) ALLGOALS (asm_simp_tac (simpset() addcongs [if_weak_cong] - addsimps (expand_ifs@pushes))) THEN + addsimps (split_ifs@pushes))) THEN (*Remove instances of pubK B: the Spy already knows all public keys. Combining the two simplifier calls makes them run extremely slowly.*) ALLGOALS (asm_simp_tac @@ -405,7 +405,7 @@ by (REPEAT_FIRST (rtac analz_image_keys_lemma)); by (ALLGOALS (*18 seconds*) (asm_simp_tac (analz_image_keys_ss - addsimps (expand_ifs@pushes) + addsimps (split_ifs@pushes) addsimps [range_sessionkeys_not_priK, analz_image_priK, certificate_def]))); by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/Yahalom.ML Mon Apr 27 16:45:27 1998 +0200 @@ -213,7 +213,7 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (simpset() addsimps (expand_ifs@pushes) + (simpset() addsimps (split_ifs@pushes) addsimps [analz_insert_eq, analz_insert_freshK]))); (*Oops*) by (blast_tac (claset() addDs [unique_session_keys]) 3); @@ -384,7 +384,7 @@ by (ALLGOALS (*12 seconds*) (asm_simp_tac (analz_image_freshK_ss - addsimps expand_ifs + addsimps split_ifs addsimps [all_conj_distrib, analz_image_freshK, KeyWithNonce_Says, KeyWithNonce_Notes, fresh_not_KeyWithNonce, @@ -499,7 +499,7 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (simpset() addsimps (expand_ifs@pushes) + (simpset() addsimps (split_ifs@pushes) addsimps [analz_insert_eq, analz_insert_freshK]))); (*Prove YM3 by showing that no NB can also be an NA*) by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] diff -r bd73675adbed -r dae4d63a1318 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Auth/Yahalom2.ML Mon Apr 27 16:45:27 1998 +0200 @@ -215,7 +215,7 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (simpset() addsimps expand_ifs + (simpset() addsimps split_ifs addsimps [analz_insert_eq, analz_insert_freshK]))); (*Oops*) by (blast_tac (claset() addDs [unique_session_keys]) 3); diff -r bd73675adbed -r dae4d63a1318 src/HOL/AxClasses/Lattice/Order.ML --- a/src/HOL/AxClasses/Lattice/Order.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/AxClasses/Lattice/Order.ML Mon Apr 27 16:45:27 1998 +0200 @@ -115,7 +115,7 @@ (** limits in linear orders **) goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)"; - by (stac expand_if 1); + by (stac split_if 1); by (REPEAT_FIRST (resolve_tac [conjI, impI])); (*case "x [= y"*) by (rtac le_refl 1); @@ -131,7 +131,7 @@ qed "min_is_inf"; goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)"; - by (stac expand_if 1); + by (stac split_if 1); by (REPEAT_FIRST (resolve_tac [conjI, impI])); (*case "x [= y"*) by (assume_tac 1); diff -r bd73675adbed -r dae4d63a1318 src/HOL/IOA/IOA.ML --- a/src/HOL/IOA/IOA.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/IOA/IOA.ML Mon Apr 27 16:45:27 1998 +0200 @@ -32,7 +32,7 @@ by (rtac ext 1); by (exhaust_tac "s(i)" 1); by (Asm_simp_tac 1); - by (asm_simp_tac (simpset() addsplits [expand_if]) 1); + by (Asm_simp_tac 1); qed "filter_oseq_idemp"; goalw IOA.thy [mk_trace_def,filter_oseq_def] @@ -42,7 +42,7 @@ \ (mk_trace A s n = Some(a)) = \ \ (s(n)=Some(a) & a : externals(asig_of(A)))"; by (exhaust_tac "s(n)" 1); - by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); + by (ALLGOALS Asm_simp_tac); by (Fast_tac 1); qed "mk_trace_thm"; @@ -138,8 +138,7 @@ \ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ \ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@ - ioa_projections) - addsplits [expand_if]) 1); + ioa_projections)) 1); qed "trans_of_par4"; goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ diff -r bd73675adbed -r dae4d63a1318 src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/IOA/Solve.ML Mon Apr 27 16:45:27 1998 +0200 @@ -102,7 +102,7 @@ addsplits [split_option_case]) 1); qed"comp2_reachable"; -Delsplits [expand_if]; +Delsplits [split_if]; (* Composition of possibility-mappings *) goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \ @@ -121,7 +121,7 @@ by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1); by (simp_tac (simpset() addsimps [par_def]) 1); by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1); -by (stac expand_if 1); +by (stac split_if 1); by (rtac conjI 1); by (rtac impI 1); by (etac disjE 1); @@ -142,7 +142,7 @@ by (Asm_full_simp_tac 2); by (Fast_tac 2); by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong] - addsplits [expand_if]) 1); + addsplits [split_if]) 1); by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN asm_full_simp_tac(simpset() addsimps[comp1_reachable, comp2_reachable])1)); @@ -176,7 +176,7 @@ by (simp_tac (simpset() addsimps [rename_def]) 1); by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1); by Safe_tac; -by (stac expand_if 1); +by (stac split_if 1); by (rtac conjI 1); by (rtac impI 1); by (etac disjE 1); @@ -209,4 +209,4 @@ by Auto_tac; qed"rename_through_pmap"; -Addsplits [expand_if]; +Addsplits [split_if]; diff -r bd73675adbed -r dae4d63a1318 src/HOL/Induct/LList.ML --- a/src/HOL/Induct/LList.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Induct/LList.ML Mon Apr 27 16:45:27 1998 +0200 @@ -6,13 +6,11 @@ SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)? *) -open LList; - bind_thm ("UN1_I", UNIV_I RS UN_I); (** Simplification **) -simpset_ref() := simpset() addsplits [expand_split, expand_sum_case]; +simpset_ref() := simpset() addsplits [split_split, split_sum_case]; (*This justifies using llist in other recursive type definitions*) @@ -68,11 +66,11 @@ (*UNUSED; obsolete? goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))"; -by (simp_tac (simpset() addsplits [expand_split]) 1); +by (Simp_tac 1); qed "split_UN1"; goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))"; -by (simp_tac (simpset() addsplits [expand_sum_case]) 1); +by (Simp_tac 1); qed "sum_case2_UN1"; *) @@ -318,7 +316,7 @@ by (rename_tac "y" 1); by (stac prem1 1); by (stac prem2 1); -by (simp_tac (simpset() addsplits [expand_sum_case]) 1); +by (Simp_tac 1); by (strip_tac 1); by (res_inst_tac [("n", "n")] natE 1); by (rename_tac "m" 2); @@ -366,15 +364,15 @@ by (rtac Rep_llist_inverse 1); qed "inj_Rep_llist"; -goal LList.thy "inj_onto Abs_llist (llist(range Leaf))"; -by (rtac inj_onto_inverseI 1); +goal LList.thy "inj_on Abs_llist (llist(range Leaf))"; +by (rtac inj_on_inverseI 1); by (etac Abs_llist_inverse 1); -qed "inj_onto_Abs_llist"; +qed "inj_on_Abs_llist"; (** Distinctness of constructors **) goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil"; -by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1); +by (rtac (CONS_not_NIL RS (inj_on_Abs_llist RS inj_on_contraD)) 1); by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1)); qed "LCons_not_LNil"; @@ -408,7 +406,7 @@ (*For reasoning about abstract llist constructors*) AddIs ([Rep_llist]@llist.intrs); -AddSDs [inj_onto_Abs_llist RS inj_ontoD, +AddSDs [inj_on_Abs_llist RS inj_onD, inj_Rep_llist RS injD, Leaf_inject]; goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)"; diff -r bd73675adbed -r dae4d63a1318 src/HOL/Induct/PropLog.ML --- a/src/HOL/Induct/PropLog.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Induct/PropLog.ML Mon Apr 27 16:45:27 1998 +0200 @@ -101,7 +101,7 @@ (*This formulation is required for strong induction hypotheses*) goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)"; -by (rtac (expand_if RS iffD2) 1); +by (rtac (split_if RS iffD2) 1); by (PropLog.pl.induct_tac "p" 1); by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H]))); by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, diff -r bd73675adbed -r dae4d63a1318 src/HOL/Induct/SList.ML --- a/src/HOL/Induct/SList.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Induct/SList.ML Mon Apr 27 16:45:27 1998 +0200 @@ -54,10 +54,10 @@ by (rtac Rep_list_inverse 1); qed "inj_Rep_list"; -goal SList.thy "inj_onto Abs_list (list(range Leaf))"; -by (rtac inj_onto_inverseI 1); +goal SList.thy "inj_on Abs_list (list(range Leaf))"; +by (rtac inj_on_inverseI 1); by (etac Abs_list_inverse 1); -qed "inj_onto_Abs_list"; +qed "inj_on_Abs_list"; (** Distinctness of constructors **) @@ -70,7 +70,7 @@ val NIL_neq_CONS = sym RS CONS_neq_NIL; goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil"; -by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1); +by (rtac (CONS_not_NIL RS (inj_on_Abs_list RS inj_on_contraD)) 1); by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1)); qed "Cons_not_Nil"; @@ -87,7 +87,7 @@ AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq]; -AddSDs [inj_onto_Abs_list RS inj_ontoD, +AddSDs [inj_on_Abs_list RS inj_onD, inj_Rep_list RS injD, Leaf_inject]; goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)"; @@ -346,7 +346,7 @@ \ (!y ys. xs=y#ys --> P(f y ys)))"; by (list_ind_tac "xs" 1); by (ALLGOALS Asm_simp_tac); -qed "expand_list_case2"; +qed "split_list_case2"; (** Additional mapping lemmas **) diff -r bd73675adbed -r dae4d63a1318 src/HOL/Induct/Simult.ML --- a/src/HOL/Induct/Simult.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Induct/Simult.ML Mon Apr 27 16:45:27 1998 +0200 @@ -109,20 +109,20 @@ by (rtac Rep_Tree_inverse 1); qed "inj_Rep_Tree"; -goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)"; -by (rtac inj_onto_inverseI 1); +goal Simult.thy "inj_on Abs_Tree (Part (TF(range Leaf)) In0)"; +by (rtac inj_on_inverseI 1); by (etac Abs_Tree_inverse 1); -qed "inj_onto_Abs_Tree"; +qed "inj_on_Abs_Tree"; goal Simult.thy "inj(Rep_Forest)"; by (rtac inj_inverseI 1); by (rtac Rep_Forest_inverse 1); qed "inj_Rep_Forest"; -goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)"; -by (rtac inj_onto_inverseI 1); +goal Simult.thy "inj_on Abs_Forest (Part (TF(range Leaf)) In1)"; +by (rtac inj_on_inverseI 1); by (etac Abs_Forest_inverse 1); -qed "inj_onto_Abs_Forest"; +qed "inj_on_Abs_Forest"; (** Introduction rules for constructors **) @@ -199,8 +199,8 @@ TCONS_neq_FNIL, FNIL_neq_TCONS, FCONS_neq_FNIL, FNIL_neq_FCONS, TCONS_neq_FCONS, FCONS_neq_TCONS]; -AddSDs [inj_onto_Abs_Tree RS inj_ontoD, - inj_onto_Abs_Forest RS inj_ontoD, +AddSDs [inj_on_Abs_Tree RS inj_onD, + inj_on_Abs_Forest RS inj_onD, inj_Rep_Tree RS injD, inj_Rep_Forest RS injD, Leaf_inject]; diff -r bd73675adbed -r dae4d63a1318 src/HOL/Integ/Integ.ML --- a/src/HOL/Integ/Integ.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Integ/Integ.ML Mon Apr 27 16:45:27 1998 +0200 @@ -79,12 +79,12 @@ by (Fast_tac 1); qed "intrel_in_integ"; -goal Integ.thy "inj_onto Abs_Integ Integ"; -by (rtac inj_onto_inverseI 1); +goal Integ.thy "inj_on Abs_Integ Integ"; +by (rtac inj_on_inverseI 1); by (etac Abs_Integ_inverse 1); -qed "inj_onto_Abs_Integ"; +qed "inj_on_Abs_Integ"; -Addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff, +Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff, intrel_iff, intrel_in_integ, Abs_Integ_inverse]; goal Integ.thy "inj(Rep_Integ)"; @@ -100,7 +100,7 @@ goal Integ.thy "inj(znat)"; by (rtac injI 1); by (rewtac znat_def); -by (dtac (inj_onto_Abs_Integ RS inj_ontoD) 1); +by (dtac (inj_on_Abs_Integ RS inj_onD) 1); by (REPEAT (rtac intrel_in_integ 1)); by (dtac eq_equiv_class 1); by (rtac equiv_intrel 1); diff -r bd73675adbed -r dae4d63a1318 src/HOL/Lambda/Eta.ML --- a/src/HOL/Lambda/Eta.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Lambda/Eta.ML Mon Apr 27 16:45:27 1998 +0200 @@ -37,7 +37,7 @@ by (dB.induct_tac "t" 1); by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong]))); by (Blast_tac 2); -by (simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1); +by (simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1); by (safe_tac HOL_cs); by (ALLGOALS trans_tac); qed "free_lift"; @@ -50,7 +50,7 @@ by (Blast_tac 2); by (asm_full_simp_tac (addsplit (simpset())) 2); by (simp_tac (simpset() addsimps [diff_Suc,subst_Var] - addsplits [expand_nat_case]) 1); + addsplits [split_nat_case]) 1); by (safe_tac (HOL_cs addSEs [nat_neqE])); by (ALLGOALS trans_tac); qed "free_subst"; diff -r bd73675adbed -r dae4d63a1318 src/HOL/Lambda/Lambda.ML --- a/src/HOL/Lambda/Lambda.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/Lambda/Lambda.ML Mon Apr 27 16:45:27 1998 +0200 @@ -46,8 +46,8 @@ (*** subst and lift ***) fun addsplit ss = ss addsimps [subst_Var] - delsplits [expand_if] - setloop (split_inside_tac [expand_if]); + delsplits [split_if] + setloop (split_inside_tac [split_if]); goal Lambda.thy "(Var k)[u/k] = u"; by (asm_full_simp_tac(addsplit(simpset())) 1); @@ -76,7 +76,7 @@ \ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; by (dB.induct_tac "t" 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift] - addsplits [expand_nat_case] + addsplits [split_nat_case] addSolver cut_trans_tac))); by (safe_tac HOL_cs); by (ALLGOALS trans_tac); @@ -105,9 +105,9 @@ by (dB.induct_tac "t" 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt] - delsplits [expand_if] - addsplits [expand_nat_case] - addloop ("if",split_inside_tac[expand_if]) + delsplits [split_if] + addsplits [split_nat_case] + addloop ("if",split_inside_tac[split_if]) addSolver cut_trans_tac))); by (safe_tac (HOL_cs addSEs [nat_neqE])); by (ALLGOALS trans_tac); diff -r bd73675adbed -r dae4d63a1318 src/HOL/W0/I.ML --- a/src/HOL/W0/I.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/W0/I.ML Mon Apr 27 16:45:27 1998 +0200 @@ -16,10 +16,10 @@ (* case Var n *) by (simp_tac (simpset() addsimps [app_subst_list] - setloop (split_inside_tac [expand_if])) 1); + setloop (split_inside_tac [split_if])) 1); (* case Abs e *) - by (asm_full_simp_tac (simpset() setloop (split_inside_tac [expand_bind])) 1); + by (asm_full_simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1); by (strip_tac 1); by (rtac conjI 1); by (strip_tac 1); @@ -37,7 +37,7 @@ less_imp_le,lessI]) 1); (** LEVEL 15 **) (* case App e1 e2 *) -by (simp_tac (simpset() setloop (split_inside_tac [expand_bind])) 1); +by (simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1); by (strip_tac 1); by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1); by (rtac conjI 1); diff -r bd73675adbed -r dae4d63a1318 src/HOL/W0/Maybe.ML --- a/src/HOL/W0/Maybe.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/W0/Maybe.ML Mon Apr 27 16:45:27 1998 +0200 @@ -16,17 +16,17 @@ Addsimps [bind_Ok,bind_Fail]; -(* expansion of bind *) +(* case splitting of bind *) goal thy "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))"; -by (maybe.induct_tac "res" 1); +by (induct_tac "res" 1); by (fast_tac (HOL_cs addss simpset()) 1); by (Asm_simp_tac 1); -qed "expand_bind"; +qed "split_bind"; goal Maybe.thy "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; -by (simp_tac (simpset() addsplits [expand_bind]) 1); +by (simp_tac (simpset() addsplits [split_bind]) 1); qed "bind_eq_Fail"; Addsimps [bind_eq_Fail]; diff -r bd73675adbed -r dae4d63a1318 src/HOL/W0/W.ML --- a/src/HOL/W0/W.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/W0/W.ML Mon Apr 27 16:45:27 1998 +0200 @@ -17,12 +17,12 @@ by (Asm_simp_tac 1); (* case Abs e *) by (asm_full_simp_tac (simpset() addsimps [app_subst_list] - addsplits [expand_bind]) 1); + addsplits [split_bind]) 1); by (strip_tac 1); by (dtac sym 1); by (fast_tac (HOL_cs addss simpset()) 1); (* case App e1 e2 *) -by (simp_tac (simpset() addsplits [expand_bind]) 1); +by (simp_tac (simpset() addsplits [split_bind]) 1); by (strip_tac 1); by ( rename_tac "sa ta na sb tb nb sc" 1); by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1); @@ -47,10 +47,10 @@ (* case Var(n) *) by (fast_tac (HOL_cs addss simpset()) 1); (* case Abs e *) -by (simp_tac (simpset() addsplits [expand_bind]) 1); +by (simp_tac (simpset() addsplits [split_bind]) 1); by (fast_tac (HOL_cs addDs [Suc_leD]) 1); (* case App e1 e2 *) -by (simp_tac (simpset() addsplits [expand_bind]) 1); +by (simp_tac (simpset() addsplits [split_bind]) 1); by (strip_tac 1); by (rename_tac "s t na sa ta nb sb sc tb m" 1); by (eres_inst_tac [("x","a")] allE 1); @@ -94,7 +94,7 @@ addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1); (* case Abs e *) by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] - addsplits [expand_bind]) 1); + addsplits [split_bind]) 1); by (strip_tac 1); by (eres_inst_tac [("x","Suc n")] allE 1); by (eres_inst_tac [("x","(TVar n)#a")] allE 1); @@ -102,7 +102,7 @@ addsimps [new_tv_subst,new_tv_Suc_list])) 1); (* case App e1 e2 *) -by (simp_tac (simpset() addsplits [expand_bind]) 1); +by (simp_tac (simpset() addsplits [split_bind]) 1); by (strip_tac 1); by (rename_tac "s t na sa ta nb sb sc tb m" 1); by (eres_inst_tac [("x","n")] allE 1); @@ -162,7 +162,7 @@ (* case Abs e *) by (asm_full_simp_tac (simpset() addsimps - [free_tv_subst] addsplits [expand_bind]) 1); + [free_tv_subst] addsplits [split_bind]) 1); by (strip_tac 1); by (rename_tac "s t na sa ta m v" 1); by (eres_inst_tac [("x","Suc n")] allE 1); @@ -176,7 +176,7 @@ addss (simpset() addsimps [less_Suc_eq])) 1); (** LEVEL 12 **) (* case App e1 e2 *) -by (simp_tac (simpset() addsplits [expand_bind]) 1); +by (simp_tac (simpset() addsplits [split_bind]) 1); by (strip_tac 1); by (rename_tac "s t na sa ta nb sb sc tb m v" 1); by (eres_inst_tac [("x","n")] allE 1); @@ -239,7 +239,7 @@ by (eres_inst_tac [("x","t2")] allE 1); by (eres_inst_tac [("x","Suc n")] allE 1); by (fast_tac (HOL_cs addss (simpset() addcongs [conj_cong] - addsplits [expand_bind])) 1); + addsplits [split_bind])) 1); (** LEVEL 17 **) (* case App e1 e2 *) @@ -321,7 +321,7 @@ by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2); by (Fast_tac 2); (** LEVEL 76 **) -by (asm_simp_tac (simpset() addsplits [expand_bind]) 1); +by (asm_simp_tac (simpset() addsplits [split_bind]) 1); by (safe_tac HOL_cs); by (dtac mgu_Ok 1); by ( fast_tac (HOL_cs addss simpset()) 1); diff -r bd73675adbed -r dae4d63a1318 src/HOL/ex/set.ML --- a/src/HOL/ex/set.ML Mon Apr 27 16:45:11 1998 +0200 +++ b/src/HOL/ex/set.ML Mon Apr 27 16:45:27 1998 +0200 @@ -101,7 +101,7 @@ qed "surj_if_then_else"; val [injf,injg,compl,bij] = goal Lfp.thy - "[| inj_onto f X; inj_onto g (Compl X); Compl(f``X) = g``Compl(X); \ + "[| inj_on f X; inj_on g (Compl X); Compl(f``X) = g``Compl(X); \ \ bij = (%z. if z:X then f(z) else g(z)) |] ==> \ \ inj(bij) & surj(bij)"; val f_eq_gE = make_elim (compl RS disj_lemma); @@ -110,10 +110,10 @@ by (rtac (compl RS surj_if_then_else) 2); by (rewtac inj_def); by (cut_facts_tac [injf,injg] 1); -by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]); -by (fast_tac (claset() addEs [inj_ontoD, sym RS f_eq_gE]) 1); -by (stac expand_if 1); -by (fast_tac (claset() addEs [inj_ontoD, f_eq_gE]) 1); +by (EVERY1 [rtac allI, rtac allI, stac split_if, rtac conjI, stac split_if]); +by (fast_tac (claset() addEs [inj_onD, sym RS f_eq_gE]) 1); +by (stac split_if 1); +by (fast_tac (claset() addEs [inj_onD, f_eq_gE]) 1); qed "bij_if_then_else"; goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))"; @@ -129,7 +129,7 @@ by (rtac exI 1); by (rtac bij_if_then_else 1); by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1, - rtac (injg RS inj_onto_inv) 1]); + rtac (injg RS inj_on_inv) 1]); by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, etac imageE, etac ssubst, rtac rangeI]); by (EVERY1 [etac ssubst, stac double_complement,