--- a/src/HOL/Word/BinGeneral.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy Mon Apr 20 09:32:07 2009 +0200
@@ -822,8 +822,8 @@
by (induct n) auto
lemma bin_rest_power_trunc [rule_format] :
- "(bin_rest ^ k) (bintrunc n bin) =
- bintrunc (n - k) ((bin_rest ^ k) bin)"
+ "(bin_rest o^ k) (bintrunc n bin) =
+ bintrunc (n - k) ((bin_rest o^ k) bin)"
by (induct k) (auto simp: bin_rest_trunc)
lemma bin_rest_trunc_i:
@@ -857,7 +857,7 @@
by (rule ext) auto
lemma rco_lem:
- "f o g o f = g o f ==> f o (g o f) ^ n = g ^ n o f"
+ "f o g o f = g o f ==> f o (g o f) o^ n = g o^ n o f"
apply (rule ext)
apply (induct_tac n)
apply (simp_all (no_asm))
@@ -867,7 +867,7 @@
apply simp
done
-lemma rco_alt: "(f o g) ^ n o f = f o (g o f) ^ n"
+lemma rco_alt: "(f o g) o^ n o f = f o (g o f) o^ n"
apply (rule ext)
apply (induct n)
apply (simp_all add: o_def)
@@ -891,8 +891,9 @@
subsection {* Miscellaneous lemmas *}
-lemmas funpow_minus_simp =
- trans [OF gen_minus [where f = "power f"] funpow_Suc, standard]
+lemma funpow_minus_simp:
+ "0 < n \<Longrightarrow> f o^ n = f \<circ> f o^ (n - 1)"
+ by (cases n) simp_all
lemmas funpow_pred_simp [simp] =
funpow_minus_simp [of "number_of bin", simplified nobm1, standard]