axclass: name space prefix is now "c_class" instead of just "c";
authorwenzelm
Tue Sep 06 16:59:48 2005 +0200 (2005-09-06)
changeset 17274746bb4c56800
parent 17273 e95f7141ba2f
child 17275 44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
doc-src/AxClass/Group/Group.thy
doc-src/IsarRef/generic.tex
src/FOL/ex/NatClass.ML
src/FOL/ex/NatClass.thy
src/HOL/Algebra/abstract/Ring.thy
src/HOL/Algebra/abstract/order.ML
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/AxClasses/Group.thy
src/HOL/Finite_Set.ML
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/Nat.ML
src/HOL/Tools/refute.ML
     1.1 --- a/doc-src/AxClass/Group/Group.thy	Tue Sep 06 16:29:39 2005 +0200
     1.2 +++ b/doc-src/AxClass/Group/Group.thy	Tue Sep 06 16:59:48 2005 +0200
     1.3 @@ -94,21 +94,21 @@
     1.4  theorem group_right_inverse: "x \<odot> x\<inv> = (\<one>\<Colon>'a\<Colon>group)"
     1.5  proof -
     1.6    have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)"
     1.7 -    by (simp only: group.left_unit)
     1.8 +    by (simp only: group_class.left_unit)
     1.9    also have "... = \<one> \<odot> x \<odot> x\<inv>"
    1.10 -    by (simp only: semigroup.assoc)
    1.11 +    by (simp only: semigroup_class.assoc)
    1.12    also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
    1.13 -    by (simp only: group.left_inverse)
    1.14 +    by (simp only: group_class.left_inverse)
    1.15    also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
    1.16 -    by (simp only: semigroup.assoc)
    1.17 +    by (simp only: semigroup_class.assoc)
    1.18    also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>"
    1.19 -    by (simp only: group.left_inverse)
    1.20 +    by (simp only: group_class.left_inverse)
    1.21    also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)"
    1.22 -    by (simp only: semigroup.assoc)
    1.23 +    by (simp only: semigroup_class.assoc)
    1.24    also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
    1.25 -    by (simp only: group.left_unit)
    1.26 +    by (simp only: group_class.left_unit)
    1.27    also have "... = \<one>"
    1.28 -    by (simp only: group.left_inverse)
    1.29 +    by (simp only: group_class.left_inverse)
    1.30    finally show ?thesis .
    1.31  qed
    1.32  
    1.33 @@ -121,13 +121,13 @@
    1.34  theorem group_right_unit: "x \<odot> \<one> = (x\<Colon>'a\<Colon>group)"
    1.35  proof -
    1.36    have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)"
    1.37 -    by (simp only: group.left_inverse)
    1.38 +    by (simp only: group_class.left_inverse)
    1.39    also have "... = x \<odot> x\<inv> \<odot> x"
    1.40 -    by (simp only: semigroup.assoc)
    1.41 +    by (simp only: semigroup_class.assoc)
    1.42    also have "... = \<one> \<odot> x"
    1.43      by (simp only: group_right_inverse)
    1.44    also have "... = x"
    1.45 -    by (simp only: group.left_unit)
    1.46 +    by (simp only: group_class.left_unit)
    1.47    finally show ?thesis .
    1.48  qed
    1.49  
    1.50 @@ -185,16 +185,16 @@
    1.51  proof
    1.52    fix x y z :: "'a\<Colon>monoid"
    1.53    show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
    1.54 -    by (rule monoid.assoc)
    1.55 +    by (rule monoid_class.assoc)
    1.56  qed
    1.57  
    1.58  instance group \<subseteq> monoid
    1.59  proof
    1.60    fix x y z :: "'a\<Colon>group"
    1.61    show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
    1.62 -    by (rule semigroup.assoc)
    1.63 +    by (rule semigroup_class.assoc)
    1.64    show "\<one> \<odot> x = x"
    1.65 -    by (rule group.left_unit)
    1.66 +    by (rule group_class.left_unit)
    1.67    show "x \<odot> \<one> = x"
    1.68      by (rule group_right_unit)
    1.69  qed
    1.70 @@ -309,7 +309,7 @@
    1.71        snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) =
    1.72         (fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r),
    1.73          snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))"
    1.74 -    by (simp add: semigroup.assoc)
    1.75 +    by (simp add: semigroup_class.assoc)
    1.76  qed
    1.77  
    1.78  text {*
     2.1 --- a/doc-src/IsarRef/generic.tex	Tue Sep 06 16:29:39 2005 +0200
     2.2 +++ b/doc-src/IsarRef/generic.tex	Tue Sep 06 16:59:48 2005 +0200
     2.3 @@ -27,18 +27,18 @@
     2.4  \end{rail}
     2.5  
     2.6  \begin{descr}
     2.7 -
     2.8 +  
     2.9  \item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
    2.10    the intersection of existing classes, with additional axioms holding.  Class
    2.11    axioms may not contain more than one type variable.  The class axioms (with
    2.12    implicit sort constraints added) are bound to the given names.  Furthermore
    2.13 -  a class introduction rule is generated (being bound as $c{.}intro$); this
    2.14 -  rule is employed by method $intro_classes$ to support instantiation proofs
    2.15 -  of this class.
    2.16 -
    2.17 +  a class introduction rule is generated (being bound as
    2.18 +  $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
    2.19 +  support instantiation proofs of this class.
    2.20 +  
    2.21    The ``axioms'' are stored as theorems according to the given name
    2.22    specifications, adding the class name $c$ as name space prefix; the same
    2.23 -  facts are also stored collectively as $c{\dtt}axioms$.
    2.24 +  facts are also stored collectively as $c_class{\dtt}axioms$.
    2.25    
    2.26  \item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
    2.27    goal stating a class relation or type arity.  The proof would usually
     3.1 --- a/src/FOL/ex/NatClass.ML	Tue Sep 06 16:29:39 2005 +0200
     3.2 +++ b/src/FOL/ex/NatClass.ML	Tue Sep 06 16:59:48 2005 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  *)
     3.5  
     3.6  Goal "Suc(k) ~= (k::'a::nat)";
     3.7 -by (res_inst_tac [("n","k")] nat.induct 1);
     3.8 +by (res_inst_tac [("n","k")] induct 1);
     3.9  by (rtac notI 1);
    3.10  by (etac Suc_neq_0 1);
    3.11  by (rtac notI 1);
    3.12 @@ -16,8 +16,8 @@
    3.13  
    3.14  
    3.15  Goal "(k+m)+n = k+(m+n)";
    3.16 -prths ([nat.induct] RL [topthm()]);  (*prints all 14 next states!*)
    3.17 -by (rtac nat.induct 1);
    3.18 +prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
    3.19 +by (rtac induct 1);
    3.20  back();
    3.21  back();
    3.22  back();
    3.23 @@ -36,24 +36,24 @@
    3.24  Addsimps [add_0, add_Suc];
    3.25  
    3.26  Goal "(k+m)+n = k+(m+n)";
    3.27 -by (res_inst_tac [("n","k")] nat.induct 1);
    3.28 +by (res_inst_tac [("n","k")] induct 1);
    3.29  by (Simp_tac 1);
    3.30  by (Asm_simp_tac 1);
    3.31  qed "add_assoc";
    3.32  
    3.33  Goal "m+0 = m";
    3.34 -by (res_inst_tac [("n","m")] nat.induct 1);
    3.35 +by (res_inst_tac [("n","m")] induct 1);
    3.36  by (Simp_tac 1);
    3.37  by (Asm_simp_tac 1);
    3.38  qed "add_0_right";
    3.39  
    3.40  Goal "m+Suc(n) = Suc(m+n)";
    3.41 -by (res_inst_tac [("n","m")] nat.induct 1);
    3.42 +by (res_inst_tac [("n","m")] induct 1);
    3.43  by (ALLGOALS (Asm_simp_tac));
    3.44  qed "add_Suc_right";
    3.45  
    3.46  val [prem] = goal (the_context ()) "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
    3.47 -by (res_inst_tac [("n","i")] nat.induct 1);
    3.48 +by (res_inst_tac [("n","i")] induct 1);
    3.49  by (Simp_tac 1);
    3.50  by (asm_simp_tac (simpset() addsimps [prem]) 1);
    3.51  result();
     4.1 --- a/src/FOL/ex/NatClass.thy	Tue Sep 06 16:29:39 2005 +0200
     4.2 +++ b/src/FOL/ex/NatClass.thy	Tue Sep 06 16:59:48 2005 +0200
     4.3 @@ -34,6 +34,6 @@
     4.4    "m + n == rec(m, n, %x y. Suc(y))"
     4.5  
     4.6  ML {* use_legacy_bindings (the_context ()) *}
     4.7 -ML {* open nat *}
     4.8 +ML {* open nat_class *}
     4.9  
    4.10  end
     5.1 --- a/src/HOL/Algebra/abstract/Ring.thy	Tue Sep 06 16:29:39 2005 +0200
     5.2 +++ b/src/HOL/Algebra/abstract/Ring.thy	Tue Sep 06 16:59:48 2005 +0200
     5.3 @@ -130,7 +130,7 @@
     5.4  proof (induct n)
     5.5    case 0 show ?case by simp
     5.6  next
     5.7 -  case Suc thus ?case by (simp add: semigroup_add.add_assoc) 
     5.8 +  case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) 
     5.9  qed
    5.10  
    5.11  lemma natsum_cong [cong]:
     6.1 --- a/src/HOL/Algebra/abstract/order.ML	Tue Sep 06 16:29:39 2005 +0200
     6.2 +++ b/src/HOL/Algebra/abstract/order.ML	Tue Sep 06 16:59:48 2005 +0200
     6.3 @@ -28,18 +28,18 @@
     6.4  
     6.5  (*** Rewrite rules ***)
     6.6  
     6.7 -val a_assoc = thm "ring.a_assoc";
     6.8 -val l_zero = thm "ring.l_zero";
     6.9 -val l_neg = thm "ring.l_neg";
    6.10 -val a_comm = thm "ring.a_comm";
    6.11 -val m_assoc = thm "ring.m_assoc";
    6.12 -val l_one = thm "ring.l_one";
    6.13 -val l_distr = thm "ring.l_distr";
    6.14 -val m_comm = thm "ring.m_comm";
    6.15 -val minus_def = thm "ring.minus_def";
    6.16 -val inverse_def = thm "ring.inverse_def";
    6.17 -val divide_def = thm "ring.divide_def";
    6.18 -val power_def = thm "ring.power_def";
    6.19 +val a_assoc = thm "ring_class.a_assoc";
    6.20 +val l_zero = thm "ring_class.l_zero";
    6.21 +val l_neg = thm "ring_class.l_neg";
    6.22 +val a_comm = thm "ring_class.a_comm";
    6.23 +val m_assoc = thm "ring_class.m_assoc";
    6.24 +val l_one = thm "ring_class.l_one";
    6.25 +val l_distr = thm "ring_class.l_distr";
    6.26 +val m_comm = thm "ring_class.m_comm";
    6.27 +val minus_def = thm "ring_class.minus_def";
    6.28 +val inverse_def = thm "ring_class.inverse_def";
    6.29 +val divide_def = thm "ring_class.divide_def";
    6.30 +val power_def = thm "ring_class.power_def";
    6.31  
    6.32  (* These are the following axioms:
    6.33  
     7.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Tue Sep 06 16:29:39 2005 +0200
     7.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Tue Sep 06 16:59:48 2005 +0200
     7.3 @@ -21,7 +21,7 @@
     7.4     apply (induct_tac m)
     7.5      apply (simp)
     7.6     apply (force)
     7.7 -  apply (simp add: ab_semigroup_add.add_commute[of m]) 
     7.8 +  apply (simp add: ab_semigroup_add_class.add_commute[of m]) 
     7.9    done
    7.10  
    7.11  end
     8.1 --- a/src/HOL/AxClasses/Group.thy	Tue Sep 06 16:29:39 2005 +0200
     8.2 +++ b/src/HOL/AxClasses/Group.thy	Tue Sep 06 16:59:48 2005 +0200
     8.3 @@ -34,34 +34,34 @@
     8.4  theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
     8.5  proof -
     8.6    have "x [*] invers x = one [*] (x [*] invers x)"
     8.7 -    by (simp only: group.left_unit)
     8.8 +    by (simp only: group_class.left_unit)
     8.9    also have "... = one [*] x [*] invers x"
    8.10 -    by (simp only: semigroup.assoc)
    8.11 +    by (simp only: semigroup_class.assoc)
    8.12    also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
    8.13 -    by (simp only: group.left_inverse)
    8.14 +    by (simp only: group_class.left_inverse)
    8.15    also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
    8.16 -    by (simp only: semigroup.assoc)
    8.17 +    by (simp only: semigroup_class.assoc)
    8.18    also have "... = invers (invers x) [*] one [*] invers x"
    8.19 -    by (simp only: group.left_inverse)
    8.20 +    by (simp only: group_class.left_inverse)
    8.21    also have "... = invers (invers x) [*] (one [*] invers x)"
    8.22 -    by (simp only: semigroup.assoc)
    8.23 +    by (simp only: semigroup_class.assoc)
    8.24    also have "... = invers (invers x) [*] invers x"
    8.25 -    by (simp only: group.left_unit)
    8.26 +    by (simp only: group_class.left_unit)
    8.27    also have "... = one"
    8.28 -    by (simp only: group.left_inverse)
    8.29 +    by (simp only: group_class.left_inverse)
    8.30    finally show ?thesis .
    8.31  qed
    8.32  
    8.33  theorem group_right_unit: "x [*] one = (x::'a::group)"
    8.34  proof -
    8.35    have "x [*] one = x [*] (invers x [*] x)"
    8.36 -    by (simp only: group.left_inverse)
    8.37 +    by (simp only: group_class.left_inverse)
    8.38    also have "... = x [*] invers x [*] x"
    8.39 -    by (simp only: semigroup.assoc)
    8.40 +    by (simp only: semigroup_class.assoc)
    8.41    also have "... = one [*] x"
    8.42      by (simp only: group_right_inverse)
    8.43    also have "... = x"
    8.44 -    by (simp only: group.left_unit)
    8.45 +    by (simp only: group_class.left_unit)
    8.46    finally show ?thesis .
    8.47  qed
    8.48  
    8.49 @@ -72,16 +72,16 @@
    8.50  proof intro_classes
    8.51    fix x y z :: "'a::monoid"
    8.52    show "x [*] y [*] z = x [*] (y [*] z)"
    8.53 -    by (rule monoid.assoc)
    8.54 +    by (rule monoid_class.assoc)
    8.55  qed
    8.56  
    8.57  instance group < monoid
    8.58  proof intro_classes
    8.59    fix x y z :: "'a::group"
    8.60    show "x [*] y [*] z = x [*] (y [*] z)"
    8.61 -    by (rule semigroup.assoc)
    8.62 +    by (rule semigroup_class.assoc)
    8.63    show "one [*] x = x"
    8.64 -    by (rule group.left_unit)
    8.65 +    by (rule group_class.left_unit)
    8.66    show "x [*] one = x"
    8.67      by (rule group_right_unit)
    8.68  qed
    8.69 @@ -118,7 +118,7 @@
    8.70        snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) =
    8.71         (fst p [*] fst (fst q [*] fst r, snd q [*] snd r),
    8.72          snd p [*] snd (fst q [*] fst r, snd q [*] snd r))"
    8.73 -    by (simp add: semigroup.assoc)
    8.74 +    by (simp add: semigroup_class.assoc)
    8.75  qed
    8.76  
    8.77  end
     9.1 --- a/src/HOL/Finite_Set.ML	Tue Sep 06 16:29:39 2005 +0200
     9.2 +++ b/src/HOL/Finite_Set.ML	Tue Sep 06 16:59:48 2005 +0200
     9.3 @@ -51,7 +51,6 @@
     9.4  val empty_foldSetE = thm "empty_foldSetE";
     9.5  val endo_inj_surj = thm "endo_inj_surj";
     9.6  val finite = thm "finite";
     9.7 -val finiteI = thm "finiteI";
     9.8  val finite_Diff = thm "finite_Diff";
     9.9  val finite_Diff_insert = thm "finite_Diff_insert";
    9.10  val finite_Field = thm "finite_Field";
    10.1 --- a/src/HOL/HOL.ML	Tue Sep 06 16:29:39 2005 +0200
    10.2 +++ b/src/HOL/HOL.ML	Tue Sep 06 16:59:48 2005 +0200
    10.3 @@ -5,9 +5,6 @@
    10.4  structure HOL =
    10.5  struct
    10.6    val thy = the_context ();
    10.7 -  val plusI = plusI;
    10.8 -  val minusI = minusI;
    10.9 -  val timesI = timesI;
   10.10    val eq_reflection = eq_reflection;
   10.11    val refl = refl;
   10.12    val subst = subst;
    11.1 --- a/src/HOL/HOL.thy	Tue Sep 06 16:29:39 2005 +0200
    11.2 +++ b/src/HOL/HOL.thy	Tue Sep 06 16:59:48 2005 +0200
    11.3 @@ -686,9 +686,6 @@
    11.4  
    11.5  ML
    11.6  {*
    11.7 -val plusI = thm "plusI"
    11.8 -val minusI = thm "minusI"
    11.9 -val timesI = thm "timesI"
   11.10  val eq_reflection = thm "eq_reflection"
   11.11  val refl = thm "refl"
   11.12  val subst = thm "subst"
    12.1 --- a/src/HOL/Nat.ML	Tue Sep 06 16:29:39 2005 +0200
    12.2 +++ b/src/HOL/Nat.ML	Tue Sep 06 16:59:48 2005 +0200
    12.3 @@ -220,7 +220,6 @@
    12.4  val one_is_add = thm "one_is_add";
    12.5  val one_le_mult_iff = thm "one_le_mult_iff";
    12.6  val one_reorient = thm "one_reorient";
    12.7 -val powerI = thm "powerI";
    12.8  val pred_nat_def = thm "pred_nat_def";
    12.9  val trans_le_add1 = thm "trans_le_add1";
   12.10  val trans_le_add2 = thm "trans_le_add2";
   12.11 @@ -234,4 +233,4 @@
   12.12  val zero_less_diff = thm "zero_less_diff";
   12.13  val zero_less_mult_iff = thm "zero_less_mult_iff";
   12.14  val zero_reorient = thm "zero_reorient";
   12.15 -val linorder_neqE_nat = thm "linorder_neqE_nat";
   12.16 \ No newline at end of file
   12.17 +val linorder_neqE_nat = thm "linorder_neqE_nat";
    13.1 --- a/src/HOL/Tools/refute.ML	Tue Sep 06 16:29:39 2005 +0200
    13.2 +++ b/src/HOL/Tools/refute.ML	Tue Sep 06 16:59:48 2005 +0200
    13.3 @@ -478,7 +478,7 @@
    13.4  					let
    13.5  						(* obtain the axioms generated by the "axclass" command *)
    13.6  						(* (string * Term.term) list *)
    13.7 -						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms
    13.8 +						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (Sign.const_of_class class ^ ".axioms_") s) axioms
    13.9  						(* replace the one schematic type variable in each axiom by the actual type 'T' *)
   13.10  						(* (string * Term.term) list *)
   13.11  						val monomorphic_class_axioms = map (fn (axname, ax) =>
   13.12 @@ -690,7 +690,7 @@
   13.13  							val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
   13.14  							(* Term.term option *)
   13.15  							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
   13.16 -							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
   13.17 +							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, s ^ ".intro")) handle Type.TYPE_MATCH => NONE)
   13.18  							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
   13.19  									(* collect relevant type axioms *)
   13.20  									collect_type_axioms (axs, T)
   13.21 @@ -701,7 +701,7 @@
   13.22  									(* collect relevant type axioms *)
   13.23  									collect_type_axioms (axs', T)
   13.24  								else
   13.25 -									(immediate_output (" " ^ class ^ ".intro");
   13.26 +									(immediate_output (" " ^ s ^ ".intro");
   13.27  									collect_term_axioms (ax :: axs', ax)))
   13.28  						in
   13.29  							axs''