tuned;
authorwenzelm
Wed Dec 05 03:06:05 2001 +0100 (2001-12-05)
changeset 1237180ca9058db95
parent 12370 f9e6af324d35
child 12372 cd3a09c7dac9
tuned;
src/FOL/ex/Natural_Numbers.thy
src/HOL/Library/Quotient.thy
src/HOL/Tools/recdef_package.ML
src/Provers/blast.ML
src/Pure/Isar/object_logic.ML
src/Pure/axclass.ML
     1.1 --- a/src/FOL/ex/Natural_Numbers.thy	Wed Dec 05 03:05:39 2001 +0100
     1.2 +++ b/src/FOL/ex/Natural_Numbers.thy	Wed Dec 05 03:06:05 2001 +0100
     1.3 @@ -1,13 +1,18 @@
     1.4  (*  Title:      FOL/ex/Natural_Numbers.thy
     1.5      ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Munich
     1.7 -
     1.8 -Theory of the natural numbers: Peano's axioms, primitive recursion.
     1.9 -(Modernized version of Larry Paulson's theory "Nat".)
    1.10 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.11  *)
    1.12  
    1.13 +header {* Natural numbers *}
    1.14 +
    1.15  theory Natural_Numbers = FOL:
    1.16  
    1.17 +text {*
    1.18 +  Theory of the natural numbers: Peano's axioms, primitive recursion.
    1.19 +  (Modernized version of Larry Paulson's theory "Nat".)  \medskip
    1.20 +*}
    1.21 +
    1.22  typedecl nat
    1.23  arities nat :: "term"
    1.24  
     2.1 --- a/src/HOL/Library/Quotient.thy	Wed Dec 05 03:05:39 2001 +0100
     2.2 +++ b/src/HOL/Library/Quotient.thy	Wed Dec 05 03:06:05 2001 +0100
     2.3 @@ -30,9 +30,9 @@
     2.4  axclass equiv \<subseteq> eqv
     2.5    equiv_refl [intro]: "x \<sim> x"
     2.6    equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
     2.7 -  equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
     2.8 +  equiv_sym [sym]: "x \<sim> y ==> y \<sim> x"
     2.9  
    2.10 -lemma not_equiv_sym [elim?]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    2.11 +lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    2.12  proof -
    2.13    assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
    2.14      by (rule contrapos_nn) (rule equiv_sym)
    2.15 @@ -99,7 +99,7 @@
    2.16   relation.
    2.17  *}
    2.18  
    2.19 -theorem quot_equality: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
    2.20 +theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
    2.21  proof
    2.22    assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
    2.23    show "a \<sim> b"
    2.24 @@ -132,18 +132,6 @@
    2.25    qed
    2.26  qed
    2.27  
    2.28 -lemma quot_equalI [intro?]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
    2.29 -  by (simp only: quot_equality)
    2.30 -
    2.31 -lemma quot_equalD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> b"
    2.32 -  by (simp only: quot_equality)
    2.33 -
    2.34 -lemma quot_not_equalI [intro?]: "\<not> (a \<sim> b) ==> \<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor>"
    2.35 -  by (simp add: quot_equality)
    2.36 -
    2.37 -lemma quot_not_equalD [dest?]: "\<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor> ==> \<not> (a \<sim> b)"
    2.38 -  by (simp add: quot_equality)
    2.39 -
    2.40  
    2.41  subsection {* Picking representing elements *}
    2.42  
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Dec 05 03:05:39 2001 +0100
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Dec 05 03:06:05 2001 +0100
     3.3 @@ -170,12 +170,12 @@
     3.4  
     3.5  in
     3.6  
     3.7 -val (simp_add_global, simp_add_local) = global_local map_simps (Drule.add_rules o single);
     3.8 -val (simp_del_global, simp_del_local) = global_local map_simps (Drule.del_rules o single);
     3.9 +val (simp_add_global, simp_add_local) = global_local map_simps Drule.add_rule;
    3.10 +val (simp_del_global, simp_del_local) = global_local map_simps Drule.del_rule;
    3.11  val (cong_add_global, cong_add_local) = global_local map_congs add_cong;
    3.12  val (cong_del_global, cong_del_local) = global_local map_congs del_cong;
    3.13 -val (wf_add_global, wf_add_local) = global_local map_wfs (Drule.add_rules o single);
    3.14 -val (wf_del_global, wf_del_local) = global_local map_wfs (Drule.del_rules o single);
    3.15 +val (wf_add_global, wf_add_local) = global_local map_wfs Drule.add_rule;
    3.16 +val (wf_del_global, wf_del_local) = global_local map_wfs Drule.del_rule;
    3.17  
    3.18  val simp_attr = mk_attr (simp_add_global, simp_add_local) (simp_del_global, simp_del_local);
    3.19  val cong_attr = mk_attr (cong_add_global, cong_add_local) (cong_del_global, cong_del_local);
     4.1 --- a/src/Provers/blast.ML	Wed Dec 05 03:05:39 2001 +0100
     4.2 +++ b/src/Provers/blast.ML	Wed Dec 05 03:06:05 2001 +0100
     4.3 @@ -62,7 +62,6 @@
     4.4    val rep_cs	: (* dependent on classical.ML *)
     4.5        claset -> {safeIs: thm list, safeEs: thm list, 
     4.6  		 hazIs: thm list, hazEs: thm list,
     4.7 -		 xtraIs: thm list, xtraEs: thm list,
     4.8  		 swrappers: (string * wrapper) list, 
     4.9  		 uwrappers: (string * wrapper) list,
    4.10  		 safe0_netpair: netpair, safep_netpair: netpair,
     5.1 --- a/src/Pure/Isar/object_logic.ML	Wed Dec 05 03:05:39 2001 +0100
     5.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Dec 05 03:06:05 2001 +0100
     5.3 @@ -111,11 +111,11 @@
     5.4  val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
     5.5  val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
     5.6  
     5.7 -val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
     5.8 -val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
     5.9 +val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
    5.10 +val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
    5.11  
    5.12 -fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
    5.13 -fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
    5.14 +fun declare_atomize (thy, th) = (add_atomize th thy, th);
    5.15 +fun declare_rulify (thy, th) = (add_rulify th thy, th);
    5.16  
    5.17  
    5.18  (* atomize *)
     6.1 --- a/src/Pure/axclass.ML	Wed Dec 05 03:05:39 2001 +0100
     6.2 +++ b/src/Pure/axclass.ML	Wed Dec 05 03:06:05 2001 +0100
     6.3 @@ -320,7 +320,7 @@
     6.4    HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
     6.5  
     6.6  val default_method =
     6.7 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some rule")
     6.8 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
     6.9  
    6.10  
    6.11  (* axclass_tac *)