--- a/src/HOL/Divides.thy Mon Jul 23 22:18:05 2007 +0200
+++ b/src/HOL/Divides.thy Tue Jul 24 15:20:45 2007 +0200
@@ -26,12 +26,10 @@
definition (in times)
dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
where
- "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
-lemmas dvd_def = dvd_def [folded times_class.dvd]
+ [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
class dvd_mod = times + div + zero + -- {* for code generation *}
- assumes dvd_def_mod: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
-lemmas dvd_def_mod [code func] = dvd_def_mod [folded times_class.dvd]
+ assumes dvd_def_mod [code func]: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
definition
quorem :: "(nat*nat) * (nat*nat) => bool" where
--- a/src/HOL/HOL.thy Mon Jul 23 22:18:05 2007 +0200
+++ b/src/HOL/HOL.thy Tue Jul 24 15:20:45 2007 +0200
@@ -299,8 +299,6 @@
notation (input)
greater_eq (infix "\<ge>" 50)
-lemmas Least_def = Least_def [folded ord_class.Least]
-
syntax
"_index1" :: index ("\<^sub>1")
translations
--- a/src/HOL/Lattices.thy Mon Jul 23 22:18:05 2007 +0200
+++ b/src/HOL/Lattices.thy Tue Jul 24 15:20:45 2007 +0200
@@ -295,7 +295,7 @@
interpretation min_max:
distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
- by (rule distrib_lattice_min_max [folded ord_class.min ord_class.max])
+ by (rule distrib_lattice_min_max)
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
by (rule ext)+ auto
@@ -367,7 +367,7 @@
apply (erule Inf_lower)
done
-lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+lemma Sup_insert [code func]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
apply (rule antisym)
apply (rule Sup_least)
apply (erule insertE)
@@ -387,7 +387,7 @@
"\<Sqinter>{a} = a"
by (auto intro: antisym Inf_lower Inf_greatest)
-lemma Sup_singleton [simp]:
+lemma Sup_singleton [simp, code func]:
"\<Squnion>{a} = a"
by (auto intro: antisym Sup_upper Sup_least)
@@ -409,15 +409,6 @@
end
-lemmas Sup_def = Sup_def [folded complete_lattice_class.Sup]
-lemmas Sup_upper = Sup_upper [folded complete_lattice_class.Sup]
-lemmas Sup_least = Sup_least [folded complete_lattice_class.Sup]
-
-lemmas Sup_insert [code func] = Sup_insert [folded complete_lattice_class.Sup]
-lemmas Sup_singleton [simp, code func] = Sup_singleton [folded complete_lattice_class.Sup]
-lemmas Sup_insert_simp = Sup_insert_simp [folded complete_lattice_class.Sup]
-lemmas Sup_binary = Sup_binary [folded complete_lattice_class.Sup]
-
definition
top :: "'a::complete_lattice"
where
--- a/src/HOL/Orderings.thy Mon Jul 23 22:18:05 2007 +0200
+++ b/src/HOL/Orderings.thy Tue Jul 24 15:20:45 2007 +0200
@@ -195,14 +195,11 @@
definition (in ord)
min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- "min a b = (if a \<^loc>\<le> b then a else b)"
+ [code unfold, code inline del]: "min a b = (if a \<^loc>\<le> b then a else b)"
definition (in ord)
max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- "max a b = (if a \<^loc>\<le> b then b else a)"
-
-lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
-lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
+ [code unfold, code inline del]: "max a b = (if a \<^loc>\<le> b then b else a)"
lemma min_le_iff_disj:
"min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
@@ -238,7 +235,8 @@
end
-subsection {* Name duplicates -- including min/max interpretation *}
+
+subsection {* Name duplicates *}
lemmas order_less_le = less_le
lemmas order_eq_refl = order_class.eq_refl
@@ -275,14 +273,14 @@
lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
-lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
-lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]
-lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [folded ord_class.min]
-lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [folded ord_class.max]
-lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [folded ord_class.min]
-lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [folded ord_class.max]
-lemmas split_min = linorder_class.split_min [folded ord_class.min]
-lemmas split_max = linorder_class.split_max [folded ord_class.max]
+lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
+lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
+lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
+lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
+lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
+lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
+lemmas split_min = linorder_class.split_min
+lemmas split_max = linorder_class.split_max
subsection {* Reasoning tools setup *}