prefer ephemeral interpretation over interpretation in proof contexts;
authorhaftmann
Thu Dec 26 22:47:49 2013 +0100 (2013-12-26)
changeset 54867c21a2465cac1
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
src/HOL/GCD.thy
src/HOL/Quotient.thy
     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.4    by (simp add: lcm_int_def)
     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.149    by (simp add: Lcm_nat_def)
   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;