--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Sep 25 14:11:48 2020 +0100
@@ -326,7 +326,7 @@
shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
proof (rule kuhn_counting_lemma)
have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
- by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
+ by (metis add_is_0 zero_neq_numeral card.infinite assms(3))
let ?F = "{f. \<exists>s\<in>simplices. face f s}"
have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"
--- a/src/HOL/Analysis/Polytope.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Polytope.thy Fri Sep 25 14:11:48 2020 +0100
@@ -2783,7 +2783,7 @@
proof (cases "affine_dependent S")
case True
have [iff]: "finite S"
- using assms using card_infinite by force
+ using assms using card.infinite by force
then have ccs: "closed (convex hull S)"
by (simp add: compact_imp_closed finite_imp_compact_convex_hull)
{ fix x T
@@ -2839,7 +2839,7 @@
by (auto simp: assms segment_convex_hull frontier_def empty_interior_convex_hull insert_commute card_insert_le_m1 hull_inc insert_absorb)
next
case False then have [simp]: "card {a, b, c} = Suc (DIM('a))"
- by (simp add: card_insert Set.insert_Diff_if assms)
+ by (simp add: card.insert_remove Set.insert_Diff_if assms)
show ?thesis
proof
show "?lhs \<subseteq> ?rhs"
@@ -3125,7 +3125,7 @@
proof
assume "n simplex {}"
then show "n = -1"
- unfolding simplex by (metis card_empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0)
+ unfolding simplex by (metis card.empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0)
next
assume "n = -1" then show "n simplex {}"
by (fastforce simp: simplex)
@@ -3141,7 +3141,7 @@
lemma zero_simplex_sing: "0 simplex {a}"
apply (simp add: simplex_def)
- by (metis affine_independent_1 card_empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI)
+ by (metis affine_independent_1 card.empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI)
lemma simplex_sing [simp]: "n simplex {a} \<longleftrightarrow> n = 0"
using aff_dim_simplex aff_dim_sing zero_simplex_sing by blast
--- a/src/HOL/Analysis/Simplex_Content.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Simplex_Content.thy Fri Sep 25 14:11:48 2020 +0100
@@ -89,7 +89,7 @@
also have "t ^ n / n / fact (card A) = t ^ n / fact n"
by (simp add: n_def)
also have "n = card (insert b A)"
- using insert.hyps by (subst card_insert) (auto simp: n_def)
+ using insert.hyps by (subst card.insert_remove) (auto simp: n_def)
finally show ?case .
qed
--- a/src/HOL/Analysis/Starlike.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Starlike.thy Fri Sep 25 14:11:48 2020 +0100
@@ -3270,7 +3270,7 @@
fix a b
assume "b \<in> S" "b \<in> affine hull (S - {b})"
then have "interior(affine hull S) = {}" using assms
- by (metis DIM_positive One_nat_def Suc_mono card.remove card_infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one)
+ by (metis DIM_positive One_nat_def Suc_mono card.remove card.infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one)
then show "interior (convex hull S) = {}"
using affine_hull_nonempty_interior by fastforce
qed
--- a/src/HOL/Binomial.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Binomial.thy Fri Sep 25 14:11:48 2020 +0100
@@ -81,11 +81,11 @@
proof -
from \<open>n \<in> K\<close> obtain L where "K = insert n L" and "n \<notin> L"
by (blast elim: Set.set_insert)
- with that show ?thesis by (simp add: card_insert)
+ with that show ?thesis by (simp add: card.insert_remove)
qed
show "K \<in> ?A \<longleftrightarrow> K \<in> ?B"
by (subst in_image_insert_iff)
- (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite
+ (auto simp add: card.insert_remove subset_eq_atLeast0_lessThan_finite
Diff_subset_conv K_finite Suc_card_K)
qed
also have "{K\<in>?Q. n \<notin> K} = ?P n (Suc k)"
--- a/src/HOL/Finite_Set.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Finite_Set.thy Fri Sep 25 14:11:48 2020 +0100
@@ -1387,12 +1387,6 @@
defines card = "folding.F (\<lambda>_. Suc) 0"
by standard rule
-lemma card_infinite: "\<not> finite A \<Longrightarrow> card A = 0"
- by (fact card.infinite)
-
-lemma card_empty: "card {} = 0"
- by (fact card.empty)
-
lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
by (fact card.insert)
@@ -1417,17 +1411,20 @@
lemma card_gt_0_iff: "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
by (simp add: neq0_conv [symmetric] card_eq_0_iff)
-lemma card_Suc_Diff1: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A"
- apply (rule insert_Diff [THEN subst, where t = A])
- apply assumption
- apply (simp del: insert_Diff_single)
- done
+lemma card_Suc_Diff1:
+ assumes "finite A" "x \<in> A" shows "Suc (card (A - {x})) = card A"
+proof -
+ have "Suc (card (A - {x})) = card (insert x (A - {x}))"
+ using assms by (simp add: card.insert_remove)
+ also have "... = card A"
+ using assms by (simp add: card_insert_if)
+ finally show ?thesis .
+qed
-lemma card_insert_le_m1: "n > 0 \<Longrightarrow> card y \<le> n - 1 \<Longrightarrow> card (insert x y) \<le> n"
- apply (cases "finite y")
- apply (cases "x \<in> y")
- apply (auto simp: insert_absorb)
- done
+lemma card_insert_le_m1:
+ assumes "n > 0" "card y \<le> n - 1" shows "card (insert x y) \<le> n"
+ using assms
+ by (cases "finite y") (auto simp: card_insert_if)
lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
by (simp add: card_Suc_Diff1 [symmetric])
@@ -1446,9 +1443,6 @@
using assms by (simp add: card_Diff_singleton)
qed
-lemma card_insert: "finite A \<Longrightarrow> card (insert x A) = Suc (card (A - {x}))"
- by (fact card.insert_remove)
-
lemma card_insert_le: "finite A \<Longrightarrow> card A \<le> card (insert x A)"
by (simp add: card_insert_if)
@@ -1482,21 +1476,24 @@
qed
qed
-lemma card_seteq: "finite B \<Longrightarrow> (\<And>A. A \<subseteq> B \<Longrightarrow> card B \<le> card A \<Longrightarrow> A = B)"
- apply (induct rule: finite_induct)
- apply simp
- apply clarify
- apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
- prefer 2 apply (blast intro: finite_subset, atomize)
- apply (drule_tac x = "A - {x}" in spec)
- apply (simp add: card_Diff_singleton_if split: if_split_asm)
- apply (case_tac "card A", auto)
- done
+lemma card_seteq:
+ assumes "finite B" and A: "A \<subseteq> B" "card B \<le> card A"
+ shows "A = B"
+ using assms
+proof (induction arbitrary: A rule: finite_induct)
+ case (insert b B)
+ then have A: "finite A" "A - {b} \<subseteq> B"
+ by force+
+ then have "card B \<le> card (A - {b})"
+ using insert by (auto simp add: card_Diff_singleton_if)
+ then have "A - {b} = B"
+ using A insert.IH by auto
+ then show ?case
+ using insert.hyps insert.prems by auto
+qed auto
lemma psubset_card_mono: "finite B \<Longrightarrow> A < B \<Longrightarrow> card A < card B"
- apply (simp add: psubset_eq linorder_not_le [symmetric])
- apply (blast dest: card_seteq)
- done
+ using card_seteq [of B A] by (auto simp add: psubset_eq)
lemma card_Un_Int:
assumes "finite A" "finite B"
@@ -1579,15 +1576,29 @@
finally show ?thesis .
qed
+lemma card_Diff1_less_iff: "card (A - {x}) < card A \<longleftrightarrow> finite A \<and> x \<in> A"
+proof (cases "finite A \<and> x \<in> A")
+ case True
+ then show ?thesis
+ by (auto simp: card_gt_0_iff intro: diff_less)
+qed auto
+
lemma card_Diff1_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) < card A"
- by (rule Suc_less_SucD) (simp add: card_Suc_Diff1 del: card_Diff_insert)
+ unfolding card_Diff1_less_iff by auto
-lemma card_Diff2_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> card (A - {x} - {y}) < card A"
- apply (cases "x = y")
- apply (simp add: card_Diff1_less del:card_Diff_insert)
- apply (rule less_trans)
- prefer 2 apply (auto intro!: card_Diff1_less simp del: card_Diff_insert)
- done
+lemma card_Diff2_less:
+ assumes "finite A" "x \<in> A" "y \<in> A" shows "card (A - {x} - {y}) < card A"
+proof (cases "x = y")
+ case True
+ with assms show ?thesis
+ by (simp add: card_Diff1_less del: card_Diff_insert)
+next
+ case False
+ then have "card (A - {x} - {y}) < card (A - {x})" "card (A - {x}) < card A"
+ using assms by (intro card_Diff1_less; simp)+
+ then show ?thesis
+ by (blast intro: less_trans)
+qed
lemma card_Diff1_le: "finite A \<Longrightarrow> card (A - {x}) \<le> card A"
by (cases "x \<in> A") (simp_all add: card_Diff1_less less_imp_le)
@@ -1618,10 +1629,8 @@
obtain f where "f ` s \<subseteq> t" "inj_on f s"
by blast
with "2.prems"(2) "2.hyps"(2) show ?case
- apply -
- apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
- apply (auto simp add: inj_on_def)
- done
+ unfolding inj_on_def
+ by (rule_tac x = "\<lambda>z. if z = x then y else f z" in exI) auto
qed
qed
@@ -1800,10 +1809,7 @@
lemma card_Suc_eq:
"card A = Suc k \<longleftrightarrow>
(\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
- apply (auto elim!: card_eq_SucD)
- apply (subst card.insert)
- apply (auto simp add: intro:ccontr)
- done
+ by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD)
lemma card_1_singletonE:
assumes "card A = 1"
@@ -1836,10 +1842,11 @@
lemma card_le_Suc_iff:
"Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
-apply(cases "finite A")
- apply (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
- dest: subset_singletonD split: nat.splits if_splits)
-by auto
+proof (cases "finite A")
+ case True
+ then show ?thesis
+ by (fastforce simp: card_Suc_eq less_eq_nat.simps split: nat.splits)
+qed auto
lemma finite_fun_UNIVD2:
assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
@@ -1886,7 +1893,7 @@
case False
obtain n::nat where n: "n > max C 0" by auto
obtain G where G: "G \<subseteq> F" "card G = n" using infinite_arbitrarily_large[OF False] by auto
- hence "finite G" using \<open>n > max C 0\<close> using card_infinite gr_implies_not0 by blast
+ hence "finite G" using \<open>n > max C 0\<close> using card.infinite gr_implies_not0 by blast
hence False using assms G n not_less by auto
thus ?thesis ..
next
@@ -2042,12 +2049,11 @@
case empty
show ?case by simp
next
- case insert
- then show ?case
- apply simp
- apply (subst card_Un_disjoint)
- apply (auto simp add: disjoint_eq_subset_Compl)
- done
+ case (insert c C)
+ then have "c \<inter> \<Union>C = {}"
+ by auto
+ with insert show ?case
+ by (simp add: card_Un_disjoint)
qed
qed
@@ -2209,10 +2215,10 @@
then have "X (A - {x})"
using psubset.hyps by blast
show False
- apply (rule psubset.IH [where B = "A - {x}"])
- apply (use \<open>x \<in> A\<close> in blast)
- apply (simp add: \<open>X (A - {x})\<close>)
- done
+ proof (rule psubset.IH [where B = "A - {x}"])
+ show "A - {x} \<subset> A"
+ using \<open>x \<in> A\<close> by blast
+ qed fact
qed
qed
--- a/src/HOL/Library/FSet.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/FSet.thy Fri Sep 25 14:11:48 2020 +0100
@@ -600,7 +600,7 @@
lemma fcard_fempty:
"fcard {||} = 0"
- by transfer (rule card_empty)
+ by transfer (rule card.empty)
lemma fcard_finsert_disjoint:
"x |\<notin>| A \<Longrightarrow> fcard (finsert x A) = Suc (fcard A)"
@@ -632,7 +632,7 @@
using assms by transfer (rule card_Diff_insert)
lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A |-| {|x|}))"
-by transfer (rule card_insert)
+by transfer (rule card.insert_remove)
lemma fcard_finsert_le: "fcard A \<le> fcard (finsert x A)"
by transfer (rule card_insert_le)
--- a/src/HOL/Library/Infinite_Set.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Fri Sep 25 14:11:48 2020 +0100
@@ -417,7 +417,7 @@
proof (induction n arbitrary: S)
case 0
then show ?case
- by (metis all_not_in_conv card_empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
+ by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
next
case (Suc n)
show ?case
--- a/src/HOL/Library/Perm.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Perm.thy Fri Sep 25 14:11:48 2020 +0100
@@ -365,7 +365,7 @@
then obtain B b where "affected f = insert b B"
by blast
with finite_affected [of f] have "card (affected f) \<ge> 1"
- by (simp add: card_insert)
+ by (simp add: card.insert_remove)
case False then have "order f a = 1"
by (simp add: order_eq_one_iff)
with \<open>card (affected f) \<ge> 1\<close> show ?thesis
--- a/src/HOL/Library/Permutations.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Permutations.thy Fri Sep 25 14:11:48 2020 +0100
@@ -334,20 +334,20 @@
case (insert x F)
{
fix n
- assume card_insert: "card (insert x F) = n"
+ assume card.insert_remove: "card (insert x F) = n"
let ?xF = "{p. p permutes insert x F}"
let ?pF = "{p. p permutes F}"
let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
have xfgpF': "?xF = ?g ` ?pF'"
by (rule permutes_insert[of x F])
- from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have Fs: "card F = n - 1"
+ from \<open>x \<notin> F\<close> \<open>finite F\<close> card.insert_remove have Fs: "card F = n - 1"
by auto
from \<open>finite F\<close> insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
by auto
then have "finite ?pF"
by (auto intro: card_ge_0_finite)
- with \<open>finite F\<close> card_insert have pF'f: "finite ?pF'"
+ with \<open>finite F\<close> card.insert_remove have pF'f: "finite ?pF'"
apply (simp only: Collect_case_prod Collect_mem_eq)
apply (rule finite_cartesian_product)
apply simp_all
@@ -383,13 +383,13 @@
then show ?thesis
unfolding inj_on_def by blast
qed
- from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have "n \<noteq> 0"
+ from \<open>x \<notin> F\<close> \<open>finite F\<close> card.insert_remove have "n \<noteq> 0"
by auto
then have "\<exists>m. n = Suc m"
by presburger
then obtain m where n: "n = Suc m"
by blast
- from pFs card_insert have *: "card ?xF = fact n"
+ from pFs card.insert_remove have *: "card ?xF = fact n"
unfolding xfgpF' card_image[OF ginj]
using \<open>finite F\<close> \<open>finite ?pF\<close>
by (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product) (simp add: n)
--- a/src/HOL/List.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/List.thy Fri Sep 25 14:11:48 2020 +0100
@@ -5326,7 +5326,7 @@
assumes "k < card A"
shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"
proof -
- from \<open>k < card A\<close> have "finite A" and "k \<le> card A" using card_infinite by force+
+ from \<open>k < card A\<close> have "finite A" and "k \<le> card A" using card.infinite by force+
from this show ?thesis by (rule card_lists_distinct_length_eq)
qed
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Fri Sep 25 14:11:48 2020 +0100
@@ -294,7 +294,7 @@
have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC"
unfolding B_def C_def BuC_def by fastforce+
then show ?thesis
- unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
+ unfolding b_def c_def using card.empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
qed
definition f_2:: "int \<Rightarrow> int"
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Fri Sep 25 14:11:48 2020 +0100
@@ -235,7 +235,7 @@
assume H: "liseq' xs j = card is" "is \<in> iseq xs (Suc j)"
"finite is" "Max is = j" "is \<noteq> {}"
from H j have "card is + 1 = card (is \<union> {i})"
- by (simp add: card_insert max_notin)
+ by (simp add: card.insert_remove max_notin)
moreover {
from H j have "xs (Max is) \<le> xs i" by simp
moreover from \<open>j < i\<close> have "Suc j \<le> i" by simp
@@ -367,7 +367,7 @@
apply (rule_tac xs=xs and i=i in liseq'_expand)
apply simp
apply (rule_tac js="isa \<union> {j}" in liseq_eq [symmetric])
- apply (simp add: card_insert card_Diff_singleton_if max_notin)
+ apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
apply (rule iseq_insert)
apply simp
apply (erule iseq_mono)
@@ -388,9 +388,9 @@
apply simp
apply (rule le_diff_iff [THEN iffD1, of 1])
apply (simp add: card_0_eq [symmetric] del: card_0_eq)
- apply (simp add: card_insert)
+ apply (simp add: card.insert_remove)
apply (subgoal_tac "card (js' - {j}) = card js' - 1")
- apply (simp add: card_insert card_Diff_singleton_if max_notin)
+ apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
apply (frule_tac A=js' in Max_in)
apply assumption
apply (simp add: card_Diff_singleton_if)
@@ -411,7 +411,7 @@
apply (rule_tac xs=xs and i=i in liseq'_expand)
apply simp
apply (rule_tac js="isa \<union> {j}" in liseq'_eq [symmetric])
- apply (simp add: card_insert card_Diff_singleton_if max_notin)
+ apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
apply (rule iseq_insert)
apply simp
apply (erule iseq_mono)
@@ -434,9 +434,9 @@
apply simp
apply (rule le_diff_iff [THEN iffD1, of 1])
apply (simp add: card_0_eq [symmetric] del: card_0_eq)
- apply (simp add: card_insert)
+ apply (simp add: card.insert_remove)
apply (subgoal_tac "card (js' - {j}) = card js' - 1")
- apply (simp add: card_insert card_Diff_singleton_if max_notin)
+ apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
apply (frule_tac A=js' in Max_in)
apply assumption
apply (simp add: card_Diff_singleton_if)
--- a/src/HOL/Set_Interval.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Set_Interval.thy Fri Sep 25 14:11:48 2020 +0100
@@ -1538,7 +1538,7 @@
also have "\<dots> = Suc (card ({k \<in> M. k < Suc i} - {0}))"
by (force intro: arg_cong [where f=card])
also have "\<dots> = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
- by (simp add: card_insert)
+ by (simp add: card.insert_remove)
also have "... = card {k \<in> M. k < Suc i}"
using assms
by (force simp add: intro: arg_cong [where f=card])
--- a/src/HOL/Vector_Spaces.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Vector_Spaces.thy Fri Sep 25 14:11:48 2020 +0100
@@ -1453,7 +1453,7 @@
have "b \<notin> f ` B1" using vs2.span_base[of b "f ` B1"] b by auto
then have "Suc (card B1) = card (insert b (f ` B1))"
- using sf[THEN inj_on_subset, of B1] by (subst card_insert) (auto intro: vs1.finite_Basis simp: card_image)
+ using sf[THEN inj_on_subset, of B1] by (subst card.insert_remove) (auto intro: vs1.finite_Basis simp: card_image)
also have "\<dots> = vs2.dim (insert b (f ` B1))"
using vs2.dim_eq_card_independent[OF **] by simp
also have "vs2.dim (insert b (f ` B1)) \<le> vs2.dim B2"