--- a/NEWS Thu Jan 28 11:48:43 2010 +0100
+++ b/NEWS Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Jan 28 11:48:49 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/Groebner_Basis.thy Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Groebner_Basis.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/HOL.thy Thu Jan 28 11:48:49 2010 +0100
@@ -1625,118 +1625,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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/prim_rec.imp Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/real.imp Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/realax.imp Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOLLight/HOLLight.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/IsaMakefile Thu Jan 28 11:48:49 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/Mutabelle/Mutabelle.thy Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Mutabelle/Mutabelle.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/NSA/NSA.thy Thu Jan 28 11:48:49 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/Orderings.thy Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Orderings.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/Func.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/HOHH.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/Test.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Prolog/Type.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Set.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/hologic.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/inductive.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/int_arith.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/meson.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/refute.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/res_clause.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Transcendental.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/Binary.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML Thu Jan 28 11:48:49 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/Tools/Domain/domain_theorems.ML Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jan 28 11:48:49 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/Provers/Arith/abel_cancel.ML Thu Jan 28 11:48:43 2010 +0100
+++ b/src/Provers/Arith/abel_cancel.ML Thu Jan 28 11:48:49 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 Thu Jan 28 11:48:43 2010 +0100
+++ b/src/Provers/Arith/cancel_div_mod.ML Thu Jan 28 11:48:49 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;