using class target
authorhaftmann
Tue, 24 Jul 2007 15:20:45 +0200
changeset 23948 261bd4678076
parent 23947 5e396bcf749e
child 23949 06a988643235
using class target
src/HOL/Divides.thy
src/HOL/HOL.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
--- 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 *}