# HG changeset patch # User nipkow # Date 948788743 -3600 # Node ID 80a24574dced105ba4cc8fd737d8d97671f19530 # Parent 037172b3623ce96e8b3a70dba983925e17746826 replaced f : A funcset B by f``A <= B. diff -r 037172b3623c -r 80a24574dced src/HOL/Finite.ML --- a/src/HOL/Finite.ML Mon Jan 24 14:48:11 2000 +0100 +++ b/src/HOL/Finite.ML Tue Jan 25 09:25:43 2000 +0100 @@ -797,14 +797,14 @@ by (auto_tac (claset() addIs [finite_subset], simpset())); qed "choose_deconstruct"; -Goal "[| finite(A); finite(B); f : A funcset B; inj_on f A |] \ +Goal "[| finite(A); finite(B); f``A <= B; inj_on f A |] \ \ ==> card A <= card B"; by (auto_tac (claset() addIs [card_mono], - simpset() addsimps [card_image RS sym, Pi_def])); + simpset() addsimps [card_image RS sym])); qed "card_inj_on_le"; Goal "[| finite A; finite B; \ -\ f: A funcset B; inj_on f A; g: B funcset A; inj_on g B |] \ +\ f``A <= B; inj_on f A; g``B <= A; inj_on g B |] \ \ ==> card(A) = card(B)"; by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset())); qed "card_bij_eq"; @@ -812,17 +812,12 @@ Goal "[| finite M; x ~: M |] \ \ ==> card{s. EX t. t <= M & card(t) = k & s = insert x t} = \ \ card {s. s <= M & card(s) = k}"; -by (res_inst_tac - [("f", "lam s: {s. EX t. t <= M & card t = k & s = insert x t}. s - {x}"), - ("g","lam s: {s. s <= M & card s = k}. insert x s")] card_bij_eq 1); +by (res_inst_tac [("f", "%s. s - {x}"), ("g","insert x")] card_bij_eq 1); by (res_inst_tac [("B","Pow(insert x M)")] finite_subset 1); by (res_inst_tac [("B","Pow(M)")] finite_subset 3); -by (TRYALL (Fast_tac)); -by (rtac funcsetI 3); -by (rtac funcsetI 1); +by(REPEAT(Fast_tac 1)); (* arity *) -by (auto_tac (claset() addSEs [equalityE], - simpset() addsimps [inj_on_def, restrict_def])); +by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def])); by (stac Diff_insert0 1); by Auto_tac; qed "constr_bij";