--- a/doc-src/AxClass/Group/Group.thy Tue Sep 06 16:29:39 2005 +0200
+++ b/doc-src/AxClass/Group/Group.thy Tue Sep 06 16:59:48 2005 +0200
@@ -94,21 +94,21 @@
theorem group_right_inverse: "x \<odot> x\<inv> = (\<one>\<Colon>'a\<Colon>group)"
proof -
have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)"
- by (simp only: group.left_unit)
+ by (simp only: group_class.left_unit)
also have "... = \<one> \<odot> x \<odot> x\<inv>"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
- by (simp only: group.left_unit)
+ by (simp only: group_class.left_unit)
also have "... = \<one>"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
finally show ?thesis .
qed
@@ -121,13 +121,13 @@
theorem group_right_unit: "x \<odot> \<one> = (x\<Colon>'a\<Colon>group)"
proof -
have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
also have "... = x \<odot> x\<inv> \<odot> x"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = \<one> \<odot> x"
by (simp only: group_right_inverse)
also have "... = x"
- by (simp only: group.left_unit)
+ by (simp only: group_class.left_unit)
finally show ?thesis .
qed
@@ -185,16 +185,16 @@
proof
fix x y z :: "'a\<Colon>monoid"
show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
- by (rule monoid.assoc)
+ by (rule monoid_class.assoc)
qed
instance group \<subseteq> monoid
proof
fix x y z :: "'a\<Colon>group"
show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
- by (rule semigroup.assoc)
+ by (rule semigroup_class.assoc)
show "\<one> \<odot> x = x"
- by (rule group.left_unit)
+ by (rule group_class.left_unit)
show "x \<odot> \<one> = x"
by (rule group_right_unit)
qed
@@ -309,7 +309,7 @@
snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) =
(fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r),
snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))"
- by (simp add: semigroup.assoc)
+ by (simp add: semigroup_class.assoc)
qed
text {*
--- a/doc-src/IsarRef/generic.tex Tue Sep 06 16:29:39 2005 +0200
+++ b/doc-src/IsarRef/generic.tex Tue Sep 06 16:59:48 2005 +0200
@@ -27,18 +27,18 @@
\end{rail}
\begin{descr}
-
+
\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
the intersection of existing classes, with additional axioms holding. Class
axioms may not contain more than one type variable. The class axioms (with
implicit sort constraints added) are bound to the given names. Furthermore
- a class introduction rule is generated (being bound as $c{.}intro$); this
- rule is employed by method $intro_classes$ to support instantiation proofs
- of this class.
-
+ a class introduction rule is generated (being bound as
+ $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
+ support instantiation proofs of this class.
+
The ``axioms'' are stored as theorems according to the given name
specifications, adding the class name $c$ as name space prefix; the same
- facts are also stored collectively as $c{\dtt}axioms$.
+ facts are also stored collectively as $c_class{\dtt}axioms$.
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
goal stating a class relation or type arity. The proof would usually
--- a/src/FOL/ex/NatClass.ML Tue Sep 06 16:29:39 2005 +0200
+++ b/src/FOL/ex/NatClass.ML Tue Sep 06 16:59:48 2005 +0200
@@ -6,7 +6,7 @@
*)
Goal "Suc(k) ~= (k::'a::nat)";
-by (res_inst_tac [("n","k")] nat.induct 1);
+by (res_inst_tac [("n","k")] induct 1);
by (rtac notI 1);
by (etac Suc_neq_0 1);
by (rtac notI 1);
@@ -16,8 +16,8 @@
Goal "(k+m)+n = k+(m+n)";
-prths ([nat.induct] RL [topthm()]); (*prints all 14 next states!*)
-by (rtac nat.induct 1);
+prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
+by (rtac induct 1);
back();
back();
back();
@@ -36,24 +36,24 @@
Addsimps [add_0, add_Suc];
Goal "(k+m)+n = k+(m+n)";
-by (res_inst_tac [("n","k")] nat.induct 1);
+by (res_inst_tac [("n","k")] induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "add_assoc";
Goal "m+0 = m";
-by (res_inst_tac [("n","m")] nat.induct 1);
+by (res_inst_tac [("n","m")] induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "add_0_right";
Goal "m+Suc(n) = Suc(m+n)";
-by (res_inst_tac [("n","m")] nat.induct 1);
+by (res_inst_tac [("n","m")] induct 1);
by (ALLGOALS (Asm_simp_tac));
qed "add_Suc_right";
val [prem] = goal (the_context ()) "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-by (res_inst_tac [("n","i")] nat.induct 1);
+by (res_inst_tac [("n","i")] induct 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [prem]) 1);
result();
--- a/src/FOL/ex/NatClass.thy Tue Sep 06 16:29:39 2005 +0200
+++ b/src/FOL/ex/NatClass.thy Tue Sep 06 16:59:48 2005 +0200
@@ -34,6 +34,6 @@
"m + n == rec(m, n, %x y. Suc(y))"
ML {* use_legacy_bindings (the_context ()) *}
-ML {* open nat *}
+ML {* open nat_class *}
end
--- a/src/HOL/Algebra/abstract/Ring.thy Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy Tue Sep 06 16:59:48 2005 +0200
@@ -130,7 +130,7 @@
proof (induct n)
case 0 show ?case by simp
next
- case Suc thus ?case by (simp add: semigroup_add.add_assoc)
+ case Suc thus ?case by (simp add: semigroup_add_class.add_assoc)
qed
lemma natsum_cong [cong]:
--- a/src/HOL/Algebra/abstract/order.ML Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/Algebra/abstract/order.ML Tue Sep 06 16:59:48 2005 +0200
@@ -28,18 +28,18 @@
(*** Rewrite rules ***)
-val a_assoc = thm "ring.a_assoc";
-val l_zero = thm "ring.l_zero";
-val l_neg = thm "ring.l_neg";
-val a_comm = thm "ring.a_comm";
-val m_assoc = thm "ring.m_assoc";
-val l_one = thm "ring.l_one";
-val l_distr = thm "ring.l_distr";
-val m_comm = thm "ring.m_comm";
-val minus_def = thm "ring.minus_def";
-val inverse_def = thm "ring.inverse_def";
-val divide_def = thm "ring.divide_def";
-val power_def = thm "ring.power_def";
+val a_assoc = thm "ring_class.a_assoc";
+val l_zero = thm "ring_class.l_zero";
+val l_neg = thm "ring_class.l_neg";
+val a_comm = thm "ring_class.a_comm";
+val m_assoc = thm "ring_class.m_assoc";
+val l_one = thm "ring_class.l_one";
+val l_distr = thm "ring_class.l_distr";
+val m_comm = thm "ring_class.m_comm";
+val minus_def = thm "ring_class.minus_def";
+val inverse_def = thm "ring_class.inverse_def";
+val divide_def = thm "ring_class.divide_def";
+val power_def = thm "ring_class.power_def";
(* These are the following axioms:
--- a/src/HOL/Algebra/poly/LongDiv.thy Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy Tue Sep 06 16:59:48 2005 +0200
@@ -21,7 +21,7 @@
apply (induct_tac m)
apply (simp)
apply (force)
- apply (simp add: ab_semigroup_add.add_commute[of m])
+ apply (simp add: ab_semigroup_add_class.add_commute[of m])
done
end
--- a/src/HOL/AxClasses/Group.thy Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/AxClasses/Group.thy Tue Sep 06 16:59:48 2005 +0200
@@ -34,34 +34,34 @@
theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
proof -
have "x [*] invers x = one [*] (x [*] invers x)"
- by (simp only: group.left_unit)
+ by (simp only: group_class.left_unit)
also have "... = one [*] x [*] invers x"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = invers (invers x) [*] one [*] invers x"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
also have "... = invers (invers x) [*] (one [*] invers x)"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = invers (invers x) [*] invers x"
- by (simp only: group.left_unit)
+ by (simp only: group_class.left_unit)
also have "... = one"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
finally show ?thesis .
qed
theorem group_right_unit: "x [*] one = (x::'a::group)"
proof -
have "x [*] one = x [*] (invers x [*] x)"
- by (simp only: group.left_inverse)
+ by (simp only: group_class.left_inverse)
also have "... = x [*] invers x [*] x"
- by (simp only: semigroup.assoc)
+ by (simp only: semigroup_class.assoc)
also have "... = one [*] x"
by (simp only: group_right_inverse)
also have "... = x"
- by (simp only: group.left_unit)
+ by (simp only: group_class.left_unit)
finally show ?thesis .
qed
@@ -72,16 +72,16 @@
proof intro_classes
fix x y z :: "'a::monoid"
show "x [*] y [*] z = x [*] (y [*] z)"
- by (rule monoid.assoc)
+ by (rule monoid_class.assoc)
qed
instance group < monoid
proof intro_classes
fix x y z :: "'a::group"
show "x [*] y [*] z = x [*] (y [*] z)"
- by (rule semigroup.assoc)
+ by (rule semigroup_class.assoc)
show "one [*] x = x"
- by (rule group.left_unit)
+ by (rule group_class.left_unit)
show "x [*] one = x"
by (rule group_right_unit)
qed
@@ -118,7 +118,7 @@
snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) =
(fst p [*] fst (fst q [*] fst r, snd q [*] snd r),
snd p [*] snd (fst q [*] fst r, snd q [*] snd r))"
- by (simp add: semigroup.assoc)
+ by (simp add: semigroup_class.assoc)
qed
end
--- a/src/HOL/Finite_Set.ML Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/Finite_Set.ML Tue Sep 06 16:59:48 2005 +0200
@@ -51,7 +51,6 @@
val empty_foldSetE = thm "empty_foldSetE";
val endo_inj_surj = thm "endo_inj_surj";
val finite = thm "finite";
-val finiteI = thm "finiteI";
val finite_Diff = thm "finite_Diff";
val finite_Diff_insert = thm "finite_Diff_insert";
val finite_Field = thm "finite_Field";
--- a/src/HOL/HOL.ML Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/HOL.ML Tue Sep 06 16:59:48 2005 +0200
@@ -5,9 +5,6 @@
structure HOL =
struct
val thy = the_context ();
- val plusI = plusI;
- val minusI = minusI;
- val timesI = timesI;
val eq_reflection = eq_reflection;
val refl = refl;
val subst = subst;
--- a/src/HOL/HOL.thy Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/HOL.thy Tue Sep 06 16:59:48 2005 +0200
@@ -686,9 +686,6 @@
ML
{*
-val plusI = thm "plusI"
-val minusI = thm "minusI"
-val timesI = thm "timesI"
val eq_reflection = thm "eq_reflection"
val refl = thm "refl"
val subst = thm "subst"
--- a/src/HOL/Nat.ML Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/Nat.ML Tue Sep 06 16:59:48 2005 +0200
@@ -220,7 +220,6 @@
val one_is_add = thm "one_is_add";
val one_le_mult_iff = thm "one_le_mult_iff";
val one_reorient = thm "one_reorient";
-val powerI = thm "powerI";
val pred_nat_def = thm "pred_nat_def";
val trans_le_add1 = thm "trans_le_add1";
val trans_le_add2 = thm "trans_le_add2";
@@ -234,4 +233,4 @@
val zero_less_diff = thm "zero_less_diff";
val zero_less_mult_iff = thm "zero_less_mult_iff";
val zero_reorient = thm "zero_reorient";
-val linorder_neqE_nat = thm "linorder_neqE_nat";
\ No newline at end of file
+val linorder_neqE_nat = thm "linorder_neqE_nat";
--- a/src/HOL/Tools/refute.ML Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/Tools/refute.ML Tue Sep 06 16:59:48 2005 +0200
@@ -478,7 +478,7 @@
let
(* obtain the axioms generated by the "axclass" command *)
(* (string * Term.term) list *)
- val class_axioms = List.filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms
+ val class_axioms = List.filter (fn (s, _) => String.isPrefix (Sign.const_of_class class ^ ".axioms_") s) axioms
(* replace the one schematic type variable in each axiom by the actual type 'T' *)
(* (string * Term.term) list *)
val monomorphic_class_axioms = map (fn (axname, ax) =>
@@ -690,7 +690,7 @@
val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
(* Term.term option *)
val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
- val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
+ val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, s ^ ".intro")) handle Type.TYPE_MATCH => NONE)
val axs' = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
(* collect relevant type axioms *)
collect_type_axioms (axs, T)
@@ -701,7 +701,7 @@
(* collect relevant type axioms *)
collect_type_axioms (axs', T)
else
- (immediate_output (" " ^ class ^ ".intro");
+ (immediate_output (" " ^ s ^ ".intro");
collect_term_axioms (ax :: axs', ax)))
in
axs''