Renamed expand_const -> split_const.
--- 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*)
--- 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*)
--- 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*)
--- 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*)
--- 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);
--- 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])));
--- 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]
--- 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);
--- 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);
--- 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) & \
--- 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];
--- 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)";
--- 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,
--- 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 **)
--- 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];
--- 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);
--- 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";
--- 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);
--- 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);
--- 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];
--- 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);
--- 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,