tuned proofs;
authorwenzelm
Fri Jun 26 00:14:10 2015 +0200 (2015-06-26)
changeset 60583a645a0e6d790
parent 60582 d694f217ee41
child 60584 6ac3172985d4
child 60585 48fdff264eb2
tuned proofs;
src/HOL/Library/Cardinality.thy
src/HOL/Library/FinFun.thy
src/HOL/Number_Theory/Eratosthenes.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Thu Jun 25 23:51:54 2015 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Jun 26 00:14:10 2015 +0200
     1.3 @@ -470,23 +470,39 @@
     1.4    in if n = 0 then False else 
     1.5          let xs' = remdups xs; ys' = remdups ys 
     1.6          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')"
     1.7 -  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
     1.8 -  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
     1.9 -  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)
    1.10 -  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)
    1.11 -proof -
    1.12 -  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
    1.13 -  proof
    1.14 -    assume ?lhs thus ?rhs
    1.15 -      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)
    1.16 -  next
    1.17 -    assume ?rhs
    1.18 -    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
    1.19 -    ultimately show ?lhs
    1.20 -      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)
    1.21 -  qed
    1.22 -  thus ?thesis2 unfolding eq_set_def by blast
    1.23 -  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
    1.24 +  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs"
    1.25 +  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
    1.26 +  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)"
    1.27 +  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)"
    1.28 +proof goals
    1.29 +  {
    1.30 +    case 1
    1.31 +    show ?case (is "?lhs \<longleftrightarrow> ?rhs")
    1.32 +    proof
    1.33 +      show ?rhs if ?lhs
    1.34 +        using that
    1.35 +        by (auto simp add: rhs_def Let_def List.card_set[symmetric]
    1.36 +          card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
    1.37 +          Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
    1.38 +      show ?lhs if ?rhs
    1.39 +      proof - 
    1.40 +        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
    1.41 +        with that show ?thesis
    1.42 +          by (auto simp add: rhs_def Let_def List.card_set[symmetric]
    1.43 +            card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
    1.44 +            dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
    1.45 +      qed
    1.46 +    qed
    1.47 +  }
    1.48 +  moreover
    1.49 +  case 2
    1.50 +  ultimately show ?case unfolding eq_set_def by blast
    1.51 +next
    1.52 +  case 3
    1.53 +  show ?case unfolding eq_set_def List.coset_def by blast
    1.54 +next
    1.55 +  case 4
    1.56 +  show ?case unfolding eq_set_def List.coset_def by blast
    1.57  qed
    1.58  
    1.59  end
     2.1 --- a/src/HOL/Library/FinFun.thy	Thu Jun 25 23:51:54 2015 +0200
     2.2 +++ b/src/HOL/Library/FinFun.thy	Fri Jun 26 00:14:10 2015 +0200
     2.3 @@ -1320,11 +1320,10 @@
     2.4  lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
     2.5    and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
     2.6    and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
     2.7 -proof -
     2.8 -  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
     2.9 +proof (atomize (full))
    2.10 +  show "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
    2.11      unfolding finfun_to_list_def
    2.12      by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
    2.13 -  thus ?thesis1 ?thesis2 ?thesis3 by simp_all
    2.14  qed
    2.15  
    2.16  lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"
     3.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Thu Jun 25 23:51:54 2015 +0200
     3.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 26 00:14:10 2015 +0200
     3.3 @@ -119,15 +119,20 @@
     3.4  qed
     3.5  
     3.6  lemma mark_out_aux_simps [simp, code]:
     3.7 -  "mark_out_aux n m [] = []" (is ?thesis1)
     3.8 -  "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs" (is ?thesis2)
     3.9 -  "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs" (is ?thesis3)
    3.10 -proof -
    3.11 -  show ?thesis1
    3.12 +  "mark_out_aux n m [] = []"
    3.13 +  "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs"
    3.14 +  "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs"
    3.15 +proof goals
    3.16 +  case 1
    3.17 +  show ?case
    3.18      by (simp add: mark_out_aux_def)
    3.19 -  show ?thesis2
    3.20 +next
    3.21 +  case 2
    3.22 +  show ?case
    3.23      by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def
    3.24        enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus)
    3.25 +next
    3.26 +  case 3
    3.27    { def v \<equiv> "Suc m" and w \<equiv> "Suc n"
    3.28      fix q
    3.29      assume "m + n \<le> q"
    3.30 @@ -150,7 +155,7 @@
    3.31        Suc n dvd Suc (Suc (q + n - m mod Suc n))"
    3.32        by (simp add: v_def w_def Suc_diff_le trans_le_add2)
    3.33    }
    3.34 -  then show ?thesis3
    3.35 +  then show ?case
    3.36      by (auto simp add: mark_out_aux_def
    3.37        enumerate_Suc_eq in_set_enumerate_eq not_less)
    3.38  qed