author paulson Tue, 20 Jul 2004 14:23:09 +0200 changeset 15067 02be3516e90b parent 15066 d2f2b908e0a4 child 15068 58d216b32199
removed some obsolete proofs
 src/HOL/Library/Word.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Library/Word.thy	Tue Jul 20 14:22:49 2004 +0200
+++ b/src/HOL/Library/Word.thy	Tue Jul 20 14:23:09 2004 +0200
@@ -9,15 +9,13 @@

subsection {* Auxilary Lemmas *}

-text {* Amazing that these are necessary, but I can't find equivalent
-ones in the other HOL theories. *}
-
lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z"

lemma max_mono:
+  fixes x :: "'a::linorder"
assumes mf: "mono f"
-  shows       "max (f (x::'a::linorder)) (f y) \<le> f (max x y)"
+  shows       "max (f x) (f y) \<le> f (max x y)"
proof -
from mf and le_maxI1 [of x y]
have fx: "f x \<le> f (max x y)"
@@ -30,209 +28,8 @@
by auto
qed

-lemma le_imp_power_le:
-  assumes b0: "0 < (b::nat)"
-  and     xy: "x \<le> y"
-  shows       "b ^ x \<le> b ^ y"
-proof (rule ccontr)
-  assume "~ b ^ x \<le> b ^ y"
-  hence bybx: "b ^ y < b ^ x"
-    by simp
-  have "y < x"
-  proof (rule nat_power_less_imp_less [OF _ bybx])
-    from b0
-    show "0 < b"
-      .
-  qed
-  with xy
-  show False
-    by simp
-qed
-
-lemma less_imp_power_less:
-  assumes b1: "1 < (b::nat)"
-  and     xy: "x < y"
-  shows       "b ^ x < b ^ y"
-proof (rule ccontr)
-  assume "~ b ^ x < b ^ y"
-  hence bybx: "b ^ y \<le> b ^ x"
-    by simp
-  have "y \<le> x"
-  proof (rule power_le_imp_le_exp [OF _ bybx])
-    from b1
-    show "1 < b"
-      .
-  qed
-  with xy
-  show False
-    by simp
-qed
-
-lemma [simp]: "1 < (b::nat) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
-  apply rule
-  apply (erule power_le_imp_le_exp)
-  apply assumption
-  apply (subgoal_tac "0 < b")
-  apply (erule le_imp_power_le)
-  apply assumption
-  apply simp
-  done
-
-lemma [simp]: "1 < (b::nat) ==> (b ^ x < b ^ y) = (x < y)"
-  apply rule
-  apply (subgoal_tac "0 < b")
-  apply (erule nat_power_less_imp_less)
-  apply assumption
-  apply simp
-  apply (erule less_imp_power_less)
-  apply assumption
-  done
-
-lemma power_le_imp_zle:
-  assumes b1:   "1 < (b::int)"
-  and     bxby: "b ^ x \<le> b ^ y"
-  shows         "x \<le> y"
-proof -
-  from b1
-  have nb1: "1 < nat b"
-    by arith
-  from b1
-  have nb0: "0 \<le> b"
-    by simp
-  from bxby
-  have "nat (b ^ x) \<le> nat (b ^ y)"
-    by arith
-  hence "nat b ^ x \<le> nat b ^ y"
-    by (simp add: nat_power_eq [OF nb0])
-  with power_le_imp_le_exp and nb1
-  show "x \<le> y"
-    by auto
-qed
-
-lemma zero_le_zpower [intro]:
-  assumes b0: "0 \<le> (b::int)"
-  shows       "0 \<le> b ^ n"
-proof (induct n,simp)
-  fix n
-  assume ind: "0 \<le> b ^ n"
-  have "b * 0 \<le> b * b ^ n"
-  proof (subst mult_le_cancel_left,auto intro!: ind)
-    assume "b < 0"
-    with b0
-    show "b ^ n \<le> 0"
-      by simp
-  qed
-  thus "0 \<le> b ^ Suc n"
-    by simp
-qed
-
-lemma zero_less_zpower [intro]:
-  assumes b0: "0 < (b::int)"
-  shows       "0 < b ^ n"
-proof -
-  from b0
-  have b0': "0 \<le> b"
-    by simp
-  from b0
-  have "0 < nat b"
-    by simp
-  hence "0 < nat b ^ n"
-    by (rule zero_less_power)
-  hence xx: "nat 0 < nat (b ^ n)"
-    by (subst nat_power_eq [OF b0'],simp)
-  show "0 < b ^ n"
-    apply (subst nat_less_eq_zless [symmetric])
-    apply simp
-    apply (rule xx)
-    done
-qed
-
-lemma power_less_imp_zless:
-  assumes b0:   "0 < (b::int)"
-  and     bxby: "b ^ x < b ^ y"
-  shows         "x < y"
-proof -
-  from b0
-  have nb0: "0 < nat b"
-    by arith
-  from b0
-  have b0': "0 \<le> b"
-    by simp
-  have "nat (b ^ x) < nat (b ^ y)"
-  proof (subst nat_less_eq_zless)
-    show "0 \<le> b ^ x"
-      by (rule zero_le_zpower [OF b0'])
-  next
-    show "b ^ x < b ^ y"
-      by (rule bxby)
-  qed
-  hence "nat b ^ x < nat b ^ y"
-    by (simp add: nat_power_eq [OF b0'])
-  with nat_power_less_imp_less [OF nb0]
-  show "x < y"
-    .
-qed
-
-lemma le_imp_power_zle:
-  assumes b0: "0 < (b::int)"
-  and     xy: "x \<le> y"
-  shows       "b ^ x \<le> b ^ y"
-proof (rule ccontr)
-  assume "~ b ^ x \<le> b ^ y"
-  hence bybx: "b ^ y < b ^ x"
-    by simp
-  have "y < x"
-  proof (rule power_less_imp_zless [OF _ bybx])
-    from b0
-    show "0 < b"
-      .
-  qed
-  with xy
-  show False
-    by simp
-qed
-
-lemma less_imp_power_zless:
-  assumes b1: "1 < (b::int)"
-  and     xy: "x < y"
-  shows       "b ^ x < b ^ y"
-proof (rule ccontr)
-  assume "~ b ^ x < b ^ y"
-  hence bybx: "b ^ y \<le> b ^ x"
-    by simp
-  have "y \<le> x"
-  proof (rule power_le_imp_zle [OF _ bybx])
-    from b1
-    show "1 < b"
-      .
-  qed
-  with xy
-  show False
-    by simp
-qed
-
-lemma [simp]: "1 < (b::int) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
-  apply rule
-  apply (erule power_le_imp_zle)
-  apply assumption
-  apply (subgoal_tac "0 < b")
-  apply (erule le_imp_power_zle)
-  apply assumption
-  apply simp
-  done
-
-lemma [simp]: "1 < (b::int) ==> (b ^ x < b ^ y) = (x < y)"
-  apply rule
-  apply (subgoal_tac "0 < b")
-  apply (erule power_less_imp_zless)
-  apply assumption
-  apply simp
-  apply (erule less_imp_power_zless)
-  apply assumption
-  done
-
-lemma suc_zero_le: "[| 0 < x ; 0 < y |] ==> Suc 0 < x + y"
-  by simp
+declare zero_le_power [intro]
+    and zero_less_power [intro]

lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
by (induct k,simp_all)
@@ -1405,7 +1202,7 @@
apply simp
apply (rule order_trans [of _ 0])
apply simp
-    apply (rule zero_le_zpower,simp)
+    apply (rule zero_le_power,simp)
apply simp
apply simp
apply (simp del: bv_to_nat1 bv_to_nat_helper)
@@ -1707,10 +1504,7 @@
by arith
hence a: "k - 1 \<le> length (int_to_bv i) - 2"
by arith
-  have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)"
-    apply (rule le_imp_power_zle,simp)
-    apply (rule a)
-    done
+  hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp
also have "... \<le> i"
proof -
have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)"
@@ -1793,7 +1587,7 @@
shows       "k < length (int_to_bv i)"
proof (rule ccontr)
have "0 < (2::int) ^ (k - 1)"
-    by (rule zero_less_zpower,simp)
+    by (rule zero_less_power,simp)
also have "... \<le> i"
by (rule wk)
finally have i0: "0 < i"
@@ -1816,10 +1610,8 @@
by (rule bv_to_int_upper_range)
finally show ?thesis .
qed
-  also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)"
-    apply (rule le_imp_power_zle,simp)
-    apply (rule a)
-    done
+  also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a
+         by simp
finally have "i < 2 ^ (k - 1)" .
with wk
show False
@@ -1851,10 +1643,8 @@
qed
also have "... \<le> -(2 ^ (k - 1))"
proof -
-    have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)"
-      apply (rule le_imp_power_zle,simp)
-      apply (rule a)
-      done
+    have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a
+      by simp
thus ?thesis
by simp
qed
@@ -1874,7 +1664,7 @@
also have "... < -1"
proof -
have "0 < (2::int) ^ (k - 1)"
-      by (rule zero_less_zpower,simp)
+      by (rule zero_less_power,simp)
hence "-((2::int) ^ (k - 1)) < 0"
by simp
thus ?thesis by simp
@@ -1890,10 +1680,7 @@
with lii0
have a: "length (int_to_bv i) - 1 \<le> k - 1"
by arith
-  have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)"
-    apply (rule le_imp_power_zle,simp)
-    apply (rule a)
-    done
+  hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp
hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))"
by simp
also have "... \<le> i"
@@ -2003,8 +1790,7 @@
proof -
have "bv_to_int w < 2 ^ (length w - 1)"
by (rule bv_to_int_upper_range)
-      also have "... \<le> 2 ^ length w"
-	by (rule le_imp_power_zle,simp_all)
+      also have "... \<le> 2 ^ length w" by simp
finally show "bv_to_int w \<le> 2 ^ length w"
by simp
qed
@@ -2301,7 +2087,7 @@
apply (rule mult_strict_mono)
apply (rule bv_to_int_upper_range)
apply (rule bv_to_int_upper_range)
-	  apply (rule zero_less_zpower)
+	  apply (rule zero_less_power)
apply simp
using bi2
apply simp
@@ -2329,7 +2115,7 @@
apply simp
using bv_to_int_lower_range [of w2]
apply simp
-	  apply (rule zero_le_zpower,simp)
+	  apply (rule zero_le_power,simp)
using bi2
apply simp
done
@@ -2380,7 +2166,7 @@
apply simp
using bv_to_int_upper_range [of w1]
apply simp
-	    apply (rule zero_le_zpower,simp)
+	    apply (rule zero_le_power,simp)
using bi1
apply simp
done
@@ -2397,7 +2183,7 @@
apply simp
using bv_to_int_upper_range [of w2]
apply simp
-	    apply (rule zero_le_zpower,simp)
+	    apply (rule zero_le_power,simp)
using bi2
apply simp
done
@@ -2418,7 +2204,7 @@
apply (subgoal_tac "0 + 0 < 2 ^ length list + bv_to_nat list")
apply simp
-  apply (rule zero_less_zpower)
+  apply (rule zero_less_power)
apply simp_all
done

@@ -2455,7 +2241,7 @@
apply (rule bv_to_nat_upper_range)
apply (rule bv_to_int_upper_range)
-	  apply (rule zero_less_zpower,simp)
+	  apply (rule zero_less_power,simp)
using biw2
apply simp
done
@@ -2521,7 +2307,7 @@