using class target
authorhaftmann
Tue Jul 24 15:20:45 2007 +0200 (2007-07-24)
changeset 23948261bd4678076
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
     1.1 --- a/src/HOL/Divides.thy	Mon Jul 23 22:18:05 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Jul 24 15:20:45 2007 +0200
     1.3 @@ -26,12 +26,10 @@
     1.4  definition (in times)
     1.5    dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
     1.6  where
     1.7 -  "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
     1.8 -lemmas dvd_def = dvd_def [folded times_class.dvd]
     1.9 +  [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
    1.10  
    1.11  class dvd_mod = times + div + zero + -- {* for code generation *}
    1.12 -  assumes dvd_def_mod: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
    1.13 -lemmas dvd_def_mod [code func] = dvd_def_mod [folded times_class.dvd]
    1.14 +  assumes dvd_def_mod [code func]: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
    1.15  
    1.16  definition
    1.17    quorem :: "(nat*nat) * (nat*nat) => bool" where
     2.1 --- a/src/HOL/HOL.thy	Mon Jul 23 22:18:05 2007 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue Jul 24 15:20:45 2007 +0200
     2.3 @@ -299,8 +299,6 @@
     2.4  notation (input)
     2.5    greater_eq  (infix "\<ge>" 50)
     2.6  
     2.7 -lemmas Least_def = Least_def [folded ord_class.Least]
     2.8 -
     2.9  syntax
    2.10    "_index1"  :: index    ("\<^sub>1")
    2.11  translations
     3.1 --- a/src/HOL/Lattices.thy	Mon Jul 23 22:18:05 2007 +0200
     3.2 +++ b/src/HOL/Lattices.thy	Tue Jul 24 15:20:45 2007 +0200
     3.3 @@ -295,7 +295,7 @@
     3.4  
     3.5  interpretation min_max:
     3.6    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
     3.7 -  by (rule distrib_lattice_min_max [folded ord_class.min ord_class.max])
     3.8 +  by (rule distrib_lattice_min_max)
     3.9  
    3.10  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    3.11    by (rule ext)+ auto
    3.12 @@ -367,7 +367,7 @@
    3.13    apply (erule Inf_lower)
    3.14    done
    3.15  
    3.16 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    3.17 +lemma Sup_insert [code func]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    3.18    apply (rule antisym)
    3.19    apply (rule Sup_least)
    3.20    apply (erule insertE)
    3.21 @@ -387,7 +387,7 @@
    3.22    "\<Sqinter>{a} = a"
    3.23    by (auto intro: antisym Inf_lower Inf_greatest)
    3.24  
    3.25 -lemma Sup_singleton [simp]:
    3.26 +lemma Sup_singleton [simp, code func]:
    3.27    "\<Squnion>{a} = a"
    3.28    by (auto intro: antisym Sup_upper Sup_least)
    3.29  
    3.30 @@ -409,15 +409,6 @@
    3.31  
    3.32  end
    3.33  
    3.34 -lemmas Sup_def = Sup_def [folded complete_lattice_class.Sup]
    3.35 -lemmas Sup_upper = Sup_upper [folded complete_lattice_class.Sup]
    3.36 -lemmas Sup_least = Sup_least [folded complete_lattice_class.Sup]
    3.37 -
    3.38 -lemmas Sup_insert [code func] = Sup_insert [folded complete_lattice_class.Sup]
    3.39 -lemmas Sup_singleton [simp, code func] = Sup_singleton [folded complete_lattice_class.Sup]
    3.40 -lemmas Sup_insert_simp = Sup_insert_simp [folded complete_lattice_class.Sup]
    3.41 -lemmas Sup_binary = Sup_binary [folded complete_lattice_class.Sup]
    3.42 -
    3.43  definition
    3.44    top :: "'a::complete_lattice"
    3.45  where
     4.1 --- a/src/HOL/Orderings.thy	Mon Jul 23 22:18:05 2007 +0200
     4.2 +++ b/src/HOL/Orderings.thy	Tue Jul 24 15:20:45 2007 +0200
     4.3 @@ -195,14 +195,11 @@
     4.4  
     4.5  definition (in ord)
     4.6    min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
     4.7 -  "min a b = (if a \<^loc>\<le> b then a else b)"
     4.8 +  [code unfold, code inline del]: "min a b = (if a \<^loc>\<le> b then a else b)"
     4.9  
    4.10  definition (in ord)
    4.11    max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.12 -  "max a b = (if a \<^loc>\<le> b then b else a)"
    4.13 -
    4.14 -lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
    4.15 -lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
    4.16 +  [code unfold, code inline del]: "max a b = (if a \<^loc>\<le> b then b else a)"
    4.17  
    4.18  lemma min_le_iff_disj:
    4.19    "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
    4.20 @@ -238,7 +235,8 @@
    4.21  
    4.22  end
    4.23  
    4.24 -subsection {* Name duplicates -- including min/max interpretation *}
    4.25 +
    4.26 +subsection {* Name duplicates *}
    4.27  
    4.28  lemmas order_less_le = less_le
    4.29  lemmas order_eq_refl = order_class.eq_refl
    4.30 @@ -275,14 +273,14 @@
    4.31  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
    4.32  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
    4.33  
    4.34 -lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
    4.35 -lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]
    4.36 -lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [folded ord_class.min]
    4.37 -lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [folded ord_class.max]
    4.38 -lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [folded ord_class.min]
    4.39 -lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [folded ord_class.max]
    4.40 -lemmas split_min = linorder_class.split_min [folded ord_class.min]
    4.41 -lemmas split_max = linorder_class.split_max [folded ord_class.max]
    4.42 +lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
    4.43 +lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
    4.44 +lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
    4.45 +lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
    4.46 +lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
    4.47 +lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
    4.48 +lemmas split_min = linorder_class.split_min
    4.49 +lemmas split_max = linorder_class.split_max
    4.50  
    4.51  
    4.52  subsection {* Reasoning tools setup *}