--- a/NEWS Sat Jan 30 17:03:46 2010 +0100
+++ b/NEWS Sun Jan 31 15:22:40 2010 +0100
@@ -12,6 +12,11 @@
*** HOL ***
+* new theory Algebras.thy contains generic algebraic structures and
+generic algebraic operations. INCOMPATIBILTY: constants zero, one,
+plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less
+have been moved from HOL.thy to Algebras.thy.
+
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.
--- a/src/HOL/Algebra/abstract/Ring2.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sun Jan 31 15:22:40 2010 +0100
@@ -205,8 +205,8 @@
ML {*
fun ring_ord (Const (a, _)) =
find_index (fn a' => a = a')
- [@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus},
- @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
+ [@{const_name Algebras.zero}, @{const_name Algebras.plus}, @{const_name Algebras.uminus},
+ @{const_name Algebras.minus}, @{const_name Algebras.one}, @{const_name Algebras.times}]
| ring_ord _ = ~1;
fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebras.thy Sun Jan 31 15:22:40 2010 +0100
@@ -0,0 +1,166 @@
+(* Title: HOL/Algebras.thy
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Generic algebraic structures and operations *}
+
+theory Algebras
+imports HOL
+begin
+
+subsection {* Generic algebraic structures *}
+
+locale semigroup =
+ fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
+ assumes assoc: "a * b * c = a * (b * c)"
+
+locale abel_semigroup = semigroup +
+ assumes commute: "a * b = b * a"
+begin
+
+lemma left_commute:
+ "b * (a * c) = a * (b * c)"
+proof -
+ have "(b * a) * c = (a * b) * c"
+ by (simp only: commute)
+ then show ?thesis
+ by (simp only: assoc)
+qed
+
+end
+
+locale semilattice = abel_semigroup +
+ assumes idem [simp]: "a * a = a"
+begin
+
+lemma left_idem [simp]:
+ "a * (a * b) = a * b"
+ by (simp add: assoc [symmetric])
+
+end
+
+locale lattice = inf!: abel_semigroup inf + sup!: abel_semigroup sup
+ for inf (infixl "\<sqinter>" 70) and sup (infixl "\<squnion>" 70) +
+ assumes sup_inf_absorb: "a \<squnion> (a \<sqinter> b) = a"
+ and inf_sup_absorb: "a \<sqinter> (a \<squnion> b) = a"
+
+sublocale lattice < inf!: semilattice inf
+proof
+ fix a
+ have "a \<sqinter> (a \<squnion> (a \<sqinter> a)) = a" by (fact inf_sup_absorb)
+ then show "a \<sqinter> a = a" by (simp add: sup_inf_absorb)
+qed
+
+sublocale lattice < sup!: semilattice sup
+proof
+ fix a
+ have "a \<squnion> (a \<sqinter> (a \<squnion> a)) = a" by (fact sup_inf_absorb)
+ then show "a \<squnion> a = a" by (simp add: inf_sup_absorb)
+qed
+
+
+subsection {* Generic algebraic operations *}
+
+class zero =
+ fixes zero :: 'a ("0")
+
+class one =
+ fixes one :: 'a ("1")
+
+lemma Let_0 [simp]: "Let 0 f = f 0"
+ unfolding Let_def ..
+
+lemma Let_1 [simp]: "Let 1 f = f 1"
+ unfolding Let_def ..
+
+setup {*
+ Reorient_Proc.add
+ (fn Const(@{const_name Algebras.zero}, _) => true
+ | Const(@{const_name Algebras.one}, _) => true
+ | _ => false)
+*}
+
+simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
+simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
+
+typed_print_translation {*
+let
+ fun tr' c = (c, fn show_sorts => fn T => fn ts =>
+ if (not o null) ts orelse T = dummyT
+ orelse not (! show_types) andalso can Term.dest_Type T
+ then raise Match
+ else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
+in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
+*} -- {* show types that are presumably too general *}
+
+hide (open) const zero one
+
+class plus =
+ fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
+
+class minus =
+ fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
+
+class uminus =
+ fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
+
+class times =
+ fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
+
+class inverse =
+ fixes inverse :: "'a \<Rightarrow> 'a"
+ and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
+
+class abs =
+ fixes abs :: "'a \<Rightarrow> 'a"
+begin
+
+notation (xsymbols)
+ abs ("\<bar>_\<bar>")
+
+notation (HTML output)
+ abs ("\<bar>_\<bar>")
+
+end
+
+class sgn =
+ fixes sgn :: "'a \<Rightarrow> 'a"
+
+class ord =
+ fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+
+notation
+ less_eq ("op <=") and
+ less_eq ("(_/ <= _)" [51, 51] 50) and
+ less ("op <") and
+ less ("(_/ < _)" [51, 51] 50)
+
+notation (xsymbols)
+ less_eq ("op \<le>") and
+ less_eq ("(_/ \<le> _)" [51, 51] 50)
+
+notation (HTML output)
+ less_eq ("op \<le>") and
+ less_eq ("(_/ \<le> _)" [51, 51] 50)
+
+abbreviation (input)
+ greater_eq (infix ">=" 50) where
+ "x >= y \<equiv> y <= x"
+
+notation (input)
+ greater_eq (infix "\<ge>" 50)
+
+abbreviation (input)
+ greater (infix ">" 50) where
+ "x > y \<equiv> y < x"
+
+end
+
+syntax
+ "_index1" :: index ("\<^sub>1")
+translations
+ (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
+
+end
\ No newline at end of file
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Jan 31 15:22:40 2010 +0100
@@ -655,7 +655,7 @@
if h aconvc y then false else if h aconvc x then true else earlier t x y;
fun dest_frac ct = case term_of ct of
- Const (@{const_name "HOL.divide"},_) $ a $ b=>
+ Const (@{const_name Algebras.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
| Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| t => Rat.rat_of_int (snd (HOLogic.dest_number t))
@@ -670,13 +670,13 @@
end
fun whatis x ct = case term_of ct of
- Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ =>
+ Const(@{const_name Algebras.plus}, _)$(Const(@{const_name Algebras.times},_)$_$y)$_ =>
if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
else ("Nox",[])
-| Const(@{const_name "HOL.plus"}, _)$y$_ =>
+| Const(@{const_name Algebras.plus}, _)$y$_ =>
if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
else ("Nox",[])
-| Const(@{const_name "HOL.times"}, _)$_$y =>
+| Const(@{const_name Algebras.times}, _)$_$y =>
if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct])
else ("Nox",[])
| t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
@@ -684,7 +684,7 @@
fun xnormalize_conv ctxt [] ct = reflexive ct
| xnormalize_conv ctxt (vs as (x::_)) ct =
case term_of ct of
- Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
+ Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -727,7 +727,7 @@
| _ => reflexive ct)
-| Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
+| Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -771,7 +771,7 @@
in rth end
| _ => reflexive ct)
-| Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) =>
+| Const("op =",_)$_$Const(@{const_name Algebras.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -816,7 +816,7 @@
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
in
fun field_isolate_conv phi ctxt vs ct = case term_of ct of
- Const(@{const_name HOL.less},_)$a$b =>
+ Const(@{const_name Algebras.less},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -825,7 +825,7 @@
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const(@{const_name HOL.less_eq},_)$a$b =>
+| Const(@{const_name Algebras.less_eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -856,11 +856,11 @@
else Ferrante_Rackoff_Data.Nox
| @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
- | Const(@{const_name HOL.less},_)$y$z =>
+ | Const(@{const_name Algebras.less},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
else Ferrante_Rackoff_Data.Nox
- | Const (@{const_name HOL.less_eq},_)$y$z =>
+ | Const (@{const_name Algebras.less_eq},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Le
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
else Ferrante_Rackoff_Data.Nox
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Jan 31 15:22:40 2010 +0100
@@ -2963,11 +2963,11 @@
fun num rT x = HOLogic.mk_number rT x;
fun rrelT rT = [rT,rT] ---> rT;
fun rrT rT = [rT, rT] ---> bT;
-fun divt rT = Const(@{const_name "HOL.divide"},rrelT rT);
-fun timest rT = Const(@{const_name "HOL.times"},rrelT rT);
-fun plust rT = Const(@{const_name "HOL.plus"},rrelT rT);
-fun minust rT = Const(@{const_name "HOL.minus"},rrelT rT);
-fun uminust rT = Const(@{const_name "HOL.uminus"}, rT --> rT);
+fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
+fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
+fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
+fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
+fun uminust rT = Const(@{const_name Algebras.uminus}, rT --> rT);
fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
val brT = [bT, bT] ---> bT;
val nott = @{term "Not"};
@@ -2975,10 +2975,10 @@
val disjt = @{term "op |"};
val impt = @{term "op -->"};
val ifft = @{term "op = :: bool => _"}
-fun llt rT = Const(@{const_name "HOL.less"},rrT rT);
-fun lle rT = Const(@{const_name "HOL.less"},rrT rT);
+fun llt rT = Const(@{const_name Algebras.less},rrT rT);
+fun lle rT = Const(@{const_name Algebras.less},rrT rT);
fun eqt rT = Const("op =",rrT rT);
-fun rz rT = Const(@{const_name "HOL.zero"},rT);
+fun rz rT = Const(@{const_name Algebras.zero},rT);
fun dest_nat t = case t of
Const ("Suc",_)$t' => 1 + dest_nat t'
@@ -2986,21 +2986,21 @@
fun num_of_term m t =
case t of
- Const(@{const_name "uminus"},_)$t => FRPar.Neg (num_of_term m t)
- | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
- | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
- | Const(@{const_name "HOL.times"},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
- | Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
- | Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ Const(@{const_name Algebras.uminus},_)$t => FRPar.Neg (num_of_term m t)
+ | Const(@{const_name Algebras.plus},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Algebras.minus},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Algebras.times},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Power.power},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
+ | Const(@{const_name Algebras.divide},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
| _ => (FRPar.C (HOLogic.dest_number t |> snd,1)
handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
fun tm_of_term m m' t =
case t of
- Const(@{const_name "uminus"},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
- | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
- | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
- | Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
+ Const(@{const_name Algebras.uminus},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
+ | Const(@{const_name Algebras.plus},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
+ | Const(@{const_name Algebras.minus},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
+ | Const(@{const_name Algebras.times},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
| _ => (FRPar.CP (num_of_term m' t)
handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
| Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
@@ -3040,9 +3040,9 @@
| Const("op =",ty)$p$q =>
if domain_type ty = bT then FRPar.Iff(fm_of_term m m' p, fm_of_term m m' q)
else FRPar.Eq (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
- | Const(@{const_name "HOL.less"},_)$p$q =>
+ | Const(@{const_name Algebras.less},_)$p$q =>
FRPar.Lt (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
- | Const(@{const_name "HOL.less_eq"},_)$p$q =>
+ | Const(@{const_name Algebras.less_eq},_)$p$q =>
FRPar.Le (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
| Const("Ex",_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Sun Jan 31 15:22:40 2010 +0100
@@ -13,8 +13,8 @@
struct
(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name HOL.zero}, T);
-fun cring_one T = Const (@{const_name HOL.one}, T);
+fun cring_zero T = Const (@{const_name Algebras.zero}, T);
+fun cring_one T = Const (@{const_name Algebras.one}, T);
(* reification functions *)
(* add two polynom expressions *)
@@ -49,13 +49,13 @@
| reif_pol T vs t = pol_Pc T $ t;
(* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
+fun reif_polex T vs (Const (@{const_name Algebras.plus}, _) $ a $ b) =
polex_add T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) =
polex_sub T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) =
polex_mul T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
+ | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) =
polex_neg T $ reif_polex T vs a
| reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
polex_pow T $ reif_polex T vs a $ n
--- a/src/HOL/GCD.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/GCD.thy Sun Jan 31 15:22:40 2010 +0100
@@ -302,28 +302,22 @@
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)
-lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
- by (rule dvd_antisym, auto)
-
-lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
- by (auto simp add: gcd_int_def gcd_commute_nat)
+interpretation gcd_nat!: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
+proof
+qed (auto intro: dvd_antisym dvd_trans)
-lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
- apply (rule dvd_antisym)
- apply (blast intro: dvd_trans)+
-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)
-lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
- by (auto simp add: gcd_int_def gcd_assoc_nat)
-
-lemmas gcd_left_commute_nat =
- mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
-
-lemmas gcd_left_commute_int =
- mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
+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
- -- {* gcd is an AC-operator *}
lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
@@ -1250,13 +1244,6 @@
lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
unfolding lcm_int_def by simp
-lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
- unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
-
-lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
- unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
-
-
lemma lcm_pos_nat:
"(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
@@ -1344,10 +1331,10 @@
done
lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
- by (subst lcm_commute_nat, rule lcm_dvd1_nat)
+ using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def times.commute gcd_nat.commute)
lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
- by (subst lcm_commute_int, rule lcm_dvd1_int)
+ using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def times.commute gcd_nat.commute)
lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
by(metis lcm_dvd1_nat dvd_trans)
@@ -1369,6 +1356,34 @@
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
by (auto intro: dvd_antisym [transferred] lcm_least_int)
+interpretation lcm_nat!: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+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 ring_simps)
+qed
+
+interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
+proof
+ fix n m p :: int
+ show "lcm (lcm n m) p = lcm n (lcm m p)"
+ by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
+ show "lcm m n = lcm n m"
+ by (simp add: lcm_int_def lcm_nat.commute)
+qed
+
+lemmas lcm_assoc_nat = lcm_nat.assoc
+lemmas lcm_commute_nat = lcm_nat.commute
+lemmas lcm_left_commute_nat = lcm_nat.left_commute
+lemmas lcm_assoc_int = lcm_int.assoc
+lemmas lcm_commute_int = lcm_int.commute
+lemmas lcm_left_commute_int = lcm_int.left_commute
+
+lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
+lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
+
lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
apply (rule sym)
apply (subst lcm_unique_nat [symmetric])
@@ -1399,18 +1414,6 @@
lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
-lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
-by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
-
-lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
-by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
-
-lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
-lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
-
-lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
-lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
-
lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
proof qed (auto simp add: gcd_ac_nat)
--- a/src/HOL/Groebner_Basis.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Groebner_Basis.thy Sun Jan 31 15:22:40 2010 +0100
@@ -527,13 +527,13 @@
val (l,r) = Thm.dest_binop ct
val T = ctyp_of_term l
in (case (term_of l, term_of r) of
- (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
+ (Const(@{const_name Algebras.divide},_)$_$_, _) =>
let val (x,y) = Thm.dest_binop l val z = r
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
val ynz = prove_nz ss T y
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
end
- | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
+ | (_, Const (@{const_name Algebras.divide},_)$_$_) =>
let val (x,y) = Thm.dest_binop r val z = l
val _ = map (HOLogic.dest_number o term_of) [x,y,z]
val ynz = prove_nz ss T y
@@ -543,49 +543,49 @@
end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
- fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b
+ fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b
| is_number t = can HOLogic.dest_number t
val is_number = is_number o term_of
fun proc3 phi ss ct =
(case term_of ct of
- Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+ Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+ | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+ | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+ | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+ | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+ | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -645,15 +645,15 @@
fun numeral_is_const ct =
case term_of ct of
- Const (@{const_name "HOL.divide"},_) $ a $ b =>
+ Const (@{const_name Algebras.divide},_) $ a $ b =>
can HOLogic.dest_number a andalso can HOLogic.dest_number b
- | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
+ | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t
| t => can HOLogic.dest_number t
fun dest_const ct = ((case term_of ct of
- Const (@{const_name "HOL.divide"},_) $ a $ b=>
+ Const (@{const_name Algebras.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const (@{const_name "HOL.inverse"},_)$t =>
+ | Const (@{const_name Algebras.inverse},_)$t =>
Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
| t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
handle TERM _ => error "ring_dest_const")
--- a/src/HOL/HOL.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/HOL.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1626,118 +1626,6 @@
by blast+
-subsection {* Generic classes and algebraic operations *}
-
-class zero =
- fixes zero :: 'a ("0")
-
-class one =
- fixes one :: 'a ("1")
-
-lemma Let_0 [simp]: "Let 0 f = f 0"
- unfolding Let_def ..
-
-lemma Let_1 [simp]: "Let 1 f = f 1"
- unfolding Let_def ..
-
-setup {*
- Reorient_Proc.add
- (fn Const(@{const_name HOL.zero}, _) => true
- | Const(@{const_name HOL.one}, _) => true
- | _ => false)
-*}
-
-simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
-simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
-
-typed_print_translation {*
-let
- fun tr' c = (c, fn show_sorts => fn T => fn ts =>
- if (not o null) ts orelse T = dummyT
- orelse not (! show_types) andalso can Term.dest_Type T
- then raise Match
- else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
-in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
-*} -- {* show types that are presumably too general *}
-
-hide (open) const zero one
-
-class plus =
- fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
-
-class minus =
- fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
-
-class uminus =
- fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
-
-class times =
- fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-
-class inverse =
- fixes inverse :: "'a \<Rightarrow> 'a"
- and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-
-class abs =
- fixes abs :: "'a \<Rightarrow> 'a"
-begin
-
-notation (xsymbols)
- abs ("\<bar>_\<bar>")
-
-notation (HTML output)
- abs ("\<bar>_\<bar>")
-
-end
-
-class sgn =
- fixes sgn :: "'a \<Rightarrow> 'a"
-
-class ord =
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-begin
-
-notation
- less_eq ("op <=") and
- less_eq ("(_/ <= _)" [51, 51] 50) and
- less ("op <") and
- less ("(_/ < _)" [51, 51] 50)
-
-notation (xsymbols)
- less_eq ("op \<le>") and
- less_eq ("(_/ \<le> _)" [51, 51] 50)
-
-notation (HTML output)
- less_eq ("op \<le>") and
- less_eq ("(_/ \<le> _)" [51, 51] 50)
-
-abbreviation (input)
- greater_eq (infix ">=" 50) where
- "x >= y \<equiv> y <= x"
-
-notation (input)
- greater_eq (infix "\<ge>" 50)
-
-abbreviation (input)
- greater (infix ">" 50) where
- "x > y \<equiv> y < x"
-
-end
-
-syntax
- "_index1" :: index ("\<^sub>1")
-translations
- (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
-lemma mk_left_commute:
- fixes f (infix "\<otimes>" 60)
- assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
- c: "\<And>x y. x \<otimes> y = y \<otimes> x"
- shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
- by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
-
-
subsection {* Basic ML bindings *}
ML {*
--- a/src/HOL/Hoare/hoare_tac.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Sun Jan 31 15:22:40 2010 +0100
@@ -58,7 +58,7 @@
let val T as Type ("fun",[t,_]) = fastype_of trm
in Collect_const t $ trm end;
-fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT);
fun Mset ctxt prop =
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sun Jan 31 15:22:40 2010 +0100
@@ -166,7 +166,7 @@
import_theory prim_rec;
const_maps
- "<" > HOL.ord_class.less :: "[nat,nat]=>bool";
+ "<" > Algebras.less :: "[nat,nat]=>bool";
end_import;
@@ -181,15 +181,15 @@
">" > HOL4Compat.nat_gt
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
- "<=" > HOL.ord_class.less_eq :: "[nat,nat]=>bool"
- "+" > HOL.plus_class.plus :: "[nat,nat]=>nat"
- "*" > HOL.times_class.times :: "[nat,nat]=>nat"
- "-" > HOL.minus_class.minus :: "[nat,nat]=>nat"
- MIN > Orderings.ord_class.min :: "[nat,nat]=>nat"
- MAX > Orderings.ord_class.max :: "[nat,nat]=>nat"
- DIV > Divides.div_class.div :: "[nat,nat]=>nat"
- MOD > Divides.div_class.mod :: "[nat,nat]=>nat"
- EXP > Power.power_class.power :: "[nat,nat]=>nat";
+ "<=" > Algebras.less_eq :: "[nat,nat]=>bool"
+ "+" > Algebras.plus :: "[nat,nat]=>nat"
+ "*" > Algebras.times :: "[nat,nat]=>nat"
+ "-" > Algebras.minus :: "[nat,nat]=>nat"
+ MIN > Orderings.min :: "[nat,nat]=>nat"
+ MAX > Orderings.max :: "[nat,nat]=>nat"
+ DIV > Divides.div :: "[nat,nat]=>nat"
+ MOD > Divides.mod :: "[nat,nat]=>nat"
+ EXP > Power.power :: "[nat,nat]=>nat";
end_import;
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Import/Generate-HOL/GenHOL4Real.thy
- ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
*)
@@ -17,13 +16,13 @@
real > RealDef.real;
const_maps
- real_0 > 0 :: real
- real_1 > 1 :: real
- real_neg > uminus :: "real => real"
- inv > HOL.inverse :: "real => real"
- real_add > HOL.plus :: "[real,real] => real"
- real_mul > HOL.times :: "[real,real] => real"
- real_lt > HOL.ord_class.less :: "[real,real] => bool";
+ real_0 > Algebras.zero :: real
+ real_1 > Algebras.one :: real
+ real_neg > Algebras.uminus :: "real => real"
+ inv > Algebras.inverse :: "real => real"
+ real_add > Algebras.plus :: "[real,real] => real"
+ real_mul > Algebras.times :: "[real,real] => real"
+ real_lt > Algebras.less :: "[real,real] => bool";
ignore_thms
real_TY_DEF
@@ -51,11 +50,11 @@
const_maps
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
- real_lte > HOL.ord_class.less_eq :: "[real,real] => bool"
- real_sub > HOL.minus :: "[real,real] => real"
- "/" > HOL.divide :: "[real,real] => real"
- pow > Power.power_class.power :: "[real,nat] => real"
- abs > HOL.abs :: "real => real"
+ real_lte > Algebras.less_eq :: "[real,real] => bool"
+ real_sub > Algebras.minus :: "[real,real] => real"
+ "/" > Algebras.divide :: "[real,real] => real"
+ pow > Power.power :: "[real,nat] => real"
+ abs > Algebras.abs :: "real => real"
real_of_num > RealDef.real :: "nat => real";
end_import;
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sun Jan 31 15:22:40 2010 +0100
@@ -76,9 +76,9 @@
SUC > Suc
PRE > HOLLightCompat.Pred
NUMERAL > HOL4Compat.NUMERAL
- "+" > HOL.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- "*" > HOL.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- "-" > HOL.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "+" > Algebras.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "*" > Algebras.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "-" > Algebras.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
BIT0 > HOLLightCompat.NUMERAL_BIT0
BIT1 > HOL4Compat.NUMERAL_BIT1
INL > Sum_Type.Inl
--- a/src/HOL/Import/HOL/arithmetic.imp Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Sun Jan 31 15:22:40 2010 +0100
@@ -23,10 +23,10 @@
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
- "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
- "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
- "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
- "*" > "HOL.times_class.times" :: "nat => nat => nat"
+ "<=" > "Algebras.ord_class.less_eq" :: "nat => nat => bool"
+ "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
+ "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
+ "*" > "Algebras.times_class.times" :: "nat => nat => nat"
thm_maps
"num_case_def" > "HOL4Compat.num_case_def"
--- a/src/HOL/Import/HOL/prim_rec.imp Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/HOL/prim_rec.imp Sun Jan 31 15:22:40 2010 +0100
@@ -18,7 +18,7 @@
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
"PRE" > "HOL4Base.prim_rec.PRE"
- "<" > "HOL.ord_class.less" :: "nat => nat => bool"
+ "<" > "Algebras.less" :: "nat => nat => bool"
thm_maps
"wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
--- a/src/HOL/Import/HOL/real.imp Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/HOL/real.imp Sun Jan 31 15:22:40 2010 +0100
@@ -10,14 +10,14 @@
const_maps
"sup" > "HOL4Real.real.sup"
"sum" > "HOL4Real.real.sum"
- "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
+ "real_sub" > "Algebras.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
- "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
+ "real_lte" > "Algebras.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"pow" > "Power.power_class.power" :: "real => nat => real"
- "abs" > "HOL.minus_class.abs" :: "real => real"
- "/" > "HOL.divides_class.divide" :: "real => real => real"
+ "abs" > "Algebras.abs" :: "real => real"
+ "/" > "Algebras.divide" :: "real => real => real"
thm_maps
"sup_def" > "HOL4Real.real.sup_def"
--- a/src/HOL/Import/HOL/realax.imp Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/HOL/realax.imp Sun Jan 31 15:22:40 2010 +0100
@@ -27,13 +27,13 @@
"treal_add" > "HOL4Real.realax.treal_add"
"treal_1" > "HOL4Real.realax.treal_1"
"treal_0" > "HOL4Real.realax.treal_0"
- "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
- "real_mul" > "HOL.times_class.times" :: "real => real => real"
- "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
- "real_add" > "HOL.plus_class.plus" :: "real => real => real"
- "real_1" > "HOL.one_class.one" :: "real"
- "real_0" > "HOL.zero_class.zero" :: "real"
- "inv" > "HOL.divide_class.inverse" :: "real => real"
+ "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
+ "real_mul" > "Algebras.times_class.times" :: "real => real => real"
+ "real_lt" > "Algebras.ord_class.less" :: "real => real => bool"
+ "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
+ "real_1" > "Algebras.one_class.one" :: "real"
+ "real_0" > "Algebras.zero_class.zero" :: "real"
+ "inv" > "Algebras.divide_class.inverse" :: "real => real"
"hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
thm_maps
--- a/src/HOL/Import/HOLLight/HOLLight.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/HOLLight/HOLLight.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1119,37 +1119,37 @@
(%x::nat.
(All::(nat => bool) => bool)
(%xa::nat.
- (op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
- ((HOL.plus::nat => nat => nat) x xa))))
+ (op =::nat => nat => bool) ((plus::nat => nat => nat) x xa)
+ ((plus::nat => nat => nat) x xa))))
((op &::bool => bool => bool)
- ((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
+ ((op =::nat => nat => bool) ((plus::nat => nat => nat) (0::nat) (0::nat))
(0::nat))
((op &::bool => bool => bool)
((All::(nat => bool) => bool)
(%x::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat) (0::nat)
+ ((plus::nat => nat => nat) (0::nat)
((NUMERAL_BIT0::nat => nat) x))
((NUMERAL_BIT0::nat => nat) x)))
((op &::bool => bool => bool)
((All::(nat => bool) => bool)
(%x::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat) (0::nat)
+ ((plus::nat => nat => nat) (0::nat)
((NUMERAL_BIT1::nat => nat) x))
((NUMERAL_BIT1::nat => nat) x)))
((op &::bool => bool => bool)
((All::(nat => bool) => bool)
(%x::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
+ ((plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
(0::nat))
((NUMERAL_BIT0::nat => nat) x)))
((op &::bool => bool => bool)
((All::(nat => bool) => bool)
(%x::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
+ ((plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
(0::nat))
((NUMERAL_BIT1::nat => nat) x)))
((op &::bool => bool => bool)
@@ -1158,44 +1158,44 @@
(All::(nat => bool) => bool)
(%xa::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT0::nat => nat) x)
((NUMERAL_BIT0::nat => nat) xa))
((NUMERAL_BIT0::nat => nat)
- ((HOL.plus::nat => nat => nat) x xa)))))
+ ((plus::nat => nat => nat) x xa)))))
((op &::bool => bool => bool)
((All::(nat => bool) => bool)
(%x::nat.
(All::(nat => bool) => bool)
(%xa::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT0::nat => nat) x)
((NUMERAL_BIT1::nat => nat) xa))
((NUMERAL_BIT1::nat => nat)
- ((HOL.plus::nat => nat => nat) x xa)))))
+ ((plus::nat => nat => nat) x xa)))))
((op &::bool => bool => bool)
((All::(nat => bool) => bool)
(%x::nat.
(All::(nat => bool) => bool)
(%xa::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT1::nat => nat) x)
((NUMERAL_BIT0::nat => nat) xa))
((NUMERAL_BIT1::nat => nat)
- ((HOL.plus::nat => nat => nat) x xa)))))
+ ((plus::nat => nat => nat) x xa)))))
((All::(nat => bool) => bool)
(%x::nat.
(All::(nat => bool) => bool)
(%xa::nat.
(op =::nat => nat => bool)
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT1::nat => nat) x)
((NUMERAL_BIT1::nat => nat) xa))
((NUMERAL_BIT0::nat => nat)
((Suc::nat => nat)
- ((HOL.plus::nat => nat => nat) x
+ ((plus::nat => nat => nat) x
xa))))))))))))))"
by (import hollight ARITH_ADD)
@@ -1258,7 +1258,7 @@
((op *::nat => nat => nat)
((NUMERAL_BIT0::nat => nat) x)
((NUMERAL_BIT1::nat => nat) xa))
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT0::nat => nat) x)
((NUMERAL_BIT0::nat => nat)
((NUMERAL_BIT0::nat => nat)
@@ -1272,7 +1272,7 @@
((op *::nat => nat => nat)
((NUMERAL_BIT1::nat => nat) x)
((NUMERAL_BIT0::nat => nat) xa))
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT0::nat => nat) xa)
((NUMERAL_BIT0::nat => nat)
((NUMERAL_BIT0::nat => nat)
@@ -1285,9 +1285,9 @@
((op *::nat => nat => nat)
((NUMERAL_BIT1::nat => nat) x)
((NUMERAL_BIT1::nat => nat) xa))
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT1::nat => nat) x)
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((NUMERAL_BIT0::nat => nat) xa)
((NUMERAL_BIT0::nat => nat)
((NUMERAL_BIT0::nat => nat)
@@ -7462,7 +7462,7 @@
(%i::nat.
($::('A::type, ('M::type, 'N::type) finite_sum) cart
=> nat => 'A::type)
- u ((HOL.plus::nat => nat => nat) i
+ u ((plus::nat => nat => nat) i
((dimindex::('M::type => bool) => nat)
(hollight.UNIV::'M::type => bool)))))"
@@ -7478,14 +7478,14 @@
(%i::nat.
($::('A::type, ('M::type, 'N::type) finite_sum) cart
=> nat => 'A::type)
- u ((HOL.plus::nat => nat => nat) i
+ u ((plus::nat => nat => nat) i
((dimindex::('M::type => bool) => nat)
(hollight.UNIV::'M::type => bool)))))"
by (import hollight DEF_sndcart)
lemma DIMINDEX_HAS_SIZE_FINITE_SUM: "(HAS_SIZE::(('M::type, 'N::type) finite_sum => bool) => nat => bool)
(hollight.UNIV::('M::type, 'N::type) finite_sum => bool)
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
((dimindex::('N::type => bool) => nat)
(hollight.UNIV::'N::type => bool)))"
@@ -7494,7 +7494,7 @@
lemma DIMINDEX_FINITE_SUM: "(op =::nat => nat => bool)
((dimindex::(('M::type, 'N::type) finite_sum => bool) => nat)
(hollight.UNIV::('M::type, 'N::type) finite_sum => bool))
- ((HOL.plus::nat => nat => nat)
+ ((plus::nat => nat => nat)
((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
((dimindex::('N::type => bool) => nat)
(hollight.UNIV::'N::type => bool)))"
@@ -8025,7 +8025,7 @@
(nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
((iterate::(nat => nat => nat)
=> ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
- (HOL.plus::nat => nat => nat))"
+ (plus::nat => nat => nat))"
lemma DEF_nsum: "(op =::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
=> (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
@@ -8033,17 +8033,17 @@
(nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
((iterate::(nat => nat => nat)
=> ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
- (HOL.plus::nat => nat => nat))"
+ (plus::nat => nat => nat))"
by (import hollight DEF_nsum)
lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
- ((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
+ ((neutral::(nat => nat => nat) => nat) (plus::nat => nat => nat)) (0::nat)"
by (import hollight NEUTRAL_ADD)
lemma NEUTRAL_MUL: "neutral op * = NUMERAL_BIT1 0"
by (import hollight NEUTRAL_MUL)
-lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (HOL.plus::nat => nat => nat)"
+lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (plus::nat => nat => nat)"
by (import hollight MONOIDAL_ADD)
lemma MONOIDAL_MUL: "(monoidal::(nat => nat => nat) => bool) (op *::nat => nat => nat)"
@@ -8068,7 +8068,7 @@
by (import hollight NSUM_DIFF)
lemma NSUM_SUPPORT: "ALL (x::'q_51214::type => nat) xa::'q_51214::type => bool.
- FINITE (support HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
+ FINITE (support plus x xa) --> nsum (support plus x xa) x = nsum xa x"
by (import hollight NSUM_SUPPORT)
lemma NSUM_ADD: "ALL (f::'q_51260::type => nat) (g::'q_51260::type => nat)
--- a/src/HOL/Import/HOLLight/hollight.imp Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp Sun Jan 31 15:22:40 2010 +0100
@@ -238,10 +238,10 @@
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
"/\\" > "op &"
- "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
+ "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
"," > "Pair"
- "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
- "*" > "HOL.times_class.times" :: "nat => nat => nat"
+ "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
+ "*" > "Algebras.times_class.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
"!" > "All"
--- a/src/HOL/IsaMakefile Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/IsaMakefile Sun Jan 31 15:22:40 2010 +0100
@@ -141,6 +141,7 @@
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
+ Algebras.thy \
Complete_Lattice.thy \
Datatype.thy \
Extraction.thy \
--- a/src/HOL/Lattices.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Lattices.thy Sun Jan 31 15:22:40 2010 +0100
@@ -112,48 +112,73 @@
subsubsection {* Equational laws *}
+sublocale lower_semilattice < inf!: semilattice inf
+proof
+ fix a b c
+ show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
+ by (rule antisym) (auto intro: le_infI1 le_infI2)
+ show "a \<sqinter> b = b \<sqinter> a"
+ by (rule antisym) auto
+ show "a \<sqinter> a = a"
+ by (rule antisym) auto
+qed
+
context lower_semilattice
begin
-lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
- by (rule antisym) auto
+lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+ by (fact inf.assoc)
-lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
- by (rule antisym) (auto intro: le_infI1 le_infI2)
+lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
+ by (fact inf.commute)
-lemma inf_idem[simp]: "x \<sqinter> x = x"
- by (rule antisym) auto
+lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
+ by (fact inf.left_commute)
-lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
- by (rule antisym) (auto intro: le_infI2)
+lemma inf_idem: "x \<sqinter> x = x"
+ by (fact inf.idem)
+
+lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+ by (fact inf.left_idem)
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
by (rule antisym) auto
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
by (rule antisym) auto
-
-lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
- by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
-
+
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
end
+sublocale upper_semilattice < sup!: semilattice sup
+proof
+ fix a b c
+ show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
+ by (rule antisym) (auto intro: le_supI1 le_supI2)
+ show "a \<squnion> b = b \<squnion> a"
+ by (rule antisym) auto
+ show "a \<squnion> a = a"
+ by (rule antisym) auto
+qed
+
context upper_semilattice
begin
-lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
- by (rule antisym) auto
+lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+ by (fact sup.assoc)
-lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
- by (rule antisym) (auto intro: le_supI1 le_supI2)
+lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
+ by (fact sup.commute)
-lemma sup_idem[simp]: "x \<squnion> x = x"
- by (rule antisym) auto
+lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
+ by (fact sup.left_commute)
-lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
- by (rule antisym) (auto intro: le_supI2)
+lemma sup_idem: "x \<squnion> x = x"
+ by (fact sup.idem)
+
+lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
+ by (fact sup.left_idem)
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
by (rule antisym) auto
@@ -161,9 +186,6 @@
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
by (rule antisym) auto
-lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
- by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
-
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
end
@@ -514,11 +536,12 @@
lemmas le_maxI1 = min_max.sup_ge1
lemmas le_maxI2 = min_max.sup_ge2
-lemmas max_ac = min_max.sup_assoc min_max.sup_commute
- mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
+lemmas min_ac = min_max.inf_assoc min_max.inf_commute
+ min_max.inf.left_commute
-lemmas min_ac = min_max.inf_assoc min_max.inf_commute
- mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
+lemmas max_ac = min_max.sup_assoc min_max.sup_commute
+ min_max.sup.left_commute
+
subsection {* Bool as lattice *}
--- a/src/HOL/Library/Boolean_Algebra.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy Sun Jan 31 15:22:40 2010 +0100
@@ -24,15 +24,22 @@
assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
+
+sublocale boolean < conj!: abel_semigroup conj proof
+qed (fact conj_assoc conj_commute)+
+
+sublocale boolean < disj!: abel_semigroup disj proof
+qed (fact disj_assoc disj_commute)+
+
+context boolean
begin
-lemmas disj_ac =
- disj_assoc disj_commute
- mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute]
+lemmas conj_left_commute = conj.left_commute
-lemmas conj_ac =
- conj_assoc conj_commute
- mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute]
+lemmas disj_left_commute = disj.left_commute
+
+lemmas conj_ac = conj.assoc conj.commute conj.left_commute
+lemmas disj_ac = disj.assoc disj.commute disj.left_commute
lemma dual: "boolean disj conj compl one zero"
apply (rule boolean.intro)
@@ -178,18 +185,9 @@
locale boolean_xor = boolean +
fixes xor :: "'a => 'a => 'a" (infixr "\<oplus>" 65)
assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
-begin
-lemma xor_def2:
- "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
-by (simp only: xor_def conj_disj_distribs
- disj_ac conj_ac conj_cancel_right disj_zero_left)
-
-lemma xor_commute: "x \<oplus> y = y \<oplus> x"
-by (simp only: xor_def conj_commute disj_commute)
-
-lemma xor_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-proof -
+sublocale boolean_xor < xor!: abel_semigroup xor proof
+ fix x y z :: 'a
let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
(\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
@@ -199,11 +197,23 @@
apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
apply (simp only: conj_disj_distribs conj_ac disj_ac)
done
+ show "x \<oplus> y = y \<oplus> x"
+ by (simp only: xor_def conj_commute disj_commute)
qed
-lemmas xor_ac =
- xor_assoc xor_commute
- mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute]
+context boolean_xor
+begin
+
+lemmas xor_assoc = xor.assoc
+lemmas xor_commute = xor.commute
+lemmas xor_left_commute = xor.left_commute
+
+lemmas xor_ac = xor.assoc xor.commute xor.left_commute
+
+lemma xor_def2:
+ "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
+by (simp only: xor_def conj_disj_distribs
+ disj_ac conj_ac conj_cancel_right disj_zero_left)
lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
--- a/src/HOL/Library/Polynomial.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Library/Polynomial.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1200,14 +1200,18 @@
by (rule poly_dvd_antisym)
qed
-lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
-by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+interpretation poly_gcd!: abel_semigroup poly_gcd
+proof
+ fix x y z :: "'a poly"
+ show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
+ by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
+ show "poly_gcd x y = poly_gcd y x"
+ by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+qed
-lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
-by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
-
-lemmas poly_gcd_left_commute =
- mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
+lemmas poly_gcd_assoc = poly_gcd.assoc
+lemmas poly_gcd_commute = poly_gcd.commute
+lemmas poly_gcd_left_commute = poly_gcd.left_commute
lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
--- a/src/HOL/Mutabelle/Mutabelle.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Mutabelle/Mutabelle.thy Sun Jan 31 15:22:40 2010 +0100
@@ -7,16 +7,16 @@
val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
val forbidden =
- [(@{const_name "power"}, "'a"),
- ("HOL.induct_equal", "'a"),
- ("HOL.induct_implies", "'a"),
- ("HOL.induct_conj", "'a"),
- (@{const_name "undefined"}, "'a"),
- (@{const_name "default"}, "'a"),
- (@{const_name "dummy_pattern"}, "'a::{}"),
- (@{const_name "uminus"}, "'a"),
- (@{const_name "Nat.size"}, "'a"),
- (@{const_name "HOL.abs"}, "'a")];
+ [(@{const_name Power.power}, "'a"),
+ (@{const_name HOL.induct_equal}, "'a"),
+ (@{const_name HOL.induct_implies}, "'a"),
+ (@{const_name HOL.induct_conj}, "'a"),
+ (@{const_name HOL.undefined}, "'a"),
+ (@{const_name HOL.default}, "'a"),
+ (@{const_name dummy_pattern}, "'a::{}"),
+ (@{const_name Algebras.uminus}, "'a"),
+ (@{const_name Nat.size}, "'a"),
+ (@{const_name Algebras.abs}, "'a")];
val forbidden_thms =
["finite_intvl_succ_class",
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Jan 31 15:22:40 2010 +0100
@@ -189,15 +189,15 @@
val forbidden =
[(* (@{const_name "power"}, "'a"), *)
- ("HOL.induct_equal", "'a"),
- ("HOL.induct_implies", "'a"),
- ("HOL.induct_conj", "'a"),
+ (@{const_name HOL.induct_equal}, "'a"),
+ (@{const_name HOL.induct_implies}, "'a"),
+ (@{const_name HOL.induct_conj}, "'a"),
(@{const_name "undefined"}, "'a"),
(@{const_name "default"}, "'a"),
(@{const_name "dummy_pattern"}, "'a::{}") (*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
- (@{const_name "HOL.abs"}, "'a") *)]
+ (@{const_name "Algebras.abs"}, "'a") *)]
val forbidden_thms =
["finite_intvl_succ_class",
--- a/src/HOL/NSA/NSA.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/NSA/NSA.thy Sun Jan 31 15:22:40 2010 +0100
@@ -671,12 +671,12 @@
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
fun reorient_proc sg _ (_ $ t $ u) =
case u of
- Const(@{const_name HOL.zero}, _) => NONE
- | Const(@{const_name HOL.one}, _) => NONE
+ Const(@{const_name Algebras.zero}, _) => NONE
+ | Const(@{const_name Algebras.one}, _) => NONE
| Const(@{const_name Int.number_of}, _) $ _ => NONE
| _ => SOME (case t of
- Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient
- | Const(@{const_name HOL.one}, _) => meta_one_approx_reorient
+ Const(@{const_name Algebras.zero}, _) => meta_zero_approx_reorient
+ | Const(@{const_name Algebras.one}, _) => meta_one_approx_reorient
| Const(@{const_name Int.number_of}, _) $ _ =>
meta_number_of_approx_reorient);
--- a/src/HOL/OrderedGroup.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/OrderedGroup.thy Sun Jan 31 15:22:40 2010 +0100
@@ -23,8 +23,7 @@
*}
ML {*
-structure Algebra_Simps = Named_Thms
-(
+structure Algebra_Simps = Named_Thms(
val name = "algebra_simps"
val description = "algebra simplification rules"
)
@@ -44,14 +43,21 @@
subsection {* Semigroups and Monoids *}
class semigroup_add = plus +
- assumes add_assoc[algebra_simps]: "(a + b) + c = a + (b + c)"
+ assumes add_assoc [algebra_simps]: "(a + b) + c = a + (b + c)"
+
+sublocale semigroup_add < plus!: semigroup plus proof
+qed (fact add_assoc)
class ab_semigroup_add = semigroup_add +
- assumes add_commute[algebra_simps]: "a + b = b + a"
+ assumes add_commute [algebra_simps]: "a + b = b + a"
+
+sublocale ab_semigroup_add < plus!: abel_semigroup plus proof
+qed (fact add_commute)
+
+context ab_semigroup_add
begin
-lemma add_left_commute[algebra_simps]: "a + (b + c) = b + (a + c)"
-by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
+lemmas add_left_commute [algebra_simps] = plus.left_commute
theorems add_ac = add_assoc add_commute add_left_commute
@@ -60,14 +66,21 @@
theorems add_ac = add_assoc add_commute add_left_commute
class semigroup_mult = times +
- assumes mult_assoc[algebra_simps]: "(a * b) * c = a * (b * c)"
+ assumes mult_assoc [algebra_simps]: "(a * b) * c = a * (b * c)"
+
+sublocale semigroup_mult < times!: semigroup times proof
+qed (fact mult_assoc)
class ab_semigroup_mult = semigroup_mult +
- assumes mult_commute[algebra_simps]: "a * b = b * a"
+ assumes mult_commute [algebra_simps]: "a * b = b * a"
+
+sublocale ab_semigroup_mult < times!: abel_semigroup times proof
+qed (fact mult_commute)
+
+context ab_semigroup_mult
begin
-lemma mult_left_commute[algebra_simps]: "a * (b * c) = b * (a * c)"
-by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
+lemmas mult_left_commute [algebra_simps] = times.left_commute
theorems mult_ac = mult_assoc mult_commute mult_left_commute
@@ -76,11 +89,15 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
class ab_semigroup_idem_mult = ab_semigroup_mult +
- assumes mult_idem[simp]: "x * x = x"
+ assumes mult_idem: "x * x = x"
+
+sublocale ab_semigroup_idem_mult < times!: semilattice times proof
+qed (fact mult_idem)
+
+context ab_semigroup_idem_mult
begin
-lemma mult_left_idem[simp]: "x * (x * y) = x * y"
- unfolding mult_assoc [symmetric, of x] mult_idem ..
+lemmas mult_left_idem = times.left_idem
end
@@ -1370,8 +1387,8 @@
(* term order for abelian groups *)
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
- [@{const_name HOL.zero}, @{const_name HOL.plus},
- @{const_name HOL.uminus}, @{const_name HOL.minus}]
+ [@{const_name Algebras.zero}, @{const_name Algebras.plus},
+ @{const_name Algebras.uminus}, @{const_name Algebras.minus}]
| agrp_ord _ = ~1;
fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
@@ -1380,9 +1397,9 @@
val ac1 = mk_meta_eq @{thm add_assoc};
val ac2 = mk_meta_eq @{thm add_commute};
val ac3 = mk_meta_eq @{thm add_left_commute};
- fun solve_add_ac thy _ (_ $ (Const (@{const_name HOL.plus},_) $ _ $ _) $ _) =
+ fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) =
SOME ac1
- | solve_add_ac thy _ (_ $ x $ (Const (@{const_name HOL.plus},_) $ y $ z)) =
+ | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) =
if termless_agrp (y, x) then SOME ac3 else NONE
| solve_add_ac thy _ (_ $ x $ y) =
if termless_agrp (y, x) then SOME ac2 else NONE
--- a/src/HOL/Orderings.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Orderings.thy Sun Jan 31 15:22:40 2010 +0100
@@ -5,7 +5,7 @@
header {* Abstract orderings *}
theory Orderings
-imports HOL
+imports Algebras
uses
"~~/src/Provers/order.ML"
"~~/src/Provers/quasi.ML" (* FIXME unused? *)
--- a/src/HOL/Prolog/Func.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Prolog/Func.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Prolog/Func.thy
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
header {* Untyped functional language, with call by value semantics *}
theory Func
-imports HOHH
+imports HOHH Algebras
begin
typedecl tm
--- a/src/HOL/Prolog/HOHH.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Prolog/HOHH.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Prolog/HOHH.thy
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
--- a/src/HOL/Prolog/Test.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Prolog/Test.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Prolog/Test.thy
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
--- a/src/HOL/Prolog/Type.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Prolog/Type.thy Sun Jan 31 15:22:40 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Prolog/Type.thy
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
--- a/src/HOL/Set.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Set.thy Sun Jan 31 15:22:40 2010 +0100
@@ -928,7 +928,7 @@
outer-level constant, which in this case is just "op :"; we instead need
to use term-nets to associate patterns with rules. Also, if a rule fails to
apply, then the formula should be kept.
- [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
+ [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
("Int", [IntD1,IntD2]),
("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
*)
--- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Sun Jan 31 15:22:40 2010 +0100
@@ -80,10 +80,10 @@
let
val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
in
- case try_proof (goals @{const_name HOL.less}) solve_tac of
+ case try_proof (goals @{const_name Algebras.less}) solve_tac of
Solved thm => Less thm
| Stuck thm =>
- (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of
+ (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
--- a/src/HOL/Tools/Function/size.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML Sun Jan 31 15:22:40 2010 +0100
@@ -25,7 +25,7 @@
val lookup_size = SizeData.get #> Symtab.lookup;
-fun plus (t1, t2) = Const ("HOL.plus_class.plus",
+fun plus (t1, t2) = Const (@{const_name Algebras.plus},
HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
fun size_of_type f g h (T as Type (s, Ts)) =
--- a/src/HOL/Tools/Function/termination.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML Sun Jan 31 15:22:40 2010 +0100
@@ -203,10 +203,10 @@
HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
$ (m2 $ r) $ (m1 $ l)))))) tac
in
- case try @{const_name HOL.less} of
+ case try @{const_name Algebras.less} of
Solved thm => Less thm
| Stuck thm =>
- (case try @{const_name HOL.less_eq} of
+ (case try @{const_name Algebras.less_eq} of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Jan 31 15:22:40 2010 +0100
@@ -74,7 +74,7 @@
Const (atom_name "" T j, T)
(* term -> real *)
-fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
(* term * term -> order *)
@@ -434,7 +434,7 @@
0 => mk_num 0
| n1 => case HOLogic.dest_number t2 |> snd of
1 => mk_num n1
- | n2 => Const (@{const_name HOL.divide},
+ | n2 => Const (@{const_name Algebras.divide},
num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
| _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Jan 31 15:22:40 2010 +0100
@@ -1561,7 +1561,7 @@
end;
(* special setup for simpset *)
-val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
+val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
@@ -1817,7 +1817,7 @@
(* make this simpset better! *)
asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
THEN print_tac' options "after prove_match:"
- THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
+ THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1
THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
THEN print_tac' options "if condition to be solved:"
THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:"))
@@ -1843,7 +1843,7 @@
in
(* remove not_False_eq_True when simpset in prove_match is better *)
simp_tac (HOL_basic_ss addsimps
- (@{thms "HOL.simp_thms"} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1
+ (@{thms HOL.simp_thms} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1
(* need better control here! *)
end
@@ -2435,8 +2435,8 @@
val [polarity, depth] = additional_arguments
val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
val depth' =
- Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
- $ depth $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})
+ Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"})
+ $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"})
in [polarity', depth'] end
}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Jan 31 15:22:40 2010 +0100
@@ -219,21 +219,21 @@
@{const_name "op &"}]
fun special_cases (c, T) = member (op =) [
- @{const_name "Product_Type.Unity"},
- @{const_name "False"},
- @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
+ @{const_name Product_Type.Unity},
+ @{const_name False},
+ @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
@{const_name Nat.one_nat_inst.one_nat},
- @{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"},
- @{const_name "HOL.zero_class.zero"},
- @{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus},
+ @{const_name Algebras.ord_class.less}, @{const_name Algebras.ord_class.less_eq},
+ @{const_name Algebras.zero},
+ @{const_name Algebras.one}, @{const_name Algebras.plus},
@{const_name Nat.ord_nat_inst.less_eq_nat},
@{const_name Nat.ord_nat_inst.less_nat},
@{const_name number_nat_inst.number_of_nat},
@{const_name Int.Bit0},
@{const_name Int.Bit1},
@{const_name Int.Pls},
- @{const_name "Int.zero_int_inst.zero_int"},
- @{const_name "List.filter"}] c
+ @{const_name Int.zero_int_inst.zero_int},
+ @{const_name List.filter}] c
fun print_specification options thy constname specs =
if show_intermediate_results options then
--- a/src/HOL/Tools/Qelim/cooper.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Jan 31 15:22:40 2010 +0100
@@ -73,15 +73,15 @@
| Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
-| Const (@{const_name HOL.less}, _) $ y$ z =>
+| Const (@{const_name Algebras.less}, _) $ y$ z =>
if term_of x aconv y then Lt (Thm.dest_arg ct)
else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
+| Const (@{const_name Algebras.less_eq}, _) $ y $ z =>
if term_of x aconv y then Le (Thm.dest_arg ct)
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
+| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
if term_of x aconv y then
NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
| _ => Nox)
@@ -175,18 +175,18 @@
(fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
fun linear_cmul 0 tm = zero
| linear_cmul n tm = case tm of
- Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
- | Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
- | Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
- | (m as Const (@{const_name HOL.uminus}, _)) $ a => m $ linear_cmul n a
+ Const (@{const_name Algebras.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
+ | Const (@{const_name Algebras.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
+ | Const (@{const_name Algebras.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
+ | (m as Const (@{const_name Algebras.uminus}, _)) $ a => m $ linear_cmul n a
| _ => numeral1 (fn m => n * m) tm;
fun earlier [] x y = false
| earlier (h::t) x y =
if h aconv y then false else if h aconv x then true else earlier t x y;
fun linear_add vars tm1 tm2 = case (tm1, tm2) of
- (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
- Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
+ (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1,
+ Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
if x1 = x2 then
let val c = numeral2 Integer.add c1 c2
in if c = zero then linear_add vars r1 r2
@@ -194,9 +194,9 @@
end
else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
- | (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, _) =>
+ | (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) =>
addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
- | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
+ | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
| (_, _) => numeral2 Integer.add tm1 tm2;
@@ -205,10 +205,10 @@
fun lint vars tm = if is_numeral tm then tm else case tm of
- Const (@{const_name HOL.uminus}, _) $ t => linear_neg (lint vars t)
-| Const (@{const_name HOL.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
-| Const (@{const_name HOL.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
-| Const (@{const_name HOL.times}, _) $ s $ t =>
+ Const (@{const_name Algebras.uminus}, _) $ t => linear_neg (lint vars t)
+| Const (@{const_name Algebras.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
+| Const (@{const_name Algebras.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
+| Const (@{const_name Algebras.times}, _) $ s $ t =>
let val s' = lint vars s
val t' = lint vars t
in if is_numeral s' then (linear_cmul (dest_numeral s') t')
@@ -217,10 +217,10 @@
end
| _ => addC $ (mulC $ one $ tm) $ zero;
-fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) =
- lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s)
- | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
- lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
+fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) =
+ lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s)
+ | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) =
+ lin vs (Const (@{const_name Algebras.less}, T) $ t $ s)
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
| lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
@@ -270,7 +270,7 @@
val d'' = Thm.rhs_of dth |> Thm.dest_arg1
in
case tt' of
- Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ =>
+ Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$_)$_ =>
let val x = dest_numeral c
in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
(Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
@@ -293,15 +293,15 @@
val ins = insert (op = : int * int -> bool)
fun h (acc,dacc) t =
case (term_of t) of
- Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
+ Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
- ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
+ ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
- | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
+ | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
if x aconv y andalso member (op =)
- [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
+ [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
- | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
+ | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
| Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
@@ -335,15 +335,15 @@
Const("op &",_)$_$_ => binop_conv unit_conv t
| Const("op |",_)$_$_ => binop_conv unit_conv t
| Const (@{const_name Not},_)$_ => arg_conv unit_conv t
- | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
+ | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
- ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
+ ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
- | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
+ | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
if x=y andalso member (op =)
- [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
+ [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
- | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
+ | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
if x=y then
let
val k = l div dest_numeral c
@@ -546,10 +546,10 @@
| @{term "0::int"} => C 0
| @{term "1::int"} => C 1
| Term.Bound i => Bound i
- | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
- | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name HOL.times},_)$t1$t2 =>
+ | Const(@{const_name Algebras.uminus},_)$t' => Neg (i_of_term vs t')
+ | Const(@{const_name Algebras.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Algebras.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Algebras.times},_)$t1$t2 =>
(Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
handle TERM _ =>
(Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
@@ -560,8 +560,8 @@
fun qf_of_term ps vs t = case t
of Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
| Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *)
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
--- a/src/HOL/Tools/Qelim/cooper_data.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Sun Jan 31 15:22:40 2010 +0100
@@ -33,7 +33,7 @@
@{term "abs :: int => _"},
@{term "max :: int => _"}, @{term "max :: nat => _"},
@{term "min :: int => _"}, @{term "min :: nat => _"},
- @{term "HOL.uminus :: int => _"}, (*@ {term "HOL.uminus :: nat => _"},*)
+ @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
@{term "Not"}, @{term "Suc"},
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
--- a/src/HOL/Tools/Qelim/presburger.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Sun Jan 31 15:22:40 2010 +0100
@@ -52,15 +52,15 @@
local
fun isnum t = case t of
- Const(@{const_name HOL.zero},_) => true
- | Const(@{const_name HOL.one},_) => true
+ Const(@{const_name Algebras.zero},_) => true
+ | Const(@{const_name Algebras.one},_) => true
| @{term "Suc"}$s => isnum s
| @{term "nat"}$s => isnum s
| @{term "int"}$s => isnum s
- | Const(@{const_name HOL.uminus},_)$s => isnum s
- | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Algebras.uminus},_)$s => isnum s
+ | Const(@{const_name Algebras.plus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Algebras.times},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Algebras.minus},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
--- a/src/HOL/Tools/arith_data.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML Sun Jan 31 15:22:40 2010 +0100
@@ -75,11 +75,11 @@
fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
fun mk_minus t =
let val T = Term.fastype_of t
- in Const (@{const_name HOL.uminus}, T --> T) $ t end;
+ in Const (@{const_name Algebras.uminus}, T --> T) $ t end;
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
fun mk_sum T [] = mk_number T 0
@@ -91,9 +91,9 @@
| long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
(*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
+fun dest_summing (pos, Const (@{const_name Algebras.plus}, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (pos, u, ts))
- | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
+ | dest_summing (pos, Const (@{const_name Algebras.minus}, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
if pos then t::ts else mk_minus t :: ts;
--- a/src/HOL/Tools/hologic.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/hologic.ML Sun Jan 31 15:22:40 2010 +0100
@@ -440,9 +440,9 @@
val natT = Type ("nat", []);
-val zero = Const ("HOL.zero_class.zero", natT);
+val zero = Const ("Algebras.zero_class.zero", natT);
-fun is_zero (Const ("HOL.zero_class.zero", _)) = true
+fun is_zero (Const ("Algebras.zero_class.zero", _)) = true
| is_zero _ = false;
fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
@@ -458,7 +458,7 @@
| mk n = mk_Suc (mk (n - 1));
in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
-fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
+fun dest_nat (Const ("Algebras.zero_class.zero", _)) = 0
| dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
| dest_nat t = raise TERM ("dest_nat", [t]);
@@ -508,12 +508,12 @@
| add_numerals (Abs (_, _, t)) = add_numerals t
| add_numerals _ = I;
-fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
- | mk_number T 1 = Const ("HOL.one_class.one", T)
+fun mk_number T 0 = Const ("Algebras.zero_class.zero", T)
+ | mk_number T 1 = Const ("Algebras.one_class.one", T)
| mk_number T i = number_of_const T $ mk_numeral i;
-fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
- | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
+fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0)
+ | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1)
| dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
(T, dest_numeral t)
| dest_number t = raise TERM ("dest_number", [t]);
--- a/src/HOL/Tools/inductive.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Jan 31 15:22:40 2010 +0100
@@ -184,7 +184,7 @@
case concl_of thm of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
| _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
- | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
+ | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
| _ => thm
@@ -561,7 +561,7 @@
(list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
val ind_concl = HOLogic.mk_Trueprop
- (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
+ (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred));
val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
--- a/src/HOL/Tools/int_arith.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/int_arith.ML Sun Jan 31 15:22:40 2010 +0100
@@ -49,13 +49,13 @@
make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
proc = proc1, identifier = []};
-fun check (Const (@{const_name HOL.one}, @{typ int})) = false
- | check (Const (@{const_name HOL.one}, _)) = true
+fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
+ | check (Const (@{const_name Algebras.one}, _)) = true
| check (Const (s, _)) = member (op =) [@{const_name "op ="},
- @{const_name HOL.times}, @{const_name HOL.uminus},
- @{const_name HOL.minus}, @{const_name HOL.plus},
- @{const_name HOL.zero},
- @{const_name HOL.less}, @{const_name HOL.less_eq}] s
+ @{const_name Algebras.times}, @{const_name Algebras.uminus},
+ @{const_name Algebras.minus}, @{const_name Algebras.plus},
+ @{const_name Algebras.zero},
+ @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
| check (a $ b) = check a andalso check b
| check _ = false;
--- a/src/HOL/Tools/lin_arith.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Jan 31 15:22:40 2010 +0100
@@ -138,8 +138,8 @@
*)
fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
let
- fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) =
- (case s of Const (@{const_name HOL.times}, _) $ s1 $ s2 =>
+ fun demult ((mC as Const (@{const_name Algebras.times}, _)) $ s $ t, m) =
+ (case s of Const (@{const_name Algebras.times}, _) $ s1 $ s2 =>
(* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *)
demult (mC $ s1 $ (mC $ s2 $ t), m)
| _ =>
@@ -150,7 +150,7 @@
(SOME t', m'') => (SOME (mC $ s' $ t'), m'')
| (NONE, m'') => (SOME s', m''))
| (NONE, m') => demult (t, m')))
- | demult ((mC as Const (@{const_name HOL.divide}, _)) $ s $ t, m) =
+ | demult ((mC as Const (@{const_name Algebras.divide}, _)) $ s $ t, m) =
(* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ? Note that
if we choose to do so here, the simpset used by arith must be able to
@@ -170,9 +170,9 @@
(SOME _, _) => (SOME (mC $ s $ t), m)
| (NONE, m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m)))
(* terms that evaluate to numeric constants *)
- | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m)
- | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero)
- | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m)
+ | demult (Const (@{const_name Algebras.uminus}, _) $ t, m) = demult (t, Rat.neg m)
+ | demult (Const (@{const_name Algebras.zero}, _), m) = (NONE, Rat.zero)
+ | demult (Const (@{const_name Algebras.one}, _), m) = (NONE, m)
(*Warning: in rare cases number_of encloses a non-numeral,
in which case dest_numeral raises TERM; hence all the handles below.
Same for Suc-terms that turn out not to be numerals -
@@ -196,23 +196,23 @@
(* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
summands and associated multiplicities, plus a constant 'i' (with implicit
multiplicity 1) *)
- fun poly (Const (@{const_name HOL.plus}, _) $ s $ t,
+ fun poly (Const (@{const_name Algebras.plus}, _) $ s $ t,
m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
- | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) =
+ | poly (all as Const (@{const_name Algebras.minus}, T) $ s $ t, m, pi) =
if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
- | poly (all as Const (@{const_name HOL.uminus}, T) $ t, m, pi) =
+ | poly (all as Const (@{const_name Algebras.uminus}, T) $ t, m, pi) =
if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
- | poly (Const (@{const_name HOL.zero}, _), _, pi) =
+ | poly (Const (@{const_name Algebras.zero}, _), _, pi) =
pi
- | poly (Const (@{const_name HOL.one}, _), m, (p, i)) =
+ | poly (Const (@{const_name Algebras.one}, _), m, (p, i)) =
(p, Rat.add i m)
| poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
poly (t, m, (p, Rat.add i m))
- | poly (all as Const (@{const_name HOL.times}, _) $ _ $ _, m, pi as (p, i)) =
+ | poly (all as Const (@{const_name Algebras.times}, _) $ _ $ _, m, pi as (p, i)) =
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) =
+ | poly (all as Const (@{const_name Algebras.divide}, _) $ _ $ _, m, pi as (p, i)) =
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
@@ -229,8 +229,8 @@
val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
in
case rel of
- @{const_name HOL.less} => SOME (p, i, "<", q, j)
- | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j)
+ @{const_name Algebras.less} => SOME (p, i, "<", q, j)
+ | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j)
| "op =" => SOME (p, i, "=", q, j)
| _ => NONE
end handle Rat.DIVZERO => NONE;
@@ -292,11 +292,11 @@
case head_of lhs of
Const (a, _) => member (op =) [@{const_name Orderings.max},
@{const_name Orderings.min},
- @{const_name HOL.abs},
- @{const_name HOL.minus},
- "Int.nat",
- "Divides.div_class.mod",
- "Divides.div_class.div"] a
+ @{const_name Algebras.abs},
+ @{const_name Algebras.minus},
+ "Int.nat" (*DYNAMIC BINDING!*),
+ "Divides.div_class.mod" (*DYNAMIC BINDING!*),
+ "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
| _ => (warning ("Lin. Arith.: wrong format for split rule " ^
Display.string_of_thm_without_context thm);
false))
@@ -372,7 +372,7 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const (@{const_name HOL.less_eq},
+ val t1_leq_t2 = Const (@{const_name Algebras.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -387,7 +387,7 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const (@{const_name HOL.less_eq},
+ val t1_leq_t2 = Const (@{const_name Algebras.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -397,16 +397,16 @@
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
(* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
- | (Const (@{const_name HOL.abs}, _), [t1]) =>
+ | (Const (@{const_name Algebras.abs}, _), [t1]) =>
let
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
- val terms2 = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
+ val terms2 = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
split_type --> split_type) $ t1)]) rev_terms
- val zero = Const (@{const_name HOL.zero}, split_type)
- val zero_leq_t1 = Const (@{const_name HOL.less_eq},
+ val zero = Const (@{const_name Algebras.zero}, split_type)
+ val zero_leq_t1 = Const (@{const_name Algebras.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ t1
- val t1_lt_zero = Const (@{const_name HOL.less},
+ val t1_lt_zero = Const (@{const_name Algebras.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
@@ -415,22 +415,22 @@
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
(* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
- | (Const (@{const_name HOL.minus}, _), [t1, t2]) =>
+ | (Const (@{const_name Algebras.minus}, _), [t1, t2]) =>
let
(* "d" in the above theorem becomes a new bound variable after NNF *)
(* transformation, therefore some adjustment of indices is necessary *)
val rev_terms = rev terms
- val zero = Const (@{const_name HOL.zero}, split_type)
+ val zero = Const (@{const_name Algebras.zero}, split_type)
val d = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)])
(map (incr_boundvars 1) rev_terms)
val t1' = incr_boundvars 1 t1
val t2' = incr_boundvars 1 t2
- val t1_lt_t2 = Const (@{const_name HOL.less},
+ val t1_lt_t2 = Const (@{const_name Algebras.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const (@{const_name HOL.plus},
+ (Const (@{const_name Algebras.plus},
split_type --> split_type --> split_type) $ t2' $ d)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
@@ -442,8 +442,8 @@
| (Const ("Int.nat", _), [t1]) =>
let
val rev_terms = rev terms
- val zero_int = Const (@{const_name HOL.zero}, HOLogic.intT)
- val zero_nat = Const (@{const_name HOL.zero}, HOLogic.natT)
+ val zero_int = Const (@{const_name Algebras.zero}, HOLogic.intT)
+ val zero_nat = Const (@{const_name Algebras.zero}, HOLogic.natT)
val n = Bound 0
val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)])
(map (incr_boundvars 1) rev_terms)
@@ -451,7 +451,7 @@
val t1' = incr_boundvars 1 t1
val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
- val t1_lt_zero = Const (@{const_name HOL.less},
+ val t1_lt_zero = Const (@{const_name Algebras.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
@@ -465,7 +465,7 @@
| (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const (@{const_name HOL.zero}, split_type)
+ val zero = Const (@{const_name Algebras.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -477,11 +477,11 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const (@{const_name HOL.less},
+ val j_lt_t2 = Const (@{const_name Algebras.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name HOL.times},
+ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Algebras.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -497,7 +497,7 @@
| (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const (@{const_name HOL.zero}, split_type)
+ val zero = Const (@{const_name Algebras.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
@@ -509,11 +509,11 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const (@{const_name HOL.less},
+ val j_lt_t2 = Const (@{const_name Algebras.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name HOL.times},
+ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Algebras.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -535,7 +535,7 @@
Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const (@{const_name HOL.zero}, split_type)
+ val zero = Const (@{const_name Algebras.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -545,21 +545,21 @@
val t2' = incr_boundvars 2 t2
val t2_eq_zero = Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val zero_lt_t2 = Const (@{const_name HOL.less},
+ val zero_lt_t2 = Const (@{const_name Algebras.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
- val t2_lt_zero = Const (@{const_name HOL.less},
+ val t2_lt_zero = Const (@{const_name Algebras.less},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
- val zero_leq_j = Const (@{const_name HOL.less_eq},
+ val zero_leq_j = Const (@{const_name Algebras.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_leq_zero = Const (@{const_name HOL.less_eq},
+ val j_leq_zero = Const (@{const_name Algebras.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
- val j_lt_t2 = Const (@{const_name HOL.less},
+ val j_lt_t2 = Const (@{const_name Algebras.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t2_lt_j = Const (@{const_name HOL.less},
+ val t2_lt_j = Const (@{const_name Algebras.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name HOL.times},
+ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Algebras.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -589,7 +589,7 @@
Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
- val zero = Const (@{const_name HOL.zero}, split_type)
+ val zero = Const (@{const_name Algebras.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
@@ -599,21 +599,21 @@
val t2' = incr_boundvars 2 t2
val t2_eq_zero = Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val zero_lt_t2 = Const (@{const_name HOL.less},
+ val zero_lt_t2 = Const (@{const_name Algebras.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
- val t2_lt_zero = Const (@{const_name HOL.less},
+ val t2_lt_zero = Const (@{const_name Algebras.less},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
- val zero_leq_j = Const (@{const_name HOL.less_eq},
+ val zero_leq_j = Const (@{const_name Algebras.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_leq_zero = Const (@{const_name HOL.less_eq},
+ val j_leq_zero = Const (@{const_name Algebras.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
- val j_lt_t2 = Const (@{const_name HOL.less},
+ val j_lt_t2 = Const (@{const_name Algebras.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t2_lt_j = Const (@{const_name HOL.less},
+ val t2_lt_j = Const (@{const_name Algebras.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
- (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name HOL.times},
+ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Algebras.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
--- a/src/HOL/Tools/meson.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/meson.ML Sun Jan 31 15:22:40 2010 +0100
@@ -403,7 +403,7 @@
(fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
(*A higher-order instance of a first-order constant? Example is the definition of
- HOL.one, 1, at a function type in theory SetsAndFunctions.*)
+ one, 1, at a function type in theory SetsAndFunctions.*)
fun higher_inst_const thy (c,T) =
case binder_types T of
[] => false (*not a function type, OK*)
--- a/src/HOL/Tools/nat_arith.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML Sun Jan 31 15:22:40 2010 +0100
@@ -19,8 +19,8 @@
(** abstract syntax of structure nat: 0, Suc, + **)
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
+val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
+val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
fun mk_sum [] = HOLogic.zero
| mk_sum [t] = t
@@ -69,24 +69,24 @@
structure LessCancelSums = CancelSumsFun
(struct
open CommonCancelSums;
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
end);
structure LeCancelSums = CancelSumsFun
(struct
open CommonCancelSums;
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
end);
structure DiffCancelSums = CancelSumsFun
(struct
open CommonCancelSums;
- val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
- val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus};
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
end);
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sun Jan 31 15:22:40 2010 +0100
@@ -32,7 +32,7 @@
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
val zero = mk_number 0;
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
fun mk_sum [] = zero
@@ -43,7 +43,7 @@
fun long_mk_sum [] = HOLogic.zero
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
+val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
(** Other simproc items **)
@@ -61,14 +61,14 @@
(*** CancelNumerals simprocs ***)
val one = mk_number 1;
-val mk_times = HOLogic.mk_binop @{const_name HOL.times};
+val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
fun mk_prod [] = one
| mk_prod [t] = t
| mk_prod (t :: ts) = if t = one then mk_prod ts
else mk_times (t, mk_prod ts);
-val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
+val dest_times = HOLogic.dest_bin @{const_name Algebras.times} HOLogic.natT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -176,8 +176,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
val bal_add1 = @{thm nat_less_add_iff1} RS trans
val bal_add2 = @{thm nat_less_add_iff2} RS trans
);
@@ -185,8 +185,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
val bal_add1 = @{thm nat_le_add_iff1} RS trans
val bal_add2 = @{thm nat_le_add_iff2} RS trans
);
@@ -194,8 +194,8 @@
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name HOL.minus}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
+ val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT
val bal_add1 = @{thm nat_diff_add_eq1} RS trans
val bal_add2 = @{thm nat_diff_add_eq2} RS trans
);
@@ -308,8 +308,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
val cancel = @{thm nat_mult_less_cancel1} RS trans
val neg_exchanges = true
)
@@ -317,8 +317,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
val cancel = @{thm nat_mult_le_cancel1} RS trans
val neg_exchanges = true
)
@@ -387,16 +387,16 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
);
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
);
--- a/src/HOL/Tools/numeral_simprocs.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Sun Jan 31 15:22:40 2010 +0100
@@ -34,12 +34,12 @@
val long_mk_sum = Arith_Data.long_mk_sum;
val dest_sum = Arith_Data.dest_sum;
-val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
-val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
+val mk_diff = HOLogic.mk_binop @{const_name Algebras.minus};
+val dest_diff = HOLogic.dest_bin @{const_name Algebras.minus} Term.dummyT;
-val mk_times = HOLogic.mk_binop @{const_name HOL.times};
+val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
-fun one_of T = Const(@{const_name HOL.one},T);
+fun one_of T = Const(@{const_name Algebras.one}, T);
(* build product with trailing 1 rather than Numeral 1 in order to avoid the
unnecessary restriction to type class number_ring
@@ -56,7 +56,7 @@
fun long_mk_prod T [] = one_of T
| long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
-val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name Algebras.times} Term.dummyT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -72,7 +72,7 @@
fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort TermOrd.term_ord (dest_prod t)
val (n, ts') = find_first_numeral [] ts
@@ -96,7 +96,7 @@
Fractions are reduced later by the cancel_numeral_factor simproc.*)
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
-val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
(*Build term (p / q) * t*)
fun mk_fcoeff ((p, q), t) =
@@ -104,8 +104,8 @@
in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
(*Express t as a product of a fraction with other sorted terms*)
-fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
- | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
+fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
+ | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) =
let val (p, t') = dest_coeff sign t
val (q, u') = dest_coeff 1 u
in (mk_frac (p, q), mk_divide (t', u')) end
@@ -230,8 +230,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
val bal_add1 = @{thm less_add_iff1} RS trans
val bal_add2 = @{thm less_add_iff2} RS trans
);
@@ -239,8 +239,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
val bal_add1 = @{thm le_add_iff1} RS trans
val bal_add2 = @{thm le_add_iff2} RS trans
);
@@ -392,8 +392,8 @@
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
val cancel = @{thm mult_divide_mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -410,8 +410,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
val cancel = @{thm mult_less_cancel_left} RS trans
val neg_exchanges = true
)
@@ -419,8 +419,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
val cancel = @{thm mult_le_cancel_left} RS trans
val neg_exchanges = true
)
@@ -485,8 +485,8 @@
in
fun sign_conv pos_th neg_th ss t =
let val T = fastype_of t;
- val zero = Const(@{const_name HOL.zero}, T);
- val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
+ val zero = Const(@{const_name Algebras.zero}, T);
+ val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
fun prove p =
Option.map Eq_True_elim (Lin_Arith.simproc ss p)
@@ -525,8 +525,8 @@
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
val simp_conv = sign_conv
@{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
);
@@ -535,8 +535,8 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
val simp_conv = sign_conv
@{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
);
@@ -571,8 +571,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
--- a/src/HOL/Tools/refute.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/refute.ML Sun Jan 31 15:22:40 2010 +0100
@@ -708,13 +708,13 @@
(* other optimizations *)
| Const (@{const_name Finite_Set.card}, _) => t
| Const (@{const_name Finite_Set.finite}, _) => t
- | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
- | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
| Const (@{const_name List.append}, _) => t
| Const (@{const_name lfp}, _) => t
@@ -883,16 +883,16 @@
| Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
| Const (@{const_name Finite_Set.finite}, T) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
| Const (@{const_name List.append}, T) => collect_type_axioms T axs
@@ -2765,13 +2765,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.less' could in principle be interpreted with *)
+ (* only an optimization: 'less' could in principle be interpreted with *)
(* interpreters available already (using its definition), but the code *)
(* below is more efficient *)
fun Nat_less_interpreter thy model args t =
case t of
- Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2788,13 +2788,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.plus' could in principle be interpreted with *)
+ (* only an optimization: 'plus' could in principle be interpreted with *)
(* interpreters available already (using its definition), but the code *)
(* below is more efficient *)
fun Nat_plus_interpreter thy model args t =
case t of
- Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2819,13 +2819,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.minus' could in principle be interpreted *)
+ (* only an optimization: 'minus' could in principle be interpreted *)
(* with interpreters available already (using its definition), but the *)
(* code below is more efficient *)
fun Nat_minus_interpreter thy model args t =
case t of
- Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2847,13 +2847,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.times' could in principle be interpreted *)
+ (* only an optimization: 'times' could in principle be interpreted *)
(* with interpreters available already (using its definition), but the *)
(* code below is more efficient *)
fun Nat_times_interpreter thy model args t =
case t of
- Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
--- a/src/HOL/Tools/res_clause.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Tools/res_clause.ML Sun Jan 31 15:22:40 2010 +0100
@@ -99,7 +99,7 @@
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
Symtab.make [(@{const_name "op ="}, "equal"),
- (@{const_name HOL.less_eq}, "lessequals"),
+ (@{const_name Algebras.less_eq}, "lessequals"),
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
(@{const_name "op -->"}, "implies"),
--- a/src/HOL/Transcendental.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/Transcendental.thy Sun Jan 31 15:22:40 2010 +0100
@@ -36,7 +36,7 @@
apply (subst setsum_op_ivl_Suc)
apply (subst lemma_realpow_diff_sumr)
apply (simp add: right_distrib del: setsum_op_ivl_Suc)
-apply (subst mult_left_commute [where a="x - y"])
+apply (subst mult_left_commute [of "x - y"])
apply (erule subst)
apply (simp add: algebra_simps)
done
--- a/src/HOL/ex/Arith_Examples.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy Sun Jan 31 15:22:40 2010 +0100
@@ -33,7 +33,7 @@
*)
subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
- @{term HOL.minus}, @{term nat}, @{term Divides.mod},
+ @{term Algebras.minus}, @{term nat}, @{term Divides.mod},
@{term Divides.div} *}
lemma "(i::nat) <= max i j"
--- a/src/HOL/ex/Binary.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/ex/Binary.thy Sun Jan 31 15:22:40 2010 +0100
@@ -27,8 +27,8 @@
| dest_bit (Const (@{const_name True}, _)) = 1
| dest_bit t = raise TERM ("dest_bit", [t]);
- fun dest_binary (Const (@{const_name HOL.zero}, Type (@{type_name nat}, _))) = 0
- | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1
+ fun dest_binary (Const (@{const_name Algebras.zero}, Type (@{type_name nat}, _))) = 0
+ | dest_binary (Const (@{const_name Algebras.one}, Type (@{type_name nat}, _))) = 1
| dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
| dest_binary t = raise TERM ("dest_binary", [t]);
--- a/src/HOL/ex/SVC_Oracle.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Sun Jan 31 15:22:40 2010 +0100
@@ -63,21 +63,21 @@
(*abstraction of a numeric literal*)
fun lit t = if can HOLogic.dest_number t then t else replace t;
(*abstraction of a real/rational expression*)
- fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
+ fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
| rat t = lit t
(*abstraction of an integer expression: no div, mod*)
- fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
+ fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (int x)
| int t = lit t
(*abstraction of a natural number expression: no minus*)
- fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
- | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+ fun nat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+ | nat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
| nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
| nat t = lit t
(*abstraction of a relation: =, <, <=*)
@@ -95,8 +95,8 @@
| fm ((c as Const("True", _))) = c
| fm ((c as Const("False", _))) = c
| fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Algebras.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
--- a/src/HOL/ex/svc_funcs.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML Sun Jan 31 15:22:40 2010 +0100
@@ -107,8 +107,8 @@
b1 orelse b2)
end
else (*might be numeric equality*) (t, is_intnat T)
- | Const(@{const_name HOL.less}, Type ("fun", [T,_])) => (t, is_intnat T)
- | Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name Algebras.less}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
| _ => (t, false)
end
in #1 o tag end;
@@ -146,16 +146,16 @@
(*translation of a literal*)
val lit = snd o HOLogic.dest_number;
(*translation of a literal expression [no variables]*)
- fun litExp (Const(@{const_name HOL.plus}, T) $ x $ y) =
+ fun litExp (Const(@{const_name Algebras.plus}, T) $ x $ y) =
if is_numeric_op T then (litExp x) + (litExp y)
else fail t
- | litExp (Const(@{const_name HOL.minus}, T) $ x $ y) =
+ | litExp (Const(@{const_name Algebras.minus}, T) $ x $ y) =
if is_numeric_op T then (litExp x) - (litExp y)
else fail t
- | litExp (Const(@{const_name HOL.times}, T) $ x $ y) =
+ | litExp (Const(@{const_name Algebras.times}, T) $ x $ y) =
if is_numeric_op T then (litExp x) * (litExp y)
else fail t
- | litExp (Const(@{const_name HOL.uminus}, T) $ x) =
+ | litExp (Const(@{const_name Algebras.uminus}, T) $ x) =
if is_numeric_op T then ~(litExp x)
else fail t
| litExp t = lit t
@@ -163,21 +163,21 @@
(*translation of a real/rational expression*)
fun suc t = Interp("+", [Int 1, t])
fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x)
- | tm (Const(@{const_name HOL.plus}, T) $ x $ y) =
+ | tm (Const(@{const_name Algebras.plus}, T) $ x $ y) =
if is_numeric_op T then Interp("+", [tm x, tm y])
else fail t
- | tm (Const(@{const_name HOL.minus}, T) $ x $ y) =
+ | tm (Const(@{const_name Algebras.minus}, T) $ x $ y) =
if is_numeric_op T then
Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
else fail t
- | tm (Const(@{const_name HOL.times}, T) $ x $ y) =
+ | tm (Const(@{const_name Algebras.times}, T) $ x $ y) =
if is_numeric_op T then Interp("*", [tm x, tm y])
else fail t
- | tm (Const(@{const_name HOL.inverse}, T) $ x) =
+ | tm (Const(@{const_name Algebras.inverse}, T) $ x) =
if domain_type T = HOLogic.realT then
Rat(1, litExp x)
else fail t
- | tm (Const(@{const_name HOL.uminus}, T) $ x) =
+ | tm (Const(@{const_name Algebras.uminus}, T) $ x) =
if is_numeric_op T then Interp("*", [Int ~1, tm x])
else fail t
| tm t = Int (lit t)
@@ -211,13 +211,13 @@
else fail t
end
(*inequalities: possible types are nat, int, real*)
- | fm pos (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name Algebras.less}, Type ("fun", [T,_])) $ x $ y) =
if not pos orelse T = HOLogic.realT then
Buildin("<", [tm x, tm y])
else if is_intnat T then
Buildin("<=", [suc (tm x), tm y])
else fail t
- | fm pos (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ x $ y) =
if pos orelse T = HOLogic.realT then
Buildin("<=", [tm x, tm y])
else if is_intnat T then
--- a/src/HOLCF/ConvexPD.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy Sun Jan 31 15:22:40 2010 +0100
@@ -279,29 +279,28 @@
"approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
-lemma convex_plus_assoc:
- "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
-apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
-apply (rule_tac x=zs in convex_pd.principal_induct, simp)
-apply (simp add: PDPlus_assoc)
-done
-
-lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
-apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
+interpretation convex_add!: semilattice convex_add proof
+ fix xs ys zs :: "'a convex_pd"
+ show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
+ apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
+ apply (rule_tac x=zs in convex_pd.principal_induct, simp)
+ apply (simp add: PDPlus_assoc)
+ done
+ show "xs +\<natural> ys = ys +\<natural> xs"
+ apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
+ apply (simp add: PDPlus_commute)
+ done
+ show "xs +\<natural> xs = xs"
+ apply (induct xs rule: convex_pd.principal_induct, simp)
+ apply (simp add: PDPlus_absorb)
+ done
+qed
-lemma convex_plus_absorb [simp]: "xs +\<natural> xs = xs"
-apply (induct xs rule: convex_pd.principal_induct, simp)
-apply (simp add: PDPlus_absorb)
-done
-
-lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
-by (rule mk_left_commute
- [of "op +\<natural>", OF convex_plus_assoc convex_plus_commute])
-
-lemma convex_plus_left_absorb [simp]: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
-by (simp only: convex_plus_assoc [symmetric] convex_plus_absorb)
+lemmas convex_plus_assoc = convex_add.assoc
+lemmas convex_plus_commute = convex_add.commute
+lemmas convex_plus_absorb = convex_add.idem
+lemmas convex_plus_left_commute = convex_add.left_commute
+lemmas convex_plus_left_absorb = convex_add.left_idem
text {* Useful for @{text "simp add: convex_plus_ac"} *}
lemmas convex_plus_ac =
--- a/src/HOLCF/LowerPD.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Sun Jan 31 15:22:40 2010 +0100
@@ -234,27 +234,28 @@
"approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
-lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
-apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
-apply (rule_tac x=zs in lower_pd.principal_induct, simp)
-apply (simp add: PDPlus_assoc)
-done
-
-lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
-apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
+interpretation lower_add!: semilattice lower_add proof
+ fix xs ys zs :: "'a lower_pd"
+ show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
+ apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
+ apply (rule_tac x=zs in lower_pd.principal_induct, simp)
+ apply (simp add: PDPlus_assoc)
+ done
+ show "xs +\<flat> ys = ys +\<flat> xs"
+ apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
+ apply (simp add: PDPlus_commute)
+ done
+ show "xs +\<flat> xs = xs"
+ apply (induct xs rule: lower_pd.principal_induct, simp)
+ apply (simp add: PDPlus_absorb)
+ done
+qed
-lemma lower_plus_absorb [simp]: "xs +\<flat> xs = xs"
-apply (induct xs rule: lower_pd.principal_induct, simp)
-apply (simp add: PDPlus_absorb)
-done
-
-lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
-by (rule mk_left_commute [of "op +\<flat>", OF lower_plus_assoc lower_plus_commute])
-
-lemma lower_plus_left_absorb [simp]: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
-by (simp only: lower_plus_assoc [symmetric] lower_plus_absorb)
+lemmas lower_plus_assoc = lower_add.assoc
+lemmas lower_plus_commute = lower_add.commute
+lemmas lower_plus_absorb = lower_add.idem
+lemmas lower_plus_left_commute = lower_add.left_commute
+lemmas lower_plus_left_absorb = lower_add.left_idem
text {* Useful for @{text "simp add: lower_plus_ac"} *}
lemmas lower_plus_ac =
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Jan 31 15:22:40 2010 +0100
@@ -719,7 +719,7 @@
val take_stricts' = rewrite_rule copy_take_defs take_stricts;
fun take_0 n dn =
let
- val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
+ val goal = mk_trp ((dc_take dn $ %%: @{const_name Algebras.zero}) `% x_name n === UU);
in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
val take_0s = mapn take_0 1 dnames;
fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
--- a/src/HOLCF/UpperPD.thy Sat Jan 30 17:03:46 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Sun Jan 31 15:22:40 2010 +0100
@@ -232,27 +232,28 @@
"approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
-lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
-apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
-apply (rule_tac x=zs in upper_pd.principal_induct, simp)
-apply (simp add: PDPlus_assoc)
-done
-
-lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
-apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
+interpretation upper_add!: semilattice upper_add proof
+ fix xs ys zs :: "'a upper_pd"
+ show "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
+ apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
+ apply (rule_tac x=zs in upper_pd.principal_induct, simp)
+ apply (simp add: PDPlus_assoc)
+ done
+ show "xs +\<sharp> ys = ys +\<sharp> xs"
+ apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
+ apply (simp add: PDPlus_commute)
+ done
+ show "xs +\<sharp> xs = xs"
+ apply (induct xs rule: upper_pd.principal_induct, simp)
+ apply (simp add: PDPlus_absorb)
+ done
+qed
-lemma upper_plus_absorb [simp]: "xs +\<sharp> xs = xs"
-apply (induct xs rule: upper_pd.principal_induct, simp)
-apply (simp add: PDPlus_absorb)
-done
-
-lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
-by (rule mk_left_commute [of "op +\<sharp>", OF upper_plus_assoc upper_plus_commute])
-
-lemma upper_plus_left_absorb [simp]: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
-by (simp only: upper_plus_assoc [symmetric] upper_plus_absorb)
+lemmas upper_plus_assoc = upper_add.assoc
+lemmas upper_plus_commute = upper_add.commute
+lemmas upper_plus_absorb = upper_add.idem
+lemmas upper_plus_left_commute = upper_add.left_commute
+lemmas upper_plus_left_absorb = upper_add.left_idem
text {* Useful for @{text "simp add: upper_plus_ac"} *}
lemmas upper_plus_ac =
--- a/src/Provers/Arith/abel_cancel.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/Provers/Arith/abel_cancel.ML Sun Jan 31 15:22:40 2010 +0100
@@ -28,29 +28,29 @@
(* FIXME dependent on abstract syntax *)
-fun zero t = Const (@{const_name HOL.zero}, t);
-fun minus t = Const (@{const_name HOL.uminus}, t --> t);
+fun zero t = Const (@{const_name Algebras.zero}, t);
+fun minus t = Const (@{const_name Algebras.uminus}, t --> t);
-fun add_terms pos (Const (@{const_name HOL.plus}, _) $ x $ y, ts) =
+fun add_terms pos (Const (@{const_name Algebras.plus}, _) $ x $ y, ts) =
add_terms pos (x, add_terms pos (y, ts))
- | add_terms pos (Const (@{const_name HOL.minus}, _) $ x $ y, ts) =
+ | add_terms pos (Const (@{const_name Algebras.minus}, _) $ x $ y, ts) =
add_terms pos (x, add_terms (not pos) (y, ts))
- | add_terms pos (Const (@{const_name HOL.uminus}, _) $ x, ts) =
+ | add_terms pos (Const (@{const_name Algebras.uminus}, _) $ x, ts) =
add_terms (not pos) (x, ts)
| add_terms pos (x, ts) = (pos,x) :: ts;
fun terms fml = add_terms true (fml, []);
-fun zero1 pt (u as (c as Const(@{const_name HOL.plus},_)) $ x $ y) =
+fun zero1 pt (u as (c as Const(@{const_name Algebras.plus},_)) $ x $ y) =
(case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
| SOME z => SOME(c $ x $ z))
| SOME z => SOME(c $ z $ y))
- | zero1 (pos,t) (u as (c as Const(@{const_name HOL.minus},_)) $ x $ y) =
+ | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.minus},_)) $ x $ y) =
(case zero1 (pos,t) x of
NONE => (case zero1 (not pos,t) y of NONE => NONE
| SOME z => SOME(c $ x $ z))
| SOME z => SOME(c $ z $ y))
- | zero1 (pos,t) (u as (c as Const(@{const_name HOL.uminus},_)) $ x) =
+ | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.uminus},_)) $ x) =
(case zero1 (not pos,t) x of NONE => NONE
| SOME z => SOME(c $ z))
| zero1 (pos,t) u =
@@ -71,7 +71,7 @@
fun cancel t =
let
val c $ lhs $ rhs = t
- val opp = case c of Const(@{const_name HOL.plus},_) => true | _ => false;
+ val opp = case c of Const(@{const_name Algebras.plus},_) => true | _ => false;
val (pos,l) = find_common opp (terms lhs) (terms rhs)
val posr = if opp then not pos else pos
val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
--- a/src/Provers/Arith/cancel_div_mod.ML Sat Jan 30 17:03:46 2010 +0100
+++ b/src/Provers/Arith/cancel_div_mod.ML Sun Jan 31 15:22:40 2010 +0100
@@ -1,5 +1,4 @@
(* Title: Provers/Arith/cancel_div_mod.ML
- ID: $Id$
Author: Tobias Nipkow, TU Muenchen
Cancel div and mod terms:
@@ -7,7 +6,7 @@
A + n*(m div n) + B + (m mod n) + C == A + B + C + m
FIXME: Is parameterized but assumes for simplicity that + and * are named
-HOL.plus and HOL.minus
+as in HOL
*)
signature CANCEL_DIV_MOD_DATA =
@@ -35,12 +34,12 @@
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
struct
-fun coll_div_mod (Const(@{const_name HOL.plus},_) $ s $ t) dms =
+fun coll_div_mod (Const(@{const_name Algebras.plus},_) $ s $ t) dms =
coll_div_mod t (coll_div_mod s dms)
- | coll_div_mod (Const(@{const_name HOL.times},_) $ m $ (Const(d,_) $ s $ n))
+ | coll_div_mod (Const(@{const_name Algebras.times},_) $ m $ (Const(d,_) $ s $ n))
(dms as (divs,mods)) =
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
- | coll_div_mod (Const(@{const_name HOL.times},_) $ (Const(d,_) $ s $ n) $ m)
+ | coll_div_mod (Const(@{const_name Algebras.times},_) $ (Const(d,_) $ s $ n) $ m)
(dms as (divs,mods)) =
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
| coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
@@ -56,8 +55,8 @@
==> thesis by transitivity
*)
-val mk_plus = Data.mk_binop @{const_name HOL.plus};
-val mk_times = Data.mk_binop @{const_name HOL.times};
+val mk_plus = Data.mk_binop @{const_name Algebras.plus};
+val mk_times = Data.mk_binop @{const_name Algebras.times};
fun rearrange t pq =
let val ts = Data.dest_sum t;