--- a/src/HOL/Library/Cardinality.thy Thu Jun 25 23:51:54 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy Fri Jun 26 00:14:10 2015 +0200
@@ -470,23 +470,39 @@
in if n = 0 then False else
let xs' = remdups xs; ys' = remdups ys
in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
- shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
- and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
- and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
- and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
-proof -
- show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
- proof
- assume ?lhs thus ?rhs
- by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
- next
- assume ?rhs
- moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
- ultimately show ?lhs
- by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
- qed
- thus ?thesis2 unfolding eq_set_def by blast
- show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
+ shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs"
+ and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
+ and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+ and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+proof goals
+ {
+ case 1
+ show ?case (is "?lhs \<longleftrightarrow> ?rhs")
+ proof
+ show ?rhs if ?lhs
+ using that
+ by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+ card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
+ Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
+ show ?lhs if ?rhs
+ proof -
+ have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
+ with that show ?thesis
+ by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+ card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
+ dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
+ qed
+ qed
+ }
+ moreover
+ case 2
+ ultimately show ?case unfolding eq_set_def by blast
+next
+ case 3
+ show ?case unfolding eq_set_def List.coset_def by blast
+next
+ case 4
+ show ?case unfolding eq_set_def List.coset_def by blast
qed
end
--- a/src/HOL/Library/FinFun.thy Thu Jun 25 23:51:54 2015 +0200
+++ b/src/HOL/Library/FinFun.thy Fri Jun 26 00:14:10 2015 +0200
@@ -1320,11 +1320,10 @@
lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
-proof -
- have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
+proof (atomize (full))
+ show "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
unfolding finfun_to_list_def
by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
- thus ?thesis1 ?thesis2 ?thesis3 by simp_all
qed
lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"
--- a/src/HOL/Number_Theory/Eratosthenes.thy Thu Jun 25 23:51:54 2015 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Fri Jun 26 00:14:10 2015 +0200
@@ -119,15 +119,20 @@
qed
lemma mark_out_aux_simps [simp, code]:
- "mark_out_aux n m [] = []" (is ?thesis1)
- "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs" (is ?thesis2)
- "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs" (is ?thesis3)
-proof -
- show ?thesis1
+ "mark_out_aux n m [] = []"
+ "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs"
+ "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs"
+proof goals
+ case 1
+ show ?case
by (simp add: mark_out_aux_def)
- show ?thesis2
+next
+ case 2
+ show ?case
by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def
enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus)
+next
+ case 3
{ def v \<equiv> "Suc m" and w \<equiv> "Suc n"
fix q
assume "m + n \<le> q"
@@ -150,7 +155,7 @@
Suc n dvd Suc (Suc (q + n - m mod Suc n))"
by (simp add: v_def w_def Suc_diff_le trans_le_add2)
}
- then show ?thesis3
+ then show ?case
by (auto simp add: mark_out_aux_def
enumerate_Suc_eq in_set_enumerate_eq not_less)
qed