dropped lemma duplicates in HOL.thy
authorhaftmann
Wed Jan 31 16:05:10 2007 +0100 (2007-01-31)
changeset 2221830a8890d2967
parent 22217 a5d983f7113f
child 22219 61b5bab471ce
dropped lemma duplicates in HOL.thy
NEWS
src/HOL/Bali/Evaln.thy
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/Inductive.thy
src/HOL/Integ/NatBin.thy
src/HOL/Tools/res_axioms.ML
     1.1 --- a/NEWS	Wed Jan 31 14:03:31 2007 +0100
     1.2 +++ b/NEWS	Wed Jan 31 16:05:10 2007 +0100
     1.3 @@ -507,11 +507,17 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10 +* Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj.
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13  * Added syntactic class "size"; overloaded constant "size" now has
    1.14  type "'a::size ==> bool"
    1.15  
    1.16  * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
    1.17 -dvd" to "Divides.div", "Divides.mod" and
    1.18 +dvd" to "Divides.div", "Divides.mod" and "Divides.dvd"
    1.19  "Divides.dvd". INCOMPATIBILITY.
    1.20  
    1.21  * Added method "lexicographic_order" automatically synthesizes
     2.1 --- a/src/HOL/Bali/Evaln.thy	Wed Jan 31 14:03:31 2007 +0100
     2.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Jan 31 16:05:10 2007 +0100
     2.3 @@ -191,7 +191,7 @@
     2.4            \<Longrightarrow>
     2.5  		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
     2.6  monos
     2.7 -  if_def2
     2.8 +  if_bool_eq_conj
     2.9  
    2.10  
    2.11  declare split_if     [split del] split_if_asm     [split del]
     3.1 --- a/src/HOL/HOL.ML	Wed Jan 31 14:03:31 2007 +0100
     3.2 +++ b/src/HOL/HOL.ML	Wed Jan 31 16:05:10 2007 +0100
     3.3 @@ -14,7 +14,6 @@
     3.4  val cong = thm "cong"
     3.5  val conj_comms = thms "conj_comms";
     3.6  val conj_cong = thm "conj_cong";
     3.7 -val def_imp_eq = thm "def_imp_eq";
     3.8  val de_Morgan_conj = thm "de_Morgan_conj";
     3.9  val de_Morgan_disj = thm "de_Morgan_disj";
    3.10  val disj_assoc = thm "disj_assoc";
     4.1 --- a/src/HOL/HOL.thy	Wed Jan 31 14:03:31 2007 +0100
     4.2 +++ b/src/HOL/HOL.thy	Wed Jan 31 16:05:10 2007 +0100
     4.3 @@ -249,12 +249,6 @@
     4.4  lemma trans: "[| r=s; s=t |] ==> r=t"
     4.5    by (erule subst)
     4.6  
     4.7 -lemma def_imp_eq:
     4.8 -  assumes meq: "A == B"
     4.9 -  shows "A = B"
    4.10 -  by (unfold meq) (rule refl)
    4.11 -
    4.12 -(*a mere copy*)
    4.13  lemma meta_eq_to_obj_eq: 
    4.14    assumes meq: "A == B"
    4.15    shows "A = B"
    4.16 @@ -818,7 +812,7 @@
    4.17    val dest_Trueprop = HOLogic.dest_Trueprop
    4.18    val dest_imp = HOLogic.dest_imp
    4.19    val eq_reflection = @{thm HOL.eq_reflection}
    4.20 -  val rev_eq_reflection = @{thm HOL.def_imp_eq}
    4.21 +  val rev_eq_reflection = @{thm HOL.meta_eq_to_obj_eq}
    4.22    val imp_intr = @{thm HOL.impI}
    4.23    val rev_mp = @{thm HOL.rev_mp}
    4.24    val subst = @{thm HOL.subst}
    4.25 @@ -1381,9 +1375,6 @@
    4.26  
    4.27  subsection {* Other simple lemmas and lemma duplicates *}
    4.28  
    4.29 -lemmas eq_sym_conv = eq_commute
    4.30 -lemmas if_def2 = if_bool_eq_conj
    4.31 -
    4.32  lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
    4.33    by blast+
    4.34  
    4.35 @@ -1410,6 +1401,8 @@
    4.36    shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
    4.37    by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
    4.38  
    4.39 +lemmas eq_sym_conv = eq_commute
    4.40 +
    4.41  
    4.42  subsection {* Basic ML bindings *}
    4.43  
     5.1 --- a/src/HOL/Inductive.thy	Wed Jan 31 14:03:31 2007 +0100
     5.2 +++ b/src/HOL/Inductive.thy	Wed Jan 31 16:05:10 2007 +0100
     5.3 @@ -64,7 +64,7 @@
     5.4  setup OldInductivePackage.setup
     5.5  
     5.6  theorems basic_monos [mono] =
     5.7 -  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
     5.8 +  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
     5.9    Collect_mono in_mono vimage_mono
    5.10    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    5.11    not_all not_ex
    5.12 @@ -75,7 +75,7 @@
    5.13  setup InductivePackage.setup
    5.14  
    5.15  theorems [mono2] =
    5.16 -  imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    5.17 +  imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    5.18    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    5.19    not_all not_ex
    5.20    Ball_def Bex_def
     6.1 --- a/src/HOL/Integ/NatBin.thy	Wed Jan 31 14:03:31 2007 +0100
     6.2 +++ b/src/HOL/Integ/NatBin.thy	Wed Jan 31 16:05:10 2007 +0100
     6.3 @@ -823,7 +823,7 @@
     6.4    "neg ((number_of Numeral.Min) \<Colon> int)"
     6.5    by auto
     6.6  
     6.7 -lemmas nat_number_expand = nat_number Let_def if_def2 if_True if_False
     6.8 +lemmas nat_number_expand = nat_number Let_def if_bool_eq_conj if_True if_False
     6.9    neg_number_of_Pls neg_number_of_Min neg_number_of_BIT Nat.plus.simps
    6.10  
    6.11  ML {*
     7.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jan 31 14:03:31 2007 +0100
     7.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jan 31 16:05:10 2007 +0100
     7.3 @@ -176,7 +176,8 @@
     7.4  
     7.5  (*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
     7.6    where some types have the empty sort.*)
     7.7 -fun mk_object_eq th = th RS def_imp_eq
     7.8 +val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
     7.9 +fun mk_object_eq th = th RS meta_eq_to_obj_eq
    7.10      handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
    7.11  
    7.12  (*Apply a function definition to an argument, beta-reducing the result.*)