# HG changeset patch # User haftmann # Date 1240212727 -7200 # Node ID 7ab2716dd93b480af62accb0a6dc04254c0fc5d5 # Parent a6e26a248f03cd8136a3f436d03bcd4df60151de power operation on functions with syntax o^; power operation on relations with syntax ^^ diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Bali/Trans.thy --- 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 \ state,nat,term \ state] \ bool" ("_\_ \_ _"[61,82,82] 81) - where "G\p \n p' \ (p,p') \ {(x, y). step G x y}^n" + where "G\p \n p' \ (p,p') \ {(x, y). step G x y}^^n" abbreviation steptr:: "[prog,term \ state,term \ state] \ bool" ("_\_ \* _"[61,82,82] 81) @@ -370,25 +370,6 @@ Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\ *) -lemma rtrancl_imp_rel_pow: "p \ R^* \ \n. p \ R^n" -proof - - assume "p \ R\<^sup>*" - moreover obtain x y where p: "p = (x,y)" by (cases p) - ultimately have "(x,y) \ R\<^sup>*" by hypsubst - hence "\n. (x,y) \ R^n" - proof induct - fix a have "(a,a) \ R^0" by simp - thus "\n. (a,a) \ R ^ n" .. - next - fix a b c assume "\n. (a,b) \ R ^ n" - then obtain n where "(a,b) \ R^n" .. - moreover assume "(b,c) \ R" - ultimately have "(a,c) \ R^(Suc n)" by auto - thus "\n. (a,c) \ R^n" .. - qed - with p show ?thesis by hypsubst -qed - (* lemma imp_eval_trans: assumes eval: "G\s0 \t\\ (v,s1)" diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Decision_Procs/Approximation.thy --- 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 \ nat" and G :: "nat \ nat \ nat" and F :: "nat \ nat" - assumes f_Suc: "\n. f (Suc n) = G ((F^n) s) (f n)" - shows "horner F G n ((F^j') s) (f j') x = (\ j = 0..< n. -1^j * (1 / real (f (j' + j))) * x^j)" + assumes f_Suc: "\n. f (Suc n) = G ((F o^ n) s) (f n)" + shows "horner F G n ((F o^ j') s) (f j') x = (\ 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 \ Ifloat x" and f_Suc: "\n. f (Suc n) = G ((F^n) s) (f n)" + assumes "0 \ Ifloat x" and f_Suc: "\n. f (Suc n) = G ((F o^ n) s) (f n)" and lb_0: "\ i k x. lb 0 i k x = 0" and lb_Suc: "\ 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: "\ i k x. ub 0 i k x = 0" and ub_Suc: "\ 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) \ horner F G n ((F^j') s) (f j') (Ifloat x) \ - horner F G n ((F^j') s) (f j') (Ifloat x) \ Ifloat (ub n ((F^j') s) (f j') x)" + shows "Ifloat (lb n ((F o^ j') s) (f j') x) \ horner F G n ((F o^ j') s) (f j') (Ifloat x) \ + horner F G n ((F o^ j') s) (f j') (Ifloat x) \ Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?lb n j' \ ?horner n j' \ ?horner n j' \ ?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'))) \ 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 \ Ifloat x` - show "- Ifloat (x * ub n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) x) \ - (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) \ - (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' \ ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps Ifloat_sub diff_def proof (rule add_mono) show "1 / real (f j') \ 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 \ Ifloat x` - show "- (Ifloat x * horner F G n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) (Ifloat x)) \ - - 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)) \ + - 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 \ nat" and G :: "nat \ nat \ nat" - assumes "0 \ Ifloat x" and f_Suc: "\n. f (Suc n) = G ((F^n) s) (f n)" + assumes "0 \ Ifloat x" and f_Suc: "\n. f (Suc n) = G ((F o^ n) s) (f n)" and lb_0: "\ i k x. lb 0 i k x = 0" and lb_Suc: "\ 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: "\ i k x. ub 0 i k x = 0" and ub_Suc: "\ 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) \ (\j=0..j=0.. Ifloat (ub n ((F^j') s) (f j') x)" (is "?ub") + shows "Ifloat (lb n ((F o^ j') s) (f j') x) \ (\j=0..j=0.. Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub") proof - have "?lb \ ?ub" using horner_bounds'[where lb=lb, OF `0 \ Ifloat x` f_Suc lb_0 lb_Suc ub_0 ub_Suc] @@ -88,13 +88,13 @@ qed lemma horner_bounds_nonpos: fixes F :: "nat \ nat" and G :: "nat \ nat \ nat" - assumes "Ifloat x \ 0" and f_Suc: "\n. f (Suc n) = G ((F^n) s) (f n)" + assumes "Ifloat x \ 0" and f_Suc: "\n. f (Suc n) = G ((F o^ n) s) (f n)" and lb_0: "\ i k x. lb 0 i k x = 0" and lb_Suc: "\ 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: "\ i k x. ub 0 i k x = 0" and ub_Suc: "\ 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) \ (\j=0..j=0.. Ifloat (ub n ((F^j') s) (f j') x)" (is "?ub") + shows "Ifloat (lb n ((F o^ j') s) (f j') x) \ (\j=0..j=0.. 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: "(\j=0..j=0..j = 0.. {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 \ {Ifloat l .. Ifloat u}" - shows "x^n \ {Ifloat l1..Ifloat u1}" + shows "x ^ n \ {Ifloat l1..Ifloat u1}" proof (cases "even n") case True show ?thesis proof (cases "0 < l") case True hence "odd n \ 0 < l" and "0 \ 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 \ 0 < l`] by auto - have "Ifloat l^n \ x^n" and "x^n \ Ifloat u^n " using `0 \ 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 \ x ^ n" and "x ^ n \ Ifloat u ^ n " using `0 \ 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: "\ (odd n \ 0 < l)" using `even n` by auto show ?thesis proof (cases "u < 0") case True hence "0 \ - Ifloat u" and "- Ifloat u \ - x" and "0 \ - x" and "-x \ - Ifloat l" using assms unfolding less_float_def by auto - hence "Ifloat u^n \ x^n" and "x^n \ Ifloat l^n" using power_mono[of "-x" "-Ifloat l" n] power_mono[of "-Ifloat u" "-x" n] + hence "Ifloat u ^ n \ x ^ n" and "x ^ n \ 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 \ 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 \ 0 < l`] by auto - have "Ifloat l^n \ x^n" and "x^n \ Ifloat u^n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto + have "Ifloat l ^ n \ x ^ n" and "x ^ n \ 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: "\ x l u. (l1, u1) = float_power_bnds n l u \ x \ {Ifloat l .. Ifloat u} \ Ifloat l1 \ x^n \ x^n \ Ifloat u1" +lemma bnds_power: "\ x l u. (l1, u1) = float_power_bnds n l u \ x \ {Ifloat l .. Ifloat u} \ Ifloat l1 \ x ^ n \ x ^ n \ 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: "\m. ((\i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto) - have "?f (Suc n) = ?f n * ((\i. i + 2) ^ n) 1 * (((\i. i + 2) ^ n) 1 + 1)" + have F: "\m. ((\i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto) + have "?f (Suc n) = ?f n * ((\i. i + 2) o^ n) 1 * (((\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 "(\ i=0.. i=0.. 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 + (\ j = 0 ..< n. 0)" by auto @@ -905,8 +905,8 @@ let "?f n" = "fact (2 * n + 1)" { fix n - have F: "\m. ((\i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto) - have "?f (Suc n) = ?f n * ((\i. i + 2) ^ n) 2 * (((\i. i + 2) ^ n) 2 + 1)" + have F: "\m. ((\i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto) + have "?f (Suc n) = ?f n * ((\i. i + 2) o^ n) 2 * (((\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) \ { 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: "\ m. ((\i. i + 1) ^ n) m = n + m" by (induct n, auto) - have "fact (Suc n) = fact n * ((\i. i + 1) ^ n) 1" unfolding F by auto } note f_eq = this + have F: "\ m. ((\i. i + 1) o^ n) m = n + m" by (induct n, auto) + have "fact (Suc n) = fact n * ((\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 \ x" and "x < 1" - shows "(\i=0..<2*n. -1^i * (1 / real (i + 1)) * x^(Suc i)) \ ln (x + 1)" (is "?lb") - and "ln (x + 1) \ (\i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x^(Suc i))" (is "?ub") + shows "(\i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \ ln (x + 1)" (is "?lb") + and "ln (x + 1) \ (\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: "(\ i. -1^i * ?a i) = ln (x + 1)" using ln_series[of "x + 1"] `0 \ 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') diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/HoareParallel/OG_Tran.thy --- 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 \ 'a) \ nat \ ('a ann_com_op \ 'a) \ bool" ("_ -_\ _"[81,81] 100) where - "con_0 -n\ con_1 \ (con_0, con_1) \ ann_transition^n" + "con_0 -n\ con_1 \ (con_0, con_1) \ ann_transition ^^ n" abbreviation ann_transitions :: "('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a) \ bool" @@ -84,7 +84,7 @@ abbreviation transition_n :: "('a com \ 'a) \ nat \ ('a com \ 'a) \ bool" ("_ -P_\ _"[81,81,81] 100) where - "con_0 -Pn\ con_1 \ (con_0, con_1) \ transition^n" + "con_0 -Pn\ con_1 \ (con_0, con_1) \ transition ^^ n" subsection {* Definition of Semantics *} diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/IMP/Compiler0.thy --- 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] \ bool" ("_ \/ (3\_,_\/ -(_)\ \_,_\)" [50,0,0,0,0,0] 50) where - "P \ \s,m\ -(i)\ \t,n\ == ((s,m),t,n) : ((stepa1 P)^i)" + "P \ \s,m\ -(i)\ \t,n\ == ((s,m),t,n) : (stepa1 P ^^ i)" subsection "The compiler" diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/IMP/Machines.thy --- 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 \ (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) \ R^n) = (n=0 \ z=x \ (\m y. n = Suc m \ (x,y) \ R \ (y,z) \ R^m))" + "((x,z) \ R ^^ n) = (n=0 \ z=x \ (\m y. n = Suc m \ (x,y) \ R \ (y,z) \ 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: "\ (x,y) \ R^m; (y,z) \ R^n \ \ (x,z) \ R^(m+n)" +lemma rel_pow_plusI: + "\ (x,y) \ R ^^ m; (y,z) \ R ^^ n \ \ (x,z) \ 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] \ bool" ("(_/ \ (1\_,/_\)/ -_\ (1\_,/_\))" [50,0,0,0,0] 50) where - "p \ \i,s\ -n\ \j,t\ == ((i,s),j,t) : (exec01 p)^n" + "p \ \i,s\ -n\ \j,t\ == ((i,s),j,t) : (exec01 p)^^n" subsection "M0 with lists" @@ -89,7 +90,7 @@ abbreviation stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \ bool" ("((1\_,/_,/_\)/ -_\ (1\_,/_,/_\))" 50) where - "\p,q,s\ -i\ \p',q',t\ == ((p,q,s),p',q',t) : (stepa1^i)" + "\p,q,s\ -i\ \p',q',t\ == ((p,q,s),p',q',t) : (stepa1^^i)" inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1" diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/IMP/Transition.thy --- 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\state),nat,(com option\state)] \ bool" ("_ -_\\<^sub>1 _" [60,60,60] 60) where - "cs -n\\<^sub>1 cs' == (cs,cs') \ evalc1^n" + "cs -n\\<^sub>1 cs' == (cs,cs') \ evalc1^^n" abbreviation evalc' :: "[(com option\state),(com option\state)] \ bool" @@ -77,28 +76,9 @@ "cs \\<^sub>1\<^sup>* cs' == (cs,cs') \ evalc1^*" (*<*) -(* fixme: move to Relation_Power.thy *) -lemma rel_pow_Suc_E2 [elim!]: - "[| (x, z) \ R ^ Suc n; !!y. [| (x, y) \ R; (y, z) \ R ^ n |] ==> P |] ==> P" - by (blast dest: rel_pow_Suc_D2) +declare rel_pow_Suc_E2 [elim!] +(*>*) -lemma rtrancl_imp_rel_pow: "p \ R^* \ \n. p \ R^n" -proof (induct p) - fix x y - assume "(x, y) \ R\<^sup>*" - thus "\n. (x, y) \ R^n" - proof induct - fix a have "(a, a) \ R^0" by simp - thus "\n. (a, a) \ R ^ n" .. - next - fix a b c assume "\n. (a, b) \ R ^ n" - then obtain n where "(a, b) \ R^n" .. - moreover assume "(b, c) \ R" - ultimately have "(a, c) \ R^(Suc n)" by auto - thus "\n. (a, c) \ 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]: "\s\ -n\\<^sub>1 y = (n = 0 \ y = \s\)" diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Import/HOL/HOL4Base.thy --- 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 diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Import/HOL/HOL4Word32.thy --- 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 - diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Import/HOL4Compat.thy --- 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) diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Coinductive_List.thy --- 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 \ '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) \ - {((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 "\ = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))" + also have "\ = 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 "\ = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))" + also have "\ = 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 diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Continuity.thy --- 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 \ lfp F" + { fix i have "(F o^ i) bot \ lfp F" proof (induct i) - show "(F^^0) bot \ lfp F" by simp + show "(F o^ 0) bot \ 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 "\ \ F(lfp F)" by(rule monoD[OF mono Suc]) also have "\ = lfp F" by(simp add:lfp_unfold[OF mono, symmetric]) finally show ?case . qed } - hence "(SUP i. (F^^i) bot) \ lfp F" by (blast intro!:SUP_leI) - moreover have "lfp F \ (SUP i. (F^^i) bot)" (is "_ \ ?U") + hence "(SUP i. (F o^ i) bot) \ lfp F" by (blast intro!:SUP_leI) + moreover have "lfp F \ (SUP i. (F o^ i) bot)" (is "_ \ ?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 \ (F^^(Suc i)) bot" + { fix i have "(F o^ i) bot \ (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 "\ \ ?U" by(fast intro:SUP_leI le_SUPI) finally show "F ?U \ ?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) diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Formal_Power_Series.thy --- 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 (\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 (\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 (\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)*} diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Library/Topology_Euclidean_Space.thy --- 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 \ s" by auto - def z \ "\ n::nat. fun_pow n f z0" + def z \ "\ n::nat. funpow n f z0" { fix n::nat have "z n \ s" unfolding z_def proof(induct n) case 0 thus ?case using `z0 \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 \ "g x" have [simp]:"y\s" unfolding y_def using gs[unfolded image_subset_iff] and `x\s` by blast - def f \ "\ n. fun_pow n g" + def f \ "\ n. funpow n g" have [simp]:"\n z. g (f n z) = f (Suc n) z" unfolding f_def by auto have [simp]:"\z. f 0 z = z" unfolding f_def by auto { fix n::nat and z assume "z\s" diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/List.thy --- 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 \ 'a list \ 'a list" where - "rotate n = rotate1 ^^ n" + "rotate n = rotate1 o^ n" definition list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/SizeChange/Interpretation.thy --- 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: "\x. \accp R x \ \accp R (f x)" by blast - let ?s = "\i. (f ^ i) x" + let ?s = "\i. (f o^ i) x" { fix i diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/UNITY/Comp.thy --- 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 \ H == \G. F\G = H" - strict_component_def: "(F < (H::'a program)) == (F \ H & F \ H)" +definition + component_def: "F \ H <-> (\G. F\G = H)" +definition + strict_component_def: "F < (H::'a program) <-> (F \ H & F \ 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" diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/UNITY/Transformers.thy --- 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 == \i \ atMost k. ((wp act)^i) B" + "wens_single_finite act B k == \i \ atMost k. (wp act o^ i) B" wens_single :: "[('a*'a) set, 'a set] => 'a set" - "wens_single act B == \i. ((wp act)^i) B" + "wens_single act B == \i. (wp act o^ i) B" lemma wens_single_Un_eq: "single_valued act diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/BinBoolList.thy --- 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) diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/BinGeneral.thy --- 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 \ f o^ n = f \ f o^ (n - 1)" + by (cases n) simp_all lemmas funpow_pred_simp [simp] = funpow_minus_simp [of "number_of bin", simplified nobm1, standard] diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/TdThs.thy --- 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) diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/WordDefinition.thy --- 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 \ word_of_int (2^len_of TYPE('a) - 1)" + "max_word \ word_of_int (2 ^ len_of TYPE('a) - 1)" consts of_bool :: "bool \ 'a::len word" diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/Word/WordShift.thy --- 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)