power operation on functions with syntax o^; power operation on relations with syntax ^^
--- a/src/HOL/Bali/Trans.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Bali/Trans.thy Mon Apr 20 09:32:07 2009 +0200
@@ -359,7 +359,7 @@
abbreviation
stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
- where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^n"
+ where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n"
abbreviation
steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
@@ -370,25 +370,6 @@
Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
*)
-lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
-proof -
- assume "p \<in> R\<^sup>*"
- moreover obtain x y where p: "p = (x,y)" by (cases p)
- ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
- hence "\<exists>n. (x,y) \<in> R^n"
- proof induct
- fix a have "(a,a) \<in> R^0" by simp
- thus "\<exists>n. (a,a) \<in> R ^ n" ..
- next
- fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
- then obtain n where "(a,b) \<in> R^n" ..
- moreover assume "(b,c) \<in> R"
- ultimately have "(a,c) \<in> R^(Suc n)" by auto
- thus "\<exists>n. (a,c) \<in> R^n" ..
- qed
- with p show ?thesis by hypsubst
-qed
-
(*
lemma imp_eval_trans:
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Apr 20 09:32:07 2009 +0200
@@ -23,8 +23,8 @@
qed
lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
- assumes f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
- shows "horner F G n ((F^j') s) (f j') x = (\<Sum> j = 0..< n. -1^j * (1 / real (f (j' + j))) * x^j)"
+ assumes f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
+ shows "horner F G n ((F o^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / real (f (j' + j))) * x ^ j)"
proof (induct n arbitrary: i k j')
case (Suc n)
@@ -33,13 +33,13 @@
qed auto
lemma horner_bounds':
- assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
+ assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
and lb_0: "\<And> i k x. lb 0 i k x = 0"
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
and ub_0: "\<And> i k x. ub 0 i k x = 0"
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
- shows "Ifloat (lb n ((F^j') s) (f j') x) \<le> horner F G n ((F^j') s) (f j') (Ifloat x) \<and>
- horner F G n ((F^j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F^j') s) (f j') x)"
+ shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> horner F G n ((F o^ j') s) (f j') (Ifloat x) \<and>
+ horner F G n ((F o^ j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)"
(is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'")
proof (induct n arbitrary: j')
case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
@@ -49,15 +49,15 @@
proof (rule add_mono)
show "Ifloat (lapprox_rat prec 1 (int (f j'))) \<le> 1 / real (f j')" using lapprox_rat[of prec 1 "int (f j')"] by auto
from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \<le> Ifloat x`
- show "- Ifloat (x * ub n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) x) \<le> - (Ifloat x * horner F G n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) (Ifloat x))"
+ show "- Ifloat (x * ub n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) x) \<le> - (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x))"
unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
qed
moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps Ifloat_sub diff_def
proof (rule add_mono)
show "1 / real (f j') \<le> Ifloat (rapprox_rat prec 1 (int (f j')))" using rapprox_rat[of 1 "int (f j')" prec] by auto
from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> Ifloat x`
- show "- (Ifloat x * horner F G n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) (Ifloat x)) \<le>
- - Ifloat (x * lb n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) x)"
+ show "- (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x)) \<le>
+ - Ifloat (x * lb n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) x)"
unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
qed
ultimately show ?case by blast
@@ -73,13 +73,13 @@
*}
lemma horner_bounds: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
+ assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
and lb_0: "\<And> i k x. lb 0 i k x = 0"
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
and ub_0: "\<And> i k x. ub 0 i k x = 0"
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
- shows "Ifloat (lb n ((F^j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1^j * (1 / real (f (j' + j))) * (Ifloat x)^j)" (is "?lb") and
- "(\<Sum>j=0..<n. -1^j * (1 / real (f (j' + j))) * (Ifloat x)^j) \<le> Ifloat (ub n ((F^j') s) (f j') x)" (is "?ub")
+ shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
+ "(\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub")
proof -
have "?lb \<and> ?ub"
using horner_bounds'[where lb=lb, OF `0 \<le> Ifloat x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
@@ -88,13 +88,13 @@
qed
lemma horner_bounds_nonpos: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
+ assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
and lb_0: "\<And> i k x. lb 0 i k x = 0"
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) + x * (ub n (F i) (G i k) x)"
and ub_0: "\<And> i k x. ub 0 i k x = 0"
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) + x * (lb n (F i) (G i k) x)"
- shows "Ifloat (lb n ((F^j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j)" (is "?lb") and
- "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j) \<le> Ifloat (ub n ((F^j') s) (f j') x)" (is "?ub")
+ shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
+ "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub")
proof -
{ fix x y z :: float have "x - y * z = x + - y * z"
by (cases x, cases y, cases z, simp add: plus_float.simps minus_float.simps uminus_float.simps times_float.simps algebra_simps)
@@ -104,13 +104,13 @@
have move_minus: "Ifloat (-x) = -1 * Ifloat x" by auto
- have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j) =
+ have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j) =
(\<Sum>j = 0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j)"
proof (rule setsum_cong, simp)
fix j assume "j \<in> {0 ..< n}"
show "1 / real (f (j' + j)) * Ifloat x ^ j = -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j"
unfolding move_minus power_mult_distrib real_mult_assoc[symmetric]
- unfolding real_mult_commute unfolding real_mult_assoc[of "-1^j", symmetric] power_mult_distrib[symmetric]
+ unfolding real_mult_commute unfolding real_mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
by auto
qed
@@ -160,21 +160,21 @@
else (0, (max (-l) u) ^ n))"
lemma float_power_bnds: assumes "(l1, u1) = float_power_bnds n l u" and "x \<in> {Ifloat l .. Ifloat u}"
- shows "x^n \<in> {Ifloat l1..Ifloat u1}"
+ shows "x ^ n \<in> {Ifloat l1..Ifloat u1}"
proof (cases "even n")
case True
show ?thesis
proof (cases "0 < l")
case True hence "odd n \<or> 0 < l" and "0 \<le> Ifloat l" unfolding less_float_def by auto
have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
- have "Ifloat l^n \<le> x^n" and "x^n \<le> Ifloat u^n " using `0 \<le> Ifloat l` and assms unfolding atLeastAtMost_iff using power_mono[of "Ifloat l" x] power_mono[of x "Ifloat u"] by auto
+ have "Ifloat l ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat u ^ n " using `0 \<le> Ifloat l` and assms unfolding atLeastAtMost_iff using power_mono[of "Ifloat l" x] power_mono[of x "Ifloat u"] by auto
thus ?thesis using assms `0 < l` unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
next
case False hence P: "\<not> (odd n \<or> 0 < l)" using `even n` by auto
show ?thesis
proof (cases "u < 0")
case True hence "0 \<le> - Ifloat u" and "- Ifloat u \<le> - x" and "0 \<le> - x" and "-x \<le> - Ifloat l" using assms unfolding less_float_def by auto
- hence "Ifloat u^n \<le> x^n" and "x^n \<le> Ifloat l^n" using power_mono[of "-x" "-Ifloat l" n] power_mono[of "-Ifloat u" "-x" n]
+ hence "Ifloat u ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat l ^ n" using power_mono[of "-x" "-Ifloat l" n] power_mono[of "-Ifloat u" "-x" n]
unfolding power_minus_even[OF `even n`] by auto
moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
ultimately show ?thesis using float_power by auto
@@ -194,11 +194,11 @@
next
case False hence "odd n \<or> 0 < l" by auto
have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
- have "Ifloat l^n \<le> x^n" and "x^n \<le> Ifloat u^n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto
+ have "Ifloat l ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat u ^ n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto
thus ?thesis unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
qed
-lemma bnds_power: "\<forall> x l u. (l1, u1) = float_power_bnds n l u \<and> x \<in> {Ifloat l .. Ifloat u} \<longrightarrow> Ifloat l1 \<le> x^n \<and> x^n \<le> Ifloat u1"
+lemma bnds_power: "\<forall> x l u. (l1, u1) = float_power_bnds n l u \<and> x \<in> {Ifloat l .. Ifloat u} \<longrightarrow> Ifloat l1 \<le> x ^ n \<and> x ^ n \<le> Ifloat u1"
using float_power_bnds by auto
section "Square root"
@@ -794,8 +794,8 @@
let "?f n" = "fact (2 * n)"
{ fix n
- have F: "\<And>m. ((\<lambda>i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
- have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^ n) 1 * (((\<lambda>i. i + 2) ^ n) 1 + 1)"
+ have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
+ have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 1 * (((\<lambda>i. i + 2) o^ n) 1 + 1)"
unfolding F by auto } note f_eq = this
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
@@ -811,7 +811,7 @@
have "0 < x * x" using `0 < x` unfolding less_float_def Ifloat_mult Ifloat_0
using mult_pos_pos[where a="Ifloat x" and b="Ifloat x"] by auto
- { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i))
+ { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
= (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
proof -
have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
@@ -905,8 +905,8 @@
let "?f n" = "fact (2 * n + 1)"
{ fix n
- have F: "\<And>m. ((\<lambda>i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
- have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^ n) 2 * (((\<lambda>i. i + 2) ^ n) 2 + 1)"
+ have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
+ have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 2 * (((\<lambda>i. i + 2) o^ n) 2 + 1)"
unfolding F by auto } note f_eq = this
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
@@ -1382,8 +1382,8 @@
shows "exp (Ifloat x) \<in> { Ifloat (lb_exp_horner prec (get_even n) 1 1 x) .. Ifloat (ub_exp_horner prec (get_odd n) 1 1 x) }"
proof -
{ fix n
- have F: "\<And> m. ((\<lambda>i. i + 1) ^ n) m = n + m" by (induct n, auto)
- have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^ n) 1" unfolding F by auto } note f_eq = this
+ have F: "\<And> m. ((\<lambda>i. i + 1) o^ n) m = n + m" by (induct n, auto)
+ have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) o^ n) 1" unfolding F by auto } note f_eq = this
note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
@@ -1631,10 +1631,10 @@
lemma ln_bounds:
assumes "0 \<le> x" and "x < 1"
- shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x^(Suc i)) \<le> ln (x + 1)" (is "?lb")
- and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x^(Suc i))" (is "?ub")
+ shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
+ and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
proof -
- let "?a n" = "(1/real (n +1)) * x^(Suc n)"
+ let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)"
using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
@@ -2479,7 +2479,7 @@
fun lift_var (Free (varname, _)) = (case AList.lookup (op =) bound_eqs varname of
SOME bound => bound
| NONE => raise TERM ("No bound equations found for " ^ varname, []))
- | lift_var t = raise TERM ("Can not convert expression " ^
+ | lift_var t = raise TERM ("Can not convert expression " ^
(Syntax.string_of_term ctxt t), [t])
val _ $ vs = HOLogic.dest_Trueprop (Logic.strip_imp_concl goal')
--- a/src/HOL/HoareParallel/OG_Tran.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/HoareParallel/OG_Tran.thy Mon Apr 20 09:32:07 2009 +0200
@@ -74,7 +74,7 @@
abbreviation
ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a)
\<Rightarrow> bool" ("_ -_\<rightarrow> _"[81,81] 100) where
- "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition^n"
+ "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition ^^ n"
abbreviation
ann_transitions :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool"
@@ -84,7 +84,7 @@
abbreviation
transition_n :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"
("_ -P_\<rightarrow> _"[81,81,81] 100) where
- "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition^n"
+ "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition ^^ n"
subsection {* Definition of Semantics *}
--- a/src/HOL/IMP/Compiler0.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/IMP/Compiler0.thy Mon Apr 20 09:32:07 2009 +0200
@@ -45,7 +45,7 @@
abbreviation
stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50) where
- "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^i)"
+ "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : (stepa1 P ^^ i)"
subsection "The compiler"
--- a/src/HOL/IMP/Machines.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/IMP/Machines.thy Mon Apr 20 09:32:07 2009 +0200
@@ -1,7 +1,6 @@
-
-(* $Id$ *)
-
-theory Machines imports Natural begin
+theory Machines
+imports Natural
+begin
lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
by (fast intro: rtrancl_into_rtrancl elim: rtranclE)
@@ -11,20 +10,22 @@
lemmas converse_rel_powE = rel_pow_E2
-lemma R_O_Rn_commute: "R O R^n = R^n O R"
+lemma R_O_Rn_commute: "R O R ^^ n = R ^^ n O R"
by (induct n) (simp, simp add: O_assoc [symmetric])
lemma converse_in_rel_pow_eq:
- "((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
+ "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
apply(rule iffI)
apply(blast elim:converse_rel_powE)
apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
done
-lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
+lemma rel_pow_plus:
+ "R ^^ (m+n) = R ^^ n O R ^^ m"
by (induct n) (simp, simp add: O_assoc)
-lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
+lemma rel_pow_plusI:
+ "\<lbrakk> (x,y) \<in> R ^^ m; (y,z) \<in> R ^^ n \<rbrakk> \<Longrightarrow> (x,z) \<in> R ^^ (m+n)"
by (simp add: rel_pow_plus rel_compI)
subsection "Instructions"
@@ -57,7 +58,7 @@
abbreviation
exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) where
- "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^n"
+ "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^^n"
subsection "M0 with lists"
@@ -89,7 +90,7 @@
abbreviation
stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
- "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^i)"
+ "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^^i)"
inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1"
--- a/src/HOL/IMP/Transition.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/IMP/Transition.thy Mon Apr 20 09:32:07 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/IMP/Transition.thy
- ID: $Id$
Author: Tobias Nipkow & Robert Sandner, TUM
Isar Version: Gerwin Klein, 2001
Copyright 1996 TUM
@@ -69,7 +68,7 @@
abbreviation
evalcn :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60) where
- "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^n"
+ "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^^n"
abbreviation
evalc' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
@@ -77,28 +76,9 @@
"cs \<longrightarrow>\<^sub>1\<^sup>* cs' == (cs,cs') \<in> evalc1^*"
(*<*)
-(* fixme: move to Relation_Power.thy *)
-lemma rel_pow_Suc_E2 [elim!]:
- "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
- by (blast dest: rel_pow_Suc_D2)
+declare rel_pow_Suc_E2 [elim!]
+(*>*)
-lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
-proof (induct p)
- fix x y
- assume "(x, y) \<in> R\<^sup>*"
- thus "\<exists>n. (x, y) \<in> R^n"
- proof induct
- fix a have "(a, a) \<in> R^0" by simp
- thus "\<exists>n. (a, a) \<in> R ^ n" ..
- next
- fix a b c assume "\<exists>n. (a, b) \<in> R ^ n"
- then obtain n where "(a, b) \<in> R^n" ..
- moreover assume "(b, c) \<in> R"
- ultimately have "(a, c) \<in> R^(Suc n)" by auto
- thus "\<exists>n. (a, c) \<in> R^n" ..
- qed
-qed
-(*>*)
text {*
As for the big step semantics you can read these rules in a
syntax directed way:
@@ -189,8 +169,8 @@
(*<*)
(* FIXME: relpow.simps don't work *)
lemmas [simp del] = relpow.simps
-lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by (simp add: relpow.simps)
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by (simp add: relpow.simps)
+lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R ^^ 0 = Id" by (simp add: relpow.simps)
+lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R ^^ Suc 0 = R" by (simp add: relpow.simps)
(*>*)
lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
--- a/src/HOL/Import/HOL/HOL4Base.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy Mon Apr 20 09:32:07 2009 +0200
@@ -2794,8 +2794,8 @@
by (import numeral numeral_fact)
lemma numeral_funpow: "ALL n::nat.
- ((f::'a::type => 'a::type) ^ n) (x::'a::type) =
- (if n = 0 then x else (f ^ (n - 1)) (f x))"
+ ((f::'a::type => 'a::type) o^ n) (x::'a::type) =
+ (if n = 0 then x else (f o^ (n - 1)) (f x))"
by (import numeral numeral_funpow)
;end_setup
--- a/src/HOL/Import/HOL/HOL4Word32.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Mon Apr 20 09:32:07 2009 +0200
@@ -434,15 +434,15 @@
by (import word32 EQUIV_QT)
lemma FUNPOW_THM: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
- (f ^ n) (f x) = f ((f ^ n) x)"
+ (f o^ n) (f x) = f ((f o^ n) x)"
by (import word32 FUNPOW_THM)
lemma FUNPOW_THM2: "ALL (f::'a::type => 'a::type) (n::nat) x::'a::type.
- (f ^ Suc n) x = f ((f ^ n) x)"
+ (f o^ Suc n) x = f ((f o^ n) x)"
by (import word32 FUNPOW_THM2)
lemma FUNPOW_COMP: "ALL (f::'a::type => 'a::type) (m::nat) (n::nat) a::'a::type.
- (f ^ m) ((f ^ n) a) = (f ^ (m + n)) a"
+ (f o^ m) ((f o^ n) a) = (f o^ (m + n)) a"
by (import word32 FUNPOW_COMP)
lemma INw_MODw: "ALL n::nat. INw (MODw n)"
@@ -1170,23 +1170,23 @@
constdefs
word_lsr :: "word32 => nat => word32"
- "word_lsr == %(a::word32) n::nat. (word_lsr1 ^ n) a"
+ "word_lsr == %(a::word32) n::nat. (word_lsr1 o^ n) a"
-lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 ^ n) a"
+lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 o^ n) a"
by (import word32 word_lsr)
constdefs
word_asr :: "word32 => nat => word32"
- "word_asr == %(a::word32) n::nat. (word_asr1 ^ n) a"
+ "word_asr == %(a::word32) n::nat. (word_asr1 o^ n) a"
-lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 ^ n) a"
+lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 o^ n) a"
by (import word32 word_asr)
constdefs
word_ror :: "word32 => nat => word32"
- "word_ror == %(a::word32) n::nat. (word_ror1 ^ n) a"
+ "word_ror == %(a::word32) n::nat. (word_ror1 o^ n) a"
-lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 ^ n) a"
+lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 o^ n) a"
by (import word32 word_ror)
consts
@@ -1583,4 +1583,3 @@
;end_setup
end
-
--- a/src/HOL/Import/HOL4Compat.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Mon Apr 20 09:32:07 2009 +0200
@@ -202,19 +202,13 @@
constdefs
FUNPOW :: "('a => 'a) => nat => 'a => 'a"
- "FUNPOW f n == f ^ n"
+ "FUNPOW f n == f o^ n"
-lemma FUNPOW: "(ALL f x. (f ^ 0) x = x) &
- (ALL f n x. (f ^ Suc n) x = (f ^ n) (f x))"
-proof auto
- fix f n x
- have "ALL x. f ((f ^ n) x) = (f ^ n) (f x)"
- by (induct n,auto)
- thus "f ((f ^ n) x) = (f ^ n) (f x)"
- ..
-qed
+lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
+ (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
+ by (simp add: funpow_swap1)
-lemma [hol4rew]: "FUNPOW f n = f ^ n"
+lemma [hol4rew]: "FUNPOW f n = f o^ n"
by (simp add: FUNPOW_def)
lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
@@ -224,7 +218,7 @@
by simp
lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
- by (simp, arith)
+ by (simp) arith
lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
by (simp add: max_def)
--- a/src/HOL/Library/Coinductive_List.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy Mon Apr 20 09:32:07 2009 +0200
@@ -786,7 +786,7 @@
lemma funpow_lmap:
fixes f :: "'a \<Rightarrow> 'a"
- shows "(lmap f ^ n) (LCons b l) = LCons ((f ^ n) b) ((lmap f ^ n) l)"
+ shows "(lmap f o^ n) (LCons b l) = LCons ((f o^ n) b) ((lmap f o^ n) l)"
by (induct n) simp_all
@@ -796,35 +796,35 @@
proof
fix x
have "(h x, iterates f x) \<in>
- {((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u)) | u n. True}"
+ {((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u)) | u n. True}"
proof -
- have "(h x, iterates f x) = ((lmap f ^ 0) (h x), (lmap f ^ 0) (iterates f x))"
+ have "(h x, iterates f x) = ((lmap f o^ 0) (h x), (lmap f o^ 0) (iterates f x))"
by simp
then show ?thesis by blast
qed
then show "h x = iterates f x"
proof (coinduct rule: llist_equalityI)
case (Eqllist q)
- then obtain u n where "q = ((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u))"
+ then obtain u n where "q = ((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u))"
(is "_ = (?q1, ?q2)")
by auto
- also have "?q1 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (h u))"
+ also have "?q1 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (h u))"
proof -
- have "?q1 = (lmap f ^ n) (LCons u (lmap f (h u)))"
+ have "?q1 = (lmap f o^ n) (LCons u (lmap f (h u)))"
by (subst h) rule
- also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))"
+ also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (lmap f (h u)))"
by (rule funpow_lmap)
- also have "(lmap f ^ n) (lmap f (h u)) = (lmap f ^ Suc n) (h u)"
+ also have "(lmap f o^ n) (lmap f (h u)) = (lmap f o^ Suc n) (h u)"
by (simp add: funpow_swap1)
finally show ?thesis .
qed
- also have "?q2 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (iterates f u))"
+ also have "?q2 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (iterates f u))"
proof -
- have "?q2 = (lmap f ^ n) (LCons u (iterates f (f u)))"
+ have "?q2 = (lmap f o^ n) (LCons u (iterates f (f u)))"
by (subst iterates) rule
- also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))"
+ also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (iterates f (f u)))"
by (rule funpow_lmap)
- also have "(lmap f ^ n) (iterates f (f u)) = (lmap f ^ Suc n) (iterates f u)"
+ also have "(lmap f o^ n) (iterates f (f u)) = (lmap f o^ Suc n) (iterates f u)"
by (simp add: lmap_iterates funpow_swap1)
finally show ?thesis .
qed
--- a/src/HOL/Library/Continuity.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Continuity.thy Mon Apr 20 09:32:07 2009 +0200
@@ -5,7 +5,7 @@
header {* Continuity and iterations (of set transformers) *}
theory Continuity
-imports Relation_Power Main
+imports Transitive_Closure Main
begin
subsection {* Continuity for complete lattices *}
@@ -48,25 +48,25 @@
qed
lemma continuous_lfp:
- assumes "continuous F" shows "lfp F = (SUP i. (F^^i) bot)"
+ assumes "continuous F" shows "lfp F = (SUP i. (F o^ i) bot)"
proof -
note mono = continuous_mono[OF `continuous F`]
- { fix i have "(F^^i) bot \<le> lfp F"
+ { fix i have "(F o^ i) bot \<le> lfp F"
proof (induct i)
- show "(F^^0) bot \<le> lfp F" by simp
+ show "(F o^ 0) bot \<le> lfp F" by simp
next
case (Suc i)
- have "(F^^(Suc i)) bot = F((F^^i) bot)" by simp
+ have "(F o^ Suc i) bot = F((F o^ i) bot)" by simp
also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
finally show ?case .
qed }
- hence "(SUP i. (F^^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
- moreover have "lfp F \<le> (SUP i. (F^^i) bot)" (is "_ \<le> ?U")
+ hence "(SUP i. (F o^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
+ moreover have "lfp F \<le> (SUP i. (F o^ i) bot)" (is "_ \<le> ?U")
proof (rule lfp_lowerbound)
- have "chain(%i. (F^^i) bot)"
+ have "chain(%i. (F o^ i) bot)"
proof -
- { fix i have "(F^^i) bot \<le> (F^^(Suc i)) bot"
+ { fix i have "(F o^ i) bot \<le> (F o^ (Suc i)) bot"
proof (induct i)
case 0 show ?case by simp
next
@@ -74,7 +74,7 @@
qed }
thus ?thesis by(auto simp add:chain_def)
qed
- hence "F ?U = (SUP i. (F^^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
+ hence "F ?U = (SUP i. (F o^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
finally show "F ?U \<le> ?U" .
qed
@@ -193,7 +193,7 @@
definition
up_iterate :: "('a set => 'a set) => nat => 'a set" where
- "up_iterate f n = (f^^n) {}"
+ "up_iterate f n = (f o^ n) {}"
lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
by (simp add: up_iterate_def)
@@ -245,7 +245,7 @@
definition
down_iterate :: "('a set => 'a set) => nat => 'a set" where
- "down_iterate f n = (f^^n) UNIV"
+ "down_iterate f n = (f o^ n) UNIV"
lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
by (simp add: down_iterate_def)
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Apr 20 09:32:07 2009 +0200
@@ -1022,13 +1022,15 @@
lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) = fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)"
by simp
-lemma XDN_linear: "(XD^n) (fps_const c * a + fps_const d * b) = fps_const c * (XD^n) a + fps_const d * (XD^n) (b :: ('a::comm_ring_1) fps)"
+lemma XDN_linear:
+ "(XD o^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD o^ n) a + fps_const d * (XD o^ n) (b :: ('a::comm_ring_1) fps)"
by (induct n, simp_all)
lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff)
-lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
-by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
+lemma fps_mult_XD_shift:
+ "(XD o^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+ by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Apr 20 09:32:07 2009 +0200
@@ -5441,7 +5441,7 @@
have "1 - c > 0" using c by auto
from s(2) obtain z0 where "z0 \<in> s" by auto
- def z \<equiv> "\<lambda> n::nat. fun_pow n f z0"
+ def z \<equiv> "\<lambda> n::nat. funpow n f z0"
{ fix n::nat
have "z n \<in> s" unfolding z_def
proof(induct n) case 0 thus ?case using `z0 \<in>s` by auto
@@ -5580,7 +5580,7 @@
using dist[THEN bspec[where x=x], THEN bspec[where x=y]] by auto } note dist' = this
def y \<equiv> "g x"
have [simp]:"y\<in>s" unfolding y_def using gs[unfolded image_subset_iff] and `x\<in>s` by blast
- def f \<equiv> "\<lambda> n. fun_pow n g"
+ def f \<equiv> "\<lambda> n. funpow n g"
have [simp]:"\<And>n z. g (f n z) = f (Suc n) z" unfolding f_def by auto
have [simp]:"\<And>z. f 0 z = z" unfolding f_def by auto
{ fix n::nat and z assume "z\<in>s"
--- a/src/HOL/List.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/List.thy Mon Apr 20 09:32:07 2009 +0200
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Relation_Power Presburger Recdef ATP_Linkup
+imports Plain Presburger Recdef ATP_Linkup
uses "Tools/string_syntax.ML"
begin
@@ -198,7 +198,7 @@
definition
rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "rotate n = rotate1 ^^ n"
+ "rotate n = rotate1 o^ n"
definition
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
--- a/src/HOL/SizeChange/Interpretation.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/SizeChange/Interpretation.thy Mon Apr 20 09:32:07 2009 +0200
@@ -35,7 +35,7 @@
and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)"
by blast
- let ?s = "\<lambda>i. (f ^ i) x"
+ let ?s = "\<lambda>i. (f o^ i) x"
{
fix i
--- a/src/HOL/UNITY/Comp.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/UNITY/Comp.thy Mon Apr 20 09:32:07 2009 +0200
@@ -15,14 +15,22 @@
header{*Composition: Basic Primitives*}
-theory Comp imports Union begin
+theory Comp
+imports Union
+begin
-instance program :: (type) ord ..
+instantiation program :: (type) ord
+begin
-defs
- component_def: "F \<le> H == \<exists>G. F\<squnion>G = H"
- strict_component_def: "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
+definition
+ component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
+definition
+ strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
+
+instance ..
+
+end
constdefs
component_of :: "'a program =>'a program=> bool"
@@ -114,7 +122,7 @@
by (auto simp add: stable_def component_constrains)
(*Used in Guar.thy to show that programs are partially ordered*)
-lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
+lemmas program_less_le = strict_component_def
subsection{*The preserves property*}
@@ -229,8 +237,7 @@
apply (blast intro: Join_assoc [symmetric])
done
-lemmas strict_component_of_eq =
- strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
+lemmas strict_component_of_eq = strict_component_of_def
(** localize **)
lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
--- a/src/HOL/UNITY/Transformers.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy Mon Apr 20 09:32:07 2009 +0200
@@ -338,10 +338,10 @@
constdefs
wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"
- "wens_single_finite act B k == \<Union>i \<in> atMost k. ((wp act)^i) B"
+ "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act o^ i) B"
wens_single :: "[('a*'a) set, 'a set] => 'a set"
- "wens_single act B == \<Union>i. ((wp act)^i) B"
+ "wens_single act B == \<Union>i. (wp act o^ i) B"
lemma wens_single_Un_eq:
"single_valued act
--- a/src/HOL/Word/BinBoolList.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy Mon Apr 20 09:32:07 2009 +0200
@@ -38,7 +38,7 @@
if y then rbl_add ws x else ws)"
lemma butlast_power:
- "(butlast ^ n) bl = take (length bl - n) bl"
+ "(butlast o^ n) bl = take (length bl - n) bl"
by (induct n) (auto simp: butlast_take)
lemma bin_to_bl_aux_Pls_minus_simp [simp]:
@@ -370,14 +370,14 @@
done
lemma nth_rest_power_bin [rule_format] :
- "ALL n. bin_nth ((bin_rest ^ k) w) n = bin_nth w (n + k)"
+ "ALL n. bin_nth ((bin_rest o^ k) w) n = bin_nth w (n + k)"
apply (induct k, clarsimp)
apply clarsimp
apply (simp only: bin_nth.Suc [symmetric] add_Suc)
done
lemma take_rest_power_bin:
- "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^ (n - m)) w)"
+ "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest o^ (n - m)) w)"
apply (rule nth_equalityI)
apply simp
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
--- 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]
--- a/src/HOL/Word/TdThs.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/TdThs.thy Mon Apr 20 09:32:07 2009 +0200
@@ -110,7 +110,7 @@
done
lemma fn_comm_power:
- "fa o tr = tr o fr ==> fa ^ n o tr = tr o fr ^ n"
+ "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n"
apply (rule ext)
apply (induct n)
apply (auto dest: fun_cong)
--- a/src/HOL/Word/WordDefinition.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy Mon Apr 20 09:32:07 2009 +0200
@@ -207,10 +207,10 @@
"shiftr1 w = word_of_int (bin_rest (uint w))"
definition
- shiftl_def: "w << n = (shiftl1 ^ n) w"
+ shiftl_def: "w << n = (shiftl1 o^ n) w"
definition
- shiftr_def: "w >> n = (shiftr1 ^ n) w"
+ shiftr_def: "w >> n = (shiftr1 o^ n) w"
instance ..
@@ -245,7 +245,7 @@
"bshiftr1 b w == of_bl (b # butlast (to_bl w))"
sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
- "w >>> n == (sshiftr1 ^ n) w"
+ "w >>> n == (sshiftr1 o^ n) w"
mask :: "nat => 'a::len word"
"mask n == (1 << n) - 1"
@@ -268,7 +268,7 @@
case ys of [] => [] | x # xs => last ys # butlast ys"
rotater :: "nat => 'a list => 'a list"
- "rotater n == rotater1 ^ n"
+ "rotater n == rotater1 o^ n"
word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
"word_rotr n w == of_bl (rotater n (to_bl w))"
@@ -303,7 +303,7 @@
constdefs
-- "Largest representable machine integer."
max_word :: "'a::len word"
- "max_word \<equiv> word_of_int (2^len_of TYPE('a) - 1)"
+ "max_word \<equiv> word_of_int (2 ^ len_of TYPE('a) - 1)"
consts
of_bool :: "bool \<Rightarrow> 'a::len word"
--- a/src/HOL/Word/WordShift.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/WordShift.thy Mon Apr 20 09:32:07 2009 +0200
@@ -361,14 +361,14 @@
lemma shiftr_no':
"w = number_of bin ==>
- (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
+ (w::'a::len0 word) >> n = number_of ((bin_rest o^ n) (bintrunc (size w) bin))"
apply clarsimp
apply (rule word_eqI)
apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
done
lemma sshiftr_no':
- "w = number_of bin ==> w >>> n = number_of ((bin_rest ^ n)
+ "w = number_of bin ==> w >>> n = number_of ((bin_rest o^ n)
(sbintrunc (size w - 1) bin))"
apply clarsimp
apply (rule word_eqI)