# HG changeset patch # User nipkow # Date 893688311 -7200 # Node ID bd73675adbed4fd136807a68a045120fd198503b # Parent aa5ea943f8e397e613ea3467ac33ef66dded86c5 Added a few lemmas. Renamed expand_const -> split_const. diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Arith.ML --- a/src/HOL/Arith.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Arith.ML Mon Apr 27 16:45:11 1998 +0200 @@ -29,7 +29,7 @@ However, none of the generalizations are currently in the simpset, and I dread to think what happens if I put them in *) goal thy "!!n. 0 < n ==> Suc(n-1) = n"; -by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1); +by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1); qed "Suc_pred"; Addsimps [Suc_pred]; @@ -114,7 +114,7 @@ goal thy "!!n. 0 m + (n-1) = (m+n)-1"; by (exhaust_tac "m" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc] - addsplits [expand_nat_case]))); + addsplits [split_nat_case]))); qed "add_pred"; Addsimps [add_pred]; diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Finite.ML --- a/src/HOL/Finite.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Finite.ML Mon Apr 27 16:45:11 1998 +0200 @@ -111,23 +111,23 @@ AddIffs [finite_Diff_singleton]; (*Lemma for proving finite_imageD*) -goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A"; +goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A"; by (etac finite_induct 1); by (ALLGOALS Asm_simp_tac); by (Clarify_tac 1); by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1); by (Clarify_tac 1); - by (full_simp_tac (simpset() addsimps [inj_onto_def]) 1); + by (full_simp_tac (simpset() addsimps [inj_on_def]) 1); by (Blast_tac 1); by (thin_tac "ALL A. ?PP(A)" 1); by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); by (Clarify_tac 1); by (res_inst_tac [("x","xa")] bexI 1); by (ALLGOALS - (asm_full_simp_tac (simpset() addsimps [inj_onto_image_set_diff]))); + (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff]))); val lemma = result(); -goal Finite.thy "!!A. [| finite(f``A); inj_onto f A |] ==> finite A"; +goal Finite.thy "!!A. [| finite(f``A); inj_on f A |] ==> finite A"; by (dtac lemma 1); by (Blast_tac 1); qed "finite_imageD"; @@ -156,7 +156,7 @@ by (rtac finite_subset 2); by (assume_tac 3); by (ALLGOALS - (fast_tac (claset() addSDs [rewrite_rule [inj_onto_def] finite_imageD]))); + (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD]))); val lemma = result(); goal Finite.thy "finite(Pow A) = finite A"; @@ -174,8 +174,8 @@ by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1); by (Asm_simp_tac 1); by (rtac iffI 1); - by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1); - by (simp_tac (simpset() addsplits [expand_split]) 1); + by (etac (rewrite_rule [inj_on_def] finite_imageD) 1); + by (simp_tac (simpset() addsplits [split_split]) 1); by (etac finite_imageI 1); by (simp_tac (simpset() addsimps [converse_def,image_def]) 1); by Auto_tac; @@ -370,11 +370,11 @@ qed "card_insert"; Addsimps [card_insert]; -goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A"; +goal Finite.thy "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A"; by (etac finite_induct 1); by (ALLGOALS Asm_simp_tac); by Safe_tac; -by (rewtac inj_onto_def); +by (rewtac inj_on_def); by (Blast_tac 1); by (stac card_insert_disjoint 1); by (etac finite_imageI 1); @@ -387,9 +387,9 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); by (stac card_Un_disjoint 1); by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1])); -by (subgoal_tac "inj_onto (insert x) (Pow F)" 1); +by (subgoal_tac "inj_on (insert x) (Pow F)" 1); by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1); -by (rewtac inj_onto_def); +by (rewtac inj_on_def); by (blast_tac (claset() addSEs [equalityE]) 1); qed "card_Pow"; Addsimps [card_Pow]; diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Fun.ML --- a/src/HOL/Fun.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Fun.ML Mon Apr 27 16:45:11 1998 +0200 @@ -77,52 +77,52 @@ qed "inj_transfer"; -(*** inj_onto f A: f is one-to-one over A ***) +(*** inj_on f A: f is one-to-one over A ***) -val prems = goalw thy [inj_onto_def] - "(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto f A"; +val prems = goalw thy [inj_on_def] + "(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A"; by (blast_tac (claset() addIs prems) 1); -qed "inj_ontoI"; +qed "inj_onI"; val [major] = goal thy - "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A"; -by (rtac inj_ontoI 1); + "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"; +by (rtac inj_onI 1); by (etac (apply_inverse RS trans) 1); by (REPEAT (eresolve_tac [asm_rl,major] 1)); -qed "inj_onto_inverseI"; +qed "inj_on_inverseI"; -val major::prems = goalw thy [inj_onto_def] - "[| inj_onto f A; f(x)=f(y); x:A; y:A |] ==> x=y"; +val major::prems = goalw thy [inj_on_def] + "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"; by (rtac (major RS bspec RS bspec RS mp) 1); by (REPEAT (resolve_tac prems 1)); -qed "inj_ontoD"; +qed "inj_onD"; -goal thy "!!x y.[| inj_onto f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; -by (blast_tac (claset() addSDs [inj_ontoD]) 1); -qed "inj_onto_iff"; +goal thy "!!x y.[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; +by (blast_tac (claset() addSDs [inj_onD]) 1); +qed "inj_on_iff"; val major::prems = goal thy - "[| inj_onto f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; + "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; by (rtac contrapos 1); -by (etac (major RS inj_ontoD) 2); +by (etac (major RS inj_onD) 2); by (REPEAT (resolve_tac prems 1)); -qed "inj_onto_contraD"; +qed "inj_on_contraD"; -goalw thy [inj_onto_def] - "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A"; +goalw thy [inj_on_def] + "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A"; by (Blast_tac 1); -qed "subset_inj_onto"; +qed "subset_inj_on"; (*** Lemmas about inj ***) goalw thy [o_def] - "!!f g. [| inj(f); inj_onto g (range f) |] ==> inj(g o f)"; -by (fast_tac (claset() addIs [injI] addEs [injD, inj_ontoD]) 1); + "!!f g. [| inj(f); inj_on g (range f) |] ==> inj(g o f)"; +by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1); qed "comp_inj"; -val [prem] = goal thy "inj(f) ==> inj_onto f A"; -by (blast_tac (claset() addIs [prem RS injD, inj_ontoI]) 1); +val [prem] = goal thy "inj(f) ==> inj_on f A"; +by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1); qed "inj_imp"; val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y"; @@ -135,20 +135,20 @@ by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1)); qed "inv_injective"; -goal thy "!!f. [| inj(f); A<=range(f) |] ==> inj_onto (inv f) A"; -by (fast_tac (claset() addIs [inj_ontoI] +goal thy "!!f. [| inj(f); A<=range(f) |] ==> inj_on (inv f) A"; +by (fast_tac (claset() addIs [inj_onI] addEs [inv_injective,injD]) 1); -qed "inj_onto_inv"; +qed "inj_on_inv"; -goalw thy [inj_onto_def] - "!!f. [| inj_onto f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; +goalw thy [inj_on_def] + "!!f. [| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; by (Blast_tac 1); -qed "inj_onto_image_Int"; +qed "inj_on_image_Int"; -goalw thy [inj_onto_def] - "!!f. [| inj_onto f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B"; +goalw thy [inj_on_def] + "!!f. [| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B"; by (Blast_tac 1); -qed "inj_onto_image_set_diff"; +qed "inj_on_image_set_diff"; goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B"; by (Blast_tac 1); diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Fun.thy Mon Apr 27 16:45:11 1998 +0200 @@ -12,15 +12,15 @@ (subset_refl,subset_trans,subset_antisym,psubset_eq) consts - inj, surj :: ('a => 'b) => bool (*inj/surjective*) - inj_onto :: ['a => 'b, 'a set] => bool - inv :: ('a => 'b) => ('b => 'a) + inj, surj :: ('a => 'b) => bool (*inj/surjective*) + inj_on :: ['a => 'b, 'a set] => bool + inv :: ('a => 'b) => ('b => 'a) defs - inj_def "inj f == ! x y. f(x)=f(y) --> x=y" - inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" - surj_def "surj f == ! y. ? x. y=f(x)" - inv_def "inv(f::'a=>'b) == (% y. @x. f(x)=y)" + inj_def "inj f == ! x y. f(x)=f(y) --> x=y" + inj_on_def "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" + surj_def "surj f == ! y. ? x. y=f(x)" + inv_def "inv(f::'a=>'b) == (% y. @x. f(x)=y)" end diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/IsaMakefile Mon Apr 27 16:45:11 1998 +0200 @@ -104,11 +104,15 @@ HOL-Lex: HOL $(LOG)/HOL-Lex.gz -$(LOG)/HOL-Lex.gz: $(OUT)/HOL Lex/Auto.thy Lex/Auto.ML \ +$(LOG)/HOL-Lex.gz: $(OUT)/HOL \ Lex/AutoChopper.thy Lex/AutoChopper.ML Lex/AutoChopper1.thy \ - Lex/Chopper.thy Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \ - Lex/Regset_of_auto.ML Lex/Regset_of_auto.thy Lex/MaxChop.thy Lex/MaxChop.ML \ - Lex/MaxPrefix.thy Lex/MaxPrefix.ML Lex/AutoMaxChop.thy Lex/AutoMaxChop.ML + Lex/AutoMaxChop.thy Lex/AutoMaxChop.ML Lex/AutoProj.thy Lex/AutoProj.ML \ + Lex/Automata.thy Lex/Automata.ML Lex/Chopper.thy Lex/DA.thy Lex/DA.ML \ + Lex/MaxChop.thy Lex/MaxChop.ML Lex/MaxPrefix.thy Lex/MaxPrefix.ML \ + Lex/NA.thy Lex/NAe.thy Lex/NAe.ML Lex/NAe_of_RegExp.thy Lex/NAe_of_RegExp.ML\ + Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \ + Lex/RegExp.thy Lex/RegSet.thy Lex/RegSet.ML \ + Lex/RegSet_of_nat_DA.thy Lex/RegSet_of_nat_DA.ML @$(ISATOOL) usedir $(OUT)/HOL Lex diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/List.ML --- a/src/HOL/List.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/List.ML Mon Apr 27 16:45:11 1998 +0200 @@ -19,6 +19,15 @@ by (Asm_simp_tac 1); qed "neq_Nil_conv"; +(* Induction over the length of a list: *) +val prems = goal thy + "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs"; +by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")] + wf_induct 1); +by (Simp_tac 1); +by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1); +by (eresolve_tac prems 1); +qed "list_length_induct"; (** "lists": the list-forming operator over sets **) @@ -219,6 +228,40 @@ qed "tl_append2"; Addsimps [tl_append2]; + +(** Snoc exhaustion and induction **) +section "Snoc exhaustion and induction"; + +goal thy "xs ~= [] --> (? ys y. xs = ys@[y])"; +by(induct_tac "xs" 1); +by(Simp_tac 1); +by(exhaust_tac "list" 1); + by(Asm_simp_tac 1); + by(res_inst_tac [("x","[]")] exI 1); + by(Simp_tac 1); +by(Asm_full_simp_tac 1); +by(Clarify_tac 1); +by(res_inst_tac [("x","a#ys")] exI 1); +by(Asm_simp_tac 1); +val lemma = result(); + +goal thy "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P"; +by(cut_facts_tac [lemma] 1); +by(Blast_tac 1); +bind_thm ("snoc_exhaust", + impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp))))); + +val prems = goal thy "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"; +by(res_inst_tac [("xs","xs")] list_length_induct 1); +by(res_inst_tac [("xs","xs")] snoc_exhaust 1); + by(Clarify_tac 1); + brs prems 1; +by(Clarify_tac 1); +brs prems 1; +auto(); +qed "snoc_induct"; + + (** map **) section "map"; diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/NatDef.ML --- a/src/HOL/NatDef.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/NatDef.ML Mon Apr 27 16:45:11 1998 +0200 @@ -85,15 +85,15 @@ by (rtac Rep_Nat_inverse 1); qed "inj_Rep_Nat"; -goal thy "inj_onto Abs_Nat Nat"; -by (rtac inj_onto_inverseI 1); +goal thy "inj_on Abs_Nat Nat"; +by (rtac inj_on_inverseI 1); by (etac Abs_Nat_inverse 1); -qed "inj_onto_Abs_Nat"; +qed "inj_on_Abs_Nat"; (*** Distinctness of constructors ***) goalw thy [Zero_def,Suc_def] "Suc(m) ~= 0"; -by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1); +by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1); by (rtac Suc_Rep_not_Zero_Rep 1); by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1)); qed "Suc_not_Zero"; @@ -109,7 +109,7 @@ goalw thy [Suc_def] "inj(Suc)"; by (rtac injI 1); -by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1); +by (dtac (inj_on_Abs_Nat RS inj_onD) 1); by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1)); by (dtac (inj_Suc_Rep RS injD) 1); by (etac (inj_Rep_Nat RS injD) 1); @@ -483,7 +483,7 @@ "m=n ==> nat_rec a f m = nat_rec a f n" (fn [prem] => [rtac (prem RS arg_cong) 1]); -qed_goal "expand_nat_case" thy +qed_goal "split_nat_case" thy "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))" (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Prod.ML --- a/src/HOL/Prod.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Prod.ML Mon Apr 27 16:45:11 1998 +0200 @@ -19,14 +19,14 @@ rtac conjI, rtac refl, rtac refl]); qed "Pair_Rep_inject"; -goal Prod.thy "inj_onto Abs_Prod Prod"; -by (rtac inj_onto_inverseI 1); +goal Prod.thy "inj_on Abs_Prod Prod"; +by (rtac inj_on_inverseI 1); by (etac Abs_Prod_inverse 1); -qed "inj_onto_Abs_Prod"; +qed "inj_on_Abs_Prod"; val prems = goalw Prod.thy [Pair_def] "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; -by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1); +by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1); by (REPEAT (ares_tac (prems@[ProdI]) 1)); qed "Pair_inject"; @@ -150,16 +150,16 @@ by (stac surjective_pairing 1); by (stac split 1); by (Blast_tac 1); -qed "expand_split"; +qed "split_split"; (* could be done after split_tac has been speeded up significantly: -simpset_ref() := simpset() addsplits [expand_split]; +simpset_ref() := simpset() addsplits [split_split]; precompute the constants involved and don't do anything unless the current goal contains one of those constants *) goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; -by (stac expand_split 1); +by (stac split_split 1); by (Simp_tac 1); qed "expand_split_asm"; diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Relation.ML --- a/src/HOL/Relation.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Relation.ML Mon Apr 27 16:45:11 1998 +0200 @@ -64,6 +64,10 @@ Addsimps [R_O_id,id_O_R]; +goal thy "(R O S) O T = R O (S O T)"; +by (Blast_tac 1); +qed "O_assoc"; + goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; by (Blast_tac 1); qed "comp_mono"; diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Set.ML --- a/src/HOL/Set.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Set.ML Mon Apr 27 16:45:11 1998 +0200 @@ -643,19 +643,19 @@ (** Rewrite rules for boolean case-splitting: faster than - addsplits[expand_if] + addsplits[split_if] **) -bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if); -bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if); +bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if); +bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if); -bind_thm ("expand_if_mem1", - read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if); -bind_thm ("expand_if_mem2", - read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if); +bind_thm ("split_if_mem1", + read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if); +bind_thm ("split_if_mem2", + read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if); -val expand_ifs = [if_bool_eq_conj, expand_if_eq1, expand_if_eq2, - expand_if_mem1, expand_if_mem2]; +val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2, + split_if_mem1, split_if_mem2]; (*Each of these has ALREADY been added to simpset() above.*) diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Sum.ML --- a/src/HOL/Sum.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Sum.ML Mon Apr 27 16:45:11 1998 +0200 @@ -19,10 +19,10 @@ by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]); qed "Inr_RepI"; -goal Sum.thy "inj_onto Abs_Sum Sum"; -by (rtac inj_onto_inverseI 1); +goal Sum.thy "inj_on Abs_Sum Sum"; +by (rtac inj_on_inverseI 1); by (etac Abs_Sum_inverse 1); -qed "inj_onto_Abs_Sum"; +qed "inj_on_Abs_Sum"; (** Distinctness of Inl and Inr **) @@ -34,7 +34,7 @@ qed "Inl_Rep_not_Inr_Rep"; goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)"; -by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1); +by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1); by (rtac Inl_Rep_not_Inr_Rep 1); by (rtac Inl_RepI 1); by (rtac Inr_RepI 1); @@ -63,7 +63,7 @@ goalw Sum.thy [Inl_def] "inj(Inl)"; by (rtac injI 1); -by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1); +by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1); by (rtac Inl_RepI 1); by (rtac Inl_RepI 1); qed "inj_Inl"; @@ -71,7 +71,7 @@ goalw Sum.thy [Inr_def] "inj(Inr)"; by (rtac injI 1); -by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1); +by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1); by (rtac Inr_RepI 1); by (rtac Inr_RepI 1); qed "inj_Inr"; @@ -150,7 +150,7 @@ \ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; by (res_inst_tac [("s","s")] sumE 1); by Auto_tac; -qed "expand_sum_case"; +qed "split_sum_case"; (*Prevents simplification of f and g: much faster*) qed_goal "sum_case_weak_cong" Sum.thy diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Trancl.ML Mon Apr 27 16:45:11 1998 +0200 @@ -115,6 +115,13 @@ qed "rtrancl_idemp"; Addsimps [rtrancl_idemp]; +goal thy "R^* O R^* = R^*"; +br set_ext 1; +by(split_all_tac 1); +by(blast_tac (claset() addIs [rtrancl_trans]) 1); +qed "rtrancl_idemp_self_comp"; +Addsimps [rtrancl_idemp_self_comp]; + goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*"; by (dtac rtrancl_mono 1); by (Asm_full_simp_tac 1); diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/Univ.ML --- a/src/HOL/Univ.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Univ.ML Mon Apr 27 16:45:11 1998 +0200 @@ -58,12 +58,12 @@ by (rtac Rep_Node_inverse 1); qed "inj_Rep_Node"; -goal Univ.thy "inj_onto Abs_Node Node"; -by (rtac inj_onto_inverseI 1); +goal Univ.thy "inj_on Abs_Node Node"; +by (rtac inj_on_inverseI 1); by (etac Abs_Node_inverse 1); -qed "inj_onto_Abs_Node"; +qed "inj_on_Abs_Node"; -val Abs_Node_inject = inj_onto_Abs_Node RS inj_ontoD; +val Abs_Node_inject = inj_on_Abs_Node RS inj_onD; (*** Introduction rules for Node ***) diff -r aa5ea943f8e3 -r bd73675adbed src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/simpdata.ML Mon Apr 27 16:45:11 1998 +0200 @@ -209,7 +209,7 @@ prove "disj_not1" "(~P | Q) = (P --> Q)"; prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *) -(*Avoids duplication of subgoals after expand_if, when the true and false +(*Avoids duplication of subgoals after split_if, when the true and false cases boil down to the same thing.*) prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q"; @@ -261,27 +261,29 @@ qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y" (K [Blast_tac 1]); -qed_goal "expand_if" HOL.thy +qed_goal "split_if" HOL.thy "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [ res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1, stac if_P 2, stac if_not_P 1, ALLGOALS (Blast_tac)]); +(* for backwards compatibility: *) +val expand_if = split_if; qed_goal "split_if_asm" HOL.thy "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" - (K [stac expand_if 1, + (K [stac split_if 1, Blast_tac 1]); (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) qed_goal "if_bool_eq_conj" HOL.thy "(if P then Q else R) = ((P-->Q) & (~P-->R))" - (K [rtac expand_if 1]); + (K [rtac split_if 1]); (*And this form is useful for expanding IFs on the LEFT*) qed_goal "if_bool_eq_disj" HOL.thy "(if P then Q else R) = ((P&Q) | (~P&R))" - (K [stac expand_if 1, + (K [stac split_if 1, Blast_tac 1]); @@ -359,10 +361,10 @@ fun Delsplits splits = (simpset_ref() := simpset() delsplits splits); qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" - (K [split_tac [expand_if] 1, Blast_tac 1]); + (K [split_tac [split_if] 1, Blast_tac 1]); qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x" - (K [split_tac [expand_if] 1, Blast_tac 1]); + (K [split_tac [split_if] 1, Blast_tac 1]); (** 'if' congruence rules: neither included by default! *) @@ -371,7 +373,7 @@ "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\ \ (if b then x else y) = (if c then u else v)" (fn rew::prems => - [stac rew 1, stac expand_if 1, stac expand_if 1, + [stac rew 1, stac split_if 1, stac split_if 1, blast_tac (HOL_cs addDs prems) 1]); (*Prevents simplification of x and y: much faster*) @@ -418,11 +420,11 @@ @ ex_simps @ all_simps @ simp_thms) addsimprocs [defALL_regroup,defEX_regroup] addcongs [imp_cong] - addsplits [expand_if]; + addsplits [split_if]; qed_goal "if_distrib" HOL.thy "f(if c then x else y) = (if c then f x else f y)" - (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); + (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]); qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h" (K [rtac ext 1, rtac refl 1]);