merged
authorberghofe
Tue Jul 14 17:18:51 2009 +0200 (2009-07-14)
changeset 32040830141c9e528
parent 32039 400a519bc888
parent 31996 1d93369079c4
child 32041 b09916780820
merged
src/HOL/GCD.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 14 17:17:37 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 14 17:18: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_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_semilattice)
    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_lattice)
   1.151 -
   1.152  context lattice
   1.153  begin
   1.154  
   1.155 @@ -2741,7 +2785,7 @@
   1.156  apply(erule exE)
   1.157  apply(rule order_trans)
   1.158  apply(erule (1) fold1_belowI)
   1.159 -apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
   1.160 +apply(erule (1) lower_semilattice.fold1_belowI [OF dual_semilattice])
   1.161  done
   1.162  
   1.163  lemma sup_Inf_absorb [simp]:
   1.164 @@ -2753,7 +2797,7 @@
   1.165  lemma inf_Sup_absorb [simp]:
   1.166    "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
   1.167  by (simp add: Sup_fin_def inf_absorb1
   1.168 -  lower_semilattice.fold1_belowI [OF dual_lattice])
   1.169 +  lower_semilattice.fold1_belowI [OF dual_semilattice])
   1.170  
   1.171  end
   1.172  
     2.1 --- a/src/HOL/GCD.thy	Tue Jul 14 17:17:37 2009 +0200
     2.2 +++ b/src/HOL/GCD.thy	Tue Jul 14 17:18:51 2009 +0200
     2.3 @@ -37,7 +37,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 @@ -540,15 +540,15 @@
    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      by(bestsimp intro!:dvd_imp_le)
    2.24  qed
    2.25  
    2.26 -lemma finite_divisors_int:
    2.27 +lemma finite_divisors_int[simp]:
    2.28    assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
    2.29  proof-
    2.30    have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
    2.31 @@ -557,10 +557,25 @@
    2.32      by(bestsimp intro!:dvd_imp_le_int)
    2.33  qed
    2.34  
    2.35 +lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
    2.36 +apply(rule antisym)
    2.37 + apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
    2.38 +apply simp
    2.39 +done
    2.40 +
    2.41 +lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
    2.42 +apply(rule antisym)
    2.43 + apply(rule Max_le_iff[THEN iffD2])
    2.44 +   apply simp
    2.45 +  apply fastsimp
    2.46 + apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
    2.47 +apply simp
    2.48 +done
    2.49 +
    2.50  lemma gcd_is_Max_divisors_nat:
    2.51    "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
    2.52  apply(rule Max_eqI[THEN sym])
    2.53 -  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
    2.54 +  apply (metis finite_Collect_conjI finite_divisors_nat)
    2.55   apply simp
    2.56   apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
    2.57  apply simp
    2.58 @@ -569,7 +584,7 @@
    2.59  lemma gcd_is_Max_divisors_int:
    2.60    "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
    2.61  apply(rule Max_eqI[THEN sym])
    2.62 -  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
    2.63 +  apply (metis finite_Collect_conjI finite_divisors_int)
    2.64   apply simp
    2.65   apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
    2.66  apply simp
    2.67 @@ -1442,31 +1457,61 @@
    2.68  lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
    2.69  by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
    2.70  
    2.71 +lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
    2.72 +by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
    2.73 +
    2.74 +lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
    2.75 +by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
    2.76 +
    2.77 +lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
    2.78 +by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
    2.79 +
    2.80 +lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
    2.81 +by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
    2.82  
    2.83  lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
    2.84 -apply(rule lcm_unique_nat[THEN iffD1])
    2.85 -apply (metis dvd.order_trans lcm_unique_nat)
    2.86 -done
    2.87 +by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
    2.88  
    2.89  lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
    2.90 -apply(rule lcm_unique_int[THEN iffD1])
    2.91 -apply (metis dvd_trans lcm_unique_int)
    2.92 -done
    2.93 +by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
    2.94  
    2.95 -lemmas lcm_left_commute_nat =
    2.96 -  mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
    2.97 -
    2.98 -lemmas lcm_left_commute_int =
    2.99 -  mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
   2.100 +lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
   2.101 +lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
   2.102  
   2.103  lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   2.104  lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   2.105  
   2.106 +lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.107 +proof qed (auto simp add: gcd_ac_nat)
   2.108 +
   2.109 +lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
   2.110 +proof qed (auto simp add: gcd_ac_int)
   2.111 +
   2.112 +lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.113 +proof qed (auto simp add: lcm_ac_nat)
   2.114 +
   2.115 +lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   2.116 +proof qed (auto simp add: lcm_ac_int)
   2.117 +
   2.118 +
   2.119 +(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
   2.120 +
   2.121 +lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
   2.122 +by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
   2.123 +
   2.124 +lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
   2.125 +by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
   2.126 +
   2.127 +lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
   2.128 +by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
   2.129 +
   2.130 +lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
   2.131 +by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
   2.132 +
   2.133  
   2.134  subsection {* Primes *}
   2.135  
   2.136 -(* Is there a better way to handle these, rather than making them
   2.137 -   elim rules? *)
   2.138 +(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
   2.139  
   2.140  lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
   2.141    by (unfold prime_nat_def, auto)
   2.142 @@ -1490,7 +1535,7 @@
   2.143    by (unfold prime_nat_def, auto)
   2.144  
   2.145  lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
   2.146 -  by (unfold prime_int_def prime_nat_def, auto)
   2.147 +  by (unfold prime_int_def prime_nat_def) auto
   2.148  
   2.149  lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
   2.150    by (unfold prime_int_def prime_nat_def, auto)
   2.151 @@ -1504,8 +1549,6 @@
   2.152  lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   2.153    by (unfold prime_int_def prime_nat_def, auto)
   2.154  
   2.155 -thm prime_nat_def;
   2.156 -thm prime_nat_def [transferred];
   2.157  
   2.158  lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   2.159      m = 1 \<or> m = p))"
   2.160 @@ -1566,35 +1609,13 @@
   2.161  lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   2.162      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   2.163    unfolding prime_nat_def dvd_def apply auto
   2.164 -  apply (subgoal_tac "k > 1")
   2.165 -  apply force
   2.166 -  apply (subgoal_tac "k ~= 0")
   2.167 -  apply force
   2.168 -  apply (rule notI)
   2.169 -  apply force
   2.170 -done
   2.171 +  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.172  
   2.173 -(* there's a lot of messing around with signs of products here --
   2.174 -   could this be made more automatic? *)
   2.175  lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   2.176      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   2.177    unfolding prime_int_altdef dvd_def
   2.178    apply auto
   2.179 -  apply (rule_tac x = m in exI)
   2.180 -  apply (rule_tac x = k in exI)
   2.181 -  apply (auto simp add: mult_compare_simps)
   2.182 -  apply (subgoal_tac "k > 0")
   2.183 -  apply arith
   2.184 -  apply (case_tac "k <= 0")
   2.185 -  apply (subgoal_tac "m * k <= 0")
   2.186 -  apply force
   2.187 -  apply (subst zero_compare_simps(8))
   2.188 -  apply auto
   2.189 -  apply (subgoal_tac "m * k <= 0")
   2.190 -  apply force
   2.191 -  apply (subst zero_compare_simps(8))
   2.192 -  apply auto
   2.193 -done
   2.194 +  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.195  
   2.196  lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
   2.197      n > 0 --> (p dvd x^n --> p dvd x)"
     3.1 --- a/src/HOL/Lattices.thy	Tue Jul 14 17:17:37 2009 +0200
     3.2 +++ b/src/HOL/Lattices.thy	Tue Jul 14 17:18:51 2009 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5  text {* Dual lattice *}
     3.6  
     3.7 -lemma dual_lattice:
     3.8 +lemma dual_semilattice:
     3.9    "lower_semilattice (op \<ge>) (op >) sup"
    3.10  by (rule lower_semilattice.intro, rule dual_order)
    3.11    (unfold_locales, simp_all add: sup_least)
    3.12 @@ -180,6 +180,11 @@
    3.13  context lattice
    3.14  begin
    3.15  
    3.16 +lemma dual_lattice:
    3.17 +  "lattice (op \<ge>) (op >) sup inf"
    3.18 +  by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order)
    3.19 +    (unfold_locales, auto)
    3.20 +
    3.21  lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    3.22    by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
    3.23  
    3.24 @@ -252,12 +257,148 @@
    3.25   "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
    3.26  by(simp add:ACI inf_sup_distrib1)
    3.27  
    3.28 +lemma dual_distrib_lattice:
    3.29 +  "distrib_lattice (op \<ge>) (op >) sup inf"
    3.30 +  by (rule distrib_lattice.intro, rule dual_lattice)
    3.31 +    (unfold_locales, fact inf_sup_distrib1)
    3.32 +
    3.33  lemmas distrib =
    3.34    sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
    3.35  
    3.36  end
    3.37  
    3.38  
    3.39 +subsection {* Boolean algebras *}
    3.40 +
    3.41 +class boolean_algebra = distrib_lattice + top + bot + minus + uminus +
    3.42 +  assumes inf_compl_bot: "x \<sqinter> - x = bot"
    3.43 +    and sup_compl_top: "x \<squnion> - x = top"
    3.44 +  assumes diff_eq: "x - y = x \<sqinter> - y"
    3.45 +begin
    3.46 +
    3.47 +lemma dual_boolean_algebra:
    3.48 +  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot"
    3.49 +  by (rule boolean_algebra.intro, rule dual_distrib_lattice)
    3.50 +    (unfold_locales,
    3.51 +      auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le)
    3.52 +
    3.53 +lemma compl_inf_bot:
    3.54 +  "- x \<sqinter> x = bot"
    3.55 +  by (simp add: inf_commute inf_compl_bot)
    3.56 +
    3.57 +lemma compl_sup_top:
    3.58 +  "- x \<squnion> x = top"
    3.59 +  by (simp add: sup_commute sup_compl_top)
    3.60 +
    3.61 +lemma inf_bot_left [simp]:
    3.62 +  "bot \<sqinter> x = bot"
    3.63 +  by (rule inf_absorb1) simp
    3.64 +
    3.65 +lemma inf_bot_right [simp]:
    3.66 +  "x \<sqinter> bot = bot"
    3.67 +  by (rule inf_absorb2) simp
    3.68 +
    3.69 +lemma sup_top_left [simp]:
    3.70 +  "top \<squnion> x = top"
    3.71 +  by (rule sup_absorb1) simp
    3.72 +
    3.73 +lemma sup_top_right [simp]:
    3.74 +  "x \<squnion> top = top"
    3.75 +  by (rule sup_absorb2) simp
    3.76 +
    3.77 +lemma inf_top_left [simp]:
    3.78 +  "top \<sqinter> x = x"
    3.79 +  by (rule inf_absorb2) simp
    3.80 +
    3.81 +lemma inf_top_right [simp]:
    3.82 +  "x \<sqinter> top = x"
    3.83 +  by (rule inf_absorb1) simp
    3.84 +
    3.85 +lemma sup_bot_left [simp]:
    3.86 +  "bot \<squnion> x = x"
    3.87 +  by (rule sup_absorb2) simp
    3.88 +
    3.89 +lemma sup_bot_right [simp]:
    3.90 +  "x \<squnion> bot = x"
    3.91 +  by (rule sup_absorb1) simp
    3.92 +
    3.93 +lemma compl_unique:
    3.94 +  assumes "x \<sqinter> y = bot"
    3.95 +    and "x \<squnion> y = top"
    3.96 +  shows "- x = y"
    3.97 +proof -
    3.98 +  have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
    3.99 +    using inf_compl_bot assms(1) by simp
   3.100 +  then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
   3.101 +    by (simp add: inf_commute)
   3.102 +  then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
   3.103 +    by (simp add: inf_sup_distrib1)
   3.104 +  then have "- x \<sqinter> top = y \<sqinter> top"
   3.105 +    using sup_compl_top assms(2) by simp
   3.106 +  then show "- x = y" by (simp add: inf_top_right)
   3.107 +qed
   3.108 +
   3.109 +lemma double_compl [simp]:
   3.110 +  "- (- x) = x"
   3.111 +  using compl_inf_bot compl_sup_top by (rule compl_unique)
   3.112 +
   3.113 +lemma compl_eq_compl_iff [simp]:
   3.114 +  "- x = - y \<longleftrightarrow> x = y"
   3.115 +proof
   3.116 +  assume "- x = - y"
   3.117 +  then have "- x \<sqinter> y = bot"
   3.118 +    and "- x \<squnion> y = top"
   3.119 +    by (simp_all add: compl_inf_bot compl_sup_top)
   3.120 +  then have "- (- x) = y" by (rule compl_unique)
   3.121 +  then show "x = y" by simp
   3.122 +next
   3.123 +  assume "x = y"
   3.124 +  then show "- x = - y" by simp
   3.125 +qed
   3.126 +
   3.127 +lemma compl_bot_eq [simp]:
   3.128 +  "- bot = top"
   3.129 +proof -
   3.130 +  from sup_compl_top have "bot \<squnion> - bot = top" .
   3.131 +  then show ?thesis by simp
   3.132 +qed
   3.133 +
   3.134 +lemma compl_top_eq [simp]:
   3.135 +  "- top = bot"
   3.136 +proof -
   3.137 +  from inf_compl_bot have "top \<sqinter> - top = bot" .
   3.138 +  then show ?thesis by simp
   3.139 +qed
   3.140 +
   3.141 +lemma compl_inf [simp]:
   3.142 +  "- (x \<sqinter> y) = - x \<squnion> - y"
   3.143 +proof (rule compl_unique)
   3.144 +  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)"
   3.145 +    by (rule inf_sup_distrib1)
   3.146 +  also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   3.147 +    by (simp only: inf_commute inf_assoc inf_left_commute)
   3.148 +  finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = bot"
   3.149 +    by (simp add: inf_compl_bot)
   3.150 +next
   3.151 +  have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
   3.152 +    by (rule sup_inf_distrib2)
   3.153 +  also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
   3.154 +    by (simp only: sup_commute sup_assoc sup_left_commute)
   3.155 +  finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = top"
   3.156 +    by (simp add: sup_compl_top)
   3.157 +qed
   3.158 +
   3.159 +lemma compl_sup [simp]:
   3.160 +  "- (x \<squnion> y) = - x \<sqinter> - y"
   3.161 +proof -
   3.162 +  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
   3.163 +    by (rule dual_boolean_algebra)
   3.164 +  then show ?thesis by simp
   3.165 +qed
   3.166 +
   3.167 +end
   3.168 +
   3.169 +
   3.170  subsection {* Uniqueness of inf and sup *}
   3.171  
   3.172  lemma (in lower_semilattice) inf_unique:
   3.173 @@ -330,17 +471,24 @@
   3.174  
   3.175  subsection {* Bool as lattice *}
   3.176  
   3.177 -instantiation bool :: distrib_lattice
   3.178 +instantiation bool :: boolean_algebra
   3.179  begin
   3.180  
   3.181  definition
   3.182 +  bool_Compl_def: "uminus = Not"
   3.183 +
   3.184 +definition
   3.185 +  bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
   3.186 +
   3.187 +definition
   3.188    inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   3.189  
   3.190  definition
   3.191    sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   3.192  
   3.193 -instance
   3.194 -  by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
   3.195 +instance proof
   3.196 +qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def
   3.197 +  bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto)
   3.198  
   3.199  end
   3.200  
   3.201 @@ -369,7 +517,33 @@
   3.202  end
   3.203  
   3.204  instance "fun" :: (type, distrib_lattice) distrib_lattice
   3.205 -  by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   3.206 +proof
   3.207 +qed (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   3.208 +
   3.209 +instantiation "fun" :: (type, uminus) uminus
   3.210 +begin
   3.211 +
   3.212 +definition
   3.213 +  fun_Compl_def: "- A = (\<lambda>x. - A x)"
   3.214 +
   3.215 +instance ..
   3.216 +
   3.217 +end
   3.218 +
   3.219 +instantiation "fun" :: (type, minus) minus
   3.220 +begin
   3.221 +
   3.222 +definition
   3.223 +  fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   3.224 +
   3.225 +instance ..
   3.226 +
   3.227 +end
   3.228 +
   3.229 +instance "fun" :: (type, boolean_algebra) boolean_algebra
   3.230 +proof
   3.231 +qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def
   3.232 +  inf_compl_bot sup_compl_top diff_eq)
   3.233  
   3.234  
   3.235  text {* redundant bindings *}
     4.1 --- a/src/HOL/Library/Countable.thy	Tue Jul 14 17:17:37 2009 +0200
     4.2 +++ b/src/HOL/Library/Countable.thy	Tue Jul 14 17:18:51 2009 +0200
     4.3 @@ -58,7 +58,7 @@
     4.4  subclass (in finite) countable
     4.5  proof
     4.6    have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
     4.7 -  with finite_conv_nat_seg_image [of UNIV]
     4.8 +  with finite_conv_nat_seg_image [of "UNIV::'a set"]
     4.9    obtain n and f :: "nat \<Rightarrow> 'a" 
    4.10      where "UNIV = f ` {i. i < n}" by auto
    4.11    then have "surj f" unfolding surj_def by auto
     5.1 --- a/src/HOL/Set.thy	Tue Jul 14 17:17:37 2009 +0200
     5.2 +++ b/src/HOL/Set.thy	Tue Jul 14 17:18:51 2009 +0200
     5.3 @@ -10,7 +10,6 @@
     5.4  
     5.5  text {* A set in HOL is simply a predicate. *}
     5.6  
     5.7 -
     5.8  subsection {* Basic syntax *}
     5.9  
    5.10  global
    5.11 @@ -363,46 +362,6 @@
    5.12    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
    5.13    Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
    5.14  
    5.15 -instantiation "fun" :: (type, minus) minus
    5.16 -begin
    5.17 -
    5.18 -definition
    5.19 -  fun_diff_def: "A - B = (%x. A x - B x)"
    5.20 -
    5.21 -instance ..
    5.22 -
    5.23 -end
    5.24 -
    5.25 -instantiation bool :: minus
    5.26 -begin
    5.27 -
    5.28 -definition
    5.29 -  bool_diff_def: "A - B = (A & ~ B)"
    5.30 -
    5.31 -instance ..
    5.32 -
    5.33 -end
    5.34 -
    5.35 -instantiation "fun" :: (type, uminus) uminus
    5.36 -begin
    5.37 -
    5.38 -definition
    5.39 -  fun_Compl_def: "- A = (%x. - A x)"
    5.40 -
    5.41 -instance ..
    5.42 -
    5.43 -end
    5.44 -
    5.45 -instantiation bool :: uminus
    5.46 -begin
    5.47 -
    5.48 -definition
    5.49 -  bool_Compl_def: "- A = (~ A)"
    5.50 -
    5.51 -instance ..
    5.52 -
    5.53 -end
    5.54 -
    5.55  definition Pow :: "'a set => 'a set set" where
    5.56    Pow_def: "Pow A = {B. B \<le> A}"
    5.57