1.1 --- a/src/HOL/Algebra/poly/PolyHomo.ML Fri Oct 05 23:58:52 2001 +0200
1.2 +++ b/src/HOL/Algebra/poly/PolyHomo.ML Sat Oct 06 00:02:46 2001 +0200
1.3 @@ -112,15 +112,15 @@
1.4 (* Examples *)
1.5
1.6 Goal
1.7 - "EVAL (x::'a::domain) (a*X^# 2 + b*X^1 + c*X^0) = a * x ^ # 2 + b * x ^ 1 + c";
1.8 + "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
1.9 by (asm_simp_tac (simpset() delsimps [power_Suc]
1.10 addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
1.11 result();
1.12
1.13 Goal
1.14 "EVAL (y::'a::domain) \
1.15 -\ (EVAL (const x) (monom 1 + const (a*X^# 2 + b*X^1 + c*X^0))) = \
1.16 -\ x ^ 1 + (a * y ^ # 2 + b * y ^ 1 + c)";
1.17 +\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
1.18 +\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
1.19 by (asm_simp_tac (simpset() delsimps [power_Suc]
1.20 addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
1.21 result();
2.1 --- a/src/HOL/Auth/KerberosIV.thy Fri Oct 05 23:58:52 2001 +0200
2.2 +++ b/src/HOL/Auth/KerberosIV.thy Sat Oct 06 00:02:46 2001 +0200
2.3 @@ -65,8 +65,8 @@
2.4 RespLife :: nat
2.5
2.6 rules
2.7 - AuthLife_LB "# 2 <= AuthLife"
2.8 - ServLife_LB "# 2 <= ServLife"
2.9 + AuthLife_LB "2 <= AuthLife"
2.10 + ServLife_LB "2 <= ServLife"
2.11 AutcLife_LB "Suc 0 <= AutcLife"
2.12 RespLife_LB "Suc 0 <= RespLife"
2.13
3.1 --- a/src/HOL/Auth/Kerberos_BAN.thy Fri Oct 05 23:58:52 2001 +0200
3.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy Sat Oct 06 00:02:46 2001 +0200
3.3 @@ -30,7 +30,7 @@
3.4
3.5 rules
3.6 (*The ticket should remain fresh for two journeys on the network at least*)
3.7 - SesKeyLife_LB "# 2 <= SesKeyLife"
3.8 + SesKeyLife_LB "2 <= SesKeyLife"
3.9
3.10 (*The authenticator only for one journey*)
3.11 AutLife_LB "Suc 0 <= AutLife"
4.1 --- a/src/HOL/GroupTheory/Exponent.ML Fri Oct 05 23:58:52 2001 +0200
4.2 +++ b/src/HOL/GroupTheory/Exponent.ML Sat Oct 06 00:02:46 2001 +0200
4.3 @@ -205,13 +205,13 @@
4.4 by (induct_tac "n" 1);
4.5 by (Asm_simp_tac 1);
4.6 by (Asm_full_simp_tac 1);
4.7 -by (subgoal_tac "# 2 * n + # 2 <= p * p^n" 1);
4.8 +by (subgoal_tac "2 * n + 2 <= p * p^n" 1);
4.9 by (Asm_full_simp_tac 1);
4.10 -by (subgoal_tac "# 2 * p^n <= p * p^n" 1);
4.11 +by (subgoal_tac "2 * p^n <= p * p^n" 1);
4.12 (*?arith_tac should handle all of this!*)
4.13 by (rtac order_trans 1);
4.14 by (assume_tac 2);
4.15 -by (dres_inst_tac [("k","# 2")] mult_le_mono2 1);
4.16 +by (dres_inst_tac [("k","2")] mult_le_mono2 1);
4.17 by (Asm_full_simp_tac 1);
4.18 by (rtac mult_le_mono1 1);
4.19 by (Asm_full_simp_tac 1);
5.1 --- a/src/HOL/Hoare/Arith2.ML Fri Oct 05 23:58:52 2001 +0200
5.2 +++ b/src/HOL/Hoare/Arith2.ML Sat Oct 06 00:02:46 2001 +0200
5.3 @@ -63,7 +63,7 @@
5.4
5.5 (*** pow ***)
5.6
5.7 -Goal "m mod # 2 = 0 ==> ((n::nat)*n)^(m div # 2) = n^m";
5.8 +Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
5.9 by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
5.10 mult_div_cancel]) 1);
5.11 qed "sq_pow_div2";
6.1 --- a/src/HOL/Hoare/Examples.ML Fri Oct 05 23:58:52 2001 +0200
6.2 +++ b/src/HOL/Hoare/Examples.ML Sat Oct 06 00:02:46 2001 +0200
6.3 @@ -50,9 +50,9 @@
6.4 Goal "|- VARS a b x y. \
6.5 \ {0<A & 0<B & a=A & b=B & x=B & y=A} \
6.6 \ WHILE a ~= b \
6.7 -\ INV {0<a & 0<b & gcd A B = gcd a b & # 2*A*B = a*x + b*y} \
6.8 +\ INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y} \
6.9 \ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \
6.10 -\ {a = gcd A B & # 2*A*B = a*(x+y)}";
6.11 +\ {a = gcd A B & 2*A*B = a*(x+y)}";
6.12 by (hoare_tac (K all_tac) 1);
6.13 by(Asm_simp_tac 1);
6.14 by(asm_simp_tac (simpset() addsimps
6.15 @@ -68,9 +68,9 @@
6.16 \ c := (1::nat); \
6.17 \ WHILE b ~= 0 \
6.18 \ INV {A^B = c * a^b} \
6.19 -\ DO WHILE b mod # 2 = 0 \
6.20 +\ DO WHILE b mod 2 = 0 \
6.21 \ INV {A^B = c * a^b} \
6.22 -\ DO a := a*a; b := b div # 2 OD; \
6.23 +\ DO a := a*a; b := b div 2 OD; \
6.24 \ c := c*a; b := b - 1 \
6.25 \ OD \
6.26 \ {c = A^B}";
6.27 @@ -114,7 +114,7 @@
6.28 \ x := X; u := 1; w := 1; r := (0::nat); \
6.29 \ WHILE w <= x \
6.30 \ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \
6.31 -\ DO r := r + 1; w := w + u + # 2; u := u + # 2 OD \
6.32 +\ DO r := r + 1; w := w + u + 2; u := u + 2 OD \
6.33 \ {r*r <= X & X < (r+1)*(r+1)}";
6.34 by (hoare_tac (SELECT_GOAL Auto_tac) 1);
6.35 qed "sqrt_without_multiplication";
7.1 --- a/src/HOL/Hyperreal/HyperArith0.ML Fri Oct 05 23:58:52 2001 +0200
7.2 +++ b/src/HOL/Hyperreal/HyperArith0.ML Sat Oct 06 00:02:46 2001 +0200
7.3 @@ -288,34 +288,34 @@
7.4 set trace_simp;
7.5 fun test s = (Goal s; by (Simp_tac 1));
7.6
7.7 -test "Numeral0 <= (y::hypreal) * # -2";
7.8 -test "# 9*x = # 12 * (y::hypreal)";
7.9 -test "(# 9*x) / (# 12 * (y::hypreal)) = z";
7.10 -test "# 9*x < # 12 * (y::hypreal)";
7.11 -test "# 9*x <= # 12 * (y::hypreal)";
7.12 +test "Numeral0 <= (y::hypreal) * -2";
7.13 +test "9*x = 12 * (y::hypreal)";
7.14 +test "(9*x) / (12 * (y::hypreal)) = z";
7.15 +test "9*x < 12 * (y::hypreal)";
7.16 +test "9*x <= 12 * (y::hypreal)";
7.17
7.18 -test "# -99*x = # 123 * (y::hypreal)";
7.19 -test "(# -99*x) / (# 123 * (y::hypreal)) = z";
7.20 -test "# -99*x < # 123 * (y::hypreal)";
7.21 -test "# -99*x <= # 123 * (y::hypreal)";
7.22 +test "-99*x = 123 * (y::hypreal)";
7.23 +test "(-99*x) / (123 * (y::hypreal)) = z";
7.24 +test "-99*x < 123 * (y::hypreal)";
7.25 +test "-99*x <= 123 * (y::hypreal)";
7.26
7.27 -test "# 999*x = # -396 * (y::hypreal)";
7.28 -test "(# 999*x) / (# -396 * (y::hypreal)) = z";
7.29 -test "# 999*x < # -396 * (y::hypreal)";
7.30 -test "# 999*x <= # -396 * (y::hypreal)";
7.31 +test "999*x = -396 * (y::hypreal)";
7.32 +test "(999*x) / (-396 * (y::hypreal)) = z";
7.33 +test "999*x < -396 * (y::hypreal)";
7.34 +test "999*x <= -396 * (y::hypreal)";
7.35
7.36 -test "# -99*x = # -81 * (y::hypreal)";
7.37 -test "(# -99*x) / (# -81 * (y::hypreal)) = z";
7.38 -test "# -99*x <= # -81 * (y::hypreal)";
7.39 -test "# -99*x < # -81 * (y::hypreal)";
7.40 +test "-99*x = -81 * (y::hypreal)";
7.41 +test "(-99*x) / (-81 * (y::hypreal)) = z";
7.42 +test "-99*x <= -81 * (y::hypreal)";
7.43 +test "-99*x < -81 * (y::hypreal)";
7.44
7.45 -test "# -2 * x = # -1 * (y::hypreal)";
7.46 -test "# -2 * x = -(y::hypreal)";
7.47 -test "(# -2 * x) / (# -1 * (y::hypreal)) = z";
7.48 -test "# -2 * x < -(y::hypreal)";
7.49 -test "# -2 * x <= # -1 * (y::hypreal)";
7.50 -test "-x < # -23 * (y::hypreal)";
7.51 -test "-x <= # -23 * (y::hypreal)";
7.52 +test "-2 * x = -1 * (y::hypreal)";
7.53 +test "-2 * x = -(y::hypreal)";
7.54 +test "(-2 * x) / (-1 * (y::hypreal)) = z";
7.55 +test "-2 * x < -(y::hypreal)";
7.56 +test "-2 * x <= -1 * (y::hypreal)";
7.57 +test "-x < -23 * (y::hypreal)";
7.58 +test "-x <= -23 * (y::hypreal)";
7.59 *)
7.60
7.61
7.62 @@ -516,18 +516,18 @@
7.63 qed "hypreal_divide_1";
7.64 Addsimps [hypreal_divide_1];
7.65
7.66 -Goal "x/# -1 = -(x::hypreal)";
7.67 +Goal "x/-1 = -(x::hypreal)";
7.68 by (Simp_tac 1);
7.69 qed "hypreal_divide_minus1";
7.70 Addsimps [hypreal_divide_minus1];
7.71
7.72 -Goal "# -1/(x::hypreal) = - (Numeral1/x)";
7.73 +Goal "-1/(x::hypreal) = - (Numeral1/x)";
7.74 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
7.75 qed "hypreal_minus1_divide";
7.76 Addsimps [hypreal_minus1_divide];
7.77
7.78 Goal "[| (Numeral0::hypreal) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
7.79 -by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1);
7.80 +by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
7.81 by (asm_simp_tac (simpset() addsimps [min_def]) 1);
7.82 qed "hypreal_lbound_gt_zero";
7.83
7.84 @@ -644,11 +644,11 @@
7.85
7.86 (*** Density of the Hyperreals ***)
7.87
7.88 -Goal "x < y ==> x < (x+y) / (# 2::hypreal)";
7.89 +Goal "x < y ==> x < (x+y) / (2::hypreal)";
7.90 by Auto_tac;
7.91 qed "hypreal_less_half_sum";
7.92
7.93 -Goal "x < y ==> (x+y)/(# 2::hypreal) < y";
7.94 +Goal "x < y ==> (x+y)/(2::hypreal) < y";
7.95 by Auto_tac;
7.96 qed "hypreal_gt_half_sum";
7.97
8.1 --- a/src/HOL/Hyperreal/HyperBin.ML Fri Oct 05 23:58:52 2001 +0200
8.2 +++ b/src/HOL/Hyperreal/HyperBin.ML Sat Oct 06 00:02:46 2001 +0200
8.3 @@ -57,18 +57,18 @@
8.4 qed "mult_hypreal_number_of";
8.5 Addsimps [mult_hypreal_number_of];
8.6
8.7 -Goal "(# 2::hypreal) = Numeral1 + Numeral1";
8.8 +Goal "(2::hypreal) = Numeral1 + Numeral1";
8.9 by (Simp_tac 1);
8.10 val lemma = result();
8.11
8.12 (*For specialist use: NOT as default simprules*)
8.13 -Goal "# 2 * z = (z+z::hypreal)";
8.14 +Goal "2 * z = (z+z::hypreal)";
8.15 by (simp_tac (simpset ()
8.16 addsimps [lemma, hypreal_add_mult_distrib,
8.17 one_eq_numeral_1 RS sym]) 1);
8.18 qed "hypreal_mult_2";
8.19
8.20 -Goal "z * # 2 = (z+z::hypreal)";
8.21 +Goal "z * 2 = (z+z::hypreal)";
8.22 by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1);
8.23 qed "hypreal_mult_2_right";
8.24
8.25 @@ -107,11 +107,11 @@
8.26
8.27 (*** New versions of existing theorems involving 0, 1hr ***)
8.28
8.29 -Goal "- Numeral1 = (# -1::hypreal)";
8.30 +Goal "- Numeral1 = (-1::hypreal)";
8.31 by (Simp_tac 1);
8.32 qed "minus_numeral_one";
8.33
8.34 -(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to # -1*)
8.35 +(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to -1*)
8.36 val hypreal_numeral_ss =
8.37 real_numeral_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1,
8.38 minus_numeral_one];
8.39 @@ -242,14 +242,14 @@
8.40 hypreal_add_ac@rel_iff_rel_0_rls) 1);
8.41 qed "hypreal_le_add_iff2";
8.42
8.43 -Goal "(z::hypreal) * # -1 = -z";
8.44 +Goal "(z::hypreal) * -1 = -z";
8.45 by (stac (minus_numeral_one RS sym) 1);
8.46 by (stac (hypreal_minus_mult_eq2 RS sym) 1);
8.47 by Auto_tac;
8.48 qed "hypreal_mult_minus_1_right";
8.49 Addsimps [hypreal_mult_minus_1_right];
8.50
8.51 -Goal "# -1 * (z::hypreal) = -z";
8.52 +Goal "-1 * (z::hypreal) = -z";
8.53 by (simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
8.54 qed "hypreal_mult_minus_1";
8.55 Addsimps [hypreal_mult_minus_1];
8.56 @@ -471,7 +471,7 @@
8.57 structure CombineNumeralsData =
8.58 struct
8.59 val add = op + : int*int -> int
8.60 - val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
8.61 + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
8.62 val dest_sum = dest_sum
8.63 val mk_coeff = mk_coeff
8.64 val dest_coeff = dest_coeff 1
8.65 @@ -530,34 +530,34 @@
8.66 set trace_simp;
8.67 fun test s = (Goal s, by (Simp_tac 1));
8.68
8.69 -test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::hypreal)";
8.70 -test "# 2*u = (u::hypreal)";
8.71 -test "(i + j + # 12 + (k::hypreal)) - # 15 = y";
8.72 -test "(i + j + # 12 + (k::hypreal)) - # 5 = y";
8.73 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hypreal)";
8.74 +test "2*u = (u::hypreal)";
8.75 +test "(i + j + 12 + (k::hypreal)) - 15 = y";
8.76 +test "(i + j + 12 + (k::hypreal)) - 5 = y";
8.77
8.78 test "y - b < (b::hypreal)";
8.79 -test "y - (# 3*b + c) < (b::hypreal) - # 2*c";
8.80 +test "y - (3*b + c) < (b::hypreal) - 2*c";
8.81
8.82 -test "(# 2*x - (u*v) + y) - v*# 3*u = (w::hypreal)";
8.83 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::hypreal)";
8.84 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::hypreal)";
8.85 -test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::hypreal)";
8.86 +test "(2*x - (u*v) + y) - v*3*u = (w::hypreal)";
8.87 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::hypreal)";
8.88 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::hypreal)";
8.89 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::hypreal)";
8.90
8.91 -test "(i + j + # 12 + (k::hypreal)) = u + # 15 + y";
8.92 -test "(i + j*# 2 + # 12 + (k::hypreal)) = j + # 5 + y";
8.93 +test "(i + j + 12 + (k::hypreal)) = u + 15 + y";
8.94 +test "(i + j*2 + 12 + (k::hypreal)) = j + 5 + y";
8.95
8.96 -test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::hypreal)";
8.97 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::hypreal)";
8.98
8.99 test "a + -(b+c) + b = (d::hypreal)";
8.100 test "a + -(b+c) - b = (d::hypreal)";
8.101
8.102 (*negative numerals*)
8.103 -test "(i + j + # -2 + (k::hypreal)) - (u + # 5 + y) = zz";
8.104 -test "(i + j + # -3 + (k::hypreal)) < u + # 5 + y";
8.105 -test "(i + j + # 3 + (k::hypreal)) < u + # -6 + y";
8.106 -test "(i + j + # -12 + (k::hypreal)) - # 15 = y";
8.107 -test "(i + j + # 12 + (k::hypreal)) - # -15 = y";
8.108 -test "(i + j + # -12 + (k::hypreal)) - # -15 = y";
8.109 +test "(i + j + -2 + (k::hypreal)) - (u + 5 + y) = zz";
8.110 +test "(i + j + -3 + (k::hypreal)) < u + 5 + y";
8.111 +test "(i + j + 3 + (k::hypreal)) < u + -6 + y";
8.112 +test "(i + j + -12 + (k::hypreal)) - 15 = y";
8.113 +test "(i + j + 12 + (k::hypreal)) - -15 = y";
8.114 +test "(i + j + -12 + (k::hypreal)) - -15 = y";
8.115 *)
8.116
8.117
9.1 --- a/src/HOL/Hyperreal/HyperPow.ML Fri Oct 05 23:58:52 2001 +0200
9.2 +++ b/src/HOL/Hyperreal/HyperPow.ML Sat Oct 06 00:02:46 2001 +0200
9.3 @@ -75,7 +75,7 @@
9.4 qed "hrabs_minus_hrealpow_one";
9.5 Addsimps [hrabs_minus_hrealpow_one];
9.6
9.7 -Goal "abs(# -1 ^ n) = (Numeral1::hypreal)";
9.8 +Goal "abs(-1 ^ n) = (Numeral1::hypreal)";
9.9 by (induct_tac "n" 1);
9.10 by Auto_tac;
9.11 qed "hrabs_hrealpow_minus_one";
9.12 @@ -134,13 +134,13 @@
9.13 by Auto_tac;
9.14 qed "hrealpow_two_ge_one";
9.15
9.16 -Goal "(Numeral1::hypreal) <= # 2 ^ n";
9.17 +Goal "(Numeral1::hypreal) <= 2 ^ n";
9.18 by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
9.19 by (rtac hrealpow_le 2);
9.20 by Auto_tac;
9.21 qed "two_hrealpow_ge_one";
9.22
9.23 -Goal "hypreal_of_nat n < # 2 ^ n";
9.24 +Goal "hypreal_of_nat n < 2 ^ n";
9.25 by (induct_tac "n" 1);
9.26 by (auto_tac (claset(),
9.27 simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib]));
9.28 @@ -149,17 +149,17 @@
9.29 qed "two_hrealpow_gt";
9.30 Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
9.31
9.32 -Goal "# -1 ^ (# 2*n) = (Numeral1::hypreal)";
9.33 +Goal "-1 ^ (2*n) = (Numeral1::hypreal)";
9.34 by (induct_tac "n" 1);
9.35 by (Auto_tac);
9.36 qed "hrealpow_minus_one";
9.37
9.38 -Goal "n+n = (# 2*n::nat)";
9.39 +Goal "n+n = (2*n::nat)";
9.40 by Auto_tac;
9.41 qed "double_lemma";
9.42
9.43 (*ugh: need to get rid fo the n+n*)
9.44 -Goal "# -1 ^ (n + n) = (Numeral1::hypreal)";
9.45 +Goal "-1 ^ (n + n) = (Numeral1::hypreal)";
9.46 by (auto_tac (claset(),
9.47 simpset() addsimps [double_lemma, hrealpow_minus_one]));
9.48 qed "hrealpow_minus_one2";
9.49 @@ -340,7 +340,7 @@
9.50 qed "hrabs_minus_hyperpow_one";
9.51 Addsimps [hrabs_minus_hyperpow_one];
9.52
9.53 -Goal "abs(# -1 pow n) = (Numeral1::hypreal)";
9.54 +Goal "abs(-1 pow n) = (Numeral1::hypreal)";
9.55 by (subgoal_tac "abs((- 1hr) pow n) = 1hr" 1);
9.56 by (Asm_full_simp_tac 1);
9.57 by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
9.58 @@ -388,7 +388,7 @@
9.59 simpset()));
9.60 qed "hyperpow_two_ge_one";
9.61
9.62 -Goal "(Numeral1::hypreal) <= # 2 pow n";
9.63 +Goal "(Numeral1::hypreal) <= 2 pow n";
9.64 by (res_inst_tac [("y","Numeral1 pow n")] order_trans 1);
9.65 by (rtac hyperpow_le 2);
9.66 by Auto_tac;
9.67 @@ -397,7 +397,7 @@
9.68
9.69 Addsimps [simplify (simpset()) realpow_minus_one];
9.70
9.71 -Goal "# -1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
9.72 +Goal "-1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
9.73 by (subgoal_tac "(-(1hr)) pow ((1hn + 1hn)*n) = 1hr" 1);
9.74 by (Asm_full_simp_tac 1);
9.75 by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
10.1 --- a/src/HOL/Hyperreal/Lim.ML Fri Oct 05 23:58:52 2001 +0200
10.2 +++ b/src/HOL/Hyperreal/Lim.ML Sat Oct 06 00:02:46 2001 +0200
10.3 @@ -29,7 +29,7 @@
10.4 Goalw [LIM_def]
10.5 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
10.6 by (Clarify_tac 1);
10.7 -by (REPEAT(dres_inst_tac [("x","r/# 2")] spec 1));
10.8 +by (REPEAT(dres_inst_tac [("x","r/2")] spec 1));
10.9 by (Asm_full_simp_tac 1);
10.10 by (Clarify_tac 1);
10.11 by (res_inst_tac [("R1.0","s"),("R2.0","sa")]
10.12 @@ -1544,15 +1544,15 @@
10.13 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
10.14 qed "Bolzano_bisect_Suc_le_snd";
10.15
10.16 -Goal "((x::real) = y / (# 2 * z)) = (# 2 * x = y/z)";
10.17 +Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)";
10.18 by Auto_tac;
10.19 -by (dres_inst_tac [("f","%u. (Numeral1/# 2)*u")] arg_cong 1);
10.20 +by (dres_inst_tac [("f","%u. (Numeral1/2)*u")] arg_cong 1);
10.21 by Auto_tac;
10.22 qed "eq_divide_2_times_iff";
10.23
10.24 Goal "a \\<le> b ==> \
10.25 \ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
10.26 -\ (b-a) / (# 2 ^ n)";
10.27 +\ (b-a) / (2 ^ n)";
10.28 by (induct_tac "n" 1);
10.29 by (auto_tac (claset(),
10.30 simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib,
10.31 @@ -1604,8 +1604,8 @@
10.32 by (rename_tac "l" 1);
10.33 by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
10.34 by (rewtac LIMSEQ_def);
10.35 -by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
10.36 -by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
10.37 +by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
10.38 +by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
10.39 by (dtac real_less_half_sum 1);
10.40 by Safe_tac;
10.41 (*linear arithmetic bug if we just use Asm_simp_tac*)
10.42 @@ -2148,12 +2148,12 @@
10.43 simpset() addsimps [real_mult_assoc]));
10.44 qed "DERIV_const_ratio_const2";
10.45
10.46 -Goal "((a + b) /# 2 - a) = (b - a)/(# 2::real)";
10.47 +Goal "((a + b) /2 - a) = (b - a)/(2::real)";
10.48 by Auto_tac;
10.49 qed "real_average_minus_first";
10.50 Addsimps [real_average_minus_first];
10.51
10.52 -Goal "((b + a)/# 2 - a) = (b - a)/(# 2::real)";
10.53 +Goal "((b + a)/2 - a) = (b - a)/(2::real)";
10.54 by Auto_tac;
10.55 qed "real_average_minus_second";
10.56 Addsimps [real_average_minus_second];
10.57 @@ -2161,7 +2161,7 @@
10.58
10.59 (* Gallileo's "trick": average velocity = av. of end velocities *)
10.60 Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
10.61 -\ ==> v((a + b)/# 2) = (v a + v b)/# 2";
10.62 +\ ==> v((a + b)/2) = (v a + v b)/2";
10.63 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
10.64 by Auto_tac;
10.65 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
11.1 --- a/src/HOL/Hyperreal/Lim.thy Fri Oct 05 23:58:52 2001 +0200
11.2 +++ b/src/HOL/Hyperreal/Lim.thy Sat Oct 06 00:02:46 2001 +0200
11.3 @@ -71,8 +71,8 @@
11.4 "Bolzano_bisect P a b 0 = (a,b)"
11.5 "Bolzano_bisect P a b (Suc n) =
11.6 (let (x,y) = Bolzano_bisect P a b n
11.7 - in if P(x, (x+y)/# 2) then ((x+y)/# 2, y)
11.8 - else (x, (x+y)/# 2) )"
11.9 + in if P(x, (x+y)/2) then ((x+y)/2, y)
11.10 + else (x, (x+y)/2) )"
11.11
11.12
11.13 end
12.1 --- a/src/HOL/Hyperreal/NSA.ML Fri Oct 05 23:58:52 2001 +0200
12.2 +++ b/src/HOL/Hyperreal/NSA.ML Sat Oct 06 00:02:46 2001 +0200
12.3 @@ -260,11 +260,11 @@
12.4 qed "Infinitesimal_zero";
12.5 AddIffs [Infinitesimal_zero];
12.6
12.7 -Goal "x/(# 2::hypreal) + x/(# 2::hypreal) = x";
12.8 +Goal "x/(2::hypreal) + x/(2::hypreal) = x";
12.9 by Auto_tac;
12.10 qed "hypreal_sum_of_halves";
12.11
12.12 -Goal "Numeral0 < r ==> Numeral0 < r/(# 2::hypreal)";
12.13 +Goal "Numeral0 < r ==> Numeral0 < r/(2::hypreal)";
12.14 by Auto_tac;
12.15 qed "hypreal_half_gt_zero";
12.16
13.1 --- a/src/HOL/Hyperreal/Series.ML Fri Oct 05 23:58:52 2001 +0200
13.2 +++ b/src/HOL/Hyperreal/Series.ML Sat Oct 06 00:02:46 2001 +0200
13.3 @@ -101,7 +101,7 @@
13.4 by (Auto_tac);
13.5 qed "sumr_shift_bounds";
13.6
13.7 -Goal "sumr 0 (# 2*n) (%i. (# -1) ^ Suc i) = Numeral0";
13.8 +Goal "sumr 0 (2*n) (%i. (-1) ^ Suc i) = Numeral0";
13.9 by (induct_tac "n" 1);
13.10 by (Auto_tac);
13.11 qed "sumr_minus_one_realpow_zero";
14.1 --- a/src/HOL/Hyperreal/hypreal_arith0.ML Fri Oct 05 23:58:52 2001 +0200
14.2 +++ b/src/HOL/Hyperreal/hypreal_arith0.ML Sat Oct 06 00:02:46 2001 +0200
14.3 @@ -115,7 +115,7 @@
14.4 qed "";
14.5
14.6 Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
14.7 -\ ==> # 6*a <= # 5*l+i";
14.8 +\ ==> 6*a <= 5*l+i";
14.9 by (fast_arith_tac 1);
14.10 qed "";
14.11 *)
15.1 --- a/src/HOL/IMP/Compiler.thy Fri Oct 05 23:58:52 2001 +0200
15.2 +++ b/src/HOL/IMP/Compiler.thy Sat Oct 06 00:02:46 2001 +0200
15.3 @@ -39,9 +39,9 @@
15.4 "compile (x:==a) = [ASIN x a]"
15.5 "compile (c1;c2) = compile c1 @ compile c2"
15.6 "compile (IF b THEN c1 ELSE c2) =
15.7 - [JMPF b (length(compile c1) + # 2)] @ compile c1 @
15.8 + [JMPF b (length(compile c1) + 2)] @ compile c1 @
15.9 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
15.10 -"compile (WHILE b DO c) = [JMPF b (length(compile c) + # 2)] @ compile c @
15.11 +"compile (WHILE b DO c) = [JMPF b (length(compile c) + 2)] @ compile c @
15.12 [JMPB (length(compile c)+1)]"
15.13
15.14 declare nth_append[simp];
16.1 --- a/src/HOL/IMP/Examples.ML Fri Oct 05 23:58:52 2001 +0200
16.2 +++ b/src/HOL/IMP/Examples.ML Sat Oct 06 00:02:46 2001 +0200
16.3 @@ -34,7 +34,7 @@
16.4 val step = resolve_tac evalc.intrs 1;
16.5 val simp = Asm_simp_tac 1;
16.6 Goalw [factorial_def] "a~=b ==> \
16.7 -\ <factorial a b, Mem(a:=# 3)> -c-> Mem(b:=# 6,a:=Numeral0)";
16.8 +\ <factorial a b, Mem(a:=3)> -c-> Mem(b:=6,a:=Numeral0)";
16.9 by (ftac not_sym 1);
16.10 by step;
16.11 by step;
17.1 --- a/src/HOL/IMPP/EvenOdd.ML Fri Oct 05 23:58:52 2001 +0200
17.2 +++ b/src/HOL/IMPP/EvenOdd.ML Sat Oct 06 00:02:46 2001 +0200
17.3 @@ -17,7 +17,7 @@
17.4 Addsimps [not_even_1];
17.5
17.6 Goalw [even_def] "even (Suc (Suc n)) = even n";
17.7 -by (subgoal_tac "Suc (Suc n) = n+# 2" 1);
17.8 +by (subgoal_tac "Suc (Suc n) = n+2" 1);
17.9 by (Simp_tac 2);
17.10 by (etac ssubst 1);
17.11 by (rtac dvd_reduce 1);
18.1 --- a/src/HOL/IMPP/EvenOdd.thy Fri Oct 05 23:58:52 2001 +0200
18.2 +++ b/src/HOL/IMPP/EvenOdd.thy Sat Oct 06 00:02:46 2001 +0200
18.3 @@ -9,7 +9,7 @@
18.4 EvenOdd = Misc +
18.5
18.6 constdefs even :: nat => bool
18.7 - "even n == # 2 dvd n"
18.8 + "even n == 2 dvd n"
18.9
18.10 consts
18.11 Even, Odd :: pname
19.1 --- a/src/HOL/Induct/Mutil.thy Fri Oct 05 23:58:52 2001 +0200
19.2 +++ b/src/HOL/Induct/Mutil.thy Sat Oct 06 00:02:46 2001 +0200
19.3 @@ -29,7 +29,7 @@
19.4
19.5 constdefs
19.6 coloured :: "nat => (nat \<times> nat) set"
19.7 - "coloured b == {(i, j). (i + j) mod # 2 = b}"
19.8 + "coloured b == {(i, j). (i + j) mod 2 = b}"
19.9
19.10
19.11 text {* \medskip The union of two disjoint tilings is a tiling *}
19.12 @@ -61,14 +61,14 @@
19.13 apply auto
19.14 done
19.15
19.16 -lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (# 2 * n) \<in> tiling domino"
19.17 +lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (2 * n) \<in> tiling domino"
19.18 apply (induct n)
19.19 apply (simp_all add: Un_assoc [symmetric])
19.20 apply (rule tiling.Un)
19.21 apply (auto simp add: sing_Times_lemma)
19.22 done
19.23
19.24 -lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (# 2 * n) \<in> tiling domino"
19.25 +lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino"
19.26 apply (induct m)
19.27 apply auto
19.28 done
19.29 @@ -78,7 +78,7 @@
19.30
19.31 lemma coloured_insert [simp]:
19.32 "coloured b \<inter> (insert (i, j) t) =
19.33 - (if (i + j) mod # 2 = b then insert (i, j) (coloured b \<inter> t)
19.34 + (if (i + j) mod 2 = b then insert (i, j) (coloured b \<inter> t)
19.35 else coloured b \<inter> t)"
19.36 apply (unfold coloured_def)
19.37 apply auto
19.38 @@ -125,7 +125,7 @@
19.39
19.40 theorem gen_mutil_not_tiling:
19.41 "t \<in> tiling domino ==>
19.42 - (i + j) mod # 2 = 0 ==> (m + n) mod # 2 = 0 ==>
19.43 + (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==>
19.44 {(i, j), (m, n)} \<subseteq> t
19.45 ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
19.46 apply (rule notI)
19.47 @@ -140,8 +140,8 @@
19.48 text {* Apply the general theorem to the well-known case *}
19.49
19.50 theorem mutil_not_tiling:
19.51 - "t = lessThan (# 2 * Suc m) \<times> lessThan (# 2 * Suc n)
19.52 - ==> t - {(0, 0)} - {(Suc (# 2 * m), Suc (# 2 * n))} \<notin> tiling domino"
19.53 + "t = lessThan (2 * Suc m) \<times> lessThan (2 * Suc n)
19.54 + ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} \<notin> tiling domino"
19.55 apply (rule gen_mutil_not_tiling)
19.56 apply (blast intro!: dominoes_tile_matrix)
19.57 apply auto
20.1 --- a/src/HOL/Integ/Bin.ML Fri Oct 05 23:58:52 2001 +0200
20.2 +++ b/src/HOL/Integ/Bin.ML Sat Oct 06 00:02:46 2001 +0200
20.3 @@ -160,7 +160,7 @@
20.4
20.5 (*The correctness of shifting. But it doesn't seem to give a measurable
20.6 speed-up.*)
20.7 -Goal "(# 2::int) * number_of w = number_of (w BIT False)";
20.8 +Goal "(2::int) * number_of w = number_of (w BIT False)";
20.9 by (induct_tac "w" 1);
20.10 by (ALLGOALS (asm_simp_tac
20.11 (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
20.12 @@ -250,11 +250,11 @@
20.13 by (Simp_tac 1);
20.14 qed "zmult_1_right";
20.15
20.16 -Goal "# -1 * z = -(z::int)";
20.17 +Goal "-1 * z = -(z::int)";
20.18 by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
20.19 qed "zmult_minus1";
20.20
20.21 -Goal "z * # -1 = -(z::int)";
20.22 +Goal "z * -1 = -(z::int)";
20.23 by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
20.24 qed "zmult_minus1_right";
20.25
21.1 --- a/src/HOL/Integ/IntArith.ML Fri Oct 05 23:58:52 2001 +0200
21.2 +++ b/src/HOL/Integ/IntArith.ML Sat Oct 06 00:02:46 2001 +0200
21.3 @@ -168,7 +168,7 @@
21.4 by Auto_tac;
21.5 qed "pos_zmult_eq_1_iff";
21.6
21.7 -Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = # -1 & n = # -1))";
21.8 +Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = -1 & n = -1))";
21.9 by (case_tac "Numeral0<m" 1);
21.10 by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
21.11 by (case_tac "m=Numeral0" 1);
22.1 --- a/src/HOL/Integ/IntDiv.ML Fri Oct 05 23:58:52 2001 +0200
22.2 +++ b/src/HOL/Integ/IntDiv.ML Sat Oct 06 00:02:46 2001 +0200
22.3 @@ -84,8 +84,8 @@
22.4
22.5
22.6 Goal "adjust a b (q,r) = (let diff = r-b in \
22.7 -\ if Numeral0 <= diff then (# 2*q + Numeral1, diff) \
22.8 -\ else (# 2*q, r))";
22.9 +\ if Numeral0 <= diff then (2*q + Numeral1, diff) \
22.10 +\ else (2*q, r))";
22.11 by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
22.12 qed "adjust_eq";
22.13 Addsimps [adjust_eq];
22.14 @@ -103,7 +103,7 @@
22.15 (**use with simproc to avoid re-proving the premise*)
22.16 Goal "Numeral0 < b ==> \
22.17 \ posDivAlg (a,b) = \
22.18 -\ (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, # 2*b)))";
22.19 +\ (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, 2*b)))";
22.20 by (rtac (posDivAlg_raw_eqn RS trans) 1);
22.21 by (Asm_simp_tac 1);
22.22 qed "posDivAlg_eqn";
22.23 @@ -141,7 +141,7 @@
22.24 (**use with simproc to avoid re-proving the premise*)
22.25 Goal "Numeral0 < b ==> \
22.26 \ negDivAlg (a,b) = \
22.27 -\ (if Numeral0<=a+b then (# -1,a+b) else adjust a b (negDivAlg(a, # 2*b)))";
22.28 +\ (if Numeral0<=a+b then (-1,a+b) else adjust a b (negDivAlg(a, 2*b)))";
22.29 by (rtac (negDivAlg_raw_eqn RS trans) 1);
22.30 by (Asm_simp_tac 1);
22.31 qed "negDivAlg_eqn";
22.32 @@ -179,7 +179,7 @@
22.33 qed "posDivAlg_0";
22.34 Addsimps [posDivAlg_0];
22.35
22.36 -Goal "negDivAlg (# -1, b) = (# -1, b-Numeral1)";
22.37 +Goal "negDivAlg (-1, b) = (-1, b-Numeral1)";
22.38 by (stac negDivAlg_raw_eqn 1);
22.39 by Auto_tac;
22.40 qed "negDivAlg_minus1";
22.41 @@ -272,7 +272,7 @@
22.42 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
22.43 qed "div_neg_neg_trivial";
22.44
22.45 -Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a div b = # -1";
22.46 +Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a div b = -1";
22.47 by (rtac quorem_div 1);
22.48 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
22.49 qed "div_pos_neg_trivial";
22.50 @@ -290,7 +290,7 @@
22.51 qed "mod_neg_neg_trivial";
22.52
22.53 Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a mod b = a+b";
22.54 -by (res_inst_tac [("q","# -1")] quorem_mod 1);
22.55 +by (res_inst_tac [("q","-1")] quorem_mod 1);
22.56 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
22.57 qed "mod_pos_neg_trivial";
22.58
22.59 @@ -411,7 +411,7 @@
22.60 by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
22.61 qed "zdiv_zero";
22.62
22.63 -Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
22.64 +Goal "(Numeral0::int) < b ==> -1 div b = -1";
22.65 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
22.66 qed "div_eq_minus1";
22.67
22.68 @@ -421,11 +421,11 @@
22.69
22.70 Addsimps [zdiv_zero, zmod_zero];
22.71
22.72 -Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
22.73 +Goal "(Numeral0::int) < b ==> -1 div b = -1";
22.74 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
22.75 qed "zdiv_minus1";
22.76
22.77 -Goal "(Numeral0::int) < b ==> # -1 mod b = b-Numeral1";
22.78 +Goal "(Numeral0::int) < b ==> -1 mod b = b-Numeral1";
22.79 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
22.80 qed "zmod_minus1";
22.81
22.82 @@ -491,15 +491,15 @@
22.83 qed "zdiv_1";
22.84 Addsimps [zdiv_1];
22.85
22.86 -Goal "a mod (# -1::int) = Numeral0";
22.87 -by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_sign 1);
22.88 -by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_bound 2);
22.89 +Goal "a mod (-1::int) = Numeral0";
22.90 +by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_sign 1);
22.91 +by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_bound 2);
22.92 by Auto_tac;
22.93 qed "zmod_minus1_right";
22.94 Addsimps [zmod_minus1_right];
22.95
22.96 -Goal "a div (# -1::int) = -a";
22.97 -by (cut_inst_tac [("a","a"),("b","# -1")] zmod_zdiv_equality 1);
22.98 +Goal "a div (-1::int) = -a";
22.99 +by (cut_inst_tac [("a","a"),("b","-1")] zmod_zdiv_equality 1);
22.100 by Auto_tac;
22.101 qed "zdiv_minus1_right";
22.102 Addsimps [zdiv_minus1_right];
22.103 @@ -861,13 +861,13 @@
22.104
22.105 (** computing "div" by shifting **)
22.106
22.107 -Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) div (# 2*a) = b div a";
22.108 +Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) div (2*a) = b div a";
22.109 by (zdiv_undefined_case_tac "a = Numeral0" 1);
22.110 by (subgoal_tac "Numeral1 <= a" 1);
22.111 by (arith_tac 2);
22.112 -by (subgoal_tac "Numeral1 < a * # 2" 1);
22.113 +by (subgoal_tac "Numeral1 < a * 2" 1);
22.114 by (arith_tac 2);
22.115 -by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
22.116 +by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
22.117 by (rtac zmult_zle_mono2 2);
22.118 by (auto_tac (claset(),
22.119 simpset() addsimps [zadd_commute, zmult_commute,
22.120 @@ -887,12 +887,12 @@
22.121 qed "pos_zdiv_mult_2";
22.122
22.123
22.124 -Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) div (# 2*a) = (b+Numeral1) div a";
22.125 -by (subgoal_tac "(Numeral1 + # 2*(-b-Numeral1)) div (# 2 * (-a)) = (-b-Numeral1) div (-a)" 1);
22.126 +Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) div (2*a) = (b+Numeral1) div a";
22.127 +by (subgoal_tac "(Numeral1 + 2*(-b-Numeral1)) div (2 * (-a)) = (-b-Numeral1) div (-a)" 1);
22.128 by (rtac pos_zdiv_mult_2 2);
22.129 by (auto_tac (claset(),
22.130 simpset() addsimps [zmult_zminus_right]));
22.131 -by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
22.132 +by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
22.133 by (Simp_tac 2);
22.134 by (asm_full_simp_tac (HOL_ss
22.135 addsimps [zdiv_zminus_zminus, zdiff_def,
22.136 @@ -921,13 +921,13 @@
22.137
22.138 (** computing "mod" by shifting (proofs resemble those for "div") **)
22.139
22.140 -Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) mod (# 2*a) = Numeral1 + # 2 * (b mod a)";
22.141 +Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) mod (2*a) = Numeral1 + 2 * (b mod a)";
22.142 by (zdiv_undefined_case_tac "a = Numeral0" 1);
22.143 by (subgoal_tac "Numeral1 <= a" 1);
22.144 by (arith_tac 2);
22.145 -by (subgoal_tac "Numeral1 < a * # 2" 1);
22.146 +by (subgoal_tac "Numeral1 < a * 2" 1);
22.147 by (arith_tac 2);
22.148 -by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
22.149 +by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
22.150 by (rtac zmult_zle_mono2 2);
22.151 by (auto_tac (claset(),
22.152 simpset() addsimps [zadd_commute, zmult_commute,
22.153 @@ -947,13 +947,13 @@
22.154 qed "pos_zmod_mult_2";
22.155
22.156
22.157 -Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) mod (# 2*a) = # 2 * ((b+Numeral1) mod a) - Numeral1";
22.158 +Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) mod (2*a) = 2 * ((b+Numeral1) mod a) - Numeral1";
22.159 by (subgoal_tac
22.160 - "(Numeral1 + # 2*(-b-Numeral1)) mod (# 2*(-a)) = Numeral1 + # 2*((-b-Numeral1) mod (-a))" 1);
22.161 + "(Numeral1 + 2*(-b-Numeral1)) mod (2*(-a)) = Numeral1 + 2*((-b-Numeral1) mod (-a))" 1);
22.162 by (rtac pos_zmod_mult_2 2);
22.163 by (auto_tac (claset(),
22.164 simpset() addsimps [zmult_zminus_right]));
22.165 -by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
22.166 +by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
22.167 by (Simp_tac 2);
22.168 by (asm_full_simp_tac (HOL_ss
22.169 addsimps [zmod_zminus_zminus, zdiff_def,
22.170 @@ -965,9 +965,9 @@
22.171 Goal "number_of (v BIT b) mod number_of (w BIT False) = \
22.172 \ (if b then \
22.173 \ if (Numeral0::int) <= number_of w \
22.174 -\ then # 2 * (number_of v mod number_of w) + Numeral1 \
22.175 -\ else # 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1 \
22.176 -\ else # 2 * (number_of v mod number_of w))";
22.177 +\ then 2 * (number_of v mod number_of w) + Numeral1 \
22.178 +\ else 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1 \
22.179 +\ else 2 * (number_of v mod number_of w))";
22.180 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
22.181 by (asm_simp_tac (simpset()
22.182 delsimps bin_arith_extra_simps@bin_rel_simps
22.183 @@ -981,10 +981,10 @@
22.184 (** Quotients of signs **)
22.185
22.186 Goal "[| a < (Numeral0::int); Numeral0 < b |] ==> a div b < Numeral0";
22.187 -by (subgoal_tac "a div b <= # -1" 1);
22.188 +by (subgoal_tac "a div b <= -1" 1);
22.189 by (Force_tac 1);
22.190 by (rtac order_trans 1);
22.191 -by (res_inst_tac [("a'","# -1")] zdiv_mono1 1);
22.192 +by (res_inst_tac [("a'","-1")] zdiv_mono1 1);
22.193 by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
22.194 qed "div_neg_pos_less0";
22.195
23.1 --- a/src/HOL/Integ/IntDiv.thy Fri Oct 05 23:58:52 2001 +0200
23.2 +++ b/src/HOL/Integ/IntDiv.thy Sat Oct 06 00:02:46 2001 +0200
23.3 @@ -15,8 +15,8 @@
23.4 (if Numeral0 < b then Numeral0<=r & r<b else b<r & r <= Numeral0)"
23.5
23.6 adjust :: "[int, int, int*int] => int*int"
23.7 - "adjust a b == %(q,r). if Numeral0 <= r-b then (# 2*q + Numeral1, r-b)
23.8 - else (# 2*q, r)"
23.9 + "adjust a b == %(q,r). if Numeral0 <= r-b then (2*q + Numeral1, r-b)
23.10 + else (2*q, r)"
23.11
23.12 (** the division algorithm **)
23.13
23.14 @@ -25,14 +25,14 @@
23.15 recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))"
23.16 "posDivAlg (a,b) =
23.17 (if (a<b | b<=Numeral0) then (Numeral0,a)
23.18 - else adjust a b (posDivAlg(a, # 2*b)))"
23.19 + else adjust a b (posDivAlg(a, 2*b)))"
23.20
23.21 (*for the case a<0, b>0*)
23.22 consts negDivAlg :: "int*int => int*int"
23.23 recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
23.24 "negDivAlg (a,b) =
23.25 - (if (Numeral0<=a+b | b<=Numeral0) then (# -1,a+b)
23.26 - else adjust a b (negDivAlg(a, # 2*b)))"
23.27 + (if (Numeral0<=a+b | b<=Numeral0) then (-1,a+b)
23.28 + else adjust a b (negDivAlg(a, 2*b)))"
23.29
23.30 (*for the general case b~=0*)
23.31
24.1 --- a/src/HOL/Integ/NatSimprocs.ML Fri Oct 05 23:58:52 2001 +0200
24.2 +++ b/src/HOL/Integ/NatSimprocs.ML Sat Oct 06 00:02:46 2001 +0200
24.3 @@ -92,40 +92,40 @@
24.4
24.5 (** Evens and Odds, for Mutilated Chess Board **)
24.6
24.7 -(*Case analysis on b<# 2*)
24.8 -Goal "(n::nat) < # 2 ==> n = Numeral0 | n = Numeral1";
24.9 +(*Case analysis on b<2*)
24.10 +Goal "(n::nat) < 2 ==> n = Numeral0 | n = Numeral1";
24.11 by (arith_tac 1);
24.12 qed "less_2_cases";
24.13
24.14 -Goal "Suc(Suc(m)) mod # 2 = m mod # 2";
24.15 -by (subgoal_tac "m mod # 2 < # 2" 1);
24.16 +Goal "Suc(Suc(m)) mod 2 = m mod 2";
24.17 +by (subgoal_tac "m mod 2 < 2" 1);
24.18 by (Asm_simp_tac 2);
24.19 be (less_2_cases RS disjE) 1;
24.20 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
24.21 qed "mod2_Suc_Suc";
24.22 Addsimps [mod2_Suc_Suc];
24.23
24.24 -Goal "!!m::nat. (0 < m mod # 2) = (m mod # 2 = Numeral1)";
24.25 -by (subgoal_tac "m mod # 2 < # 2" 1);
24.26 +Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = Numeral1)";
24.27 +by (subgoal_tac "m mod 2 < 2" 1);
24.28 by (Asm_simp_tac 2);
24.29 by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
24.30 qed "mod2_gr_0";
24.31 Addsimps [mod2_gr_0, rename_numerals mod2_gr_0];
24.32
24.33 -(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) # 2 **)
24.34 +(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **)
24.35
24.36 -Goal "# 2 + n = Suc (Suc n)";
24.37 +Goal "2 + n = Suc (Suc n)";
24.38 by (Simp_tac 1);
24.39 qed "add_2_eq_Suc";
24.40
24.41 -Goal "n + # 2 = Suc (Suc n)";
24.42 +Goal "n + 2 = Suc (Suc n)";
24.43 by (Simp_tac 1);
24.44 qed "add_2_eq_Suc'";
24.45
24.46 Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
24.47
24.48 (*Can be used to eliminate long strings of Sucs, but not by default*)
24.49 -Goal "Suc (Suc (Suc n)) = # 3 + n";
24.50 +Goal "Suc (Suc (Suc n)) = 3 + n";
24.51 by (Simp_tac 1);
24.52 qed "Suc3_eq_add_3";
24.53
24.54 @@ -136,21 +136,21 @@
24.55 We already have some rules to simplify operands smaller than 3.
24.56 **)
24.57
24.58 -Goal "m div (Suc (Suc (Suc n))) = m div (# 3+n)";
24.59 +Goal "m div (Suc (Suc (Suc n))) = m div (3+n)";
24.60 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
24.61 qed "div_Suc_eq_div_add3";
24.62
24.63 -Goal "m mod (Suc (Suc (Suc n))) = m mod (# 3+n)";
24.64 +Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)";
24.65 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
24.66 qed "mod_Suc_eq_mod_add3";
24.67
24.68 Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3];
24.69
24.70 -Goal "(Suc (Suc (Suc m))) div n = (# 3+m) div n";
24.71 +Goal "(Suc (Suc (Suc m))) div n = (3+m) div n";
24.72 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
24.73 qed "Suc_div_eq_add3_div";
24.74
24.75 -Goal "(Suc (Suc (Suc m))) mod n = (# 3+m) mod n";
24.76 +Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n";
24.77 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
24.78 qed "Suc_mod_eq_add3_mod";
24.79
25.1 --- a/src/HOL/Integ/int_arith1.ML Fri Oct 05 23:58:52 2001 +0200
25.2 +++ b/src/HOL/Integ/int_arith1.ML Sat Oct 06 00:02:46 2001 +0200
25.3 @@ -279,7 +279,7 @@
25.4 structure CombineNumeralsData =
25.5 struct
25.6 val add = op + : int*int -> int
25.7 - val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
25.8 + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
25.9 val dest_sum = dest_sum
25.10 val mk_coeff = mk_coeff
25.11 val dest_coeff = dest_coeff 1
25.12 @@ -318,35 +318,35 @@
25.13 set trace_simp;
25.14 fun test s = (Goal s; by (Simp_tac 1));
25.15
25.16 -test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::int)";
25.17 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
25.18
25.19 -test "# 2*u = (u::int)";
25.20 -test "(i + j + # 12 + (k::int)) - # 15 = y";
25.21 -test "(i + j + # 12 + (k::int)) - # 5 = y";
25.22 +test "2*u = (u::int)";
25.23 +test "(i + j + 12 + (k::int)) - 15 = y";
25.24 +test "(i + j + 12 + (k::int)) - 5 = y";
25.25
25.26 test "y - b < (b::int)";
25.27 -test "y - (# 3*b + c) < (b::int) - # 2*c";
25.28 +test "y - (3*b + c) < (b::int) - 2*c";
25.29
25.30 -test "(# 2*x - (u*v) + y) - v*# 3*u = (w::int)";
25.31 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::int)";
25.32 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::int)";
25.33 -test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::int)";
25.34 +test "(2*x - (u*v) + y) - v*3*u = (w::int)";
25.35 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
25.36 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
25.37 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
25.38
25.39 -test "(i + j + # 12 + (k::int)) = u + # 15 + y";
25.40 -test "(i + j*# 2 + # 12 + (k::int)) = j + # 5 + y";
25.41 +test "(i + j + 12 + (k::int)) = u + 15 + y";
25.42 +test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
25.43
25.44 -test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::int)";
25.45 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)";
25.46
25.47 test "a + -(b+c) + b = (d::int)";
25.48 test "a + -(b+c) - b = (d::int)";
25.49
25.50 (*negative numerals*)
25.51 -test "(i + j + # -2 + (k::int)) - (u + # 5 + y) = zz";
25.52 -test "(i + j + # -3 + (k::int)) < u + # 5 + y";
25.53 -test "(i + j + # 3 + (k::int)) < u + # -6 + y";
25.54 -test "(i + j + # -12 + (k::int)) - # 15 = y";
25.55 -test "(i + j + # 12 + (k::int)) - # -15 = y";
25.56 -test "(i + j + # -12 + (k::int)) - # -15 = y";
25.57 +test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
25.58 +test "(i + j + -3 + (k::int)) < u + 5 + y";
25.59 +test "(i + j + 3 + (k::int)) < u + -6 + y";
25.60 +test "(i + j + -12 + (k::int)) - 15 = y";
25.61 +test "(i + j + 12 + (k::int)) - -15 = y";
25.62 +test "(i + j + -12 + (k::int)) - -15 = y";
25.63 *)
25.64
25.65
25.66 @@ -455,7 +455,7 @@
25.67 (* Some test data
25.68 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
25.69 by (fast_arith_tac 1);
25.70 -Goal "!!a::int. [| a < b; c < d |] ==> a-d+ # 2 <= b+(-c)";
25.71 +Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
25.72 by (fast_arith_tac 1);
25.73 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d";
25.74 by (fast_arith_tac 1);
25.75 @@ -465,7 +465,7 @@
25.76 \ ==> a+a <= j+j";
25.77 by (fast_arith_tac 1);
25.78 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
25.79 -\ ==> a+a - - # -1 < j+j - # 3";
25.80 +\ ==> a+a - - -1 < j+j - 3";
25.81 by (fast_arith_tac 1);
25.82 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
25.83 by (arith_tac 1);
25.84 @@ -482,6 +482,6 @@
25.85 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
25.86 by (fast_arith_tac 1);
25.87 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
25.88 -\ ==> # 6*a <= # 5*l+i";
25.89 +\ ==> 6*a <= 5*l+i";
25.90 by (fast_arith_tac 1);
25.91 *)
26.1 --- a/src/HOL/Integ/int_arith2.ML Fri Oct 05 23:58:52 2001 +0200
26.2 +++ b/src/HOL/Integ/int_arith2.ML Sat Oct 06 00:02:46 2001 +0200
26.3 @@ -75,7 +75,7 @@
26.4 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
26.5 qed "nat_1";
26.6
26.7 -Goal "nat # 2 = Suc (Suc 0)";
26.8 +Goal "nat 2 = Suc (Suc 0)";
26.9 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
26.10 qed "nat_2";
26.11
27.1 --- a/src/HOL/Integ/int_factor_simprocs.ML Fri Oct 05 23:58:52 2001 +0200
27.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML Sat Oct 06 00:02:46 2001 +0200
27.3 @@ -114,33 +114,33 @@
27.4 set trace_simp;
27.5 fun test s = (Goal s; by (Simp_tac 1));
27.6
27.7 -test "# 9*x = # 12 * (y::int)";
27.8 -test "(# 9*x) div (# 12 * (y::int)) = z";
27.9 -test "# 9*x < # 12 * (y::int)";
27.10 -test "# 9*x <= # 12 * (y::int)";
27.11 +test "9*x = 12 * (y::int)";
27.12 +test "(9*x) div (12 * (y::int)) = z";
27.13 +test "9*x < 12 * (y::int)";
27.14 +test "9*x <= 12 * (y::int)";
27.15
27.16 -test "# -99*x = # 132 * (y::int)";
27.17 -test "(# -99*x) div (# 132 * (y::int)) = z";
27.18 -test "# -99*x < # 132 * (y::int)";
27.19 -test "# -99*x <= # 132 * (y::int)";
27.20 +test "-99*x = 132 * (y::int)";
27.21 +test "(-99*x) div (132 * (y::int)) = z";
27.22 +test "-99*x < 132 * (y::int)";
27.23 +test "-99*x <= 132 * (y::int)";
27.24
27.25 -test "# 999*x = # -396 * (y::int)";
27.26 -test "(# 999*x) div (# -396 * (y::int)) = z";
27.27 -test "# 999*x < # -396 * (y::int)";
27.28 -test "# 999*x <= # -396 * (y::int)";
27.29 +test "999*x = -396 * (y::int)";
27.30 +test "(999*x) div (-396 * (y::int)) = z";
27.31 +test "999*x < -396 * (y::int)";
27.32 +test "999*x <= -396 * (y::int)";
27.33
27.34 -test "# -99*x = # -81 * (y::int)";
27.35 -test "(# -99*x) div (# -81 * (y::int)) = z";
27.36 -test "# -99*x <= # -81 * (y::int)";
27.37 -test "# -99*x < # -81 * (y::int)";
27.38 +test "-99*x = -81 * (y::int)";
27.39 +test "(-99*x) div (-81 * (y::int)) = z";
27.40 +test "-99*x <= -81 * (y::int)";
27.41 +test "-99*x < -81 * (y::int)";
27.42
27.43 -test "# -2 * x = # -1 * (y::int)";
27.44 -test "# -2 * x = -(y::int)";
27.45 -test "(# -2 * x) div (# -1 * (y::int)) = z";
27.46 -test "# -2 * x < -(y::int)";
27.47 -test "# -2 * x <= # -1 * (y::int)";
27.48 -test "-x < # -23 * (y::int)";
27.49 -test "-x <= # -23 * (y::int)";
27.50 +test "-2 * x = -1 * (y::int)";
27.51 +test "-2 * x = -(y::int)";
27.52 +test "(-2 * x) div (-1 * (y::int)) = z";
27.53 +test "-2 * x < -(y::int)";
27.54 +test "-2 * x <= -1 * (y::int)";
27.55 +test "-x < -23 * (y::int)";
27.56 +test "-x <= -23 * (y::int)";
27.57 *)
27.58
27.59
28.1 --- a/src/HOL/Integ/nat_bin.ML Fri Oct 05 23:58:52 2001 +0200
28.2 +++ b/src/HOL/Integ/nat_bin.ML Sat Oct 06 00:02:46 2001 +0200
28.3 @@ -25,7 +25,7 @@
28.4 by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def, One_nat_def]) 1);
28.5 qed "numeral_1_eq_1";
28.6
28.7 -Goal "# 2 = Suc 1";
28.8 +Goal "2 = Suc 1";
28.9 by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def, One_nat_def]) 1);
28.10 qed "numeral_2_eq_2";
28.11
28.12 @@ -77,7 +77,7 @@
28.13 by (Simp_tac 1);
28.14 qed "Suc_numeral_0_eq_1";
28.15
28.16 -Goal "Suc Numeral1 = # 2";
28.17 +Goal "Suc Numeral1 = 2";
28.18 by (Simp_tac 1);
28.19 qed "Suc_numeral_1_eq_2";
28.20
28.21 @@ -384,7 +384,7 @@
28.22 qed "power_one";
28.23 Addsimps [power_zero, power_one];
28.24
28.25 -Goal "(p::nat) ^ # 2 = p*p";
28.26 +Goal "(p::nat) ^ 2 = p*p";
28.27 by (simp_tac numeral_ss 1);
28.28 qed "power_two";
28.29
28.30 @@ -497,7 +497,7 @@
28.31
28.32 Goal "m+m ~= int (Suc 0) + n + n";
28.33 by Auto_tac;
28.34 -by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
28.35 +by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
28.36 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
28.37 val lemma2 = result();
28.38
28.39 @@ -514,7 +514,7 @@
28.40 by (res_inst_tac [("x", "number_of v")] spec 1);
28.41 by Safe_tac;
28.42 by (ALLGOALS Full_simp_tac);
28.43 -by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
28.44 +by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
28.45 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
28.46 qed "eq_number_of_BIT_Pls";
28.47
28.48 @@ -524,7 +524,7 @@
28.49 [number_of_BIT, number_of_Min, eq_commute]) 1);
28.50 by (res_inst_tac [("x", "number_of v")] spec 1);
28.51 by Auto_tac;
28.52 -by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
28.53 +by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
28.54 by Auto_tac;
28.55 qed "eq_number_of_BIT_Min";
28.56
29.1 --- a/src/HOL/Integ/nat_simprocs.ML Fri Oct 05 23:58:52 2001 +0200
29.2 +++ b/src/HOL/Integ/nat_simprocs.ML Sat Oct 06 00:02:46 2001 +0200
29.3 @@ -319,7 +319,7 @@
29.4 structure CombineNumeralsData =
29.5 struct
29.6 val add = op + : int*int -> int
29.7 - val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
29.8 + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
29.9 val dest_sum = restricted_dest_Sucs_sum
29.10 val mk_coeff = mk_coeff
29.11 val dest_coeff = dest_coeff
29.12 @@ -504,62 +504,62 @@
29.13 fun test s = (Goal s; by (Simp_tac 1));
29.14
29.15 (*cancel_numerals*)
29.16 -test "l +( # 2) + (# 2) + # 2 + (l + # 2) + (oo + # 2) = (uu::nat)";
29.17 -test "(# 2*length xs < # 2*length xs + j)";
29.18 -test "(# 2*length xs < length xs * # 2 + j)";
29.19 -test "# 2*u = (u::nat)";
29.20 -test "# 2*u = Suc (u)";
29.21 -test "(i + j + # 12 + (k::nat)) - # 15 = y";
29.22 -test "(i + j + # 12 + (k::nat)) - # 5 = y";
29.23 -test "Suc u - # 2 = y";
29.24 -test "Suc (Suc (Suc u)) - # 2 = y";
29.25 -test "(i + j + # 2 + (k::nat)) - 1 = y";
29.26 +test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)";
29.27 +test "(2*length xs < 2*length xs + j)";
29.28 +test "(2*length xs < length xs * 2 + j)";
29.29 +test "2*u = (u::nat)";
29.30 +test "2*u = Suc (u)";
29.31 +test "(i + j + 12 + (k::nat)) - 15 = y";
29.32 +test "(i + j + 12 + (k::nat)) - 5 = y";
29.33 +test "Suc u - 2 = y";
29.34 +test "Suc (Suc (Suc u)) - 2 = y";
29.35 +test "(i + j + 2 + (k::nat)) - 1 = y";
29.36 test "(i + j + Numeral1 + (k::nat)) - 2 = y";
29.37
29.38 -test "(# 2*x + (u*v) + y) - v*# 3*u = (w::nat)";
29.39 -test "(# 2*x*u*v + # 5 + (u*v)*# 4 + y) - v*u*# 4 = (w::nat)";
29.40 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::nat)";
29.41 -test "Suc (Suc (# 2*x*u*v + u*# 4 + y)) - u = w";
29.42 -test "Suc ((u*v)*# 4) - v*# 3*u = w";
29.43 -test "Suc (Suc ((u*v)*# 3)) - v*# 3*u = w";
29.44 +test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
29.45 +test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
29.46 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
29.47 +test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
29.48 +test "Suc ((u*v)*4) - v*3*u = w";
29.49 +test "Suc (Suc ((u*v)*3)) - v*3*u = w";
29.50
29.51 -test "(i + j + # 12 + (k::nat)) = u + # 15 + y";
29.52 -test "(i + j + # 32 + (k::nat)) - (u + # 15 + y) = zz";
29.53 -test "(i + j + # 12 + (k::nat)) = u + # 5 + y";
29.54 +test "(i + j + 12 + (k::nat)) = u + 15 + y";
29.55 +test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
29.56 +test "(i + j + 12 + (k::nat)) = u + 5 + y";
29.57 (*Suc*)
29.58 -test "(i + j + # 12 + k) = Suc (u + y)";
29.59 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + # 41 + k)";
29.60 -test "(i + j + # 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
29.61 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) - # 5 = v";
29.62 -test "(i + j + # 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
29.63 -test "# 2*y + # 3*z + # 2*u = Suc (u)";
29.64 -test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = Suc (u)";
29.65 -test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::nat)";
29.66 -test "# 6 + # 2*y + # 3*z + # 4*u = Suc (vv + # 2*u + z)";
29.67 -test "(# 2*n*m) < (# 3*(m*n)) + (u::nat)";
29.68 +test "(i + j + 12 + k) = Suc (u + y)";
29.69 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
29.70 +test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
29.71 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
29.72 +test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
29.73 +test "2*y + 3*z + 2*u = Suc (u)";
29.74 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
29.75 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)";
29.76 +test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
29.77 +test "(2*n*m) < (3*(m*n)) + (u::nat)";
29.78
29.79 (*negative numerals: FAIL*)
29.80 -test "(i + j + # -23 + (k::nat)) < u + # 15 + y";
29.81 -test "(i + j + # 3 + (k::nat)) < u + # -15 + y";
29.82 -test "(i + j + # -12 + (k::nat)) - # 15 = y";
29.83 -test "(i + j + # 12 + (k::nat)) - # -15 = y";
29.84 -test "(i + j + # -12 + (k::nat)) - # -15 = y";
29.85 +test "(i + j + -23 + (k::nat)) < u + 15 + y";
29.86 +test "(i + j + 3 + (k::nat)) < u + -15 + y";
29.87 +test "(i + j + -12 + (k::nat)) - 15 = y";
29.88 +test "(i + j + 12 + (k::nat)) - -15 = y";
29.89 +test "(i + j + -12 + (k::nat)) - -15 = y";
29.90
29.91 (*combine_numerals*)
29.92 -test "k + # 3*k = (u::nat)";
29.93 -test "Suc (i + # 3) = u";
29.94 -test "Suc (i + j + # 3 + k) = u";
29.95 -test "k + j + # 3*k + j = (u::nat)";
29.96 -test "Suc (j*i + i + k + # 5 + # 3*k + i*j*# 4) = (u::nat)";
29.97 -test "(# 2*n*m) + (# 3*(m*n)) = (u::nat)";
29.98 +test "k + 3*k = (u::nat)";
29.99 +test "Suc (i + 3) = u";
29.100 +test "Suc (i + j + 3 + k) = u";
29.101 +test "k + j + 3*k + j = (u::nat)";
29.102 +test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
29.103 +test "(2*n*m) + (3*(m*n)) = (u::nat)";
29.104 (*negative numerals: FAIL*)
29.105 -test "Suc (i + j + # -3 + k) = u";
29.106 +test "Suc (i + j + -3 + k) = u";
29.107
29.108 (*cancel_numeral_factors*)
29.109 -test "# 9*x = # 12 * (y::nat)";
29.110 -test "(# 9*x) div (# 12 * (y::nat)) = z";
29.111 -test "# 9*x < # 12 * (y::nat)";
29.112 -test "# 9*x <= # 12 * (y::nat)";
29.113 +test "9*x = 12 * (y::nat)";
29.114 +test "(9*x) div (12 * (y::nat)) = z";
29.115 +test "9*x < 12 * (y::nat)";
29.116 +test "9*x <= 12 * (y::nat)";
29.117
29.118 (*cancel_factor*)
29.119 test "x*k = k*(y::nat)";
30.1 --- a/src/HOL/Isar_examples/Fibonacci.thy Fri Oct 05 23:58:52 2001 +0200
30.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy Sat Oct 06 00:02:46 2001 +0200
30.3 @@ -39,7 +39,7 @@
30.4 text {* Alternative induction rule. *}
30.5
30.6 theorem fib_induct:
30.7 - "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + # 2)) ==> P (n::nat)"
30.8 + "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
30.9 by (induct rule: fib.induct, simp+)
30.10
30.11
30.12 @@ -56,7 +56,7 @@
30.13 show "?P 0" by simp
30.14 show "?P 1" by simp
30.15 fix n
30.16 - have "fib (n + # 2 + k + 1)
30.17 + have "fib (n + 2 + k + 1)
30.18 = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
30.19 also assume "fib (n + k + 1)
30.20 = fib (k + 1) * fib (n + 1) + fib k * fib n"
30.21 @@ -65,9 +65,9 @@
30.22 = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
30.23 (is " _ = ?R2")
30.24 also have "?R1 + ?R2
30.25 - = fib (k + 1) * fib (n + # 2 + 1) + fib k * fib (n + # 2)"
30.26 + = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
30.27 by (simp add: add_mult_distrib2)
30.28 - finally show "?P (n + # 2)" .
30.29 + finally show "?P (n + 2)" .
30.30 qed
30.31
30.32 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
30.33 @@ -75,14 +75,14 @@
30.34 show "?P 0" by simp
30.35 show "?P 1" by simp
30.36 fix n
30.37 - have "fib (n + # 2 + 1) = fib (n + 1) + fib (n + # 2)"
30.38 + have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
30.39 by simp
30.40 - also have "gcd (fib (n + # 2), ...) = gcd (fib (n + # 2), fib (n + 1))"
30.41 + also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
30.42 by (simp only: gcd_add2')
30.43 also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
30.44 by (simp add: gcd_commute)
30.45 also assume "... = 1"
30.46 - finally show "?P (n + # 2)" .
30.47 + finally show "?P (n + 2)" .
30.48 qed
30.49
30.50 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
31.1 --- a/src/HOL/Isar_examples/HoareEx.thy Fri Oct 05 23:58:52 2001 +0200
31.2 +++ b/src/HOL/Isar_examples/HoareEx.thy Sat Oct 06 00:02:46 2001 +0200
31.3 @@ -39,7 +39,7 @@
31.4 *}
31.5
31.6 lemma
31.7 - "|- .{\<acute>(N_update (# 2 * \<acute>N)) : .{\<acute>N = # 10}.}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
31.8 + "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
31.9 by (rule assign)
31.10
31.11 text {*
31.12 @@ -49,13 +49,13 @@
31.13 ``obvious'' consequences as well.
31.14 *}
31.15
31.16 -lemma "|- .{True}. \<acute>N := # 10 .{\<acute>N = # 10}."
31.17 +lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
31.18 by hoare
31.19
31.20 -lemma "|- .{# 2 * \<acute>N = # 10}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
31.21 +lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
31.22 by hoare
31.23
31.24 -lemma "|- .{\<acute>N = # 5}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
31.25 +lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
31.26 by hoare simp
31.27
31.28 lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
32.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 05 23:58:52 2001 +0200
32.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sat Oct 06 00:02:46 2001 +0200
32.3 @@ -76,7 +76,7 @@
32.4 by (simp add: below_def less_Suc_eq) blast
32.5
32.6 lemma Sigma_Suc2:
32.7 - "m = n + # 2 ==> A <*> below m =
32.8 + "m = n + 2 ==> A <*> below m =
32.9 (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
32.10 by (auto simp add: below_def) arith
32.11
32.12 @@ -87,10 +87,10 @@
32.13
32.14 constdefs
32.15 evnodd :: "(nat * nat) set => nat => (nat * nat) set"
32.16 - "evnodd A b == A Int {(i, j). (i + j) mod # 2 = b}"
32.17 + "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
32.18
32.19 lemma evnodd_iff:
32.20 - "(i, j): evnodd A b = ((i, j): A & (i + j) mod # 2 = b)"
32.21 + "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"
32.22 by (simp add: evnodd_def)
32.23
32.24 lemma evnodd_subset: "evnodd A b <= A"
32.25 @@ -112,7 +112,7 @@
32.26 by (simp add: evnodd_def)
32.27
32.28 lemma evnodd_insert: "evnodd (insert (i, j) C) b =
32.29 - (if (i + j) mod # 2 = b
32.30 + (if (i + j) mod 2 = b
32.31 then insert (i, j) (evnodd C b) else evnodd C b)"
32.32 by (simp add: evnodd_def) blast
32.33
32.34 @@ -128,21 +128,21 @@
32.35 vertl: "{(i, j), (i + 1, j)} : domino"
32.36
32.37 lemma dominoes_tile_row:
32.38 - "{i} <*> below (# 2 * n) : tiling domino"
32.39 + "{i} <*> below (2 * n) : tiling domino"
32.40 (is "?P n" is "?B n : ?T")
32.41 proof (induct n)
32.42 show "?P 0" by (simp add: below_0 tiling.empty)
32.43
32.44 fix n assume hyp: "?P n"
32.45 - let ?a = "{i} <*> {# 2 * n + 1} Un {i} <*> {# 2 * n}"
32.46 + let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
32.47
32.48 have "?B (Suc n) = ?a Un ?B n"
32.49 by (auto simp add: Sigma_Suc Un_assoc)
32.50 also have "... : ?T"
32.51 proof (rule tiling.Un)
32.52 - have "{(i, # 2 * n), (i, # 2 * n + 1)} : domino"
32.53 + have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
32.54 by (rule domino.horiz)
32.55 - also have "{(i, # 2 * n), (i, # 2 * n + 1)} = ?a" by blast
32.56 + also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
32.57 finally show "... : domino" .
32.58 from hyp show "?B n : ?T" .
32.59 show "?a <= - ?B n" by blast
32.60 @@ -151,13 +151,13 @@
32.61 qed
32.62
32.63 lemma dominoes_tile_matrix:
32.64 - "below m <*> below (# 2 * n) : tiling domino"
32.65 + "below m <*> below (2 * n) : tiling domino"
32.66 (is "?P m" is "?B m : ?T")
32.67 proof (induct m)
32.68 show "?P 0" by (simp add: below_0 tiling.empty)
32.69
32.70 fix m assume hyp: "?P m"
32.71 - let ?t = "{m} <*> below (# 2 * n)"
32.72 + let ?t = "{m} <*> below (2 * n)"
32.73
32.74 have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
32.75 also have "... : ?T"
32.76 @@ -170,9 +170,9 @@
32.77 qed
32.78
32.79 lemma domino_singleton:
32.80 - "d : domino ==> b < # 2 ==> EX i j. evnodd d b = {(i, j)}"
32.81 + "d : domino ==> b < 2 ==> EX i j. evnodd d b = {(i, j)}"
32.82 proof -
32.83 - assume b: "b < # 2"
32.84 + assume b: "b < 2"
32.85 assume "d : domino"
32.86 thus ?thesis (is "?P d")
32.87 proof induct
32.88 @@ -227,9 +227,9 @@
32.89 and at: "a <= - t"
32.90
32.91 have card_suc:
32.92 - "!!b. b < # 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
32.93 + "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
32.94 proof -
32.95 - fix b :: nat assume "b < # 2"
32.96 + fix b :: nat assume "b < 2"
32.97 have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
32.98 also obtain i j where e: "?e a b = {(i, j)}"
32.99 proof -
32.100 @@ -260,15 +260,15 @@
32.101 constdefs
32.102 mutilated_board :: "nat => nat => (nat * nat) set"
32.103 "mutilated_board m n ==
32.104 - below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))
32.105 - - {(0, 0)} - {(# 2 * m + 1, # 2 * n + 1)}"
32.106 + below (2 * (m + 1)) <*> below (2 * (n + 1))
32.107 + - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
32.108
32.109 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
32.110 proof (unfold mutilated_board_def)
32.111 let ?T = "tiling domino"
32.112 - let ?t = "below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))"
32.113 + let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
32.114 let ?t' = "?t - {(0, 0)}"
32.115 - let ?t'' = "?t' - {(# 2 * m + 1, # 2 * n + 1)}"
32.116 + let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
32.117
32.118 show "?t'' ~: ?T"
32.119 proof
32.120 @@ -282,12 +282,12 @@
32.121 note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff
32.122 have "card (?e ?t'' 0) < card (?e ?t' 0)"
32.123 proof -
32.124 - have "card (?e ?t' 0 - {(# 2 * m + 1, # 2 * n + 1)})
32.125 + have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
32.126 < card (?e ?t' 0)"
32.127 proof (rule card_Diff1_less)
32.128 from _ fin show "finite (?e ?t' 0)"
32.129 by (rule finite_subset) auto
32.130 - show "(# 2 * m + 1, # 2 * n + 1) : ?e ?t' 0" by simp
32.131 + show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
32.132 qed
32.133 thus ?thesis by simp
32.134 qed
33.1 --- a/src/HOL/Isar_examples/Summation.thy Fri Oct 05 23:58:52 2001 +0200
33.2 +++ b/src/HOL/Isar_examples/Summation.thy Sat Oct 06 00:02:46 2001 +0200
33.3 @@ -31,14 +31,14 @@
33.4 *}
33.5
33.6 theorem sum_of_naturals:
33.7 - "# 2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
33.8 + "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
33.9 (is "?P n" is "?S n = _")
33.10 proof (induct n)
33.11 show "?P 0" by simp
33.12 next
33.13 - fix n have "?S (n + 1) = ?S n + # 2 * (n + 1)" by simp
33.14 + fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
33.15 also assume "?S n = n * (n + 1)"
33.16 - also have "... + # 2 * (n + 1) = (n + 1) * (n + # 2)" by simp
33.17 + also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
33.18 finally show "?P (Suc n)" by simp
33.19 qed
33.20
33.21 @@ -86,14 +86,14 @@
33.22 *}
33.23
33.24 theorem sum_of_odds:
33.25 - "(\<Sum>i < n. # 2 * i + 1) = n^Suc (Suc 0)"
33.26 + "(\<Sum>i < n. 2 * i + 1) = n^Suc (Suc 0)"
33.27 (is "?P n" is "?S n = _")
33.28 proof (induct n)
33.29 show "?P 0" by simp
33.30 next
33.31 - fix n have "?S (n + 1) = ?S n + # 2 * n + 1" by simp
33.32 + fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
33.33 also assume "?S n = n^Suc (Suc 0)"
33.34 - also have "... + # 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
33.35 + also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
33.36 finally show "?P (Suc n)" by simp
33.37 qed
33.38
33.39 @@ -106,28 +106,28 @@
33.40 lemmas distrib = add_mult_distrib add_mult_distrib2
33.41
33.42 theorem sum_of_squares:
33.43 - "# 6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (# 2 * n + 1)"
33.44 + "6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
33.45 (is "?P n" is "?S n = _")
33.46 proof (induct n)
33.47 show "?P 0" by simp
33.48 next
33.49 - fix n have "?S (n + 1) = ?S n + # 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
33.50 - also assume "?S n = n * (n + 1) * (# 2 * n + 1)"
33.51 - also have "... + # 6 * (n + 1)^Suc (Suc 0) =
33.52 - (n + 1) * (n + # 2) * (# 2 * (n + 1) + 1)" by (simp add: distrib)
33.53 + fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
33.54 + also assume "?S n = n * (n + 1) * (2 * n + 1)"
33.55 + also have "... + 6 * (n + 1)^Suc (Suc 0) =
33.56 + (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
33.57 finally show "?P (Suc n)" by simp
33.58 qed
33.59
33.60 theorem sum_of_cubes:
33.61 - "# 4 * (\<Sum>i < n + 1. i^# 3) = (n * (n + 1))^Suc (Suc 0)"
33.62 + "4 * (\<Sum>i < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
33.63 (is "?P n" is "?S n = _")
33.64 proof (induct n)
33.65 show "?P 0" by (simp add: power_eq_if)
33.66 next
33.67 - fix n have "?S (n + 1) = ?S n + # 4 * (n + 1)^# 3"
33.68 + fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
33.69 by (simp add: power_eq_if distrib)
33.70 also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
33.71 - also have "... + # 4 * (n + 1)^# 3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
33.72 + also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
33.73 by (simp add: power_eq_if distrib)
33.74 finally show "?P (Suc n)" by simp
33.75 qed
34.1 --- a/src/HOL/Lambda/Type.thy Fri Oct 05 23:58:52 2001 +0200
34.2 +++ b/src/HOL/Lambda/Type.thy Sat Oct 06 00:02:46 2001 +0200
34.3 @@ -59,11 +59,11 @@
34.4
34.5 subsection {* Some examples *}
34.6
34.7 -lemma "e |- Abs (Abs (Abs (Var 1 $ (Var # 2 $ Var 1 $ Var 0)))) : ?T"
34.8 +lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T"
34.9 apply force
34.10 done
34.11
34.12 -lemma "e |- Abs (Abs (Abs (Var # 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
34.13 +lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
34.14 apply force
34.15 done
34.16
35.1 --- a/src/HOL/Library/While_Combinator.thy Fri Oct 05 23:58:52 2001 +0200
35.2 +++ b/src/HOL/Library/While_Combinator.thy Sat Oct 06 00:02:46 2001 +0200
35.3 @@ -135,14 +135,14 @@
35.4 theory.}
35.5 *}
35.6
35.7 -theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + # 2) mod # 6 | n. n \<in> N})) =
35.8 - P {Numeral0, # 4, # 2}"
35.9 +theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
35.10 + P {Numeral0, 4, 2}"
35.11 proof -
35.12 have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
35.13 apply blast
35.14 done
35.15 show ?thesis
35.16 - apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, # 2, # 3, # 4, # 5}"])
35.17 + apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
35.18 apply (rule monoI)
35.19 apply blast
35.20 apply simp
36.1 --- a/src/HOL/NumberTheory/EulerFermat.thy Fri Oct 05 23:58:52 2001 +0200
36.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy Sat Oct 06 00:02:46 2001 +0200
36.3 @@ -55,7 +55,7 @@
36.4 zcongm :: "int => int => int => bool"
36.5 "zcongm m == \<lambda>a b. zcong a b m"
36.6
36.7 -lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = # -1)"
36.8 +lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = -1)"
36.9 -- {* LCP: not sure why this lemma is needed now *}
36.10 apply (auto simp add: zabs_def)
36.11 done
37.1 --- a/src/HOL/NumberTheory/Fib.thy Fri Oct 05 23:58:52 2001 +0200
37.2 +++ b/src/HOL/NumberTheory/Fib.thy Sat Oct 06 00:02:46 2001 +0200
37.3 @@ -67,14 +67,14 @@
37.4 *}
37.5
37.6 lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
37.7 - (if n mod # 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
37.8 + (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
37.9 else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
37.10 apply (induct n rule: fib.induct)
37.11 apply (simp add: fib.Suc_Suc)
37.12 apply (simp add: fib.Suc_Suc mod_Suc)
37.13 apply (simp add: fib.Suc_Suc
37.14 add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
37.15 - apply (subgoal_tac "x mod # 2 < # 2", arith)
37.16 + apply (subgoal_tac "x mod 2 < 2", arith)
37.17 apply simp
37.18 done
37.19
38.1 --- a/src/HOL/NumberTheory/WilsonBij.thy Fri Oct 05 23:58:52 2001 +0200
38.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy Sat Oct 06 00:02:46 2001 +0200
38.3 @@ -133,15 +133,15 @@
38.4 apply auto
38.5 done
38.6
38.7 -lemma aux3: "x \<le> p - # 2 ==> x < (p::int)"
38.8 +lemma aux3: "x \<le> p - 2 ==> x < (p::int)"
38.9 apply auto
38.10 done
38.11
38.12 -lemma aux4: "x \<le> p - # 2 ==> x < (p::int)-Numeral1"
38.13 +lemma aux4: "x \<le> p - 2 ==> x < (p::int)-Numeral1"
38.14 apply auto
38.15 done
38.16
38.17 -lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - # 2))"
38.18 +lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - 2))"
38.19 apply (unfold inj_on_def)
38.20 apply auto
38.21 apply (rule zcong_zless_imp_eq)
38.22 @@ -160,7 +160,7 @@
38.23 done
38.24
38.25 lemma inv_d22set_d22set:
38.26 - "p \<in> zprime ==> inv p ` d22set (p - # 2) = d22set (p - # 2)"
38.27 + "p \<in> zprime ==> inv p ` d22set (p - 2) = d22set (p - 2)"
38.28 apply (rule endo_inj_surj)
38.29 apply (rule d22set_fin)
38.30 apply (erule_tac [2] inv_inj)
38.31 @@ -173,9 +173,9 @@
38.32 done
38.33
38.34 lemma d22set_d22set_bij:
38.35 - "p \<in> zprime ==> (d22set (p - # 2), d22set (p - # 2)) \<in> bijR (reciR p)"
38.36 + "p \<in> zprime ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)"
38.37 apply (unfold reciR_def)
38.38 - apply (rule_tac s = "(d22set (p - # 2), inv p ` d22set (p - # 2))" in subst)
38.39 + apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst)
38.40 apply (simp add: inv_d22set_d22set)
38.41 apply (rule inj_func_bijR)
38.42 apply (rule_tac [3] d22set_fin)
38.43 @@ -187,7 +187,7 @@
38.44 apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4)
38.45 done
38.46
38.47 -lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - # 2))"
38.48 +lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - 2))"
38.49 apply (unfold reciR_def bijP_def)
38.50 apply auto
38.51 apply (rule d22set_mem)
38.52 @@ -217,7 +217,7 @@
38.53 apply auto
38.54 done
38.55
38.56 -lemma bijER_d22set: "p \<in> zprime ==> d22set (p - # 2) \<in> bijER (reciR p)"
38.57 +lemma bijER_d22set: "p \<in> zprime ==> d22set (p - 2) \<in> bijER (reciR p)"
38.58 apply (rule bijR_bijER)
38.59 apply (erule d22set_d22set_bij)
38.60 apply (erule reciP_bijP)
38.61 @@ -245,12 +245,12 @@
38.62 apply auto
38.63 done
38.64
38.65 -theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
38.66 - apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - # 2)) (# -1 * Numeral1) p")
38.67 +theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
38.68 + apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - 2)) (-1 * Numeral1) p")
38.69 apply (rule_tac [2] zcong_zmult)
38.70 apply (simp add: zprime_def)
38.71 apply (subst zfact.simps)
38.72 - apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
38.73 + apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
38.74 apply auto
38.75 apply (simp add: zcong_def)
38.76 apply (subst d22set_prod_zfact [symmetric])
39.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Oct 05 23:58:52 2001 +0200
39.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy Sat Oct 06 00:02:46 2001 +0200
39.3 @@ -20,7 +20,7 @@
39.4 wset :: "int * int => int set"
39.5
39.6 defs
39.7 - inv_def: "inv p a == (a^(nat (p - # 2))) mod p"
39.8 + inv_def: "inv p a == (a^(nat (p - 2))) mod p"
39.9
39.10 recdef wset
39.11 "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
39.12 @@ -32,7 +32,7 @@
39.13
39.14 text {* \medskip @{term [source] inv} *}
39.15
39.16 -lemma aux: "Numeral1 < m ==> Suc (nat (m - # 2)) = nat (m - Numeral1)"
39.17 +lemma aux: "Numeral1 < m ==> Suc (nat (m - 2)) = nat (m - Numeral1)"
39.18 apply (subst int_int_eq [symmetric])
39.19 apply auto
39.20 done
39.21 @@ -137,8 +137,8 @@
39.22 apply (simp add: pos_mod_bound)
39.23 done
39.24
39.25 -lemma aux: "# 5 \<le> p ==>
39.26 - nat (p - # 2) * nat (p - # 2) = Suc (nat (p - Numeral1) * nat (p - # 3))"
39.27 +lemma aux: "5 \<le> p ==>
39.28 + nat (p - 2) * nat (p - 2) = Suc (nat (p - Numeral1) * nat (p - 3))"
39.29 apply (subst int_int_eq [symmetric])
39.30 apply (simp add: zmult_int [symmetric])
39.31 apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
39.32 @@ -154,7 +154,7 @@
39.33 done
39.34
39.35 lemma inv_inv: "p \<in> zprime \<Longrightarrow>
39.36 - # 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
39.37 + 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
39.38 apply (unfold inv_def)
39.39 apply (subst zpower_zmod)
39.40 apply (subst zpower_zpower)
39.41 @@ -165,7 +165,7 @@
39.42 apply (subst zcong_zmod [symmetric])
39.43 apply (subst aux)
39.44 apply (subgoal_tac [2]
39.45 - "zcong (a * a^(nat (p - Numeral1) * nat (p - # 3))) (a * Numeral1) p")
39.46 + "zcong (a * a^(nat (p - Numeral1) * nat (p - 3))) (a * Numeral1) p")
39.47 apply (rule_tac [3] zcong_zmult)
39.48 apply (rule_tac [4] zcong_zpower_zmult)
39.49 apply (erule_tac [4] Little_Fermat)
39.50 @@ -256,7 +256,7 @@
39.51 done
39.52
39.53 lemma wset_mem_inv_mem [rule_format]:
39.54 - "p \<in> zprime --> # 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
39.55 + "p \<in> zprime --> 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
39.56 --> inv p b \<in> wset (a, p)"
39.57 apply (induct a p rule: wset_induct)
39.58 apply auto
39.59 @@ -274,7 +274,7 @@
39.60 done
39.61
39.62 lemma wset_inv_mem_mem:
39.63 - "p \<in> zprime \<Longrightarrow> # 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
39.64 + "p \<in> zprime \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
39.65 \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
39.66 apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
39.67 apply (rule_tac [2] wset_mem_inv_mem)
39.68 @@ -292,7 +292,7 @@
39.69
39.70 lemma wset_zcong_prod_1 [rule_format]:
39.71 "p \<in> zprime -->
39.72 - # 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
39.73 + 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
39.74 apply (induct a p rule: wset_induct)
39.75 prefer 2
39.76 apply (subst wset.simps)
39.77 @@ -314,7 +314,7 @@
39.78 apply auto
39.79 done
39.80
39.81 -lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - # 2) = wset (p - # 2, p)"
39.82 +lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - 2) = wset (p - 2, p)"
39.83 apply safe
39.84 apply (erule wset_mem)
39.85 apply (rule_tac [2] d22set_g_1)
39.86 @@ -323,7 +323,7 @@
39.87 apply (erule_tac [4] wset_g_1)
39.88 prefer 6
39.89 apply (subst zle_add1_eq_le [symmetric])
39.90 - apply (subgoal_tac "p - # 2 + Numeral1 = p - Numeral1")
39.91 + apply (subgoal_tac "p - 2 + Numeral1 = p - Numeral1")
39.92 apply (simp (no_asm_simp))
39.93 apply (erule wset_less)
39.94 apply auto
39.95 @@ -332,36 +332,36 @@
39.96
39.97 subsection {* Wilson *}
39.98
39.99 -lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> # 2 \<Longrightarrow> p \<noteq> # 3 ==> # 5 \<le> p"
39.100 +lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
39.101 apply (unfold zprime_def dvd_def)
39.102 - apply (case_tac "p = # 4")
39.103 + apply (case_tac "p = 4")
39.104 apply auto
39.105 apply (rule notE)
39.106 prefer 2
39.107 apply assumption
39.108 apply (simp (no_asm))
39.109 - apply (rule_tac x = "# 2" in exI)
39.110 + apply (rule_tac x = "2" in exI)
39.111 apply safe
39.112 - apply (rule_tac x = "# 2" in exI)
39.113 + apply (rule_tac x = "2" in exI)
39.114 apply auto
39.115 apply arith
39.116 done
39.117
39.118 theorem Wilson_Russ:
39.119 - "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
39.120 - apply (subgoal_tac "[(p - Numeral1) * zfact (p - # 2) = # -1 * Numeral1] (mod p)")
39.121 + "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
39.122 + apply (subgoal_tac "[(p - Numeral1) * zfact (p - 2) = -1 * Numeral1] (mod p)")
39.123 apply (rule_tac [2] zcong_zmult)
39.124 apply (simp only: zprime_def)
39.125 apply (subst zfact.simps)
39.126 - apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
39.127 + apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
39.128 apply auto
39.129 apply (simp only: zcong_def)
39.130 apply (simp (no_asm_simp))
39.131 - apply (case_tac "p = # 2")
39.132 + apply (case_tac "p = 2")
39.133 apply (simp add: zfact.simps)
39.134 - apply (case_tac "p = # 3")
39.135 + apply (case_tac "p = 3")
39.136 apply (simp add: zfact.simps)
39.137 - apply (subgoal_tac "# 5 \<le> p")
39.138 + apply (subgoal_tac "5 \<le> p")
39.139 apply (erule_tac [2] prime_g_5)
39.140 apply (subst d22set_prod_zfact [symmetric])
39.141 apply (subst d22set_eq_wset)
40.1 --- a/src/HOL/Numeral.thy Fri Oct 05 23:58:52 2001 +0200
40.2 +++ b/src/HOL/Numeral.thy Sat Oct 06 00:02:46 2001 +0200
40.3 @@ -24,7 +24,7 @@
40.4
40.5 syntax
40.6 "_constify" :: "num => numeral" ("_")
40.7 - "_Numeral" :: "numeral => 'a" ("#_")
40.8 + "_Numeral" :: "numeral => 'a" ("_")
40.9 Numeral0 :: 'a
40.10 Numeral1 :: 'a
40.11
41.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Oct 05 23:58:52 2001 +0200
41.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sat Oct 06 00:02:46 2001 +0200
41.3 @@ -86,7 +86,7 @@
41.4 by (unfold is_vectorspace_def) simp
41.5
41.6 lemma negate_eq2a:
41.7 - "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> # -1 \<cdot> x = - x"
41.8 + "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
41.9 by (unfold is_vectorspace_def) simp
41.10
41.11 lemma diff_eq2:
42.1 --- a/src/HOL/Real/RComplete.ML Fri Oct 05 23:58:52 2001 +0200
42.2 +++ b/src/HOL/Real/RComplete.ML Sat Oct 06 00:02:46 2001 +0200
42.3 @@ -8,7 +8,7 @@
42.4
42.5 claset_ref() := claset() delWrapper "bspec";
42.6
42.7 -Goal "x/# 2 + x/# 2 = (x::real)";
42.8 +Goal "x/2 + x/2 = (x::real)";
42.9 by (Simp_tac 1);
42.10 qed "real_sum_of_halves";
42.11
43.1 --- a/src/HOL/Real/RealArith0.ML Fri Oct 05 23:58:52 2001 +0200
43.2 +++ b/src/HOL/Real/RealArith0.ML Sat Oct 06 00:02:46 2001 +0200
43.3 @@ -276,34 +276,34 @@
43.4 set trace_simp;
43.5 fun test s = (Goal s; by (Simp_tac 1));
43.6
43.7 -test "Numeral0 <= (y::real) * # -2";
43.8 -test "# 9*x = # 12 * (y::real)";
43.9 -test "(# 9*x) / (# 12 * (y::real)) = z";
43.10 -test "# 9*x < # 12 * (y::real)";
43.11 -test "# 9*x <= # 12 * (y::real)";
43.12 +test "Numeral0 <= (y::real) * -2";
43.13 +test "9*x = 12 * (y::real)";
43.14 +test "(9*x) / (12 * (y::real)) = z";
43.15 +test "9*x < 12 * (y::real)";
43.16 +test "9*x <= 12 * (y::real)";
43.17
43.18 -test "# -99*x = # 132 * (y::real)";
43.19 -test "(# -99*x) / (# 132 * (y::real)) = z";
43.20 -test "# -99*x < # 132 * (y::real)";
43.21 -test "# -99*x <= # 132 * (y::real)";
43.22 +test "-99*x = 132 * (y::real)";
43.23 +test "(-99*x) / (132 * (y::real)) = z";
43.24 +test "-99*x < 132 * (y::real)";
43.25 +test "-99*x <= 132 * (y::real)";
43.26
43.27 -test "# 999*x = # -396 * (y::real)";
43.28 -test "(# 999*x) / (# -396 * (y::real)) = z";
43.29 -test "# 999*x < # -396 * (y::real)";
43.30 -test "# 999*x <= # -396 * (y::real)";
43.31 +test "999*x = -396 * (y::real)";
43.32 +test "(999*x) / (-396 * (y::real)) = z";
43.33 +test "999*x < -396 * (y::real)";
43.34 +test "999*x <= -396 * (y::real)";
43.35
43.36 -test "# -99*x = # -81 * (y::real)";
43.37 -test "(# -99*x) / (# -81 * (y::real)) = z";
43.38 -test "# -99*x <= # -81 * (y::real)";
43.39 -test "# -99*x < # -81 * (y::real)";
43.40 +test "-99*x = -81 * (y::real)";
43.41 +test "(-99*x) / (-81 * (y::real)) = z";
43.42 +test "-99*x <= -81 * (y::real)";
43.43 +test "-99*x < -81 * (y::real)";
43.44
43.45 -test "# -2 * x = # -1 * (y::real)";
43.46 -test "# -2 * x = -(y::real)";
43.47 -test "(# -2 * x) / (# -1 * (y::real)) = z";
43.48 -test "# -2 * x < -(y::real)";
43.49 -test "# -2 * x <= # -1 * (y::real)";
43.50 -test "-x < # -23 * (y::real)";
43.51 -test "-x <= # -23 * (y::real)";
43.52 +test "-2 * x = -1 * (y::real)";
43.53 +test "-2 * x = -(y::real)";
43.54 +test "(-2 * x) / (-1 * (y::real)) = z";
43.55 +test "-2 * x < -(y::real)";
43.56 +test "-2 * x <= -1 * (y::real)";
43.57 +test "-x < -23 * (y::real)";
43.58 +test "-x <= -23 * (y::real)";
43.59 *)
43.60
43.61
43.62 @@ -505,18 +505,18 @@
43.63 qed "real_divide_1";
43.64 Addsimps [real_divide_1];
43.65
43.66 -Goal "x/# -1 = -(x::real)";
43.67 +Goal "x/-1 = -(x::real)";
43.68 by (Simp_tac 1);
43.69 qed "real_divide_minus1";
43.70 Addsimps [real_divide_minus1];
43.71
43.72 -Goal "# -1/(x::real) = - (Numeral1/x)";
43.73 +Goal "-1/(x::real) = - (Numeral1/x)";
43.74 by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
43.75 qed "real_minus1_divide";
43.76 Addsimps [real_minus1_divide];
43.77
43.78 Goal "[| (Numeral0::real) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
43.79 -by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1);
43.80 +by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
43.81 by (asm_simp_tac (simpset() addsimps [min_def]) 1);
43.82 qed "real_lbound_gt_zero";
43.83
43.84 @@ -647,11 +647,11 @@
43.85
43.86 (*** Density of the Reals ***)
43.87
43.88 -Goal "x < y ==> x < (x+y) / (# 2::real)";
43.89 +Goal "x < y ==> x < (x+y) / (2::real)";
43.90 by Auto_tac;
43.91 qed "real_less_half_sum";
43.92
43.93 -Goal "x < y ==> (x+y)/(# 2::real) < y";
43.94 +Goal "x < y ==> (x+y)/(2::real) < y";
43.95 by Auto_tac;
43.96 qed "real_gt_half_sum";
43.97
44.1 --- a/src/HOL/Real/RealBin.ML Fri Oct 05 23:58:52 2001 +0200
44.2 +++ b/src/HOL/Real/RealBin.ML Sat Oct 06 00:02:46 2001 +0200
44.3 @@ -58,18 +58,18 @@
44.4
44.5 Addsimps [mult_real_number_of];
44.6
44.7 -Goal "(# 2::real) = Numeral1 + Numeral1";
44.8 +Goal "(2::real) = Numeral1 + Numeral1";
44.9 by (Simp_tac 1);
44.10 val lemma = result();
44.11
44.12 (*For specialist use: NOT as default simprules*)
44.13 -Goal "# 2 * z = (z+z::real)";
44.14 +Goal "2 * z = (z+z::real)";
44.15 by (simp_tac (simpset ()
44.16 addsimps [lemma, real_add_mult_distrib,
44.17 one_eq_numeral_1 RS sym]) 1);
44.18 qed "real_mult_2";
44.19
44.20 -Goal "z * # 2 = (z+z::real)";
44.21 +Goal "z * 2 = (z+z::real)";
44.22 by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
44.23 qed "real_mult_2_right";
44.24
44.25 @@ -111,12 +111,12 @@
44.26
44.27 (*** New versions of existing theorems involving 0, 1r ***)
44.28
44.29 -Goal "- Numeral1 = (# -1::real)";
44.30 +Goal "- Numeral1 = (-1::real)";
44.31 by (Simp_tac 1);
44.32 qed "minus_numeral_one";
44.33
44.34
44.35 -(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to # -1*)
44.36 +(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to -1*)
44.37 val real_numeral_ss =
44.38 HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1,
44.39 minus_numeral_one];
44.40 @@ -488,7 +488,7 @@
44.41 structure CombineNumeralsData =
44.42 struct
44.43 val add = op + : int*int -> int
44.44 - val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
44.45 + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
44.46 val dest_sum = dest_sum
44.47 val mk_coeff = mk_coeff
44.48 val dest_coeff = dest_coeff 1
44.49 @@ -548,35 +548,35 @@
44.50 set trace_simp;
44.51 fun test s = (Goal s; by (Simp_tac 1));
44.52
44.53 -test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::real)";
44.54 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::real)";
44.55
44.56 -test "# 2*u = (u::real)";
44.57 -test "(i + j + # 12 + (k::real)) - # 15 = y";
44.58 -test "(i + j + # 12 + (k::real)) - # 5 = y";
44.59 +test "2*u = (u::real)";
44.60 +test "(i + j + 12 + (k::real)) - 15 = y";
44.61 +test "(i + j + 12 + (k::real)) - 5 = y";
44.62
44.63 test "y - b < (b::real)";
44.64 -test "y - (# 3*b + c) < (b::real) - # 2*c";
44.65 +test "y - (3*b + c) < (b::real) - 2*c";
44.66
44.67 -test "(# 2*x - (u*v) + y) - v*# 3*u = (w::real)";
44.68 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::real)";
44.69 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::real)";
44.70 -test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::real)";
44.71 +test "(2*x - (u*v) + y) - v*3*u = (w::real)";
44.72 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::real)";
44.73 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::real)";
44.74 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::real)";
44.75
44.76 -test "(i + j + # 12 + (k::real)) = u + # 15 + y";
44.77 -test "(i + j*# 2 + # 12 + (k::real)) = j + # 5 + y";
44.78 +test "(i + j + 12 + (k::real)) = u + 15 + y";
44.79 +test "(i + j*2 + 12 + (k::real)) = j + 5 + y";
44.80
44.81 -test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::real)";
44.82 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::real)";
44.83
44.84 test "a + -(b+c) + b = (d::real)";
44.85 test "a + -(b+c) - b = (d::real)";
44.86
44.87 (*negative numerals*)
44.88 -test "(i + j + # -2 + (k::real)) - (u + # 5 + y) = zz";
44.89 -test "(i + j + # -3 + (k::real)) < u + # 5 + y";
44.90 -test "(i + j + # 3 + (k::real)) < u + # -6 + y";
44.91 -test "(i + j + # -12 + (k::real)) - # 15 = y";
44.92 -test "(i + j + # 12 + (k::real)) - # -15 = y";
44.93 -test "(i + j + # -12 + (k::real)) - # -15 = y";
44.94 +test "(i + j + -2 + (k::real)) - (u + 5 + y) = zz";
44.95 +test "(i + j + -3 + (k::real)) < u + 5 + y";
44.96 +test "(i + j + 3 + (k::real)) < u + -6 + y";
44.97 +test "(i + j + -12 + (k::real)) - 15 = y";
44.98 +test "(i + j + 12 + (k::real)) - -15 = y";
44.99 +test "(i + j + -12 + (k::real)) - -15 = y";
44.100 *)
44.101
44.102
45.1 --- a/src/HOL/Real/RealPow.ML Fri Oct 05 23:58:52 2001 +0200
45.2 +++ b/src/HOL/Real/RealPow.ML Sat Oct 06 00:02:46 2001 +0200
45.3 @@ -76,7 +76,7 @@
45.4 qed "realpow_eq_one";
45.5 Addsimps [realpow_eq_one];
45.6
45.7 -Goal "abs((# -1) ^ n) = (Numeral1::real)";
45.8 +Goal "abs((-1) ^ n) = (Numeral1::real)";
45.9 by (induct_tac "n" 1);
45.10 by (auto_tac (claset(), simpset() addsimps [abs_mult]));
45.11 qed "abs_realpow_minus_one";
45.12 @@ -127,13 +127,13 @@
45.13 by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
45.14 qed "realpow_ge_one2";
45.15
45.16 -Goal "(Numeral1::real) <= # 2 ^ n";
45.17 +Goal "(Numeral1::real) <= 2 ^ n";
45.18 by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
45.19 by (rtac realpow_le 2);
45.20 by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
45.21 qed "two_realpow_ge_one";
45.22
45.23 -Goal "real (n::nat) < # 2 ^ n";
45.24 +Goal "real (n::nat) < 2 ^ n";
45.25 by (induct_tac "n" 1);
45.26 by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
45.27 by (stac real_mult_2 1);
45.28 @@ -142,18 +142,18 @@
45.29 qed "two_realpow_gt";
45.30 Addsimps [two_realpow_gt,two_realpow_ge_one];
45.31
45.32 -Goal "(# -1) ^ (# 2*n) = (Numeral1::real)";
45.33 +Goal "(-1) ^ (2*n) = (Numeral1::real)";
45.34 by (induct_tac "n" 1);
45.35 by Auto_tac;
45.36 qed "realpow_minus_one";
45.37 Addsimps [realpow_minus_one];
45.38
45.39 -Goal "(# -1) ^ Suc (# 2*n) = -(Numeral1::real)";
45.40 +Goal "(-1) ^ Suc (2*n) = -(Numeral1::real)";
45.41 by Auto_tac;
45.42 qed "realpow_minus_one_odd";
45.43 Addsimps [realpow_minus_one_odd];
45.44
45.45 -Goal "(# -1) ^ Suc (Suc (# 2*n)) = (Numeral1::real)";
45.46 +Goal "(-1) ^ Suc (Suc (2*n)) = (Numeral1::real)";
45.47 by Auto_tac;
45.48 qed "realpow_minus_one_even";
45.49 Addsimps [realpow_minus_one_even];
46.1 --- a/src/HOL/Real/ex/BinEx.thy Fri Oct 05 23:58:52 2001 +0200
46.2 +++ b/src/HOL/Real/ex/BinEx.thy Sat Oct 06 00:02:46 2001 +0200
46.3 @@ -15,52 +15,52 @@
46.4
46.5 text {* \medskip Addition *}
46.6
46.7 -lemma "(# 1359::real) + # -2468 = # -1109"
46.8 +lemma "(1359::real) + -2468 = -1109"
46.9 by simp
46.10
46.11 -lemma "(# 93746::real) + # -46375 = # 47371"
46.12 +lemma "(93746::real) + -46375 = 47371"
46.13 by simp
46.14
46.15
46.16 text {* \medskip Negation *}
46.17
46.18 -lemma "- (# 65745::real) = # -65745"
46.19 +lemma "- (65745::real) = -65745"
46.20 by simp
46.21
46.22 -lemma "- (# -54321::real) = # 54321"
46.23 +lemma "- (-54321::real) = 54321"
46.24 by simp
46.25
46.26
46.27 text {* \medskip Multiplication *}
46.28
46.29 -lemma "(# -84::real) * # 51 = # -4284"
46.30 +lemma "(-84::real) * 51 = -4284"
46.31 by simp
46.32
46.33 -lemma "(# 255::real) * # 255 = # 65025"
46.34 +lemma "(255::real) * 255 = 65025"
46.35 by simp
46.36
46.37 -lemma "(# 1359::real) * # -2468 = # -3354012"
46.38 +lemma "(1359::real) * -2468 = -3354012"
46.39 by simp
46.40
46.41
46.42 text {* \medskip Inequalities *}
46.43
46.44 -lemma "(# 89::real) * # 10 \<noteq> # 889"
46.45 +lemma "(89::real) * 10 \<noteq> 889"
46.46 by simp
46.47
46.48 -lemma "(# 13::real) < # 18 - # 4"
46.49 +lemma "(13::real) < 18 - 4"
46.50 by simp
46.51
46.52 -lemma "(# -345::real) < # -242 + # -100"
46.53 +lemma "(-345::real) < -242 + -100"
46.54 by simp
46.55
46.56 -lemma "(# 13557456::real) < # 18678654"
46.57 +lemma "(13557456::real) < 18678654"
46.58 by simp
46.59
46.60 -lemma "(# 999999::real) \<le> (# 1000001 + Numeral1)-# 2"
46.61 +lemma "(999999::real) \<le> (1000001 + Numeral1) - 2"
46.62 by simp
46.63
46.64 -lemma "(# 1234567::real) \<le> # 1234567"
46.65 +lemma "(1234567::real) \<le> 1234567"
46.66 by simp
46.67
46.68
47.1 --- a/src/HOL/Real/ex/Sqrt_Irrational.thy Fri Oct 05 23:58:52 2001 +0200
47.2 +++ b/src/HOL/Real/ex/Sqrt_Irrational.thy Sat Oct 06 00:02:46 2001 +0200
47.3 @@ -114,15 +114,15 @@
47.4 this formally :-).
47.5 *}
47.6
47.7 -theorem "x\<twosuperior> = real (# 2::nat) ==> x \<notin> \<rat>"
47.8 +theorem "x\<twosuperior> = real (2::nat) ==> x \<notin> \<rat>"
47.9 proof (rule sqrt_prime_irrational)
47.10 {
47.11 - fix m :: nat assume dvd: "m dvd # 2"
47.12 - hence "m \<le> # 2" by (simp add: dvd_imp_le)
47.13 + fix m :: nat assume dvd: "m dvd 2"
47.14 + hence "m \<le> 2" by (simp add: dvd_imp_le)
47.15 moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
47.16 - ultimately have "m = 1 \<or> m = # 2" by arith
47.17 + ultimately have "m = 1 \<or> m = 2" by arith
47.18 }
47.19 - thus "# 2 \<in> prime" by (simp add: prime_def)
47.20 + thus "2 \<in> prime" by (simp add: prime_def)
47.21 qed
47.22
47.23 text {*
48.1 --- a/src/HOL/Real/real_arith0.ML Fri Oct 05 23:58:52 2001 +0200
48.2 +++ b/src/HOL/Real/real_arith0.ML Sat Oct 06 00:02:46 2001 +0200
48.3 @@ -118,7 +118,7 @@
48.4 qed "";
48.5
48.6 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
48.7 -\ ==> # 6*a <= # 5*l+i";
48.8 +\ ==> 6*a <= 5*l+i";
48.9 by (fast_arith_tac 1);
48.10 qed "";
48.11 *)
49.1 --- a/src/HOL/UNITY/Simple/Mutex.ML Fri Oct 05 23:58:52 2001 +0200
49.2 +++ b/src/HOL/UNITY/Simple/Mutex.ML Sat Oct 06 00:02:46 2001 +0200
49.3 @@ -25,7 +25,7 @@
49.4 qed "IV";
49.5
49.6 (*The safety property: mutual exclusion*)
49.7 -Goal "Mutex : Always {s. ~ (m s = # 3 & n s = # 3)}";
49.8 +Goal "Mutex : Always {s. ~ (m s = 3 & n s = 3)}";
49.9 by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
49.10 by Auto_tac;
49.11 qed "mutual_exclusion";
49.12 @@ -42,33 +42,33 @@
49.13 getgoal 1;
49.14
49.15
49.16 -Goal "((Numeral1::int) <= i & i <= # 3) = (i = Numeral1 | i = # 2 | i = # 3)";
49.17 +Goal "((Numeral1::int) <= i & i <= 3) = (i = Numeral1 | i = 2 | i = 3)";
49.18 by (arith_tac 1);
49.19 qed "eq_123";
49.20
49.21
49.22 (*** Progress for U ***)
49.23
49.24 -Goalw [Unless_def] "Mutex : {s. m s=# 2} Unless {s. m s=# 3}";
49.25 +Goalw [Unless_def] "Mutex : {s. m s=2} Unless {s. m s=3}";
49.26 by (constrains_tac 1);
49.27 qed "U_F0";
49.28
49.29 -Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = # 2}";
49.30 +Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = 2}";
49.31 by (ensures_tac "U1" 1);
49.32 qed "U_F1";
49.33
49.34 -Goal "Mutex : {s. ~ p s & m s = # 2} LeadsTo {s. m s = # 3}";
49.35 +Goal "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}";
49.36 by (cut_facts_tac [IU] 1);
49.37 by (ensures_tac "U2" 1);
49.38 qed "U_F2";
49.39
49.40 -Goal "Mutex : {s. m s = # 3} LeadsTo {s. p s}";
49.41 -by (res_inst_tac [("B", "{s. m s = # 4}")] LeadsTo_Trans 1);
49.42 +Goal "Mutex : {s. m s = 3} LeadsTo {s. p s}";
49.43 +by (res_inst_tac [("B", "{s. m s = 4}")] LeadsTo_Trans 1);
49.44 by (ensures_tac "U4" 2);
49.45 by (ensures_tac "U3" 1);
49.46 qed "U_F3";
49.47
49.48 -Goal "Mutex : {s. m s = # 2} LeadsTo {s. p s}";
49.49 +Goal "Mutex : {s. m s = 2} LeadsTo {s. p s}";
49.50 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
49.51 MRS LeadsTo_Diff) 1);
49.52 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
49.53 @@ -80,7 +80,7 @@
49.54 by (Blast_tac 1);
49.55 val U_lemma1 = result();
49.56
49.57 -Goal "Mutex : {s. Numeral1 <= m s & m s <= # 3} LeadsTo {s. p s}";
49.58 +Goal "Mutex : {s. Numeral1 <= m s & m s <= 3} LeadsTo {s. p s}";
49.59 by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
49.60 U_lemma1, U_lemma2, U_F3] ) 1);
49.61 val U_lemma123 = result();
49.62 @@ -95,26 +95,26 @@
49.63 (*** Progress for V ***)
49.64
49.65
49.66 -Goalw [Unless_def] "Mutex : {s. n s=# 2} Unless {s. n s=# 3}";
49.67 +Goalw [Unless_def] "Mutex : {s. n s=2} Unless {s. n s=3}";
49.68 by (constrains_tac 1);
49.69 qed "V_F0";
49.70
49.71 -Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = # 2}";
49.72 +Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = 2}";
49.73 by (ensures_tac "V1" 1);
49.74 qed "V_F1";
49.75
49.76 -Goal "Mutex : {s. p s & n s = # 2} LeadsTo {s. n s = # 3}";
49.77 +Goal "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}";
49.78 by (cut_facts_tac [IV] 1);
49.79 by (ensures_tac "V2" 1);
49.80 qed "V_F2";
49.81
49.82 -Goal "Mutex : {s. n s = # 3} LeadsTo {s. ~ p s}";
49.83 -by (res_inst_tac [("B", "{s. n s = # 4}")] LeadsTo_Trans 1);
49.84 +Goal "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}";
49.85 +by (res_inst_tac [("B", "{s. n s = 4}")] LeadsTo_Trans 1);
49.86 by (ensures_tac "V4" 2);
49.87 by (ensures_tac "V3" 1);
49.88 qed "V_F3";
49.89
49.90 -Goal "Mutex : {s. n s = # 2} LeadsTo {s. ~ p s}";
49.91 +Goal "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}";
49.92 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
49.93 MRS LeadsTo_Diff) 1);
49.94 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
49.95 @@ -126,7 +126,7 @@
49.96 by (Blast_tac 1);
49.97 val V_lemma1 = result();
49.98
49.99 -Goal "Mutex : {s. Numeral1 <= n s & n s <= # 3} LeadsTo {s. ~ p s}";
49.100 +Goal "Mutex : {s. Numeral1 <= n s & n s <= 3} LeadsTo {s. ~ p s}";
49.101 by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
49.102 V_lemma1, V_lemma2, V_F3] ) 1);
49.103 val V_lemma123 = result();
49.104 @@ -142,7 +142,7 @@
49.105 (** Absence of starvation **)
49.106
49.107 (*Misra's F6*)
49.108 -Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = # 3}";
49.109 +Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = 3}";
49.110 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
49.111 by (rtac U_F2 2);
49.112 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
49.113 @@ -154,7 +154,7 @@
49.114 qed "m1_Leadsto_3";
49.115
49.116 (*The same for V*)
49.117 -Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = # 3}";
49.118 +Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = 3}";
49.119 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
49.120 by (rtac V_F2 2);
49.121 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
50.1 --- a/src/HOL/UNITY/Simple/Mutex.thy Fri Oct 05 23:58:52 2001 +0200
50.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy Sat Oct 06 00:02:46 2001 +0200
50.3 @@ -25,16 +25,16 @@
50.4 "U0 == {(s,s'). s' = s (|u:=True, m:=Numeral1|) & m s = Numeral0}"
50.5
50.6 U1 :: command
50.7 - "U1 == {(s,s'). s' = s (|p:= v s, m:=# 2|) & m s = Numeral1}"
50.8 + "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = Numeral1}"
50.9
50.10 U2 :: command
50.11 - "U2 == {(s,s'). s' = s (|m:=# 3|) & ~ p s & m s = # 2}"
50.12 + "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}"
50.13
50.14 U3 :: command
50.15 - "U3 == {(s,s'). s' = s (|u:=False, m:=# 4|) & m s = # 3}"
50.16 + "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}"
50.17
50.18 U4 :: command
50.19 - "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = # 4}"
50.20 + "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = 4}"
50.21
50.22 (** The program for process V **)
50.23
50.24 @@ -42,16 +42,16 @@
50.25 "V0 == {(s,s'). s' = s (|v:=True, n:=Numeral1|) & n s = Numeral0}"
50.26
50.27 V1 :: command
50.28 - "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=# 2|) & n s = Numeral1}"
50.29 + "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = Numeral1}"
50.30
50.31 V2 :: command
50.32 - "V2 == {(s,s'). s' = s (|n:=# 3|) & p s & n s = # 2}"
50.33 + "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}"
50.34
50.35 V3 :: command
50.36 - "V3 == {(s,s'). s' = s (|v:=False, n:=# 4|) & n s = # 3}"
50.37 + "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}"
50.38
50.39 V4 :: command
50.40 - "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = # 4}"
50.41 + "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = 4}"
50.42
50.43 Mutex :: state program
50.44 "Mutex == mk_program ({s. ~ u s & ~ v s & m s = Numeral0 & n s = Numeral0},
50.45 @@ -62,15 +62,15 @@
50.46 (** The correct invariants **)
50.47
50.48 IU :: state set
50.49 - "IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) & (m s = # 3 --> ~ p s)}"
50.50 + "IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
50.51
50.52 IV :: state set
50.53 - "IV == {s. (v s = (Numeral1 <= n s & n s <= # 3)) & (n s = # 3 --> p s)}"
50.54 + "IV == {s. (v s = (Numeral1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
50.55
50.56 (** The faulty invariant (for U alone) **)
50.57
50.58 bad_IU :: state set
50.59 - "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) &
50.60 - (# 3 <= m s & m s <= # 4 --> ~ p s)}"
50.61 + "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) &
50.62 + (3 <= m s & m s <= 4 --> ~ p s)}"
50.63
50.64 end
51.1 --- a/src/HOL/UNITY/Union.ML Fri Oct 05 23:58:52 2001 +0200
51.2 +++ b/src/HOL/UNITY/Union.ML Sat Oct 06 00:02:46 2001 +0200
51.3 @@ -352,7 +352,7 @@
51.4
51.5 bind_thm ("ok_sym", ok_commute RS iffD1);
51.6
51.7 -Goal "OK {(Numeral0::int,F),(Numeral1,G),(# 2,H)} snd = (F ok G & (F Join G) ok H)";
51.8 +Goal "OK {(Numeral0::int,F),(Numeral1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
51.9 by (asm_full_simp_tac
51.10 (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def,
51.11 OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);
52.1 --- a/src/HOL/Unix/ROOT.ML Fri Oct 05 23:58:52 2001 +0200
52.2 +++ b/src/HOL/Unix/ROOT.ML Sat Oct 06 00:02:46 2001 +0200
52.3 @@ -1,3 +1,3 @@
52.4
52.5 -Library.setmp print_mode (! print_mode @ ["no_brackets"])
52.6 +Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
52.7 use_thy "Unix";
53.1 --- a/src/HOL/arith_data.ML Fri Oct 05 23:58:52 2001 +0200
53.2 +++ b/src/HOL/arith_data.ML Sat Oct 06 00:02:46 2001 +0200
53.3 @@ -438,7 +438,7 @@
53.4 [Simplifier.change_simpset_of (op addSolver)
53.5 (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
53.6 Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
53.7 - Method.add_methods [("arith", (arith_method o # 2) oo Method.syntax Args.bang_facts,
53.8 + Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
53.9 "decide linear arithmethic")],
53.10 Attrib.add_attributes [("arith_split",
53.11 (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
54.1 --- a/src/HOL/ex/BinEx.thy Fri Oct 05 23:58:52 2001 +0200
54.2 +++ b/src/HOL/ex/BinEx.thy Sat Oct 06 00:02:46 2001 +0200
54.3 @@ -12,75 +12,75 @@
54.4
54.5 text {* Addition *}
54.6
54.7 -lemma "(# 13::int) + # 19 = # 32"
54.8 +lemma "(13::int) + 19 = 32"
54.9 by simp
54.10
54.11 -lemma "(# 1234::int) + # 5678 = # 6912"
54.12 +lemma "(1234::int) + 5678 = 6912"
54.13 by simp
54.14
54.15 -lemma "(# 1359::int) + # -2468 = # -1109"
54.16 +lemma "(1359::int) + -2468 = -1109"
54.17 by simp
54.18
54.19 -lemma "(# 93746::int) + # -46375 = # 47371"
54.20 +lemma "(93746::int) + -46375 = 47371"
54.21 by simp
54.22
54.23
54.24 text {* \medskip Negation *}
54.25
54.26 -lemma "- (# 65745::int) = # -65745"
54.27 +lemma "- (65745::int) = -65745"
54.28 by simp
54.29
54.30 -lemma "- (# -54321::int) = # 54321"
54.31 +lemma "- (-54321::int) = 54321"
54.32 by simp
54.33
54.34
54.35 text {* \medskip Multiplication *}
54.36
54.37 -lemma "(# 13::int) * # 19 = # 247"
54.38 +lemma "(13::int) * 19 = 247"
54.39 by simp
54.40
54.41 -lemma "(# -84::int) * # 51 = # -4284"
54.42 +lemma "(-84::int) * 51 = -4284"
54.43 by simp
54.44
54.45 -lemma "(# 255::int) * # 255 = # 65025"
54.46 +lemma "(255::int) * 255 = 65025"
54.47 by simp
54.48
54.49 -lemma "(# 1359::int) * # -2468 = # -3354012"
54.50 +lemma "(1359::int) * -2468 = -3354012"
54.51 by simp
54.52
54.53 -lemma "(# 89::int) * # 10 \<noteq> # 889"
54.54 +lemma "(89::int) * 10 \<noteq> 889"
54.55 by simp
54.56
54.57 -lemma "(# 13::int) < # 18 - # 4"
54.58 +lemma "(13::int) < 18 - 4"
54.59 by simp
54.60
54.61 -lemma "(# -345::int) < # -242 + # -100"
54.62 +lemma "(-345::int) < -242 + -100"
54.63 by simp
54.64
54.65 -lemma "(# 13557456::int) < # 18678654"
54.66 +lemma "(13557456::int) < 18678654"
54.67 by simp
54.68
54.69 -lemma "(# 999999::int) \<le> (# 1000001 + Numeral1) - # 2"
54.70 +lemma "(999999::int) \<le> (1000001 + Numeral1) - 2"
54.71 by simp
54.72
54.73 -lemma "(# 1234567::int) \<le> # 1234567"
54.74 +lemma "(1234567::int) \<le> 1234567"
54.75 by simp
54.76
54.77
54.78 text {* \medskip Quotient and Remainder *}
54.79
54.80 -lemma "(# 10::int) div # 3 = # 3"
54.81 +lemma "(10::int) div 3 = 3"
54.82 by simp
54.83
54.84 -lemma "(# 10::int) mod # 3 = Numeral1"
54.85 +lemma "(10::int) mod 3 = Numeral1"
54.86 by simp
54.87
54.88 text {* A negative divisor *}
54.89
54.90 -lemma "(# 10::int) div # -3 = # -4"
54.91 +lemma "(10::int) div -3 = -4"
54.92 by simp
54.93
54.94 -lemma "(# 10::int) mod # -3 = # -2"
54.95 +lemma "(10::int) mod -3 = -2"
54.96 by simp
54.97
54.98 text {*
54.99 @@ -88,50 +88,50 @@
54.100 convention but not with the hardware of most computers}
54.101 *}
54.102
54.103 -lemma "(# -10::int) div # 3 = # -4"
54.104 +lemma "(-10::int) div 3 = -4"
54.105 by simp
54.106
54.107 -lemma "(# -10::int) mod # 3 = # 2"
54.108 +lemma "(-10::int) mod 3 = 2"
54.109 by simp
54.110
54.111 text {* A negative dividend \emph{and} divisor *}
54.112
54.113 -lemma "(# -10::int) div # -3 = # 3"
54.114 +lemma "(-10::int) div -3 = 3"
54.115 by simp
54.116
54.117 -lemma "(# -10::int) mod # -3 = # -1"
54.118 +lemma "(-10::int) mod -3 = -1"
54.119 by simp
54.120
54.121 text {* A few bigger examples *}
54.122
54.123 -lemma "(# 8452::int) mod # 3 = Numeral1"
54.124 +lemma "(8452::int) mod 3 = Numeral1"
54.125 by simp
54.126
54.127 -lemma "(# 59485::int) div # 434 = # 137"
54.128 +lemma "(59485::int) div 434 = 137"
54.129 by simp
54.130
54.131 -lemma "(# 1000006::int) mod # 10 = # 6"
54.132 +lemma "(1000006::int) mod 10 = 6"
54.133 by simp
54.134
54.135
54.136 text {* \medskip Division by shifting *}
54.137
54.138 -lemma "# 10000000 div # 2 = (# 5000000::int)"
54.139 +lemma "10000000 div 2 = (5000000::int)"
54.140 by simp
54.141
54.142 -lemma "# 10000001 mod # 2 = (Numeral1::int)"
54.143 +lemma "10000001 mod 2 = (Numeral1::int)"
54.144 by simp
54.145
54.146 -lemma "# 10000055 div # 32 = (# 312501::int)"
54.147 +lemma "10000055 div 32 = (312501::int)"
54.148 by simp
54.149
54.150 -lemma "# 10000055 mod # 32 = (# 23::int)"
54.151 +lemma "10000055 mod 32 = (23::int)"
54.152 by simp
54.153
54.154 -lemma "# 100094 div # 144 = (# 695::int)"
54.155 +lemma "100094 div 144 = (695::int)"
54.156 by simp
54.157
54.158 -lemma "# 100094 mod # 144 = (# 14::int)"
54.159 +lemma "100094 mod 144 = (14::int)"
54.160 by simp
54.161
54.162
54.163 @@ -139,65 +139,65 @@
54.164
54.165 text {* Successor *}
54.166
54.167 -lemma "Suc # 99999 = # 100000"
54.168 +lemma "Suc 99999 = 100000"
54.169 by (simp add: Suc_nat_number_of)
54.170 -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
54.171
54.172
54.173 text {* \medskip Addition *}
54.174
54.175 -lemma "(# 13::nat) + # 19 = # 32"
54.176 +lemma "(13::nat) + 19 = 32"
54.177 by simp
54.178
54.179 -lemma "(# 1234::nat) + # 5678 = # 6912"
54.180 +lemma "(1234::nat) + 5678 = 6912"
54.181 by simp
54.182
54.183 -lemma "(# 973646::nat) + # 6475 = # 980121"
54.184 +lemma "(973646::nat) + 6475 = 980121"
54.185 by simp
54.186
54.187
54.188 text {* \medskip Subtraction *}
54.189
54.190 -lemma "(# 32::nat) - # 14 = # 18"
54.191 +lemma "(32::nat) - 14 = 18"
54.192 by simp
54.193
54.194 -lemma "(# 14::nat) - # 15 = Numeral0"
54.195 +lemma "(14::nat) - 15 = Numeral0"
54.196 by simp
54.197
54.198 -lemma "(# 14::nat) - # 1576644 = Numeral0"
54.199 +lemma "(14::nat) - 1576644 = Numeral0"
54.200 by simp
54.201
54.202 -lemma "(# 48273776::nat) - # 3873737 = # 44400039"
54.203 +lemma "(48273776::nat) - 3873737 = 44400039"
54.204 by simp
54.205
54.206
54.207 text {* \medskip Multiplication *}
54.208
54.209 -lemma "(# 12::nat) * # 11 = # 132"
54.210 +lemma "(12::nat) * 11 = 132"
54.211 by simp
54.212
54.213 -lemma "(# 647::nat) * # 3643 = # 2357021"
54.214 +lemma "(647::nat) * 3643 = 2357021"
54.215 by simp
54.216
54.217
54.218 text {* \medskip Quotient and Remainder *}
54.219
54.220 -lemma "(# 10::nat) div # 3 = # 3"
54.221 +lemma "(10::nat) div 3 = 3"
54.222 by simp
54.223
54.224 -lemma "(# 10::nat) mod # 3 = Numeral1"
54.225 +lemma "(10::nat) mod 3 = Numeral1"
54.226 by simp
54.227
54.228 -lemma "(# 10000::nat) div # 9 = # 1111"
54.229 +lemma "(10000::nat) div 9 = 1111"
54.230 by simp
54.231
54.232 -lemma "(# 10000::nat) mod # 9 = Numeral1"
54.233 +lemma "(10000::nat) mod 9 = Numeral1"
54.234 by simp
54.235
54.236 -lemma "(# 10000::nat) div # 16 = # 625"
54.237 +lemma "(10000::nat) div 16 = 625"
54.238 by simp
54.239
54.240 -lemma "(# 10000::nat) mod # 16 = Numeral0"
54.241 +lemma "(10000::nat) mod 16 = Numeral0"
54.242 by simp
54.243
54.244
55.1 --- a/src/HOL/ex/NatSum.thy Fri Oct 05 23:58:52 2001 +0200
55.2 +++ b/src/HOL/ex/NatSum.thy Sat Oct 06 00:02:46 2001 +0200
55.3 @@ -36,8 +36,8 @@
55.4 *}
55.5
55.6 lemma sum_of_odd_squares:
55.7 - "# 3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
55.8 - n * (# 4 * n * n - Numeral1)"
55.9 + "3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
55.10 + n * (4 * n * n - Numeral1)"
55.11 apply (induct n)
55.12 txt {* This removes the @{term "-Numeral1"} from the inductive step *}
55.13 apply (case_tac [2] n)
55.14 @@ -51,7 +51,7 @@
55.15
55.16 lemma sum_of_odd_cubes:
55.17 "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
55.18 - n * n * (# 2 * n * n - Numeral1)"
55.19 + n * n * (2 * n * n - Numeral1)"
55.20 apply (induct "n")
55.21 txt {* This removes the @{term "-Numeral1"} from the inductive step *}
55.22 apply (case_tac [2] "n")
55.23 @@ -63,19 +63,19 @@
55.24 @{text "n (n + 1) / 2"}.*}
55.25
55.26 lemma sum_of_naturals:
55.27 - "# 2 * setsum id (atMost n) = n * Suc n"
55.28 + "2 * setsum id (atMost n) = n * Suc n"
55.29 apply (induct n)
55.30 apply auto
55.31 done
55.32
55.33 lemma sum_of_squares:
55.34 - "# 6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (# 2 * n)"
55.35 + "6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (2 * n)"
55.36 apply (induct n)
55.37 apply auto
55.38 done
55.39
55.40 lemma sum_of_cubes:
55.41 - "# 4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
55.42 + "4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
55.43 apply (induct n)
55.44 apply auto
55.45 done
55.46 @@ -86,8 +86,8 @@
55.47 *}
55.48
55.49 lemma sum_of_fourth_powers:
55.50 - "# 30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
55.51 - n * Suc n * Suc (# 2 * n) * (# 3 * n * n + # 3 * n - Numeral1)"
55.52 + "30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
55.53 + n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - Numeral1)"
55.54 apply (induct n)
55.55 apply auto
55.56 txt {* Eliminates the subtraction *}
55.57 @@ -107,9 +107,9 @@
55.58 zdiff_zmult_distrib2 [simp]
55.59
55.60 lemma int_sum_of_fourth_powers:
55.61 - "# 30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
55.62 - int m * (int m - Numeral1) * (int (# 2 * m) - Numeral1) *
55.63 - (int (# 3 * m * m) - int (# 3 * m) - Numeral1)"
55.64 + "30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
55.65 + int m * (int m - Numeral1) * (int (2 * m) - Numeral1) *
55.66 + (int (3 * m * m) - int (3 * m) - Numeral1)"
55.67 apply (induct m)
55.68 apply simp_all
55.69 done
55.70 @@ -118,12 +118,12 @@
55.71 text {*
55.72 \medskip Sums of geometric series: 2, 3 and the general case *}
55.73
55.74 -lemma sum_of_2_powers: "setsum (\<lambda>i. # 2^i) (lessThan n) = # 2^n - (1::nat)"
55.75 +lemma sum_of_2_powers: "setsum (\<lambda>i. 2^i) (lessThan n) = 2^n - (1::nat)"
55.76 apply (induct n)
55.77 apply (auto split: nat_diff_split)
55.78 done
55.79
55.80 -lemma sum_of_3_powers: "# 2 * setsum (\<lambda>i. # 3^i) (lessThan n) = # 3^n - (1::nat)"
55.81 +lemma sum_of_3_powers: "2 * setsum (\<lambda>i. 3^i) (lessThan n) = 3^n - (1::nat)"
55.82 apply (induct n)
55.83 apply auto
55.84 done
56.1 --- a/src/HOL/ex/Primrec.thy Fri Oct 05 23:58:52 2001 +0200
56.2 +++ b/src/HOL/ex/Primrec.thy Sat Oct 06 00:02:46 2001 +0200
56.3 @@ -159,7 +159,7 @@
56.4
56.5 text {* PROPERTY A 8 *}
56.6
56.7 -lemma ack_1 [simp]: "ack (Suc 0, j) = j + # 2"
56.8 +lemma ack_1 [simp]: "ack (Suc 0, j) = j + 2"
56.9 apply (induct j)
56.10 apply simp_all
56.11 done
56.12 @@ -168,7 +168,7 @@
56.13 text {* PROPERTY A 9. The unary @{text 1} and @{text 2} in @{term
56.14 ack} is essential for the rewriting. *}
56.15
56.16 -lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = # 2 * j + # 3"
56.17 +lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = 2 * j + 3"
56.18 apply (induct j)
56.19 apply simp_all
56.20 done
56.21 @@ -203,7 +203,7 @@
56.22
56.23 text {* PROPERTY A 10 *}
56.24
56.25 -lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (# 2 + (i1 + i2), j)"
56.26 +lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (2 + (i1 + i2), j)"
56.27 apply (simp add: numerals)
56.28 apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
56.29 apply simp
56.30 @@ -215,7 +215,7 @@
56.31
56.32 text {* PROPERTY A 11 *}
56.33
56.34 -lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (# 4 + (i1 + i2), j)"
56.35 +lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (4 + (i1 + i2), j)"
56.36 apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans)
56.37 prefer 2
56.38 apply (rule ack_nest_bound [THEN less_le_trans])
56.39 @@ -231,7 +231,7 @@
56.40 used @{text "k + 4"}. Quantified version must be nested @{text
56.41 "\<exists>k'. \<forall>i j. ..."} *}
56.42
56.43 -lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (# 4 + k, j)"
56.44 +lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (4 + k, j)"
56.45 apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
56.46 prefer 2
56.47 apply (rule ack_add_bound [THEN less_le_trans])
57.1 --- a/src/HOL/ex/Records.thy Fri Oct 05 23:58:52 2001 +0200
57.2 +++ b/src/HOL/ex/Records.thy Sat Oct 06 00:02:46 2001 +0200
57.3 @@ -182,7 +182,7 @@
57.4
57.5 constdefs
57.6 foo10 :: nat
57.7 - "foo10 == getX (| x = # 2, y = 0, colour = Blue |)"
57.8 + "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
57.9
57.10
57.11 subsubsection {* Non-coercive structural subtyping *}
57.12 @@ -194,7 +194,7 @@
57.13
57.14 constdefs
57.15 foo11 :: cpoint
57.16 - "foo11 == setX (| x = # 2, y = 0, colour = Blue |) 0"
57.17 + "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
57.18
57.19
57.20 subsection {* Other features *}
57.21 @@ -207,7 +207,7 @@
57.22
57.23 text {*
57.24 \noindent May not apply @{term getX} to
57.25 - @{term [source] "(| x' = # 2, y' = 0 |)"}.
57.26 + @{term [source] "(| x' = 2, y' = 0 |)"}.
57.27 *}
57.28
57.29 text {* \medskip Polymorphic records. *}
58.1 --- a/src/HOL/ex/svc_test.ML Fri Oct 05 23:58:52 2001 +0200
58.2 +++ b/src/HOL/ex/svc_test.ML Sat Oct 06 00:02:46 2001 +0200
58.3 @@ -231,9 +231,9 @@
58.4
58.5 (** Linear arithmetic **)
58.6
58.7 -Goal "x ~= # 14 & x ~= # 13 & x ~= # 12 & x ~= # 11 & x ~= # 10 & x ~= # 9 & \
58.8 -\ x ~= # 8 & x ~= # 7 & x ~= # 6 & x ~= # 5 & x ~= # 4 & x ~= # 3 & \
58.9 -\ x ~= # 2 & x ~= Numeral1 & Numeral0 < x & x < # 16 --> # 15 = (x::int)";
58.10 +Goal "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & \
58.11 +\ x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & \
58.12 +\ x ~= 2 & x ~= Numeral1 & Numeral0 < x & x < 16 --> 15 = (x::int)";
58.13 by (svc_tac 1);
58.14 qed "";
58.15
58.16 @@ -244,11 +244,11 @@
58.17
58.18 (** Natural number examples requiring implicit "non-negative" assumptions*)
58.19
58.20 -Goal "(# 3::nat)*a <= # 2 + # 4*b + # 6*c & # 11 <= # 2*a + b + # 2*c & \
58.21 -\ a + # 3*b <= # 5 + # 2*c --> # 2 + # 3*b <= # 2*a + # 6*c";
58.22 +Goal "(3::nat)*a <= 2 + 4*b + 6*c & 11 <= 2*a + b + 2*c & \
58.23 +\ a + 3*b <= 5 + 2*c --> 2 + 3*b <= 2*a + 6*c";
58.24 by (svc_tac 1);
58.25 qed "";
58.26
58.27 -Goal "(n::nat) < # 2 ==> (n = Numeral0) | (n = Numeral1)";
58.28 +Goal "(n::nat) < 2 ==> (n = Numeral0) | (n = Numeral1)";
58.29 by (svc_tac 1);
58.30 qed "";
59.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML Fri Oct 05 23:58:52 2001 +0200
59.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML Sat Oct 06 00:02:46 2001 +0200
59.3 @@ -110,7 +110,7 @@
59.4 Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
59.5 \ (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
59.6 \ (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
59.7 -by (res_inst_tac [("x","%i. # 2*i")] exI 1);
59.8 +by (res_inst_tac [("x","%i. 2*i")] exI 1);
59.9 by (rtac allI 1);
59.10 by (nat_ind_tac "i" 1);
59.11 by ( Simp_tac 1);
59.12 @@ -129,10 +129,10 @@
59.13 \\<lbrakk>f \\<in> BufEq;
59.14 \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
59.15 x \\<sqsubseteq> s \\<longrightarrow>
59.16 - Fin (# 2 * i) < #x \\<longrightarrow>
59.17 + Fin (2 * i) < #x \\<longrightarrow>
59.18 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
59.19 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
59.20 - Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (# 2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
59.21 + Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
59.22 (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
59.23 \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
59.24 *)
59.25 @@ -147,11 +147,11 @@
59.26 by (hyp_subst_tac 1);
59.27 (*
59.28 1. \\<And>i d xa ya t ff ffa.
59.29 - \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (# 2 * i) < #ya;
59.30 + \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (2 * i) < #ya;
59.31 (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
59.32 \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
59.33 x \\<sqsubseteq> s \\<longrightarrow>
59.34 - Fin (# 2 * i) < #x \\<longrightarrow>
59.35 + Fin (2 * i) < #x \\<longrightarrow>
59.36 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
59.37 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
59.38 xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>