Added a few lemmas.
authornipkow
Mon Apr 27 16:45:11 1998 +0200 (1998-04-27)
changeset 4830bd73675adbed
parent 4829 aa5ea943f8e3
child 4831 dae4d63a1318
Added a few lemmas.
Renamed expand_const -> split_const.
src/HOL/Arith.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/IsaMakefile
src/HOL/List.ML
src/HOL/NatDef.ML
src/HOL/Prod.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4     However, none of the generalizations are currently in the simpset,
     1.5     and I dread to think what happens if I put them in *)
     1.6  goal thy "!!n. 0 < n ==> Suc(n-1) = n";
     1.7 -by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
     1.8 +by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
     1.9  qed "Suc_pred";
    1.10  Addsimps [Suc_pred];
    1.11  
    1.12 @@ -114,7 +114,7 @@
    1.13  goal thy "!!n. 0<n ==> m + (n-1) = (m+n)-1";
    1.14  by (exhaust_tac "m" 1);
    1.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.16 -                                      addsplits [expand_nat_case])));
    1.17 +                                      addsplits [split_nat_case])));
    1.18  qed "add_pred";
    1.19  Addsimps [add_pred];
    1.20  
     2.1 --- a/src/HOL/Finite.ML	Mon Apr 27 13:47:46 1998 +0200
     2.2 +++ b/src/HOL/Finite.ML	Mon Apr 27 16:45:11 1998 +0200
     2.3 @@ -111,23 +111,23 @@
     2.4  AddIffs [finite_Diff_singleton];
     2.5  
     2.6  (*Lemma for proving finite_imageD*)
     2.7 -goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
     2.8 +goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A";
     2.9  by (etac finite_induct 1);
    2.10   by (ALLGOALS Asm_simp_tac);
    2.11  by (Clarify_tac 1);
    2.12  by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
    2.13   by (Clarify_tac 1);
    2.14 - by (full_simp_tac (simpset() addsimps [inj_onto_def]) 1);
    2.15 + by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
    2.16   by (Blast_tac 1);
    2.17  by (thin_tac "ALL A. ?PP(A)" 1);
    2.18  by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
    2.19  by (Clarify_tac 1);
    2.20  by (res_inst_tac [("x","xa")] bexI 1);
    2.21  by (ALLGOALS 
    2.22 -    (asm_full_simp_tac (simpset() addsimps [inj_onto_image_set_diff])));
    2.23 +    (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
    2.24  val lemma = result();
    2.25  
    2.26 -goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
    2.27 +goal Finite.thy "!!A. [| finite(f``A);  inj_on f A |] ==> finite A";
    2.28  by (dtac lemma 1);
    2.29  by (Blast_tac 1);
    2.30  qed "finite_imageD";
    2.31 @@ -156,7 +156,7 @@
    2.32  by (rtac finite_subset 2);
    2.33  by (assume_tac 3);
    2.34  by (ALLGOALS
    2.35 -    (fast_tac (claset() addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
    2.36 +    (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD])));
    2.37  val lemma = result();
    2.38  
    2.39  goal Finite.thy "finite(Pow A) = finite A";
    2.40 @@ -174,8 +174,8 @@
    2.41  by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
    2.42   by (Asm_simp_tac 1);
    2.43   by (rtac iffI 1);
    2.44 -  by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
    2.45 -  by (simp_tac (simpset() addsplits [expand_split]) 1);
    2.46 +  by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
    2.47 +  by (simp_tac (simpset() addsplits [split_split]) 1);
    2.48   by (etac finite_imageI 1);
    2.49  by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
    2.50  by Auto_tac;
    2.51 @@ -370,11 +370,11 @@
    2.52  qed "card_insert";
    2.53  Addsimps [card_insert];
    2.54  
    2.55 -goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A";
    2.56 +goal Finite.thy "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A";
    2.57  by (etac finite_induct 1);
    2.58  by (ALLGOALS Asm_simp_tac);
    2.59  by Safe_tac;
    2.60 -by (rewtac inj_onto_def);
    2.61 +by (rewtac inj_on_def);
    2.62  by (Blast_tac 1);
    2.63  by (stac card_insert_disjoint 1);
    2.64  by (etac finite_imageI 1);
    2.65 @@ -387,9 +387,9 @@
    2.66  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
    2.67  by (stac card_Un_disjoint 1);
    2.68  by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
    2.69 -by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
    2.70 +by (subgoal_tac "inj_on (insert x) (Pow F)" 1);
    2.71  by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
    2.72 -by (rewtac inj_onto_def);
    2.73 +by (rewtac inj_on_def);
    2.74  by (blast_tac (claset() addSEs [equalityE]) 1);
    2.75  qed "card_Pow";
    2.76  Addsimps [card_Pow];
     3.1 --- a/src/HOL/Fun.ML	Mon Apr 27 13:47:46 1998 +0200
     3.2 +++ b/src/HOL/Fun.ML	Mon Apr 27 16:45:11 1998 +0200
     3.3 @@ -77,52 +77,52 @@
     3.4  qed "inj_transfer";
     3.5  
     3.6  
     3.7 -(*** inj_onto f A: f is one-to-one over A ***)
     3.8 +(*** inj_on f A: f is one-to-one over A ***)
     3.9  
    3.10 -val prems = goalw thy [inj_onto_def]
    3.11 -    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    3.12 +val prems = goalw thy [inj_on_def]
    3.13 +    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
    3.14  by (blast_tac (claset() addIs prems) 1);
    3.15 -qed "inj_ontoI";
    3.16 +qed "inj_onI";
    3.17  
    3.18  val [major] = goal thy 
    3.19 -    "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
    3.20 -by (rtac inj_ontoI 1);
    3.21 +    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
    3.22 +by (rtac inj_onI 1);
    3.23  by (etac (apply_inverse RS trans) 1);
    3.24  by (REPEAT (eresolve_tac [asm_rl,major] 1));
    3.25 -qed "inj_onto_inverseI";
    3.26 +qed "inj_on_inverseI";
    3.27  
    3.28 -val major::prems = goalw thy [inj_onto_def]
    3.29 -    "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
    3.30 +val major::prems = goalw thy [inj_on_def]
    3.31 +    "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
    3.32  by (rtac (major RS bspec RS bspec RS mp) 1);
    3.33  by (REPEAT (resolve_tac prems 1));
    3.34 -qed "inj_ontoD";
    3.35 +qed "inj_onD";
    3.36  
    3.37 -goal thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    3.38 -by (blast_tac (claset() addSDs [inj_ontoD]) 1);
    3.39 -qed "inj_onto_iff";
    3.40 +goal thy "!!x y.[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    3.41 +by (blast_tac (claset() addSDs [inj_onD]) 1);
    3.42 +qed "inj_on_iff";
    3.43  
    3.44  val major::prems = goal thy
    3.45 -    "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
    3.46 +    "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
    3.47  by (rtac contrapos 1);
    3.48 -by (etac (major RS inj_ontoD) 2);
    3.49 +by (etac (major RS inj_onD) 2);
    3.50  by (REPEAT (resolve_tac prems 1));
    3.51 -qed "inj_onto_contraD";
    3.52 +qed "inj_on_contraD";
    3.53  
    3.54 -goalw thy [inj_onto_def]
    3.55 -    "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
    3.56 +goalw thy [inj_on_def]
    3.57 +    "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
    3.58  by (Blast_tac 1);
    3.59 -qed "subset_inj_onto";
    3.60 +qed "subset_inj_on";
    3.61  
    3.62  
    3.63  (*** Lemmas about inj ***)
    3.64  
    3.65  goalw thy [o_def]
    3.66 -    "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
    3.67 -by (fast_tac (claset() addIs [injI] addEs [injD, inj_ontoD]) 1);
    3.68 +    "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
    3.69 +by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
    3.70  qed "comp_inj";
    3.71  
    3.72 -val [prem] = goal thy "inj(f) ==> inj_onto f A";
    3.73 -by (blast_tac (claset() addIs [prem RS injD, inj_ontoI]) 1);
    3.74 +val [prem] = goal thy "inj(f) ==> inj_on f A";
    3.75 +by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
    3.76  qed "inj_imp";
    3.77  
    3.78  val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
    3.79 @@ -135,20 +135,20 @@
    3.80  by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
    3.81  qed "inv_injective";
    3.82  
    3.83 -goal thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
    3.84 -by (fast_tac (claset() addIs [inj_ontoI] 
    3.85 +goal thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
    3.86 +by (fast_tac (claset() addIs [inj_onI] 
    3.87                        addEs [inv_injective,injD]) 1);
    3.88 -qed "inj_onto_inv";
    3.89 +qed "inj_on_inv";
    3.90  
    3.91 -goalw thy [inj_onto_def]
    3.92 -   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    3.93 +goalw thy [inj_on_def]
    3.94 +   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    3.95  by (Blast_tac 1);
    3.96 -qed "inj_onto_image_Int";
    3.97 +qed "inj_on_image_Int";
    3.98  
    3.99 -goalw thy [inj_onto_def]
   3.100 -   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   3.101 +goalw thy [inj_on_def]
   3.102 +   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   3.103  by (Blast_tac 1);
   3.104 -qed "inj_onto_image_set_diff";
   3.105 +qed "inj_on_image_set_diff";
   3.106  
   3.107  goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
   3.108  by (Blast_tac 1);
     4.1 --- a/src/HOL/Fun.thy	Mon Apr 27 13:47:46 1998 +0200
     4.2 +++ b/src/HOL/Fun.thy	Mon Apr 27 16:45:11 1998 +0200
     4.3 @@ -12,15 +12,15 @@
     4.4                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     4.5  consts
     4.6  
     4.7 -  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
     4.8 -  inj_onto      :: ['a => 'b, 'a set] => bool
     4.9 -  inv           :: ('a => 'b) => ('b => 'a)
    4.10 +  inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    4.11 +  inj_on      :: ['a => 'b, 'a set] => bool
    4.12 +  inv         :: ('a => 'b) => ('b => 'a)
    4.13  
    4.14  defs
    4.15  
    4.16 -  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    4.17 -  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    4.18 -  surj_def      "surj f         == ! y. ? x. y=f(x)"
    4.19 -  inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    4.20 +  inj_def     "inj f          == ! x y. f(x)=f(y) --> x=y"
    4.21 +  inj_on_def  "inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    4.22 +  surj_def    "surj f         == ! y. ? x. y=f(x)"
    4.23 +  inv_def     "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    4.24  
    4.25  end
     5.1 --- a/src/HOL/IsaMakefile	Mon Apr 27 13:47:46 1998 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Mon Apr 27 16:45:11 1998 +0200
     5.3 @@ -104,11 +104,15 @@
     5.4  
     5.5  HOL-Lex: HOL $(LOG)/HOL-Lex.gz
     5.6  
     5.7 -$(LOG)/HOL-Lex.gz: $(OUT)/HOL Lex/Auto.thy Lex/Auto.ML \
     5.8 +$(LOG)/HOL-Lex.gz: $(OUT)/HOL \
     5.9    Lex/AutoChopper.thy Lex/AutoChopper.ML Lex/AutoChopper1.thy \
    5.10 -  Lex/Chopper.thy Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \
    5.11 -  Lex/Regset_of_auto.ML Lex/Regset_of_auto.thy Lex/MaxChop.thy Lex/MaxChop.ML \
    5.12 -  Lex/MaxPrefix.thy Lex/MaxPrefix.ML Lex/AutoMaxChop.thy Lex/AutoMaxChop.ML
    5.13 +  Lex/AutoMaxChop.thy Lex/AutoMaxChop.ML Lex/AutoProj.thy Lex/AutoProj.ML \
    5.14 +  Lex/Automata.thy Lex/Automata.ML Lex/Chopper.thy Lex/DA.thy Lex/DA.ML \
    5.15 +  Lex/MaxChop.thy Lex/MaxChop.ML Lex/MaxPrefix.thy Lex/MaxPrefix.ML \
    5.16 +  Lex/NA.thy Lex/NAe.thy Lex/NAe.ML Lex/NAe_of_RegExp.thy Lex/NAe_of_RegExp.ML\
    5.17 +  Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \
    5.18 +  Lex/RegExp.thy Lex/RegSet.thy Lex/RegSet.ML \
    5.19 +  Lex/RegSet_of_nat_DA.thy Lex/RegSet_of_nat_DA.ML
    5.20  	@$(ISATOOL) usedir $(OUT)/HOL Lex
    5.21  
    5.22  
     6.1 --- a/src/HOL/List.ML	Mon Apr 27 13:47:46 1998 +0200
     6.2 +++ b/src/HOL/List.ML	Mon Apr 27 16:45:11 1998 +0200
     6.3 @@ -19,6 +19,15 @@
     6.4  by (Asm_simp_tac 1);
     6.5  qed "neq_Nil_conv";
     6.6  
     6.7 +(* Induction over the length of a list: *)
     6.8 +val prems = goal thy
     6.9 + "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
    6.10 +by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
    6.11 +     wf_induct 1);
    6.12 +by (Simp_tac 1);
    6.13 +by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
    6.14 +by (eresolve_tac prems 1);
    6.15 +qed "list_length_induct";
    6.16  
    6.17  (** "lists": the list-forming operator over sets **)
    6.18  
    6.19 @@ -219,6 +228,40 @@
    6.20  qed "tl_append2";
    6.21  Addsimps [tl_append2];
    6.22  
    6.23 +
    6.24 +(** Snoc exhaustion and induction **)
    6.25 +section "Snoc exhaustion and induction";
    6.26 +
    6.27 +goal thy "xs ~= [] --> (? ys y. xs = ys@[y])";
    6.28 +by(induct_tac "xs" 1);
    6.29 +by(Simp_tac 1);
    6.30 +by(exhaust_tac "list" 1);
    6.31 + by(Asm_simp_tac 1);
    6.32 + by(res_inst_tac [("x","[]")] exI 1);
    6.33 + by(Simp_tac 1);
    6.34 +by(Asm_full_simp_tac 1);
    6.35 +by(Clarify_tac 1);
    6.36 +by(res_inst_tac [("x","a#ys")] exI 1);
    6.37 +by(Asm_simp_tac 1);
    6.38 +val lemma = result();
    6.39 +
    6.40 +goal thy  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
    6.41 +by(cut_facts_tac [lemma] 1);
    6.42 +by(Blast_tac 1);
    6.43 +bind_thm ("snoc_exhaust",
    6.44 +  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
    6.45 +
    6.46 +val prems = goal thy "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
    6.47 +by(res_inst_tac [("xs","xs")] list_length_induct 1);
    6.48 +by(res_inst_tac [("xs","xs")] snoc_exhaust 1);
    6.49 + by(Clarify_tac 1);
    6.50 + brs prems 1;
    6.51 +by(Clarify_tac 1);
    6.52 +brs prems 1;
    6.53 +auto();
    6.54 +qed "snoc_induct";
    6.55 +
    6.56 +
    6.57  (** map **)
    6.58  
    6.59  section "map";
     7.1 --- a/src/HOL/NatDef.ML	Mon Apr 27 13:47:46 1998 +0200
     7.2 +++ b/src/HOL/NatDef.ML	Mon Apr 27 16:45:11 1998 +0200
     7.3 @@ -85,15 +85,15 @@
     7.4  by (rtac Rep_Nat_inverse 1);
     7.5  qed "inj_Rep_Nat";
     7.6  
     7.7 -goal thy "inj_onto Abs_Nat Nat";
     7.8 -by (rtac inj_onto_inverseI 1);
     7.9 +goal thy "inj_on Abs_Nat Nat";
    7.10 +by (rtac inj_on_inverseI 1);
    7.11  by (etac Abs_Nat_inverse 1);
    7.12 -qed "inj_onto_Abs_Nat";
    7.13 +qed "inj_on_Abs_Nat";
    7.14  
    7.15  (*** Distinctness of constructors ***)
    7.16  
    7.17  goalw thy [Zero_def,Suc_def] "Suc(m) ~= 0";
    7.18 -by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
    7.19 +by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1);
    7.20  by (rtac Suc_Rep_not_Zero_Rep 1);
    7.21  by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
    7.22  qed "Suc_not_Zero";
    7.23 @@ -109,7 +109,7 @@
    7.24  
    7.25  goalw thy [Suc_def] "inj(Suc)";
    7.26  by (rtac injI 1);
    7.27 -by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1);
    7.28 +by (dtac (inj_on_Abs_Nat RS inj_onD) 1);
    7.29  by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1));
    7.30  by (dtac (inj_Suc_Rep RS injD) 1);
    7.31  by (etac (inj_Rep_Nat RS injD) 1);
    7.32 @@ -483,7 +483,7 @@
    7.33    "m=n ==> nat_rec a f m = nat_rec a f n"
    7.34    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    7.35  
    7.36 -qed_goal "expand_nat_case" thy
    7.37 +qed_goal "split_nat_case" thy
    7.38    "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))"
    7.39    (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    7.40  
     8.1 --- a/src/HOL/Prod.ML	Mon Apr 27 13:47:46 1998 +0200
     8.2 +++ b/src/HOL/Prod.ML	Mon Apr 27 16:45:11 1998 +0200
     8.3 @@ -19,14 +19,14 @@
     8.4              rtac conjI, rtac refl, rtac refl]);
     8.5  qed "Pair_Rep_inject";
     8.6  
     8.7 -goal Prod.thy "inj_onto Abs_Prod Prod";
     8.8 -by (rtac inj_onto_inverseI 1);
     8.9 +goal Prod.thy "inj_on Abs_Prod Prod";
    8.10 +by (rtac inj_on_inverseI 1);
    8.11  by (etac Abs_Prod_inverse 1);
    8.12 -qed "inj_onto_Abs_Prod";
    8.13 +qed "inj_on_Abs_Prod";
    8.14  
    8.15  val prems = goalw Prod.thy [Pair_def]
    8.16      "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
    8.17 -by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
    8.18 +by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
    8.19  by (REPEAT (ares_tac (prems@[ProdI]) 1));
    8.20  qed "Pair_inject";
    8.21  
    8.22 @@ -150,16 +150,16 @@
    8.23  by (stac surjective_pairing 1);
    8.24  by (stac split 1);
    8.25  by (Blast_tac 1);
    8.26 -qed "expand_split";
    8.27 +qed "split_split";
    8.28  
    8.29  (* could be done after split_tac has been speeded up significantly:
    8.30 -simpset_ref() := simpset() addsplits [expand_split];
    8.31 +simpset_ref() := simpset() addsplits [split_split];
    8.32     precompute the constants involved and don't do anything unless
    8.33     the current goal contains one of those constants
    8.34  *)
    8.35  
    8.36  goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
    8.37 -by (stac expand_split 1);
    8.38 +by (stac split_split 1);
    8.39  by (Simp_tac 1);
    8.40  qed "expand_split_asm";
    8.41  
     9.1 --- a/src/HOL/Relation.ML	Mon Apr 27 13:47:46 1998 +0200
     9.2 +++ b/src/HOL/Relation.ML	Mon Apr 27 16:45:11 1998 +0200
     9.3 @@ -64,6 +64,10 @@
     9.4  
     9.5  Addsimps [R_O_id,id_O_R];
     9.6  
     9.7 +goal thy "(R O S) O T = R O (S O T)";
     9.8 +by (Blast_tac 1);
     9.9 +qed "O_assoc";
    9.10 +
    9.11  goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    9.12  by (Blast_tac 1);
    9.13  qed "comp_mono";
    10.1 --- a/src/HOL/Set.ML	Mon Apr 27 13:47:46 1998 +0200
    10.2 +++ b/src/HOL/Set.ML	Mon Apr 27 16:45:11 1998 +0200
    10.3 @@ -643,19 +643,19 @@
    10.4  
    10.5  
    10.6  (** Rewrite rules for boolean case-splitting: faster than 
    10.7 -	addsplits[expand_if]
    10.8 +	addsplits[split_if]
    10.9  **)
   10.10  
   10.11 -bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
   10.12 -bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
   10.13 +bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
   10.14 +bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
   10.15  
   10.16 -bind_thm ("expand_if_mem1", 
   10.17 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if);
   10.18 -bind_thm ("expand_if_mem2", 
   10.19 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if);
   10.20 +bind_thm ("split_if_mem1", 
   10.21 +    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
   10.22 +bind_thm ("split_if_mem2", 
   10.23 +    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
   10.24  
   10.25 -val expand_ifs = [if_bool_eq_conj, expand_if_eq1, expand_if_eq2,
   10.26 -		  expand_if_mem1, expand_if_mem2];
   10.27 +val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
   10.28 +		  split_if_mem1, split_if_mem2];
   10.29  
   10.30  
   10.31  (*Each of these has ALREADY been added to simpset() above.*)
    11.1 --- a/src/HOL/Sum.ML	Mon Apr 27 13:47:46 1998 +0200
    11.2 +++ b/src/HOL/Sum.ML	Mon Apr 27 16:45:11 1998 +0200
    11.3 @@ -19,10 +19,10 @@
    11.4  by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]);
    11.5  qed "Inr_RepI";
    11.6  
    11.7 -goal Sum.thy "inj_onto Abs_Sum Sum";
    11.8 -by (rtac inj_onto_inverseI 1);
    11.9 +goal Sum.thy "inj_on Abs_Sum Sum";
   11.10 +by (rtac inj_on_inverseI 1);
   11.11  by (etac Abs_Sum_inverse 1);
   11.12 -qed "inj_onto_Abs_Sum";
   11.13 +qed "inj_on_Abs_Sum";
   11.14  
   11.15  (** Distinctness of Inl and Inr **)
   11.16  
   11.17 @@ -34,7 +34,7 @@
   11.18  qed "Inl_Rep_not_Inr_Rep";
   11.19  
   11.20  goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
   11.21 -by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1);
   11.22 +by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1);
   11.23  by (rtac Inl_Rep_not_Inr_Rep 1);
   11.24  by (rtac Inl_RepI 1);
   11.25  by (rtac Inr_RepI 1);
   11.26 @@ -63,7 +63,7 @@
   11.27  
   11.28  goalw Sum.thy [Inl_def] "inj(Inl)";
   11.29  by (rtac injI 1);
   11.30 -by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1);
   11.31 +by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1);
   11.32  by (rtac Inl_RepI 1);
   11.33  by (rtac Inl_RepI 1);
   11.34  qed "inj_Inl";
   11.35 @@ -71,7 +71,7 @@
   11.36  
   11.37  goalw Sum.thy [Inr_def] "inj(Inr)";
   11.38  by (rtac injI 1);
   11.39 -by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1);
   11.40 +by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1);
   11.41  by (rtac Inr_RepI 1);
   11.42  by (rtac Inr_RepI 1);
   11.43  qed "inj_Inr";
   11.44 @@ -150,7 +150,7 @@
   11.45  \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
   11.46  by (res_inst_tac [("s","s")] sumE 1);
   11.47  by Auto_tac;
   11.48 -qed "expand_sum_case";
   11.49 +qed "split_sum_case";
   11.50  
   11.51  (*Prevents simplification of f and g: much faster*)
   11.52  qed_goal "sum_case_weak_cong" Sum.thy
    12.1 --- a/src/HOL/Trancl.ML	Mon Apr 27 13:47:46 1998 +0200
    12.2 +++ b/src/HOL/Trancl.ML	Mon Apr 27 16:45:11 1998 +0200
    12.3 @@ -115,6 +115,13 @@
    12.4  qed "rtrancl_idemp";
    12.5  Addsimps [rtrancl_idemp];
    12.6  
    12.7 +goal thy "R^* O R^* = R^*";
    12.8 +br set_ext 1;
    12.9 +by(split_all_tac 1);
   12.10 +by(blast_tac (claset() addIs [rtrancl_trans]) 1);
   12.11 +qed "rtrancl_idemp_self_comp";
   12.12 +Addsimps [rtrancl_idemp_self_comp];
   12.13 +
   12.14  goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*";
   12.15  by (dtac rtrancl_mono 1);
   12.16  by (Asm_full_simp_tac 1);
    13.1 --- a/src/HOL/Univ.ML	Mon Apr 27 13:47:46 1998 +0200
    13.2 +++ b/src/HOL/Univ.ML	Mon Apr 27 16:45:11 1998 +0200
    13.3 @@ -58,12 +58,12 @@
    13.4  by (rtac Rep_Node_inverse 1);
    13.5  qed "inj_Rep_Node";
    13.6  
    13.7 -goal Univ.thy "inj_onto Abs_Node Node";
    13.8 -by (rtac inj_onto_inverseI 1);
    13.9 +goal Univ.thy "inj_on Abs_Node Node";
   13.10 +by (rtac inj_on_inverseI 1);
   13.11  by (etac Abs_Node_inverse 1);
   13.12 -qed "inj_onto_Abs_Node";
   13.13 +qed "inj_on_Abs_Node";
   13.14  
   13.15 -val Abs_Node_inject = inj_onto_Abs_Node RS inj_ontoD;
   13.16 +val Abs_Node_inject = inj_on_Abs_Node RS inj_onD;
   13.17  
   13.18  
   13.19  (*** Introduction rules for Node ***)
    14.1 --- a/src/HOL/simpdata.ML	Mon Apr 27 13:47:46 1998 +0200
    14.2 +++ b/src/HOL/simpdata.ML	Mon Apr 27 16:45:11 1998 +0200
    14.3 @@ -209,7 +209,7 @@
    14.4  prove "disj_not1" "(~P | Q) = (P --> Q)";
    14.5  prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
    14.6  
    14.7 -(*Avoids duplication of subgoals after expand_if, when the true and false 
    14.8 +(*Avoids duplication of subgoals after split_if, when the true and false 
    14.9    cases boil down to the same thing.*) 
   14.10  prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
   14.11  
   14.12 @@ -261,27 +261,29 @@
   14.13  qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
   14.14   (K [Blast_tac 1]);
   14.15  
   14.16 -qed_goal "expand_if" HOL.thy
   14.17 +qed_goal "split_if" HOL.thy
   14.18      "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
   14.19  	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
   14.20           stac if_P 2,
   14.21           stac if_not_P 1,
   14.22           ALLGOALS (Blast_tac)]);
   14.23 +(* for backwards compatibility: *)
   14.24 +val expand_if = split_if;
   14.25  
   14.26  qed_goal "split_if_asm" HOL.thy
   14.27      "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
   14.28 -    (K [stac expand_if 1,
   14.29 +    (K [stac split_if 1,
   14.30  	Blast_tac 1]);
   14.31  
   14.32  (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
   14.33  qed_goal "if_bool_eq_conj" HOL.thy
   14.34      "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   14.35 -    (K [rtac expand_if 1]);
   14.36 +    (K [rtac split_if 1]);
   14.37  
   14.38  (*And this form is useful for expanding IFs on the LEFT*)
   14.39  qed_goal "if_bool_eq_disj" HOL.thy
   14.40      "(if P then Q else R) = ((P&Q) | (~P&R))"
   14.41 -    (K [stac expand_if 1,
   14.42 +    (K [stac split_if 1,
   14.43  	Blast_tac 1]);
   14.44  
   14.45  
   14.46 @@ -359,10 +361,10 @@
   14.47  fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
   14.48  
   14.49  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   14.50 -  (K [split_tac [expand_if] 1, Blast_tac 1]);
   14.51 +  (K [split_tac [split_if] 1, Blast_tac 1]);
   14.52  
   14.53  qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
   14.54 -  (K [split_tac [expand_if] 1, Blast_tac 1]);
   14.55 +  (K [split_tac [split_if] 1, Blast_tac 1]);
   14.56  
   14.57  (** 'if' congruence rules: neither included by default! *)
   14.58  
   14.59 @@ -371,7 +373,7 @@
   14.60    "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
   14.61  \  (if b then x else y) = (if c then u else v)"
   14.62    (fn rew::prems =>
   14.63 -   [stac rew 1, stac expand_if 1, stac expand_if 1,
   14.64 +   [stac rew 1, stac split_if 1, stac split_if 1,
   14.65      blast_tac (HOL_cs addDs prems) 1]);
   14.66  
   14.67  (*Prevents simplification of x and y: much faster*)
   14.68 @@ -418,11 +420,11 @@
   14.69       @ ex_simps @ all_simps @ simp_thms)
   14.70       addsimprocs [defALL_regroup,defEX_regroup]
   14.71       addcongs [imp_cong]
   14.72 -     addsplits [expand_if];
   14.73 +     addsplits [split_if];
   14.74  
   14.75  qed_goal "if_distrib" HOL.thy
   14.76    "f(if c then x else y) = (if c then f x else f y)" 
   14.77 -  (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
   14.78 +  (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
   14.79  
   14.80  qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
   14.81    (K [rtac ext 1, rtac refl 1]);