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
--- a/src/HOL/Finite_Set.thy Wed Dec 25 22:35:29 2013 +0100
+++ b/src/HOL/Finite_Set.thy Thu Dec 26 22:47:49 2013 +0100
@@ -1085,6 +1085,9 @@
assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
begin
+interpretation comp_fun_commute f
+ by default (insert comp_fun_commute, simp add: fun_eq_iff)
+
definition F :: "'a set \<Rightarrow> 'b"
where
eq_fold: "F A = fold f z A"
@@ -1101,8 +1104,6 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = f x (F A)"
proof -
- interpret comp_fun_commute f
- by default (insert comp_fun_commute, simp add: fun_eq_iff)
from fold_insert assms
have "fold f z (insert x A) = f x (fold f z A)" by simp
with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
@@ -1134,12 +1135,13 @@
declare insert [simp del]
+interpretation comp_fun_idem f
+ by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
+
lemma insert_idem [simp]:
assumes "finite A"
shows "F (insert x A) = f x (F A)"
proof -
- interpret comp_fun_idem f
- by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
from fold_insert_idem assms
have "fold f z (insert x A) = f x (fold f z A)" by simp
with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
--- a/src/HOL/GCD.thy Wed Dec 25 22:35:29 2013 +0100
+++ b/src/HOL/GCD.thy Thu Dec 26 22:47:49 2013 +0100
@@ -197,14 +197,14 @@
by (simp add: lcm_int_def)
(* was gcd_0, etc. *)
-lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
+lemma gcd_0_nat: "gcd (x::nat) 0 = x"
by simp
(* was igcd_0, etc. *)
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
by (unfold gcd_int_def, auto)
-lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
+lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
by simp
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
@@ -243,7 +243,7 @@
lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
apply (induct m n rule: gcd_nat_induct)
- apply (simp_all add: gcd_non_0_nat)
+ apply (simp_all add: gcd_non_0_nat gcd_0_nat)
apply (blast dest: dvd_mod_imp_dvd)
done
@@ -278,7 +278,7 @@
by (rule zdvd_imp_le, auto)
lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
-by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
+by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
lemma gcd_greatest_int:
"(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
@@ -307,25 +307,6 @@
lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
-interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
-proof
-qed (auto intro: dvd_antisym dvd_trans)
-
-interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
-proof
-qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
-
-lemmas gcd_assoc_nat = gcd_nat.assoc
-lemmas gcd_commute_nat = gcd_nat.commute
-lemmas gcd_left_commute_nat = gcd_nat.left_commute
-lemmas gcd_assoc_int = gcd_int.assoc
-lemmas gcd_commute_int = gcd_int.commute
-lemmas gcd_left_commute_int = gcd_int.left_commute
-
-lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
-
-lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
-
lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
apply auto
@@ -343,18 +324,40 @@
apply (auto intro: gcd_greatest_int)
done
+interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ + 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)"
+apply default
+apply (auto intro: dvd_antisym dvd_trans)[4]
+apply (metis dvd.dual_order.refl gcd_unique_nat)
+apply (auto intro: dvdI elim: dvdE)
+done
+
+interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
+proof
+qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
+
+lemmas gcd_assoc_nat = gcd_nat.assoc
+lemmas gcd_commute_nat = gcd_nat.commute
+lemmas gcd_left_commute_nat = gcd_nat.left_commute
+lemmas gcd_assoc_int = gcd_int.assoc
+lemmas gcd_commute_int = gcd_int.commute
+lemmas gcd_left_commute_int = gcd_int.left_commute
+
+lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
+
+lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
+
lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
-by (metis dvd.eq_iff gcd_unique_nat)
+ by (fact gcd_nat.absorb1)
lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
-by (metis dvd.eq_iff gcd_unique_nat)
+ by (fact gcd_nat.absorb2)
-lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
-by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
+lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
+ by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
-lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
-by (metis gcd_proj1_if_dvd_int gcd_commute_int)
-
+lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
+ by (metis gcd_proj1_if_dvd_int gcd_commute_int)
text {*
\medskip Multiplication laws
@@ -1391,12 +1394,17 @@
by (auto intro: dvd_antisym [transferred] lcm_least_int)
interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
proof
fix n m p :: nat
show "lcm (lcm n m) p = lcm n (lcm m p)"
by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
show "lcm m n = lcm n m"
by (simp add: lcm_nat_def gcd_commute_nat field_simps)
+ show "lcm m m = m"
+ by (metis dvd.order_refl lcm_unique_nat)
+ show "lcm m 1 = m"
+ by (metis dvd.dual_order.refl lcm_unique_nat one_dvd)
qed
interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
@@ -1478,10 +1486,6 @@
subsection {* The complete divisibility lattice *}
-lemma semilattice_neutr_set_lcm_one_nat:
- "semilattice_neutr_set lcm (1::nat)"
- by default simp_all
-
interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
proof
case goal3 thus ?case by(metis gcd_unique_nat)
@@ -1508,28 +1512,19 @@
definition
"Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)"
+interpretation semilattice_neutr_set lcm "1::nat" ..
+
lemma Lcm_nat_infinite:
"\<not> finite M \<Longrightarrow> Lcm M = (0::nat)"
by (simp add: Lcm_nat_def)
lemma Lcm_nat_empty:
"Lcm {} = (1::nat)"
-proof -
- interpret semilattice_neutr_set lcm "1::nat"
- by (fact semilattice_neutr_set_lcm_one_nat)
- show ?thesis by (simp add: Lcm_nat_def)
-qed
+ by (simp add: Lcm_nat_def)
lemma Lcm_nat_insert:
"Lcm (insert n M) = lcm (n::nat) (Lcm M)"
-proof (cases "finite M")
- interpret semilattice_neutr_set lcm "1::nat"
- by (fact semilattice_neutr_set_lcm_one_nat)
- case True
- then show ?thesis by (simp add: Lcm_nat_def)
-next
- case False then show ?thesis by (simp add: Lcm_nat_infinite)
-qed
+ by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
definition
"Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
@@ -1587,7 +1582,7 @@
qed
lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
- by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *)
+ by (fact Lcm_nat_empty)
lemma Gcd_empty_nat: "Gcd {} = (0::nat)"
by (fact gcd_lcm_complete_lattice_nat.Inf_empty) (* already simp *)
@@ -1688,6 +1683,7 @@
lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
+
subsubsection {* Setwise gcd and lcm for integers *}
instantiation int :: Gcd
--- a/src/HOL/Quotient.thy Wed Dec 25 22:35:29 2013 +0100
+++ b/src/HOL/Quotient.thy Thu Dec 26 22:47:49 2013 +0100
@@ -46,75 +46,94 @@
shows "Quotient3 R Abs Rep"
using assms unfolding Quotient3_def by blast
-lemma Quotient3_abs_rep:
+context
+ fixes R Abs Rep
assumes a: "Quotient3 R Abs Rep"
- shows "Abs (Rep a) = a"
+begin
+
+lemma Quotient3_abs_rep:
+ "Abs (Rep a) = a"
using a
unfolding Quotient3_def
by simp
lemma Quotient3_rep_reflp:
- assumes a: "Quotient3 R Abs Rep"
- shows "R (Rep a) (Rep a)"
+ "R (Rep a) (Rep a)"
using a
unfolding Quotient3_def
by blast
lemma Quotient3_rel:
- assumes a: "Quotient3 R Abs Rep"
- shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
+ "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
using a
unfolding Quotient3_def
by blast
lemma Quotient3_refl1:
- assumes a: "Quotient3 R Abs Rep"
- shows "R r s \<Longrightarrow> R r r"
+ "R r s \<Longrightarrow> R r r"
using a unfolding Quotient3_def
by fast
lemma Quotient3_refl2:
- assumes a: "Quotient3 R Abs Rep"
- shows "R r s \<Longrightarrow> R s s"
+ "R r s \<Longrightarrow> R s s"
using a unfolding Quotient3_def
by fast
lemma Quotient3_rel_rep:
- assumes a: "Quotient3 R Abs Rep"
- shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
+ "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
using a
unfolding Quotient3_def
by metis
lemma Quotient3_rep_abs:
- assumes a: "Quotient3 R Abs Rep"
- shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
+ "R r r \<Longrightarrow> R (Rep (Abs r)) r"
using a unfolding Quotient3_def
by blast
lemma Quotient3_rel_abs:
- assumes a: "Quotient3 R Abs Rep"
- shows "R r s \<Longrightarrow> Abs r = Abs s"
+ "R r s \<Longrightarrow> Abs r = Abs s"
using a unfolding Quotient3_def
by blast
lemma Quotient3_symp:
- assumes a: "Quotient3 R Abs Rep"
- shows "symp R"
+ "symp R"
using a unfolding Quotient3_def using sympI by metis
lemma Quotient3_transp:
- assumes a: "Quotient3 R Abs Rep"
- shows "transp R"
+ "transp R"
using a unfolding Quotient3_def using transpI by (metis (full_types))
lemma Quotient3_part_equivp:
- assumes a: "Quotient3 R Abs Rep"
- shows "part_equivp R"
-by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
+ "part_equivp R"
+ by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI)
+
+lemma abs_o_rep:
+ "Abs o Rep = id"
+ unfolding fun_eq_iff
+ by (simp add: Quotient3_abs_rep)
+
+lemma equals_rsp:
+ assumes b: "R xa xb" "R ya yb"
+ shows "R xa ya = R xb yb"
+ using b Quotient3_symp Quotient3_transp
+ by (blast elim: sympE transpE)
+
+lemma rep_abs_rsp:
+ assumes b: "R x1 x2"
+ shows "R x1 (Rep (Abs x2))"
+ using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
+ by metis
+
+lemma rep_abs_rsp_left:
+ assumes b: "R x1 x2"
+ shows "R (Rep (Abs x1)) x2"
+ using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
+ by metis
+
+end
lemma identity_quotient3:
- shows "Quotient3 (op =) id id"
+ "Quotient3 (op =) id id"
unfolding Quotient3_def id_def
by blast
@@ -157,19 +176,6 @@
ultimately show ?thesis by (intro Quotient3I) (assumption+)
qed
-lemma abs_o_rep:
- assumes a: "Quotient3 R Abs Rep"
- shows "Abs o Rep = id"
- unfolding fun_eq_iff
- by (simp add: Quotient3_abs_rep[OF a])
-
-lemma equals_rsp:
- assumes q: "Quotient3 R Abs Rep"
- and a: "R xa xb" "R ya yb"
- shows "R xa ya = R xb yb"
- using a Quotient3_symp[OF q] Quotient3_transp[OF q]
- by (blast elim: sympE transpE)
-
lemma lambda_prs:
assumes q1: "Quotient3 R1 Abs1 Rep1"
and q2: "Quotient3 R2 Abs2 Rep2"
@@ -186,20 +192,6 @@
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
by simp
-lemma rep_abs_rsp:
- assumes q: "Quotient3 R Abs Rep"
- and a: "R x1 x2"
- shows "R x1 (Rep (Abs x2))"
- using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
- by metis
-
-lemma rep_abs_rsp_left:
- assumes q: "Quotient3 R Abs Rep"
- and a: "R x1 x2"
- shows "R (Rep (Abs x1)) x2"
- using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
- by metis
-
text{*
In the following theorem R1 can be instantiated with anything,
but we know some of the types of the Rep and Abs functions;