author nipkow Sun Jul 12 10:14:51 2009 +0200 (2009-07-12) changeset 31992 f8aed98faae7 parent 31990 1d4d0b305f16 child 31993 2ce88db62a84
More about gcd/lcm, and some cleaning up
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/Library/Countable.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jul 10 09:24:50 2009 +0200
1.2 +++ b/src/HOL/Finite_Set.thy	Sun Jul 12 10:14:51 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_lattice)
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_lattice)
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_lattice)
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_lattice)
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_lattice)
1.151 -
1.152  context lattice
1.153  begin
1.154
```
```     2.1 --- a/src/HOL/GCD.thy	Fri Jul 10 09:24:50 2009 +0200
2.2 +++ b/src/HOL/GCD.thy	Sun Jul 12 10:14:51 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	Fri Jul 10 09:24:50 2009 +0200
3.2 +++ b/src/HOL/Library/Countable.thy	Sun Jul 12 10:14:51 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
```