# HG changeset patch
# User huffman
# Date 1179675021 -7200
# Node ID e98ed26577a2acb1e89b8d456925315a191df224
# Parent  722f583795384f96fdfe118ef9ba81def05ee549
add lemma power2_eq_imp_eq

diff -r 722f58379538 -r e98ed26577a2 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Sun May 20 13:39:46 2007 +0200
+++ b/src/HOL/Integ/NatBin.thy	Sun May 20 17:30:21 2007 +0200
@@ -336,6 +336,11 @@
   shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
 by (rule power_less_imp_less_base)
 
+lemma power2_eq_imp_eq:
+  fixes x y :: "'a::{ordered_semidom,recpower}"
+  shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
+unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
+
 lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
 apply (induct "n")
 apply (auto simp add: power_Suc power_add power2_minus)