author haftmann Thu Dec 26 22:47:49 2013 +0100 (2013-12-26) changeset 54867 c21a2465cac1 parent 54866 7b9a67cbd48f child 54868 bab6cade3cc5
prefer ephemeral interpretation over interpretation in proof contexts;
prefer context begin ... end blocks for often-occuring assumptions;
slightly more complete interpretations into abstract algebraic structures for gcd/lcm
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/Quotient.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Wed Dec 25 22:35:29 2013 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 26 22:47:49 2013 +0100
1.3 @@ -1085,6 +1085,9 @@
1.4    assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
1.5  begin
1.6
1.7 +interpretation comp_fun_commute f
1.8 +  by default (insert comp_fun_commute, simp add: fun_eq_iff)
1.9 +
1.10  definition F :: "'a set \<Rightarrow> 'b"
1.11  where
1.12    eq_fold: "F A = fold f z A"
1.13 @@ -1101,8 +1104,6 @@
1.14    assumes "finite A" and "x \<notin> A"
1.15    shows "F (insert x A) = f x (F A)"
1.16  proof -
1.17 -  interpret comp_fun_commute f
1.18 -    by default (insert comp_fun_commute, simp add: fun_eq_iff)
1.19    from fold_insert assms
1.20    have "fold f z (insert x A) = f x (fold f z A)" by simp
1.21    with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
1.22 @@ -1134,12 +1135,13 @@
1.23
1.24  declare insert [simp del]
1.25
1.26 +interpretation comp_fun_idem f
1.27 +  by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
1.28 +
1.29  lemma insert_idem [simp]:
1.30    assumes "finite A"
1.31    shows "F (insert x A) = f x (F A)"
1.32  proof -
1.33 -  interpret comp_fun_idem f
1.34 -    by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
1.35    from fold_insert_idem assms
1.36    have "fold f z (insert x A) = f x (fold f z A)" by simp
1.37    with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
```
```     2.1 --- a/src/HOL/GCD.thy	Wed Dec 25 22:35:29 2013 +0100
2.2 +++ b/src/HOL/GCD.thy	Thu Dec 26 22:47:49 2013 +0100
2.3 @@ -197,14 +197,14 @@
2.5
2.6  (* was gcd_0, etc. *)
2.7 -lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
2.8 +lemma gcd_0_nat: "gcd (x::nat) 0 = x"
2.9    by simp
2.10
2.11  (* was igcd_0, etc. *)
2.12  lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
2.13    by (unfold gcd_int_def, auto)
2.14
2.15 -lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
2.16 +lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
2.17    by simp
2.18
2.19  lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
2.20 @@ -243,7 +243,7 @@
2.21  lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
2.22    and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
2.23    apply (induct m n rule: gcd_nat_induct)
2.24 -  apply (simp_all add: gcd_non_0_nat)
2.25 +  apply (simp_all add: gcd_non_0_nat gcd_0_nat)
2.26    apply (blast dest: dvd_mod_imp_dvd)
2.27  done
2.28
2.29 @@ -278,7 +278,7 @@
2.30    by (rule zdvd_imp_le, auto)
2.31
2.32  lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
2.33 -by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
2.34 +by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
2.35
2.36  lemma gcd_greatest_int:
2.37    "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
2.38 @@ -307,25 +307,6 @@
2.39  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
2.40    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
2.41
2.42 -interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
2.43 -proof
2.44 -qed (auto intro: dvd_antisym dvd_trans)
2.45 -
2.46 -interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
2.47 -proof
2.48 -qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
2.49 -
2.50 -lemmas gcd_assoc_nat = gcd_nat.assoc
2.51 -lemmas gcd_commute_nat = gcd_nat.commute
2.52 -lemmas gcd_left_commute_nat = gcd_nat.left_commute
2.53 -lemmas gcd_assoc_int = gcd_int.assoc
2.54 -lemmas gcd_commute_int = gcd_int.commute
2.55 -lemmas gcd_left_commute_int = gcd_int.left_commute
2.56 -
2.57 -lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
2.58 -
2.59 -lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
2.60 -
2.61  lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
2.62      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
2.63    apply auto
2.64 @@ -343,18 +324,40 @@
2.65   apply (auto intro: gcd_greatest_int)
2.66  done
2.67
2.68 +interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
2.69 +  + gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
2.70 +apply default
2.71 +apply (auto intro: dvd_antisym dvd_trans)[4]
2.72 +apply (metis dvd.dual_order.refl gcd_unique_nat)
2.73 +apply (auto intro: dvdI elim: dvdE)
2.74 +done
2.75 +
2.76 +interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
2.77 +proof
2.78 +qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
2.79 +
2.80 +lemmas gcd_assoc_nat = gcd_nat.assoc
2.81 +lemmas gcd_commute_nat = gcd_nat.commute
2.82 +lemmas gcd_left_commute_nat = gcd_nat.left_commute
2.83 +lemmas gcd_assoc_int = gcd_int.assoc
2.84 +lemmas gcd_commute_int = gcd_int.commute
2.85 +lemmas gcd_left_commute_int = gcd_int.left_commute
2.86 +
2.87 +lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
2.88 +
2.89 +lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
2.90 +
2.91  lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
2.92 -by (metis dvd.eq_iff gcd_unique_nat)
2.93 +  by (fact gcd_nat.absorb1)
2.94
2.95  lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
2.96 -by (metis dvd.eq_iff gcd_unique_nat)
2.97 +  by (fact gcd_nat.absorb2)
2.98
2.99 -lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
2.100 -by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
2.101 +lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
2.102 +  by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
2.103
2.104 -lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
2.105 -by (metis gcd_proj1_if_dvd_int gcd_commute_int)
2.106 -
2.107 +lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
2.108 +  by (metis gcd_proj1_if_dvd_int gcd_commute_int)
2.109
2.110  text {*
2.111    \medskip Multiplication laws
2.112 @@ -1391,12 +1394,17 @@
2.113    by (auto intro: dvd_antisym [transferred] lcm_least_int)
2.114
2.115  interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
2.116 +  + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
2.117  proof
2.118    fix n m p :: nat
2.119    show "lcm (lcm n m) p = lcm n (lcm m p)"
2.120      by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
2.121    show "lcm m n = lcm n m"
2.122      by (simp add: lcm_nat_def gcd_commute_nat field_simps)
2.123 +  show "lcm m m = m"
2.124 +    by (metis dvd.order_refl lcm_unique_nat)
2.125 +  show "lcm m 1 = m"
2.126 +    by (metis dvd.dual_order.refl lcm_unique_nat one_dvd)
2.127  qed
2.128
2.129  interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
2.130 @@ -1478,10 +1486,6 @@
2.131
2.132  subsection {* The complete divisibility lattice *}
2.133
2.134 -lemma semilattice_neutr_set_lcm_one_nat:
2.135 -  "semilattice_neutr_set lcm (1::nat)"
2.136 -  by default simp_all
2.137 -
2.138  interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
2.139  proof
2.140    case goal3 thus ?case by(metis gcd_unique_nat)
2.141 @@ -1508,28 +1512,19 @@
2.142  definition
2.143    "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)"
2.144
2.145 +interpretation semilattice_neutr_set lcm "1::nat" ..
2.146 +
2.147  lemma Lcm_nat_infinite:
2.148    "\<not> finite M \<Longrightarrow> Lcm M = (0::nat)"
2.150
2.151  lemma Lcm_nat_empty:
2.152    "Lcm {} = (1::nat)"
2.153 -proof -
2.154 -  interpret semilattice_neutr_set lcm "1::nat"
2.155 -    by (fact semilattice_neutr_set_lcm_one_nat)
2.156 -  show ?thesis by (simp add: Lcm_nat_def)
2.157 -qed
2.158 +  by (simp add: Lcm_nat_def)
2.159
2.160  lemma Lcm_nat_insert:
2.161    "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
2.162 -proof (cases "finite M")
2.163 -  interpret semilattice_neutr_set lcm "1::nat"
2.164 -    by (fact semilattice_neutr_set_lcm_one_nat)
2.165 -  case True
2.166 -  then show ?thesis by (simp add: Lcm_nat_def)
2.167 -next
2.168 -  case False then show ?thesis by (simp add: Lcm_nat_infinite)
2.169 -qed
2.170 +  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
2.171
2.172  definition
2.173    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
2.174 @@ -1587,7 +1582,7 @@
2.175  qed
2.176
2.177  lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
2.178 -  by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *)
2.179 +  by (fact Lcm_nat_empty)
2.180
2.181  lemma Gcd_empty_nat: "Gcd {} = (0::nat)"
2.182    by (fact gcd_lcm_complete_lattice_nat.Inf_empty) (* already simp *)
2.183 @@ -1688,6 +1683,7 @@
2.184  lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
2.185  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
2.186
2.187 +
2.188  subsubsection {* Setwise gcd and lcm for integers *}
2.189
2.190  instantiation int :: Gcd
```
```     3.1 --- a/src/HOL/Quotient.thy	Wed Dec 25 22:35:29 2013 +0100
3.2 +++ b/src/HOL/Quotient.thy	Thu Dec 26 22:47:49 2013 +0100
3.3 @@ -46,75 +46,94 @@
3.4    shows "Quotient3 R Abs Rep"
3.5    using assms unfolding Quotient3_def by blast
3.6
3.7 -lemma Quotient3_abs_rep:
3.8 +context
3.9 +  fixes R Abs Rep
3.10    assumes a: "Quotient3 R Abs Rep"
3.11 -  shows "Abs (Rep a) = a"
3.12 +begin
3.13 +
3.14 +lemma Quotient3_abs_rep:
3.15 +  "Abs (Rep a) = a"
3.16    using a
3.17    unfolding Quotient3_def
3.18    by simp
3.19
3.20  lemma Quotient3_rep_reflp:
3.21 -  assumes a: "Quotient3 R Abs Rep"
3.22 -  shows "R (Rep a) (Rep a)"
3.23 +  "R (Rep a) (Rep a)"
3.24    using a
3.25    unfolding Quotient3_def
3.26    by blast
3.27
3.28  lemma Quotient3_rel:
3.29 -  assumes a: "Quotient3 R Abs Rep"
3.30 -  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
3.31 +  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
3.32    using a
3.33    unfolding Quotient3_def
3.34    by blast
3.35
3.36  lemma Quotient3_refl1:
3.37 -  assumes a: "Quotient3 R Abs Rep"
3.38 -  shows "R r s \<Longrightarrow> R r r"
3.39 +  "R r s \<Longrightarrow> R r r"
3.40    using a unfolding Quotient3_def
3.41    by fast
3.42
3.43  lemma Quotient3_refl2:
3.44 -  assumes a: "Quotient3 R Abs Rep"
3.45 -  shows "R r s \<Longrightarrow> R s s"
3.46 +  "R r s \<Longrightarrow> R s s"
3.47    using a unfolding Quotient3_def
3.48    by fast
3.49
3.50  lemma Quotient3_rel_rep:
3.51 -  assumes a: "Quotient3 R Abs Rep"
3.52 -  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
3.53 +  "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
3.54    using a
3.55    unfolding Quotient3_def
3.56    by metis
3.57
3.58  lemma Quotient3_rep_abs:
3.59 -  assumes a: "Quotient3 R Abs Rep"
3.60 -  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
3.61 +  "R r r \<Longrightarrow> R (Rep (Abs r)) r"
3.62    using a unfolding Quotient3_def
3.63    by blast
3.64
3.65  lemma Quotient3_rel_abs:
3.66 -  assumes a: "Quotient3 R Abs Rep"
3.67 -  shows "R r s \<Longrightarrow> Abs r = Abs s"
3.68 +  "R r s \<Longrightarrow> Abs r = Abs s"
3.69    using a unfolding Quotient3_def
3.70    by blast
3.71
3.72  lemma Quotient3_symp:
3.73 -  assumes a: "Quotient3 R Abs Rep"
3.74 -  shows "symp R"
3.75 +  "symp R"
3.76    using a unfolding Quotient3_def using sympI by metis
3.77
3.78  lemma Quotient3_transp:
3.79 -  assumes a: "Quotient3 R Abs Rep"
3.80 -  shows "transp R"
3.81 +  "transp R"
3.82    using a unfolding Quotient3_def using transpI by (metis (full_types))
3.83
3.84  lemma Quotient3_part_equivp:
3.85 -  assumes a: "Quotient3 R Abs Rep"
3.86 -  shows "part_equivp R"
3.87 -by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
3.88 +  "part_equivp R"
3.89 +  by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI)
3.90 +
3.91 +lemma abs_o_rep:
3.92 +  "Abs o Rep = id"
3.93 +  unfolding fun_eq_iff
3.94 +  by (simp add: Quotient3_abs_rep)
3.95 +
3.96 +lemma equals_rsp:
3.97 +  assumes b: "R xa xb" "R ya yb"
3.98 +  shows "R xa ya = R xb yb"
3.99 +  using b Quotient3_symp Quotient3_transp
3.100 +  by (blast elim: sympE transpE)
3.101 +
3.102 +lemma rep_abs_rsp:
3.103 +  assumes b: "R x1 x2"
3.104 +  shows "R x1 (Rep (Abs x2))"
3.105 +  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
3.106 +  by metis
3.107 +
3.108 +lemma rep_abs_rsp_left:
3.109 +  assumes b: "R x1 x2"
3.110 +  shows "R (Rep (Abs x1)) x2"
3.111 +  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
3.112 +  by metis
3.113 +
3.114 +end
3.115
3.116  lemma identity_quotient3:
3.117 -  shows "Quotient3 (op =) id id"
3.118 +  "Quotient3 (op =) id id"
3.119    unfolding Quotient3_def id_def
3.120    by blast
3.121
3.122 @@ -157,19 +176,6 @@
3.123   ultimately show ?thesis by (intro Quotient3I) (assumption+)
3.124  qed
3.125
3.126 -lemma abs_o_rep:
3.127 -  assumes a: "Quotient3 R Abs Rep"
3.128 -  shows "Abs o Rep = id"
3.129 -  unfolding fun_eq_iff
3.130 -  by (simp add: Quotient3_abs_rep[OF a])
3.131 -
3.132 -lemma equals_rsp:
3.133 -  assumes q: "Quotient3 R Abs Rep"
3.134 -  and     a: "R xa xb" "R ya yb"
3.135 -  shows "R xa ya = R xb yb"
3.136 -  using a Quotient3_symp[OF q] Quotient3_transp[OF q]
3.137 -  by (blast elim: sympE transpE)
3.138 -
3.139  lemma lambda_prs:
3.140    assumes q1: "Quotient3 R1 Abs1 Rep1"
3.141    and     q2: "Quotient3 R2 Abs2 Rep2"
3.142 @@ -186,20 +192,6 @@
3.143    using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
3.144    by simp
3.145
3.146 -lemma rep_abs_rsp:
3.147 -  assumes q: "Quotient3 R Abs Rep"
3.148 -  and     a: "R x1 x2"
3.149 -  shows "R x1 (Rep (Abs x2))"
3.150 -  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
3.151 -  by metis
3.152 -
3.153 -lemma rep_abs_rsp_left:
3.154 -  assumes q: "Quotient3 R Abs Rep"
3.155 -  and     a: "R x1 x2"
3.156 -  shows "R (Rep (Abs x1)) x2"
3.157 -  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
3.158 -  by metis
3.159 -
3.160  text{*
3.161    In the following theorem R1 can be instantiated with anything,
3.162    but we know some of the types of the Rep and Abs functions;
```