# HG changeset patch
# User huffman
# Date 1322512081 -3600
# Node ID 0ea1c705eebbbe26f95270cd2dfa73f2168a1b82
# Parent  ec6ba4b1f6d58175c6ade8d8b15a693e40ceeca4
use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)

diff -r ec6ba4b1f6d5 -r 0ea1c705eebb src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Nov 28 17:06:29 2011 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Nov 28 21:28:01 2011 +0100
@@ -27,7 +27,7 @@
 
 (*Maps n to #n for n = 0, 1, 2*)
 val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
-val numeral_sym_ss = HOL_ss addsimps numeral_syms;
+val numeral_sym_ss = HOL_basic_ss addsimps numeral_syms;
 
 val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory};
 
@@ -64,6 +64,7 @@
       @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
       @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
       @{thm less_nat_number_of}, 
+      @{thm if_True}, @{thm if_False}, @{thm not_False_eq_True},
       @{thm Let_number_of}, @{thm nat_number_of}] @
      @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
 
@@ -168,7 +169,7 @@
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
 
-  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
+  val numeral_simp_ss = HOL_basic_ss addsimps add_0s @ bin_simps;
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   val simplify_meta_eq  = simplify_meta_eq
   val prove_conv = Arith_Data.prove_conv
@@ -233,7 +234,7 @@
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
 
-  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
+  val numeral_simp_ss = HOL_basic_ss addsimps add_0s @ bin_simps;
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = simplify_meta_eq
 end;
@@ -258,7 +259,7 @@
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
 
-  val numeral_simp_ss = HOL_ss addsimps bin_simps
+  val numeral_simp_ss = HOL_basic_ss addsimps bin_simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = simplify_meta_eq
   val prove_conv = Arith_Data.prove_conv
@@ -339,7 +340,7 @@
   val dest_coeff = dest_coeff
   val find_first = find_first_t []
   val trans_tac = Numeral_Simprocs.trans_tac
-  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
+  val norm_ss = HOL_basic_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq
   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
diff -r ec6ba4b1f6d5 -r 0ea1c705eebb src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon Nov 28 17:06:29 2011 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Nov 28 21:28:01 2011 +0100
@@ -169,7 +169,7 @@
 
 fun numtermless tu = (numterm_ord tu = LESS);
 
-val num_ss = HOL_ss |> Simplifier.set_termless numtermless;
+val num_ss = HOL_basic_ss |> Simplifier.set_termless numtermless;
 
 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
@@ -244,7 +244,7 @@
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
-  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
+  val numeral_simp_ss = HOL_basic_ss addsimps add_0s @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
   val prove_conv = Arith_Data.prove_conv
@@ -296,7 +296,7 @@
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
-  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
+  val numeral_simp_ss = HOL_basic_ss addsimps add_0s @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
 end;
@@ -323,7 +323,7 @@
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
-  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
+  val numeral_simp_ss = HOL_basic_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}, @{thm not_False_eq_True}]
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps
 end;
@@ -340,7 +340,7 @@
 
 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
 struct
-  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
+  val assoc_ss = HOL_basic_ss addsimps @{thms mult_ac}
   val eq_reflection = eq_reflection
   val is_numeral = can HOLogic.dest_number
 end;
@@ -363,8 +363,11 @@
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
-  val numeral_simp_ss = HOL_ss addsimps
+  (* simp_thms are necessary because some of the cancellation rules below
+  (e.g. mult_less_cancel_left) introduce various logical connectives *)
+  val numeral_simp_ss = HOL_basic_ss addsimps
     [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps
+     @ @{thms simp_thms}
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq
     ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps)
@@ -477,7 +480,7 @@
   val dest_coeff = dest_coeff
   val find_first = find_first_t []
   val trans_tac = trans_tac
-  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
+  val norm_ss = HOL_basic_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))