resolvd conflict
authornipkow
Sun Jul 12 11:25:56 2009 +0200 (2009-07-12)
changeset 319932ce88db62a84
parent 31991 37390299214a
parent 31992 f8aed98faae7
child 31994 f88e4f494832
resolvd conflict
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sat Jul 11 21:33:01 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sun Jul 12 11:25:56 2009 +0200
     1.3 @@ -218,6 +218,12 @@
     1.4   "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
     1.5  by (induct rule:finite_induct) simp_all
     1.6  
     1.7 +lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)"
     1.8 +by (blast intro: Inter_lower finite_subset)
     1.9 +
    1.10 +lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)"
    1.11 +by (blast intro: INT_lower finite_subset)
    1.12 +
    1.13  lemma finite_empty_induct:
    1.14    assumes "finite A"
    1.15      and "P A"
    1.16 @@ -784,6 +790,62 @@
    1.17  
    1.18  end
    1.19  
    1.20 +context ab_semigroup_idem_mult
    1.21 +begin
    1.22 +
    1.23 +lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
    1.24 +apply unfold_locales
    1.25 + apply (simp add: mult_ac)
    1.26 +apply (simp add: mult_idem mult_assoc[symmetric])
    1.27 +done
    1.28 +
    1.29 +end
    1.30 +
    1.31 +context lower_semilattice
    1.32 +begin
    1.33 +
    1.34 +lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
    1.35 +proof qed (rule inf_assoc inf_commute inf_idem)+
    1.36 +
    1.37 +lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
    1.38 +by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
    1.39 +
    1.40 +lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
    1.41 +by (induct pred:finite) auto
    1.42 +
    1.43 +lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
    1.44 +proof(induct arbitrary: a pred:finite)
    1.45 +  case empty thus ?case by simp
    1.46 +next
    1.47 +  case (insert x A)
    1.48 +  show ?case
    1.49 +  proof cases
    1.50 +    assume "A = {}" thus ?thesis using insert by simp
    1.51 +  next
    1.52 +    assume "A \<noteq> {}" thus ?thesis using insert by auto
    1.53 +  qed
    1.54 +qed
    1.55 +
    1.56 +end
    1.57 +
    1.58 +context upper_semilattice
    1.59 +begin
    1.60 +
    1.61 +lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
    1.62 +by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
    1.63 +
    1.64 +lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
    1.65 +by(rule lower_semilattice.fold_inf_insert)(rule dual_semlattice)
    1.66 +
    1.67 +lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
    1.68 +by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice)
    1.69 +
    1.70 +lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
    1.71 +by(rule lower_semilattice.fold_inf_le_inf)(rule dual_semilattice)
    1.72 +
    1.73 +end
    1.74 +
    1.75 +
    1.76  subsubsection{* The derived combinator @{text fold_image} *}
    1.77  
    1.78  definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
    1.79 @@ -801,7 +863,7 @@
    1.80  proof -
    1.81    interpret I: fun_left_comm "%x y. (g x) * y"
    1.82      by unfold_locales (simp add: mult_ac)
    1.83 -  show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
    1.84 +  show ?thesis using assms by(simp add:fold_image_def)
    1.85  qed
    1.86  
    1.87  (*
    1.88 @@ -829,10 +891,7 @@
    1.89  lemma fold_image_reindex:
    1.90  assumes fin: "finite A"
    1.91  shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
    1.92 -using fin apply induct
    1.93 - apply simp
    1.94 -apply simp
    1.95 -done
    1.96 +using fin by induct auto
    1.97  
    1.98  (*
    1.99  text{*
   1.100 @@ -2351,14 +2410,15 @@
   1.101  shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
   1.102  by(fastsimp simp:surj_def dest!: endo_inj_surj)
   1.103  
   1.104 -corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
   1.105 +corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
   1.106  proof
   1.107    assume "finite(UNIV::nat set)"
   1.108    with finite_UNIV_inj_surj[of Suc]
   1.109    show False by simp (blast dest: Suc_neq_Zero surjD)
   1.110  qed
   1.111  
   1.112 -lemma infinite_UNIV_char_0:
   1.113 +(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
   1.114 +lemma infinite_UNIV_char_0[noatp]:
   1.115    "\<not> finite (UNIV::'a::semiring_char_0 set)"
   1.116  proof
   1.117    assume "finite (UNIV::'a set)"
   1.118 @@ -2499,13 +2559,6 @@
   1.119  context ab_semigroup_idem_mult
   1.120  begin
   1.121  
   1.122 -lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
   1.123 -apply unfold_locales
   1.124 - apply (simp add: mult_ac)
   1.125 -apply (simp add: mult_idem mult_assoc[symmetric])
   1.126 -done
   1.127 -
   1.128 -
   1.129  lemma fold1_insert_idem [simp]:
   1.130    assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   1.131    shows "fold1 times (insert x A) = x * fold1 times A"
   1.132 @@ -2667,10 +2720,6 @@
   1.133  context lower_semilattice
   1.134  begin
   1.135  
   1.136 -lemma ab_semigroup_idem_mult_inf:
   1.137 -  "ab_semigroup_idem_mult inf"
   1.138 -  proof qed (rule inf_assoc inf_commute inf_idem)+
   1.139 -
   1.140  lemma below_fold1_iff:
   1.141    assumes "finite A" "A \<noteq> {}"
   1.142    shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   1.143 @@ -2716,11 +2765,6 @@
   1.144  
   1.145  end
   1.146  
   1.147 -lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
   1.148 -  "ab_semigroup_idem_mult sup"
   1.149 -  by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
   1.150 -    (rule dual_semilattice)
   1.151 -
   1.152  context lattice
   1.153  begin
   1.154  
     2.1 --- a/src/HOL/GCD.thy	Sat Jul 11 21:33:01 2009 +0200
     2.2 +++ b/src/HOL/GCD.thy	Sun Jul 12 11:25:56 2009 +0200
     2.3 @@ -34,7 +34,7 @@
     2.4  
     2.5  subsection {* gcd *}
     2.6  
     2.7 -class gcd = one +
     2.8 +class gcd = zero + one + dvd +
     2.9  
    2.10  fixes
    2.11    gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    2.12 @@ -537,8 +537,8 @@
    2.13  
    2.14  (* to do: add the three variations of these, and for ints? *)
    2.15  
    2.16 -lemma finite_divisors_nat:
    2.17 -  assumes "(m::nat)~= 0" shows "finite{d. d dvd m}"
    2.18 +lemma finite_divisors_nat[simp]:
    2.19 +  assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
    2.20  proof-
    2.21    have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
    2.22    from finite_subset[OF _ this] show ?thesis using assms
    2.23 @@ -1439,31 +1439,46 @@
    2.24  lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
    2.25  by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
    2.26  
    2.27 +lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
    2.28 +by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
    2.29 +
    2.30 +lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
    2.31 +by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
    2.32 +
    2.33 +lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
    2.34 +by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
    2.35 +
    2.36 +lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
    2.37 +by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
    2.38  
    2.39  lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
    2.40 -apply(rule lcm_unique_nat[THEN iffD1])
    2.41 -apply (metis dvd.order_trans lcm_unique_nat)
    2.42 -done
    2.43 +by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
    2.44  
    2.45  lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
    2.46 -apply(rule lcm_unique_int[THEN iffD1])
    2.47 -apply (metis dvd_trans lcm_unique_int)
    2.48 -done
    2.49 +by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
    2.50  
    2.51 -lemmas lcm_left_commute_nat =
    2.52 -  mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
    2.53 -
    2.54 -lemmas lcm_left_commute_int =
    2.55 -  mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
    2.56 +lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
    2.57 +lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
    2.58  
    2.59  lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
    2.60  lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
    2.61  
    2.62 +lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
    2.63 +proof qed (auto simp add: gcd_ac_nat)
    2.64 +
    2.65 +lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
    2.66 +proof qed (auto simp add: gcd_ac_int)
    2.67 +
    2.68 +lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
    2.69 +proof qed (auto simp add: lcm_ac_nat)
    2.70 +
    2.71 +lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
    2.72 +proof qed (auto simp add: lcm_ac_int)
    2.73 +
    2.74  
    2.75  subsection {* Primes *}
    2.76  
    2.77 -(* Is there a better way to handle these, rather than making them
    2.78 -   elim rules? *)
    2.79 +(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    2.80  
    2.81  lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
    2.82    by (unfold prime_nat_def, auto)
    2.83 @@ -1487,7 +1502,7 @@
    2.84    by (unfold prime_nat_def, auto)
    2.85  
    2.86  lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
    2.87 -  by (unfold prime_int_def prime_nat_def, auto)
    2.88 +  by (unfold prime_int_def prime_nat_def) auto
    2.89  
    2.90  lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
    2.91    by (unfold prime_int_def prime_nat_def, auto)
    2.92 @@ -1501,8 +1516,6 @@
    2.93  lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
    2.94    by (unfold prime_int_def prime_nat_def, auto)
    2.95  
    2.96 -thm prime_nat_def;
    2.97 -thm prime_nat_def [transferred];
    2.98  
    2.99  lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   2.100      m = 1 \<or> m = p))"
   2.101 @@ -1563,35 +1576,13 @@
   2.102  lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   2.103      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   2.104    unfolding prime_nat_def dvd_def apply auto
   2.105 -  apply (subgoal_tac "k > 1")
   2.106 -  apply force
   2.107 -  apply (subgoal_tac "k ~= 0")
   2.108 -  apply force
   2.109 -  apply (rule notI)
   2.110 -  apply force
   2.111 -done
   2.112 +  by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   2.113  
   2.114 -(* there's a lot of messing around with signs of products here --
   2.115 -   could this be made more automatic? *)
   2.116  lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   2.117      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   2.118    unfolding prime_int_altdef dvd_def
   2.119    apply auto
   2.120 -  apply (rule_tac x = m in exI)
   2.121 -  apply (rule_tac x = k in exI)
   2.122 -  apply (auto simp add: mult_compare_simps)
   2.123 -  apply (subgoal_tac "k > 0")
   2.124 -  apply arith
   2.125 -  apply (case_tac "k <= 0")
   2.126 -  apply (subgoal_tac "m * k <= 0")
   2.127 -  apply force
   2.128 -  apply (subst zero_compare_simps(8))
   2.129 -  apply auto
   2.130 -  apply (subgoal_tac "m * k <= 0")
   2.131 -  apply force
   2.132 -  apply (subst zero_compare_simps(8))
   2.133 -  apply auto
   2.134 -done
   2.135 +  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
   2.136  
   2.137  lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
   2.138      n > 0 --> (p dvd x^n --> p dvd x)"
     3.1 --- a/src/HOL/Library/Countable.thy	Sat Jul 11 21:33:01 2009 +0200
     3.2 +++ b/src/HOL/Library/Countable.thy	Sun Jul 12 11:25:56 2009 +0200
     3.3 @@ -58,7 +58,7 @@
     3.4  subclass (in finite) countable
     3.5  proof
     3.6    have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
     3.7 -  with finite_conv_nat_seg_image [of UNIV]
     3.8 +  with finite_conv_nat_seg_image [of "UNIV::'a set"]
     3.9    obtain n and f :: "nat \<Rightarrow> 'a" 
    3.10      where "UNIV = f ` {i. i < n}" by auto
    3.11    then have "surj f" unfolding surj_def by auto