--- a/NEWS Sun Feb 21 23:05:37 2010 +0100
+++ b/NEWS Mon Feb 22 09:17:49 2010 +0100
@@ -52,6 +52,12 @@
*** HOL ***
+* Multisets: changed orderings:
+ * pointwise ordering is instance of class order with standard syntax <= and <;
+ * multiset ordering has syntax <=# and <#; partial order properties are provided
+ by means of interpretation with prefix multiset_order.
+INCOMPATIBILITY.
+
* New set of rules "ac_simps" provides combined assoc / commute rewrites
for all interpretations of the appropriate generic locales.
@@ -63,7 +69,7 @@
* Some generic constants have been put to appropriate theories:
less_eq, less: Orderings
- abs, sgn: Groups
+ zero, one, plus, minus, uminus, times, abs, sgn: Groups
inverse, divide: Rings
INCOMPATIBILITY.
@@ -123,8 +129,7 @@
INCOMPATIBILITY.
* New theory Algebras contains generic algebraic structures and
-generic algebraic operations. INCOMPATIBILTY: constants zero, one,
-plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy.
+generic algebraic operations.
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.
@@ -133,10 +138,11 @@
replaced by new-style primrec, especially in theory List. The corresponding
constants now have authentic syntax. INCOMPATIBILITY.
-* Reorganized theory Multiset: less duplication, less historical
-organization of sections, conversion from associations lists to
-multisets, rudimentary code generation. Use insert_DiffM2 [symmetric]
-instead of elem_imp_eq_diff_union, if needed. INCOMPATIBILITY.
+* Reorganized theory Multiset: swapped notation of pointwise and multiset
+order; less duplication, less historical organization of sections,
+conversion from associations lists to multisets, rudimentary code generation.
+Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
+INCOMPATIBILITY.
* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax.
INCOMPATIBILITY.
--- a/src/HOL/Algebra/Divisibility.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Mon Feb 22 09:17:49 2010 +0100
@@ -2250,7 +2250,7 @@
assumes ab: "a divides b"
and afs: "wfactors G as a" and bfs: "wfactors G bs b"
and carr: "a \<in> carrier G" "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G"
- shows "fmset G as \<le># fmset G bs"
+ shows "fmset G as \<le> fmset G bs"
using ab
proof (elim dividesE)
fix c
@@ -2270,7 +2270,7 @@
qed
lemma (in comm_monoid_cancel) fmsubset_divides:
- assumes msubset: "fmset G as \<le># fmset G bs"
+ assumes msubset: "fmset G as \<le> fmset G bs"
and afs: "wfactors G as a" and bfs: "wfactors G bs b"
and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
@@ -2323,7 +2323,7 @@
assumes "wfactors G as a" and "wfactors G bs b"
and "a \<in> carrier G" and "b \<in> carrier G"
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
- shows "a divides b = (fmset G as \<le># fmset G bs)"
+ shows "a divides b = (fmset G as \<le> fmset G bs)"
using assms
by (blast intro: divides_fmsubset fmsubset_divides)
@@ -2331,7 +2331,7 @@
text {* Proper factors on multisets *}
lemma (in factorial_monoid) fmset_properfactor:
- assumes asubb: "fmset G as \<le># fmset G bs"
+ assumes asubb: "fmset G as \<le> fmset G bs"
and anb: "fmset G as \<noteq> fmset G bs"
and "wfactors G as a" and "wfactors G bs b"
and "a \<in> carrier G" and "b \<in> carrier G"
@@ -2341,10 +2341,10 @@
apply (rule fmsubset_divides[of as bs], fact+)
proof
assume "b divides a"
- hence "fmset G bs \<le># fmset G as"
+ hence "fmset G bs \<le> fmset G as"
by (rule divides_fmsubset) fact+
with asubb
- have "fmset G as = fmset G bs" by (simp add: mset_le_antisym)
+ have "fmset G as = fmset G bs" by (rule order_antisym)
with anb
show "False" ..
qed
@@ -2354,7 +2354,7 @@
and "wfactors G as a" and "wfactors G bs b"
and "a \<in> carrier G" and "b \<in> carrier G"
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
- shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
+ shows "fmset G as \<le> fmset G bs \<and> fmset G as \<noteq> fmset G bs"
using pf
apply (elim properfactorE)
apply rule
@@ -2738,12 +2738,12 @@
have "c gcdof a b"
proof (simp add: isgcd_def, safe)
from csmset
- have "fmset G cs \<le># fmset G as"
+ have "fmset G cs \<le> fmset G as"
by (simp add: multiset_inter_def mset_le_def)
thus "c divides a" by (rule fmsubset_divides) fact+
next
from csmset
- have "fmset G cs \<le># fmset G bs"
+ have "fmset G cs \<le> fmset G bs"
by (simp add: multiset_inter_def mset_le_def, force)
thus "c divides b" by (rule fmsubset_divides) fact+
next
@@ -2756,13 +2756,13 @@
by auto
assume "y divides a"
- hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+
+ hence ya: "fmset G ys \<le> fmset G as" by (rule divides_fmsubset) fact+
assume "y divides b"
- hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+
+ hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
from ya yb csmset
- have "fmset G ys \<le># fmset G cs" by (simp add: mset_le_def multiset_inter_count)
+ have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)
thus "y divides c" by (rule fmsubset_divides) fact+
qed
@@ -2837,10 +2837,10 @@
have "c lcmof a b"
proof (simp add: islcm_def, safe)
- from csmset have "fmset G as \<le># fmset G cs" by (simp add: mset_le_def, force)
+ from csmset have "fmset G as \<le> fmset G cs" by (simp add: mset_le_def, force)
thus "a divides c" by (rule fmsubset_divides) fact+
next
- from csmset have "fmset G bs \<le># fmset G cs" by (simp add: mset_le_def)
+ from csmset have "fmset G bs \<le> fmset G cs" by (simp add: mset_le_def)
thus "b divides c" by (rule fmsubset_divides) fact+
next
fix y
@@ -2852,13 +2852,13 @@
by auto
assume "a divides y"
- hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+
+ hence ya: "fmset G as \<le> fmset G ys" by (rule divides_fmsubset) fact+
assume "b divides y"
- hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+
+ hence yb: "fmset G bs \<le> fmset G ys" by (rule divides_fmsubset) fact+
from ya yb csmset
- have "fmset G cs \<le># fmset G ys"
+ have "fmset G cs \<le> fmset G ys"
apply (simp add: mset_le_def, clarify)
apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
apply simp
--- a/src/HOL/Algebra/abstract/Ring2.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Feb 22 09:17:49 2010 +0100
@@ -205,8 +205,8 @@
ML {*
fun ring_ord (Const (a, _)) =
find_index (fn a' => a = a')
- [@{const_name Algebras.zero}, @{const_name Algebras.plus}, @{const_name Algebras.uminus},
- @{const_name Algebras.minus}, @{const_name Algebras.one}, @{const_name Algebras.times}]
+ [@{const_name Groups.zero}, @{const_name Groups.plus}, @{const_name Groups.uminus},
+ @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}]
| ring_ord _ = ~1;
fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
--- a/src/HOL/Algebras.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Algebras.thy Mon Feb 22 09:17:49 2010 +0100
@@ -8,8 +8,6 @@
imports HOL
begin
-subsection {* Generic algebraic structures *}
-
text {*
These locales provide basic structures for interpretation into
bigger structures; extensions require careful thinking, otherwise
@@ -54,58 +52,4 @@
end
-
-subsection {* Generic syntactic operations *}
-
-class zero =
- fixes zero :: 'a ("0")
-
-class one =
- fixes one :: 'a ("1")
-
-hide (open) const zero one
-
-syntax
- "_index1" :: index ("\<^sub>1")
-translations
- (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
-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 *}
-
-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)
-
end
\ No newline at end of file
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 22 09:17:49 2010 +0100
@@ -670,13 +670,13 @@
end
fun whatis x ct = case term_of ct of
- Const(@{const_name Algebras.plus}, _)$(Const(@{const_name Algebras.times},_)$_$y)$_ =>
+ Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.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 Algebras.plus}, _)$y$_ =>
+| Const(@{const_name Groups.plus}, _)$y$_ =>
if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
else ("Nox",[])
-| Const(@{const_name Algebras.times}, _)$_$y =>
+| Const(@{const_name Groups.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 Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) =>
+ Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -727,7 +727,7 @@
| _ => reflexive ct)
-| Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
+| Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.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 Algebras.zero},_) =>
+| Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 22 09:17:49 2010 +0100
@@ -2947,10 +2947,10 @@
fun rrelT rT = [rT,rT] ---> rT;
fun rrT rT = [rT, rT] ---> bT;
fun divt rT = Const(@{const_name Rings.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 timest rT = Const(@{const_name Groups.times},rrelT rT);
+fun plust rT = Const(@{const_name Groups.plus},rrelT rT);
+fun minust rT = Const(@{const_name Groups.minus},rrelT rT);
+fun uminust rT = Const(@{const_name Groups.uminus}, rT --> rT);
fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
val brT = [bT, bT] ---> bT;
val nott = @{term "Not"};
@@ -2961,7 +2961,7 @@
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
fun lle rT = Const(@{const_name Orderings.less},rrT rT);
fun eqt rT = Const("op =",rrT rT);
-fun rz rT = Const(@{const_name Algebras.zero},rT);
+fun rz rT = Const(@{const_name Groups.zero},rT);
fun dest_nat t = case t of
Const ("Suc",_)$t' => 1 + dest_nat t'
@@ -2969,10 +2969,10 @@
fun num_of_term m t =
case t of
- Const(@{const_name Algebras.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
- | Const(@{const_name Algebras.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
- | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
- | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
+ Const(@{const_name Groups.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
+ | Const(@{const_name Groups.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
+ | Const(@{const_name Groups.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
| Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
| Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
| _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1)
@@ -2980,10 +2980,10 @@
fun tm_of_term m m' t =
case t of
- Const(@{const_name Algebras.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
- | Const(@{const_name Algebras.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
- | Const(@{const_name Algebras.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
- | Const(@{const_name Algebras.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
+ Const(@{const_name Groups.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
+ | Const(@{const_name Groups.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
+ | Const(@{const_name Groups.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
+ | Const(@{const_name Groups.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
| _ => (@{code CP} (num_of_term m' t)
handle TERM _ => @{code Bound} (AList.lookup (op aconv) m t |> the)
| Option => @{code Bound} (AList.lookup (op aconv) m t |> the));
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Feb 22 09:17:49 2010 +0100
@@ -13,8 +13,8 @@
struct
(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name Algebras.zero}, T);
-fun cring_one T = Const (@{const_name Algebras.one}, T);
+fun cring_zero T = Const (@{const_name Groups.zero}, T);
+fun cring_one T = Const (@{const_name Groups.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 Algebras.plus}, _) $ a $ b) =
+fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
polex_add T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
polex_sub T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) =
+ | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) =
polex_mul T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) =
+ | reif_polex T vs (Const (@{const_name Groups.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/Finite_Set.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Finite_Set.thy Mon Feb 22 09:17:49 2010 +0100
@@ -1055,7 +1055,7 @@
subsection {* Generalized summation over a set *}
-interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
+interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add"
proof qed (auto intro: add_assoc add_commute)
definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
--- a/src/HOL/Groups.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Groups.thy Mon Feb 22 09:17:49 2010 +0100
@@ -6,9 +6,64 @@
theory Groups
imports Orderings
-uses "~~/src/Provers/Arith/abel_cancel.ML"
+uses ("~~/src/Provers/Arith/abel_cancel.ML")
begin
+subsection {* Generic operations *}
+
+class zero =
+ fixes zero :: 'a ("0")
+
+class one =
+ fixes one :: 'a ("1")
+
+hide (open) const zero one
+
+syntax
+ "_index1" :: index ("\<^sub>1")
+translations
+ (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
+
+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 Groups.zero}, _) => true
+ | Const(@{const_name Groups.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 Groups.one}, @{const_syntax Groups.zero}] end;
+*} -- {* show types that are presumably too general *}
+
+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)
+
+use "~~/src/Provers/Arith/abel_cancel.ML"
+
text {*
The theory of partially ordered groups is taken from the books:
\begin{itemize}
@@ -1129,8 +1184,8 @@
(* term order for abelian groups *)
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
- [@{const_name Algebras.zero}, @{const_name Algebras.plus},
- @{const_name Algebras.uminus}, @{const_name Algebras.minus}]
+ [@{const_name Groups.zero}, @{const_name Groups.plus},
+ @{const_name Groups.uminus}, @{const_name Groups.minus}]
| agrp_ord _ = ~1;
fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
@@ -1139,9 +1194,9 @@
val ac1 = mk_meta_eq @{thm add_assoc};
val ac2 = mk_meta_eq @{thm add_commute};
val ac3 = mk_meta_eq @{thm add_left_commute};
- fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) =
+ fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
SOME ac1
- | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) =
+ | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
if termless_agrp (y, x) then SOME ac3 else NONE
| solve_add_ac thy _ (_ $ x $ y) =
if termless_agrp (y, x) then SOME ac2 else NONE
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Mon Feb 22 09:17:49 2010 +0100
@@ -182,9 +182,9 @@
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
"<=" > Orderings.less_eq :: "[nat,nat]=>bool"
- "+" > Algebras.plus :: "[nat,nat]=>nat"
- "*" > Algebras.times :: "[nat,nat]=>nat"
- "-" > Algebras.minus :: "[nat,nat]=>nat"
+ "+" > Groups.plus :: "[nat,nat]=>nat"
+ "*" > Groups.times :: "[nat,nat]=>nat"
+ "-" > Groups.minus :: "[nat,nat]=>nat"
MIN > Orderings.min :: "[nat,nat]=>nat"
MAX > Orderings.max :: "[nat,nat]=>nat"
DIV > Divides.div :: "[nat,nat]=>nat"
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Mon Feb 22 09:17:49 2010 +0100
@@ -16,12 +16,12 @@
real > RealDef.real;
const_maps
- 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_0 > Groups.zero :: real
+ real_1 > Groups.one :: real
+ real_neg > Groups.uminus :: "real => real"
+ inv > Groups.inverse :: "real => real"
+ real_add > Groups.plus :: "[real,real] => real"
+ real_mul > Groups.times :: "[real,real] => real"
real_lt > Orderings.less :: "[real,real] => bool";
ignore_thms
@@ -51,8 +51,8 @@
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
real_lte > Orderings.less_eq :: "[real,real] => bool"
- real_sub > Algebras.minus :: "[real,real] => real"
- "/" > Algebras.divide :: "[real,real] => real"
+ real_sub > Groups.minus :: "[real,real] => real"
+ "/" > Rings.divide :: "[real,real] => real"
pow > Power.power :: "[real,nat] => real"
abs > Groups.abs :: "real => real"
real_of_num > RealDef.real :: "nat => real";
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Feb 22 09:17:49 2010 +0100
@@ -76,9 +76,9 @@
SUC > Suc
PRE > HOLLightCompat.Pred
NUMERAL > HOL4Compat.NUMERAL
- "+" > Algebras.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- "*" > Algebras.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- "-" > Algebras.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "+" > Groups.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "*" > Groups.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "-" > Groups.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 Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Mon Feb 22 09:17:49 2010 +0100
@@ -24,9 +24,9 @@
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
"<=" > "Orderings.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"
+ "-" > "Groups.minus" :: "nat => nat => nat"
+ "+" > "Groups.plus" :: "nat => nat => nat"
+ "*" > "Groups.times" :: "nat => nat => nat"
thm_maps
"num_case_def" > "HOL4Compat.num_case_def"
--- a/src/HOL/Import/HOL/real.imp Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Import/HOL/real.imp Mon Feb 22 09:17:49 2010 +0100
@@ -10,7 +10,7 @@
const_maps
"sup" > "HOL4Real.real.sup"
"sum" > "HOL4Real.real.sum"
- "real_sub" > "Algebras.minus" :: "real => real => real"
+ "real_sub" > "Groups.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
"real_lte" > "Orderings.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
--- a/src/HOL/Import/HOL/realax.imp Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Import/HOL/realax.imp Mon Feb 22 09:17:49 2010 +0100
@@ -27,12 +27,12 @@
"treal_add" > "HOL4Real.realax.treal_add"
"treal_1" > "HOL4Real.realax.treal_1"
"treal_0" > "HOL4Real.realax.treal_0"
- "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
- "real_mul" > "Algebras.times_class.times" :: "real => real => real"
+ "real_neg" > "Groups.uminus" :: "real => real"
+ "real_mul" > "Groups.times" :: "real => real => real"
"real_lt" > "Orderings.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"
+ "real_add" > "Groups.plus" :: "real => real => real"
+ "real_1" > "Groups.one" :: "real"
+ "real_0" > "Groups.zero" :: "real"
"inv" > "Ring.inverse" :: "real => real"
"hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
--- a/src/HOL/Import/HOLLight/hollight.imp Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp Mon Feb 22 09:17:49 2010 +0100
@@ -238,10 +238,10 @@
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
"/\\" > "op &"
- "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
+ "-" > "Groups.minus" :: "nat => nat => nat"
"," > "Pair"
- "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
- "*" > "Algebras.times_class.times" :: "nat => nat => nat"
+ "+" > "Groups.plus" :: "nat => nat => nat"
+ "*" > "Groups.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
"!" > "All"
--- a/src/HOL/Library/Multiset.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Feb 22 09:17:49 2010 +0100
@@ -176,64 +176,6 @@
by (simp add: multiset_eq_conv_count_eq)
-subsubsection {* Intersection *}
-
-definition multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
- "multiset_inter A B = A - (A - B)"
-
-lemma multiset_inter_count:
- "count (A #\<inter> B) x = min (count A x) (count B x)"
- by (simp add: multiset_inter_def multiset_typedef)
-
-lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
- by (rule multi_count_ext) (simp add: multiset_inter_count)
-
-lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
- by (rule multi_count_ext) (simp add: multiset_inter_count)
-
-lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
- by (rule multi_count_ext) (simp add: multiset_inter_count)
-
-lemmas multiset_inter_ac =
- multiset_inter_commute
- multiset_inter_assoc
- multiset_inter_left_commute
-
-lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
- by (rule multi_count_ext) (auto simp add: multiset_inter_count)
-
-lemma multiset_union_diff_commute:
- assumes "B #\<inter> C = {#}"
- shows "A + B - C = A - C + B"
-proof (rule multi_count_ext)
- fix x
- from assms have "min (count B x) (count C x) = 0"
- by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
- then have "count B x = 0 \<or> count C x = 0"
- by auto
- then show "count (A + B - C) x = count (A - C + B) x"
- by auto
-qed
-
-
-subsubsection {* Comprehension (filter) *}
-
-lemma count_MCollect [simp]:
- "count {# x:#M. P x #} a = (if P a then count M a else 0)"
- by (simp add: MCollect_def in_multiset multiset_typedef)
-
-lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
- by (rule multi_count_ext) simp
-
-lemma MCollect_single [simp]:
- "MCollect {#x#} P = (if P x then {#x#} else {#})"
- by (rule multi_count_ext) simp
-
-lemma MCollect_union [simp]:
- "MCollect (M + N) f = MCollect M f + MCollect N f"
- by (rule multi_count_ext) simp
-
-
subsubsection {* Equality of multisets *}
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
@@ -335,64 +277,61 @@
subsubsection {* Pointwise ordering induced by count *}
-definition mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
- "A \<le># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
+instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
+begin
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ mset_le_def: "A \<le> B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
-definition mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
- "A <# B \<longleftrightarrow> A \<le># B \<and> A \<noteq> B"
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
-notation mset_le (infix "\<subseteq>#" 50)
-notation mset_less (infix "\<subset>#" 50)
+instance proof
+qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym)
+
+end
lemma mset_less_eqI:
- "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<subseteq># B"
+ "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B"
by (simp add: mset_le_def)
-lemma mset_le_refl[simp]: "A \<le># A"
-unfolding mset_le_def by auto
-
-lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C"
-unfolding mset_le_def by (fast intro: order_trans)
-
-lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B"
-apply (unfold mset_le_def)
-apply (rule multiset_eq_conv_count_eq [THEN iffD2])
-apply (blast intro: order_antisym)
-done
-
-lemma mset_le_exists_conv: "(A \<le># B) = (\<exists>C. B = A + C)"
+lemma mset_le_exists_conv:
+ "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
done
-lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)"
-unfolding mset_le_def by auto
+lemma mset_le_mono_add_right_cancel [simp]:
+ "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
+ by (fact add_le_cancel_right)
-lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)"
-unfolding mset_le_def by auto
+lemma mset_le_mono_add_left_cancel [simp]:
+ "C + (A::'a multiset) \<le> C + B \<longleftrightarrow> A \<le> B"
+ by (fact add_le_cancel_left)
+
+lemma mset_le_mono_add:
+ "(A::'a multiset) \<le> B \<Longrightarrow> C \<le> D \<Longrightarrow> A + C \<le> B + D"
+ by (fact add_mono)
-lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D"
-apply (unfold mset_le_def)
-apply auto
-apply (erule_tac x = a in allE)+
-apply auto
-done
+lemma mset_le_add_left [simp]:
+ "(A::'a multiset) \<le> A + B"
+ unfolding mset_le_def by auto
+
+lemma mset_le_add_right [simp]:
+ "B \<le> (A::'a multiset) + B"
+ unfolding mset_le_def by auto
-lemma mset_le_add_left[simp]: "A \<le># A + B"
-unfolding mset_le_def by auto
-
-lemma mset_le_add_right[simp]: "B \<le># A + B"
-unfolding mset_le_def by auto
+lemma mset_le_single:
+ "a :# B \<Longrightarrow> {#a#} \<le> B"
+ by (simp add: mset_le_def)
-lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
-by (simp add: mset_le_def)
-
-lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
-by (simp add: multiset_eq_conv_count_eq mset_le_def)
+lemma multiset_diff_union_assoc:
+ "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
+ by (simp add: multiset_eq_conv_count_eq mset_le_def)
lemma mset_le_multiset_union_diff_commute:
-assumes "B \<le># A"
-shows "A - B + C = A + C - B"
+ assumes "B \<le> A"
+ shows "(A::'a multiset) - B + C = A + C - B"
proof -
from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
from this obtain D where "A = B + D" ..
@@ -410,31 +349,19 @@
done
qed
-interpretation mset_order: order "op \<le>#" "op <#"
-proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
- mset_le_trans simp: mset_less_def)
-
-interpretation mset_order_cancel_semigroup:
- ordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
-proof qed (erule mset_le_mono_add [OF mset_le_refl])
-
-interpretation mset_order_semigroup_cancel:
- ordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
-proof qed simp
-
-lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
+lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
apply (clarsimp simp: mset_le_def mset_less_def)
apply (erule_tac x=x in allE)
apply auto
done
-lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
+lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
apply (clarsimp simp: mset_le_def mset_less_def)
apply (erule_tac x = x in allE)
apply auto
done
-lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
+lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)"
apply (rule conjI)
apply (simp add: mset_lessD)
apply (clarsimp simp: mset_le_def mset_less_def)
@@ -443,30 +370,90 @@
apply (auto split: split_if_asm)
done
-lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
+lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> B)"
apply (rule conjI)
apply (simp add: mset_leD)
apply (force simp: mset_le_def mset_less_def split: split_if_asm)
done
-lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
+lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
-lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
-by (auto simp: mset_le_def mset_less_def)
+lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
+ by (auto simp: mset_le_def mset_less_def)
-lemma multi_psub_self[simp]: "A \<subset># A = False"
-by (auto simp: mset_le_def mset_less_def)
+lemma multi_psub_self[simp]: "(A::'a multiset) < A = False"
+ by simp
lemma mset_less_add_bothsides:
- "T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S"
-by (auto simp: mset_le_def mset_less_def)
+ "T + {#x#} < S + {#x#} \<Longrightarrow> T < S"
+ by (fact add_less_imp_less_right)
+
+lemma mset_less_empty_nonempty:
+ "{#} < S \<longleftrightarrow> S \<noteq> {#}"
+ by (auto simp: mset_le_def mset_less_def)
+
+lemma mset_less_diff_self:
+ "c \<in># B \<Longrightarrow> B - {#c#} < B"
+ by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
+
+
+subsubsection {* Intersection *}
+
+instantiation multiset :: (type) semilattice_inf
+begin
+
+definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+ multiset_inter_def: "inf_multiset A B = A - (A - B)"
+
+instance proof -
+ have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
+ show "OFCLASS('a multiset, semilattice_inf_class)" proof
+ qed (auto simp add: multiset_inter_def mset_le_def aux)
+qed
+
+end
+
+abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
+ "multiset_inter \<equiv> inf"
-lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})"
-by (auto simp: mset_le_def mset_less_def)
+lemma multiset_inter_count:
+ "count (A #\<inter> B) x = min (count A x) (count B x)"
+ by (simp add: multiset_inter_def multiset_typedef)
+
+lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
+ by (rule multi_count_ext) (auto simp add: multiset_inter_count)
-lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
- by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
+lemma multiset_union_diff_commute:
+ assumes "B #\<inter> C = {#}"
+ shows "A + B - C = A - C + B"
+proof (rule multi_count_ext)
+ fix x
+ from assms have "min (count B x) (count C x) = 0"
+ by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
+ then have "count B x = 0 \<or> count C x = 0"
+ by auto
+ then show "count (A + B - C) x = count (A - C + B) x"
+ by auto
+qed
+
+
+subsubsection {* Comprehension (filter) *}
+
+lemma count_MCollect [simp]:
+ "count {# x:#M. P x #} a = (if P a then count M a else 0)"
+ by (simp add: MCollect_def in_multiset multiset_typedef)
+
+lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
+ by (rule multi_count_ext) simp
+
+lemma MCollect_single [simp]:
+ "MCollect {#x#} P = (if P x then {#x#} else {#})"
+ by (rule multi_count_ext) simp
+
+lemma MCollect_union [simp]:
+ "MCollect (M + N) f = MCollect M f + MCollect N f"
+ by (rule multi_count_ext) simp
subsubsection {* Set of elements *}
@@ -657,7 +644,7 @@
apply auto
done
-lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B"
+lemma mset_less_size: "(A::'a multiset) < B \<Longrightarrow> size A < size B"
proof (induct A arbitrary: B)
case (empty M)
then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
@@ -666,12 +653,12 @@
then show ?case by simp
next
case (add S x T)
- have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
- have SxsubT: "S + {#x#} \<subset># T" by fact
- then have "x \<in># T" and "S \<subset># T" by (auto dest: mset_less_insertD)
+ have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact
+ have SxsubT: "S + {#x#} < T" by fact
+ then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD)
then obtain T' where T: "T = T' + {#x#}"
by (blast dest: multi_member_split)
- then have "S \<subset># T'" using SxsubT
+ then have "S < T'" using SxsubT
by (blast intro: mset_less_add_bothsides)
then have "size S < size T'" using IH by simp
then show ?case using T by simp
@@ -686,7 +673,7 @@
definition
mset_less_rel :: "('a multiset * 'a multiset) set" where
- "mset_less_rel = {(A,B). A \<subset># B}"
+ "mset_less_rel = {(A,B). A < B}"
lemma multiset_add_sub_el_shuffle:
assumes "c \<in># B" and "b \<noteq> c"
@@ -709,29 +696,29 @@
text {* The induction rules: *}
lemma full_multiset_induct [case_names less]:
-assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
+assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B"
shows "P B"
apply (rule wf_mset_less_rel [THEN wf_induct])
apply (rule ih, auto simp: mset_less_rel_def)
done
lemma multi_subset_induct [consumes 2, case_names empty add]:
-assumes "F \<subseteq># A"
+assumes "F \<le> A"
and empty: "P {#}"
and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
shows "P F"
proof -
- from `F \<subseteq># A`
+ from `F \<le> A`
show ?thesis
proof (induct F)
show "P {#}" by fact
next
fix x F
- assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
+ assume P: "F \<le> A \<Longrightarrow> P F" and i: "F + {#x#} \<le> A"
show "P (F + {#x#})"
proof (rule insert)
from i show "x \<in># A" by (auto dest: mset_le_insertD)
- from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
+ from i have "F \<le> A" by (auto dest: mset_le_insertD)
with P show "P F" .
qed
qed
@@ -875,12 +862,8 @@
by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
qed
-lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
-apply (induct xs)
- apply auto
-apply (rule mset_le_trans)
- apply auto
-done
+lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
+ by (induct xs) (auto intro: order_trans)
lemma multiset_of_update:
"i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
@@ -969,7 +952,7 @@
by (simp add: multiset_eq_conv_count_eq count_of_filter)
lemma mset_less_eq_Bag [code]:
- "Bag xs \<subseteq># A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
+ "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs then show ?rhs
@@ -990,10 +973,10 @@
begin
definition
- "HOL.eq A B \<longleftrightarrow> A \<subseteq># B \<and> B \<subseteq># A"
+ "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
instance proof
-qed (simp add: eq_multiset_def mset_order.eq_iff)
+qed (simp add: eq_multiset_def eq_iff)
end
@@ -1223,76 +1206,46 @@
subsubsection {* Partial-order properties *}
-instantiation multiset :: (order) order
-begin
-
-definition less_multiset_def:
- "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset_def:
- "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
-
-lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
-unfolding trans_def by (blast intro: order_less_trans)
-
-text {*
- \medskip Irreflexivity.
-*}
+definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
+ "M' <# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-lemma mult_irrefl_aux:
- "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
-by (induct rule: finite_induct) (auto intro: order_less_trans)
+definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
+ "M' <=# M \<longleftrightarrow> M' <# M \<or> M' = M"
-lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
-apply (unfold less_multiset_def, auto)
-apply (drule trans_base_order [THEN mult_implies_one_step], auto)
-apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
-apply (simp add: set_of_eq_empty_iff)
-done
-
-lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
-using insert mult_less_not_refl by fast
-
-
-text {* Transitivity. *}
+notation (xsymbol) less_multiset (infix "\<subset>#" 50)
+notation (xsymbol) le_multiset (infix "\<subseteq>#" 50)
-theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
-unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-
-text {* Asymmetry. *}
-
-theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
-apply auto
-apply (rule mult_less_not_refl [THEN notE])
-apply (erule mult_less_trans, assumption)
-done
-
-theorem mult_less_asym:
- "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
-using mult_less_not_sym by blast
-
-theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
-unfolding le_multiset_def by auto
+interpretation multiset_order: order le_multiset less_multiset
+proof -
+ have irrefl: "\<And>M :: 'a multiset. \<not> M \<subset># M"
+ proof
+ fix M :: "'a multiset"
+ assume "M \<subset># M"
+ then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
+ have "trans {(x'::'a, x). x' < x}"
+ by (rule transI) simp
+ moreover note MM
+ ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
+ \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
+ by (rule mult_implies_one_step)
+ then obtain I J K where "M = I + J" and "M = I + K"
+ and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
+ then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
+ have "finite (set_of K)" by simp
+ moreover note aux2
+ ultimately have "set_of K = {}"
+ by (induct rule: finite_induct) (auto intro: order_less_trans)
+ with aux1 show False by simp
+ qed
+ have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
+ unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
+ show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
+ qed (auto simp add: le_multiset_def irrefl dest: trans)
+qed
-text {* Anti-symmetry. *}
-
-theorem mult_le_antisym:
- "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
-unfolding le_multiset_def by (blast dest: mult_less_not_sym)
-
-text {* Transitivity. *}
-
-theorem mult_le_trans:
- "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
-unfolding le_multiset_def by (blast intro: mult_less_trans)
-
-theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
-unfolding le_multiset_def by auto
-
-instance proof
-qed (auto simp add: mult_less_le dest: mult_le_antisym elim: mult_le_trans)
-
-end
+lemma mult_less_irrefl [elim!]:
+ "M \<subset># (M::'a::order multiset) ==> R"
+ by (simp add: multiset_order.less_irrefl)
subsubsection {* Monotonicity of multiset union *}
@@ -1306,52 +1259,26 @@
apply (simp add: add_assoc)
done
-lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)"
+lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)"
apply (unfold less_multiset_def mult_def)
apply (erule trancl_induct)
apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
done
-lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
+lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)"
apply (subst add_commute [of B C])
apply (subst add_commute [of D C])
apply (erule union_less_mono2)
done
lemma union_less_mono:
- "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
-by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
-
-lemma union_le_mono:
- "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
-unfolding le_multiset_def
-by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
+ "A \<subset># C ==> B \<subset># D ==> A + B \<subset># C + (D::'a::order multiset)"
+ by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
-lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)"
-apply (unfold le_multiset_def less_multiset_def)
-apply (case_tac "M = {#}")
- prefer 2
- apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
- prefer 2
- apply (rule one_step_implies_mult)
- apply (simp only: trans_def)
- apply auto
-done
-
-lemma union_upper1: "A <= A + (B::'a::order multiset)"
-proof -
- have "A + {#} <= A + B" by (blast intro: union_le_mono)
- then show ?thesis by simp
-qed
-
-lemma union_upper2: "B <= A + (B::'a::order multiset)"
-by (subst add_commute) (rule union_upper1)
-
-instance multiset :: (order) ordered_ab_semigroup_add
-apply intro_classes
-apply (erule union_le_mono[OF mult_le_refl])
-done
+interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
+proof
+qed (auto simp add: le_multiset_def intro: union_less_mono2)
subsection {* The fold combinator *}
@@ -1406,7 +1333,7 @@
"fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
proof (induct arbitrary: x y z rule: full_multiset_induct)
case (less M x\<^isub>1 x\<^isub>2 Z)
- have IH: "\<forall>A. A \<subset># M \<longrightarrow>
+ have IH: "\<forall>A. A < M \<longrightarrow>
(\<forall>x x' x''. fold_msetG f x'' A x \<longrightarrow> fold_msetG f x'' A x'
\<longrightarrow> x' = x)" by fact
have Mfoldx\<^isub>1: "fold_msetG f Z M x\<^isub>1" and Mfoldx\<^isub>2: "fold_msetG f Z M x\<^isub>2" by fact+
@@ -1426,8 +1353,8 @@
fix C c v
assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "fold_msetG f Z C v"
then have MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto
- then have CsubM: "C \<subset># M" by simp
- from MBb have BsubM: "B \<subset># M" by simp
+ then have CsubM: "C < M" by simp
+ from MBb have BsubM: "B < M" by simp
show ?case
proof cases
assume "b=c"
@@ -1438,8 +1365,8 @@
let ?D = "B - {#c#}"
have cinB: "c \<in># B" and binC: "b \<in># C" using MBb MCc diff
by (auto intro: insert_noteq_member dest: sym)
- have "B - {#c#} \<subset># B" using cinB by (rule mset_less_diff_self)
- then have DsubM: "?D \<subset># M" using BsubM by (blast intro: mset_order.less_trans)
+ have "B - {#c#} < B" using cinB by (rule mset_less_diff_self)
+ then have DsubM: "?D < M" using BsubM by (blast intro: order_less_trans)
from MBb MCc have "B + {#b#} = C + {#c#}" by blast
then have [simp]: "B + {#b#} - {#c#} = C"
using MBb MCc binC cinB by auto
@@ -1769,6 +1696,37 @@
lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
by (fact add_imp_eq)
-lemmas mset_less_trans = mset_order.less_trans
+lemma mset_less_trans: "(M::'a multiset) < K \<Longrightarrow> K < N \<Longrightarrow> M < N"
+ by (fact order_less_trans)
+
+lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
+ by (fact inf.commute)
+
+lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
+ by (fact inf.assoc [symmetric])
+
+lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
+ by (fact inf.left_commute)
+
+lemmas multiset_inter_ac =
+ multiset_inter_commute
+ multiset_inter_assoc
+ multiset_inter_left_commute
+
+lemma mult_less_not_refl:
+ "\<not> M \<subset># (M::'a::order multiset)"
+ by (fact multiset_order.less_irrefl)
+
+lemma mult_less_trans:
+ "K \<subset># M ==> M \<subset># N ==> K \<subset># (N::'a::order multiset)"
+ by (fact multiset_order.less_trans)
+
+lemma mult_less_not_sym:
+ "M \<subset># N ==> \<not> N \<subset># (M::'a::order multiset)"
+ by (fact multiset_order.less_not_sym)
+
+lemma mult_less_asym:
+ "M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P"
+ by (fact multiset_order.less_asym)
end
\ No newline at end of file
--- a/src/HOL/Library/Permutation.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Library/Permutation.thy Mon Feb 22 09:17:49 2010 +0100
@@ -154,7 +154,7 @@
done
lemma multiset_of_le_perm_append:
- "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)"
+ "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
apply (insert surj_multiset_of, drule surjD)
apply (blast intro: sym)+
--- a/src/HOL/Library/SetsAndFunctions.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy Mon Feb 22 09:17:49 2010 +0100
@@ -119,14 +119,14 @@
apply (force simp add: mult_assoc)
done
-interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
+interpretation set_comm_monoid_add: comm_monoid_add "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
apply default
apply (unfold set_plus_def)
apply (force simp add: add_ac)
apply force
done
-interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
+interpretation set_comm_monoid_mult: comm_monoid_mult "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}"
apply default
apply (unfold set_times_def)
apply (force simp add: mult_ac)
--- a/src/HOL/List.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/List.thy Mon Feb 22 09:17:49 2010 +0100
@@ -2365,7 +2365,7 @@
proof (induct xss arbitrary: xs)
case Nil show ?case by simp
next
- interpret monoid_add "[]" "op @" proof qed simp_all
+ interpret monoid_add "op @" "[]" proof qed simp_all
case Cons then show ?case by (simp add: foldl_absorb0)
qed
--- a/src/HOL/Mutabelle/Mutabelle.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Mutabelle/Mutabelle.thy Mon Feb 22 09:17:49 2010 +0100
@@ -14,7 +14,7 @@
(@{const_name HOL.undefined}, "'a"),
(@{const_name HOL.default}, "'a"),
(@{const_name dummy_pattern}, "'a::{}"),
- (@{const_name Algebras.uminus}, "'a"),
+ (@{const_name Groups.uminus}, "'a"),
(@{const_name Nat.size}, "'a"),
(@{const_name Groups.abs}, "'a")];
--- a/src/HOL/NSA/NSA.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/NSA/NSA.thy Mon Feb 22 09:17: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 Algebras.zero}, _) => NONE
- | Const(@{const_name Algebras.one}, _) => NONE
+ Const(@{const_name Groups.zero}, _) => NONE
+ | Const(@{const_name Groups.one}, _) => NONE
| Const(@{const_name Int.number_of}, _) $ _ => NONE
| _ => SOME (case t of
- Const(@{const_name Algebras.zero}, _) => meta_zero_approx_reorient
- | Const(@{const_name Algebras.one}, _) => meta_one_approx_reorient
+ Const(@{const_name Groups.zero}, _) => meta_zero_approx_reorient
+ | Const(@{const_name Groups.one}, _) => meta_one_approx_reorient
| Const(@{const_name Int.number_of}, _) $ _ =>
meta_number_of_approx_reorient);
--- a/src/HOL/Prolog/Func.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Prolog/Func.thy Mon Feb 22 09:17:49 2010 +0100
@@ -10,31 +10,28 @@
typedecl tm
-consts
- abs :: "(tm => tm) => tm"
- app :: "tm => tm => tm"
+axiomatization
+ abs :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and
+ app :: "tm \<Rightarrow> tm \<Rightarrow> tm" and
- cond :: "tm => tm => tm => tm"
- "fix" :: "(tm => tm) => tm"
-
- true :: tm
- false :: tm
- "and" :: "tm => tm => tm" (infixr "and" 999)
- eq :: "tm => tm => tm" (infixr "eq" 999)
+ cond :: "tm \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" and
+ "fix" :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and
- Z :: tm ("Z")
- S :: "tm => tm"
-(*
- "++", "--",
- "**" :: tm => tm => tm (infixr 999)
-*)
- eval :: "[tm, tm] => bool"
+ true :: tm and
+ false :: tm and
+ "and" :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixr "and" 999) and
+ eq :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixr "eq" 999) and
+
+ Z :: tm ("Z") and
+ S :: "tm \<Rightarrow> tm" and
-instance tm :: plus ..
-instance tm :: minus ..
-instance tm :: times ..
+ plus :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixl "+" 65) and
+ minus :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixl "-" 65) and
+ times :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixl "*" 70) and
-axioms eval: "
+ eval :: "tm \<Rightarrow> tm \<Rightarrow> bool" where
+
+eval: "
eval (abs RR) (abs RR)..
eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
@@ -59,7 +56,6 @@
eval ( Z * M) Z..
eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
-
lemmas prog_Func = eval
lemma "eval ((S (S Z)) + (S Z)) ?X"
--- a/src/HOL/Random.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Random.thy Mon Feb 22 09:17:49 2010 +0100
@@ -168,6 +168,7 @@
hide (open) type seed
hide (open) const inc_shift minus_shift log "next" split_seed
iterate range select pick select_weight
+hide (open) fact range_def
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Tools/Function/size.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML Mon Feb 22 09:17:49 2010 +0100
@@ -25,7 +25,7 @@
val lookup_size = SizeData.get #> Symtab.lookup;
-fun plus (t1, t2) = Const (@{const_name Algebras.plus},
+fun plus (t1, t2) = Const (@{const_name Groups.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/Predicate_Compile/predicate_compile_core.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Feb 22 09:17:49 2010 +0100
@@ -2436,8 +2436,8 @@
val [polarity, depth] = additional_arguments
val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
val depth' =
- Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"})
- $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"})
+ Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+ $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
in [polarity', depth'] end
}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Feb 22 09:17:49 2010 +0100
@@ -224,8 +224,8 @@
@{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
@{const_name Nat.one_nat_inst.one_nat},
@{const_name Orderings.less}, @{const_name Orderings.less_eq},
- @{const_name Algebras.zero},
- @{const_name Algebras.one}, @{const_name Algebras.plus},
+ @{const_name Groups.zero},
+ @{const_name Groups.one}, @{const_name Groups.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},
--- a/src/HOL/Tools/Qelim/cooper.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Feb 22 09:17:49 2010 +0100
@@ -79,9 +79,9 @@
| Const (@{const_name Orderings.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 Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
+| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.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 Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.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 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
+ Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
+ | Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
+ | Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
+ | (m as Const (@{const_name Groups.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 Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1,
- Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
+ (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1,
+ Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.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 Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) =>
+ | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) =>
addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
- | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
+ | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.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 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 =>
+ Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
+| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
+| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
+| Const (@{const_name Groups.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')
@@ -270,7 +270,7 @@
val d'' = Thm.rhs_of dth |> Thm.dest_arg1
in
case tt' of
- Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$_)$_ =>
+ Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.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 Algebras.times},_)$c$y)$ _ =>
+ Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
- | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
+ | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x aconv y andalso member (op =)
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
- | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
+ | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.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 Algebras.times},_)$c$y)$ _ =>
+ | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
- | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
+ | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x=y andalso member (op =)
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
- | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
+ | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.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 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 =>
+ | Const(@{const_name Groups.uminus},_)$t' => Neg (i_of_term vs t')
+ | Const(@{const_name Groups.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Groups.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+ | Const(@{const_name Groups.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)
--- a/src/HOL/Tools/Qelim/presburger.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Mon Feb 22 09:17:49 2010 +0100
@@ -52,15 +52,15 @@
local
fun isnum t = case t of
- Const(@{const_name Algebras.zero},_) => true
- | Const(@{const_name Algebras.one},_) => true
+ Const(@{const_name Groups.zero},_) => true
+ | Const(@{const_name Groups.one},_) => true
| @{term "Suc"}$s => isnum s
| @{term "nat"}$s => isnum s
| @{term "int"}$s => isnum s
- | 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 Groups.uminus},_)$s => isnum s
+ | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Groups.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 Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML Mon Feb 22 09:17: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 Algebras.plus};
+val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
fun mk_minus t =
let val T = Term.fastype_of t
- in Const (@{const_name Algebras.uminus}, T --> T) $ t end;
+ in Const (@{const_name Groups.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 Algebras.plus}, _) $ t $ u, ts) =
+fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (pos, u, ts))
- | dest_summing (pos, Const (@{const_name Algebras.minus}, _) $ t $ u, ts) =
+ | dest_summing (pos, Const (@{const_name Groups.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 Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/hologic.ML Mon Feb 22 09:17:49 2010 +0100
@@ -440,9 +440,9 @@
val natT = Type ("nat", []);
-val zero = Const ("Algebras.zero_class.zero", natT);
+val zero = Const ("Groups.zero_class.zero", natT);
-fun is_zero (Const ("Algebras.zero_class.zero", _)) = true
+fun is_zero (Const ("Groups.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 ("Algebras.zero_class.zero", _)) = 0
+fun dest_nat (Const ("Groups.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 ("Algebras.zero_class.zero", T)
- | mk_number T 1 = Const ("Algebras.one_class.one", T)
+fun mk_number T 0 = Const ("Groups.zero_class.zero", T)
+ | mk_number T 1 = Const ("Groups.one_class.one", T)
| mk_number T i = number_of_const T $ mk_numeral i;
-fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0)
- | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1)
+fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
+ | dest_number (Const ("Groups.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/int_arith.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/int_arith.ML Mon Feb 22 09:17:49 2010 +0100
@@ -49,12 +49,12 @@
make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
proc = proc1, identifier = []};
-fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
- | check (Const (@{const_name Algebras.one}, _)) = true
+fun check (Const (@{const_name Groups.one}, @{typ int})) = false
+ | check (Const (@{const_name Groups.one}, _)) = true
| check (Const (s, _)) = member (op =) [@{const_name "op ="},
- @{const_name Algebras.times}, @{const_name Algebras.uminus},
- @{const_name Algebras.minus}, @{const_name Algebras.plus},
- @{const_name Algebras.zero},
+ @{const_name Groups.times}, @{const_name Groups.uminus},
+ @{const_name Groups.minus}, @{const_name Groups.plus},
+ @{const_name Groups.zero},
@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
| check (a $ b) = check a andalso check b
| check _ = false;
--- a/src/HOL/Tools/lin_arith.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Mon Feb 22 09:17: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 Algebras.times}, _)) $ s $ t, m) =
- (case s of Const (@{const_name Algebras.times}, _) $ s1 $ s2 =>
+ fun demult ((mC as Const (@{const_name Groups.times}, _)) $ s $ t, m) =
+ (case s of Const (@{const_name Groups.times}, _) $ s1 $ s2 =>
(* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *)
demult (mC $ s1 $ (mC $ s2 $ t), m)
| _ =>
@@ -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 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)
+ | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
+ | demult (Const (@{const_name Groups.zero}, _), m) = (NONE, Rat.zero)
+ | demult (Const (@{const_name Groups.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,19 +196,19 @@
(* 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 Algebras.plus}, _) $ s $ t,
+ fun poly (Const (@{const_name Groups.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 Algebras.minus}, T) $ s $ t, m, pi) =
+ | poly (all as Const (@{const_name Groups.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 Algebras.uminus}, T) $ t, m, pi) =
+ | poly (all as Const (@{const_name Groups.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 Algebras.zero}, _), _, pi) =
+ | poly (Const (@{const_name Groups.zero}, _), _, pi) =
pi
- | poly (Const (@{const_name Algebras.one}, _), m, (p, i)) =
+ | poly (Const (@{const_name Groups.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 Algebras.times}, _) $ _ $ _, m, pi as (p, i)) =
+ | poly (all as Const (@{const_name Groups.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)
@@ -293,7 +293,7 @@
Const (a, _) => member (op =) [@{const_name Orderings.max},
@{const_name Orderings.min},
@{const_name Groups.abs},
- @{const_name Algebras.minus},
+ @{const_name Groups.minus},
"Int.nat" (*DYNAMIC BINDING!*),
"Divides.div_class.mod" (*DYNAMIC BINDING!*),
"Divides.div_class.div" (*DYNAMIC BINDING!*)] a
@@ -401,9 +401,9 @@
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 Algebras.uminus},
+ val terms2 = map (subst_term [(split_term, Const (@{const_name Groups.uminus},
split_type --> split_type) $ t1)]) rev_terms
- val zero = Const (@{const_name Algebras.zero}, split_type)
+ val zero = Const (@{const_name Groups.zero}, split_type)
val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ t1
val t1_lt_zero = Const (@{const_name Orderings.less},
@@ -415,12 +415,12 @@
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
(* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
- | (Const (@{const_name Algebras.minus}, _), [t1, t2]) =>
+ | (Const (@{const_name Groups.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 Algebras.zero}, split_type)
+ val zero = Const (@{const_name Groups.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)])
@@ -430,7 +430,7 @@
val t1_lt_t2 = Const (@{const_name Orderings.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 Algebras.plus},
+ (Const (@{const_name Groups.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 Algebras.zero}, HOLogic.intT)
- val zero_nat = Const (@{const_name Algebras.zero}, HOLogic.natT)
+ val zero_int = Const (@{const_name Groups.zero}, HOLogic.intT)
+ val zero_nat = Const (@{const_name Groups.zero}, HOLogic.natT)
val n = Bound 0
val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)])
(map (incr_boundvars 1) rev_terms)
@@ -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 Algebras.zero}, split_type)
+ val zero = Const (@{const_name Groups.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -480,8 +480,8 @@
val j_lt_t2 = Const (@{const_name Orderings.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 Algebras.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name Algebras.times},
+ (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Groups.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 Algebras.zero}, split_type)
+ val zero = Const (@{const_name Groups.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
@@ -512,8 +512,8 @@
val j_lt_t2 = Const (@{const_name Orderings.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 Algebras.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name Algebras.times},
+ (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Groups.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 Algebras.zero}, split_type)
+ val zero = Const (@{const_name Groups.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
@@ -558,8 +558,8 @@
val t2_lt_j = Const (@{const_name Orderings.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 Algebras.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name Algebras.times},
+ (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Groups.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 Algebras.zero}, split_type)
+ val zero = Const (@{const_name Groups.zero}, split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
@@ -612,8 +612,8 @@
val t2_lt_j = Const (@{const_name Orderings.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 Algebras.plus}, split_type --> split_type --> split_type) $
- (Const (@{const_name Algebras.times},
+ (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
+ (Const (@{const_name Groups.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/nat_arith.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML Mon Feb 22 09:17:49 2010 +0100
@@ -19,8 +19,8 @@
(** abstract syntax of structure nat: 0, Suc, + **)
-val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
-val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
+val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
+val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
fun mk_sum [] = HOLogic.zero
| mk_sum [t] = t
@@ -85,8 +85,8 @@
structure DiffCancelSums = CancelSumsFun
(struct
open CommonCancelSums;
- val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus};
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
+ val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
end);
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Mon Feb 22 09:17: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 Algebras.plus};
+val mk_plus = HOLogic.mk_binop @{const_name Groups.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 Algebras.plus} HOLogic.natT;
+val dest_plus = HOLogic.dest_bin @{const_name Groups.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 Algebras.times};
+val mk_times = HOLogic.mk_binop @{const_name Groups.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 Algebras.times} HOLogic.natT;
+val dest_times = HOLogic.dest_bin @{const_name Groups.times} HOLogic.natT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -194,8 +194,8 @@
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus}
- val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT
+ val mk_bal = HOLogic.mk_binop @{const_name Groups.minus}
+ val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT
val bal_add1 = @{thm nat_diff_add_eq1} RS trans
val bal_add2 = @{thm nat_diff_add_eq2} RS trans
);
--- a/src/HOL/Tools/numeral_simprocs.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Feb 22 09:17: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 Algebras.minus};
-val dest_diff = HOLogic.dest_bin @{const_name Algebras.minus} Term.dummyT;
+val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
+val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT;
-val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
+val mk_times = HOLogic.mk_binop @{const_name Groups.times};
-fun one_of T = Const(@{const_name Algebras.one}, T);
+fun one_of T = Const(@{const_name Groups.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 Algebras.times} Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name Groups.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 Algebras.uminus}, _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name Groups.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
@@ -104,7 +104,7 @@
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 Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
+fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
| dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
let val (p, t') = dest_coeff sign t
val (q, u') = dest_coeff 1 u
@@ -484,7 +484,7 @@
in
fun sign_conv pos_th neg_th ss t =
let val T = fastype_of t;
- val zero = Const(@{const_name Algebras.zero}, T);
+ val zero = Const(@{const_name Groups.zero}, T);
val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
fun prove p =
--- a/src/HOL/Tools/refute.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/Tools/refute.ML Mon Feb 22 09:17:49 2010 +0100
@@ -710,11 +710,11 @@
| Const (@{const_name Finite_Set.finite}, _) => t
| Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
- | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
| Const (@{const_name List.append}, _) => t
| Const (@{const_name lfp}, _) => t
@@ -886,13 +886,13 @@
| Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Groups.plus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Groups.minus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Groups.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
@@ -2794,7 +2794,7 @@
fun Nat_plus_interpreter thy model args t =
case t of
- Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2825,7 +2825,7 @@
fun Nat_minus_interpreter thy model args t =
case t of
- Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2853,7 +2853,7 @@
fun Nat_times_interpreter thy model args t =
case t of
- Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Groups.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/UNITY/Comp/AllocBase.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Mon Feb 22 09:17:49 2010 +0100
@@ -58,9 +58,8 @@
apply (rule monoI)
apply (unfold prefix_def)
apply (erule genPrefix.induct, auto)
-apply (simp add: union_le_mono)
apply (erule order_trans)
-apply (rule union_upper1)
+apply simp
done
(** setsum **)
--- a/src/HOL/UNITY/Follows.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/UNITY/Follows.thy Mon Feb 22 09:17:49 2010 +0100
@@ -176,7 +176,7 @@
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
apply (drule bspec, assumption)
-apply (blast intro: union_le_mono order_trans)
+apply (blast intro: add_mono order_trans)
done
lemma Increasing_union:
@@ -187,14 +187,14 @@
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
apply (drule bspec, assumption)
-apply (blast intro: union_le_mono order_trans)
+apply (blast intro: add_mono order_trans)
done
lemma Always_union:
"[| F \<in> Always {s. f' s \<le> f s}; F \<in> Always {s. g' s \<le> g s} |]
==> F \<in> Always {s. f' s + g' s \<le> f s + (g s :: ('a::order) multiset)}"
apply (simp add: Always_eq_includes_reachable)
-apply (blast intro: union_le_mono)
+apply (blast intro: add_mono)
done
(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
@@ -211,7 +211,7 @@
apply (rule PSP_Stable)
apply (erule_tac x = "f s" in spec)
apply (erule Stable_Int, assumption, blast)
-apply (blast intro: union_le_mono order_trans)
+apply (blast intro: add_mono order_trans)
done
(*The !! is there to influence to effect of permutative rewriting at the end*)
--- a/src/HOL/ex/Arith_Examples.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy Mon Feb 22 09:17:49 2010 +0100
@@ -33,7 +33,7 @@
*)
subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
- @{term Algebras.minus}, @{term nat}, @{term Divides.mod},
+ @{term minus}, @{term nat}, @{term Divides.mod},
@{term Divides.div} *}
lemma "(i::nat) <= max i j"
--- a/src/HOL/ex/Binary.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/ex/Binary.thy Mon Feb 22 09:17:49 2010 +0100
@@ -24,8 +24,8 @@
| dest_bit (Const (@{const_name True}, _)) = 1
| dest_bit t = raise TERM ("dest_bit", [t]);
- 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
+ fun dest_binary (Const (@{const_name Groups.zero}, Type (@{type_name nat}, _))) = 0
+ | dest_binary (Const (@{const_name Groups.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 Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Mon Feb 22 09:17: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 Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Rings.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 ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
| rat t = lit t
(*abstraction of an integer expression: no div, mod*)
- 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)
+ fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x)
| int t = lit t
(*abstraction of a natural number expression: no minus*)
- 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)
+ fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+ | nat ((c as Const(@{const_name Groups.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: =, <, <=*)
--- a/src/HOL/ex/Summation.thy Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/ex/Summation.thy Mon Feb 22 09:17:49 2010 +0100
@@ -28,7 +28,7 @@
lemma \<Delta>_same_shift:
assumes "\<Delta> f = \<Delta> g"
- shows "\<exists>l. (op +) l \<circ> f = g"
+ shows "\<exists>l. plus l \<circ> f = g"
proof -
fix k
from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
@@ -44,9 +44,9 @@
show "f k - g k = f 0 - g 0"
by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
qed
- then have "\<And>k. ((op +) (g 0 - f 0) \<circ> f) k = g k"
+ then have "\<And>k. (plus (g 0 - f 0) \<circ> f) k = g k"
by (simp add: algebra_simps)
- then have "(op +) (g 0 - f 0) \<circ> f = g" ..
+ then have "plus (g 0 - f 0) \<circ> f = g" ..
then show ?thesis ..
qed
@@ -99,7 +99,7 @@
"\<Sigma> (\<Delta> f) j l = f l - f j"
proof -
from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
- then obtain k where "(op +) k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
+ then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
then show ?thesis by simp
qed
--- a/src/HOL/ex/svc_funcs.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML Mon Feb 22 09:17:49 2010 +0100
@@ -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 Algebras.plus}, T) $ x $ y) =
+ fun litExp (Const(@{const_name Groups.plus}, T) $ x $ y) =
if is_numeric_op T then (litExp x) + (litExp y)
else fail t
- | litExp (Const(@{const_name Algebras.minus}, T) $ x $ y) =
+ | litExp (Const(@{const_name Groups.minus}, T) $ x $ y) =
if is_numeric_op T then (litExp x) - (litExp y)
else fail t
- | litExp (Const(@{const_name Algebras.times}, T) $ x $ y) =
+ | litExp (Const(@{const_name Groups.times}, T) $ x $ y) =
if is_numeric_op T then (litExp x) * (litExp y)
else fail t
- | litExp (Const(@{const_name Algebras.uminus}, T) $ x) =
+ | litExp (Const(@{const_name Groups.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 Algebras.plus}, T) $ x $ y) =
+ | tm (Const(@{const_name Groups.plus}, T) $ x $ y) =
if is_numeric_op T then Interp("+", [tm x, tm y])
else fail t
- | tm (Const(@{const_name Algebras.minus}, T) $ x $ y) =
+ | tm (Const(@{const_name Groups.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 Algebras.times}, T) $ x $ y) =
+ | tm (Const(@{const_name Groups.times}, T) $ x $ y) =
if is_numeric_op T then Interp("*", [tm x, tm y])
else fail t
| tm (Const(@{const_name Rings.inverse}, T) $ x) =
if domain_type T = HOLogic.realT then
Rat(1, litExp x)
else fail t
- | tm (Const(@{const_name Algebras.uminus}, T) $ x) =
+ | tm (Const(@{const_name Groups.uminus}, T) $ x) =
if is_numeric_op T then Interp("*", [Int ~1, tm x])
else fail t
| tm t = Int (lit t)
--- a/src/Provers/Arith/abel_cancel.ML Sun Feb 21 23:05:37 2010 +0100
+++ b/src/Provers/Arith/abel_cancel.ML Mon Feb 22 09:17:49 2010 +0100
@@ -28,29 +28,29 @@
(* FIXME dependent on abstract syntax *)
-fun zero t = Const (@{const_name Algebras.zero}, t);
-fun minus t = Const (@{const_name Algebras.uminus}, t --> t);
+fun zero t = Const (@{const_name Groups.zero}, t);
+fun minus t = Const (@{const_name Groups.uminus}, t --> t);
-fun add_terms pos (Const (@{const_name Algebras.plus}, _) $ x $ y, ts) =
+fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
add_terms pos (x, add_terms pos (y, ts))
- | add_terms pos (Const (@{const_name Algebras.minus}, _) $ x $ y, ts) =
+ | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
add_terms pos (x, add_terms (not pos) (y, ts))
- | add_terms pos (Const (@{const_name Algebras.uminus}, _) $ x, ts) =
+ | add_terms pos (Const (@{const_name Groups.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 Algebras.plus},_)) $ x $ y) =
+fun zero1 pt (u as (c as Const(@{const_name Groups.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 Algebras.minus},_)) $ x $ y) =
+ | zero1 (pos,t) (u as (c as Const(@{const_name Groups.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 Algebras.uminus},_)) $ x) =
+ | zero1 (pos,t) (u as (c as Const(@{const_name Groups.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 Algebras.plus},_) => true | _ => false;
+ val opp = case c of Const(@{const_name Groups.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 Sun Feb 21 23:05:37 2010 +0100
+++ b/src/Provers/Arith/cancel_div_mod.ML Mon Feb 22 09:17:49 2010 +0100
@@ -34,12 +34,12 @@
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
struct
-fun coll_div_mod (Const(@{const_name Algebras.plus},_) $ s $ t) dms =
+fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
coll_div_mod t (coll_div_mod s dms)
- | coll_div_mod (Const(@{const_name Algebras.times},_) $ m $ (Const(d,_) $ s $ n))
+ | coll_div_mod (Const(@{const_name Groups.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 Algebras.times},_) $ (Const(d,_) $ s $ n) $ m)
+ | coll_div_mod (Const(@{const_name Groups.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)) =
@@ -55,8 +55,8 @@
==> thesis by transitivity
*)
-val mk_plus = Data.mk_binop @{const_name Algebras.plus};
-val mk_times = Data.mk_binop @{const_name Algebras.times};
+val mk_plus = Data.mk_binop @{const_name Groups.plus};
+val mk_times = Data.mk_binop @{const_name Groups.times};
fun rearrange t pq =
let val ts = Data.dest_sum t;