author paulson Wed, 11 Jan 2006 10:59:55 +0100 changeset 18648 22f96cd085d5 parent 18647 5f5d37e763c4 child 18649 bb99c2e705ca
tidied, and giving theorems names
 src/HOL/Integ/IntDiv.thy file | annotate | diff | comparison | revisions src/HOL/Integ/NatSimprocs.thy file | annotate | diff | comparison | revisions src/HOL/Integ/Parity.thy file | annotate | diff | comparison | revisions src/HOL/Nat.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integ/IntDiv.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -250,16 +250,19 @@
apply (auto simp add: quorem_def mod_def)
done

-lemmas pos_mod_sign[simp]  = pos_mod_conj [THEN conjunct1, standard]
-   and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard]
+lemmas pos_mod_sign  = pos_mod_conj [THEN conjunct1, standard]
+   and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard]
+
+declare pos_mod_sign[simp] pos_mod_bound[simp]

lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
apply (cut_tac a = a and b = b in divAlg_correct)
apply (auto simp add: quorem_def div_def mod_def)
done

-lemmas neg_mod_sign[simp]  = neg_mod_conj [THEN conjunct1, standard]
-   and neg_mod_bound[simp] = neg_mod_conj [THEN conjunct2, standard]
+lemmas neg_mod_sign  = neg_mod_conj [THEN conjunct1, standard]
+   and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard]
+declare neg_mod_sign[simp] neg_mod_bound[simp]

```
```--- a/src/HOL/Integ/NatSimprocs.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -360,7 +360,7 @@
"(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
by auto

-lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2]
+lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
declare half_gt_zero [simp]

(* The following lemma should appear in Divides.thy, but there the proof```
```--- a/src/HOL/Integ/Parity.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Integ/Parity.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -348,10 +348,7 @@
done

lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
-  apply (induct n)
-  apply simp
-  apply auto
-done
+  by (induct n, auto)

lemma power_minus_even [simp]: "even n ==>
(- x)^n = (x^n::'a::{recpower,comm_ring_1})"```
```--- a/src/HOL/Nat.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Nat.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -58,8 +58,8 @@

defs
Zero_nat_def: "0 == Abs_Nat Zero_Rep"
-  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
-  One_nat_def [simp]: "1 == Suc 0"
+  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
+  One_nat_def:  "1 == Suc 0"

-- {* nat operations *}
pred_nat_def: "pred_nat == {(m, n). n = Suc m}"
@@ -68,6 +68,8 @@

le_def: "m \<le> (n::nat) == ~ (n < m)"

+declare One_nat_def [simp]
+

text {* Induction *}
```