--- a/src/HOL/Algebra/poly/PolyHomo.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.ML Sat Oct 06 00:02:46 2001 +0200
@@ -112,15 +112,15 @@
(* Examples *)
Goal
- "EVAL (x::'a::domain) (a*X^# 2 + b*X^1 + c*X^0) = a * x ^ # 2 + b * x ^ 1 + c";
+ "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
by (asm_simp_tac (simpset() delsimps [power_Suc]
addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
result();
Goal
"EVAL (y::'a::domain) \
-\ (EVAL (const x) (monom 1 + const (a*X^# 2 + b*X^1 + c*X^0))) = \
-\ x ^ 1 + (a * y ^ # 2 + b * y ^ 1 + c)";
+\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
+\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
by (asm_simp_tac (simpset() delsimps [power_Suc]
addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
result();
--- a/src/HOL/Auth/KerberosIV.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Sat Oct 06 00:02:46 2001 +0200
@@ -65,8 +65,8 @@
RespLife :: nat
rules
- AuthLife_LB "# 2 <= AuthLife"
- ServLife_LB "# 2 <= ServLife"
+ AuthLife_LB "2 <= AuthLife"
+ ServLife_LB "2 <= ServLife"
AutcLife_LB "Suc 0 <= AutcLife"
RespLife_LB "Suc 0 <= RespLife"
--- a/src/HOL/Auth/Kerberos_BAN.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Sat Oct 06 00:02:46 2001 +0200
@@ -30,7 +30,7 @@
rules
(*The ticket should remain fresh for two journeys on the network at least*)
- SesKeyLife_LB "# 2 <= SesKeyLife"
+ SesKeyLife_LB "2 <= SesKeyLife"
(*The authenticator only for one journey*)
AutLife_LB "Suc 0 <= AutLife"
--- a/src/HOL/GroupTheory/Exponent.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.ML Sat Oct 06 00:02:46 2001 +0200
@@ -205,13 +205,13 @@
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
by (Asm_full_simp_tac 1);
-by (subgoal_tac "# 2 * n + # 2 <= p * p^n" 1);
+by (subgoal_tac "2 * n + 2 <= p * p^n" 1);
by (Asm_full_simp_tac 1);
-by (subgoal_tac "# 2 * p^n <= p * p^n" 1);
+by (subgoal_tac "2 * p^n <= p * p^n" 1);
(*?arith_tac should handle all of this!*)
by (rtac order_trans 1);
by (assume_tac 2);
-by (dres_inst_tac [("k","# 2")] mult_le_mono2 1);
+by (dres_inst_tac [("k","2")] mult_le_mono2 1);
by (Asm_full_simp_tac 1);
by (rtac mult_le_mono1 1);
by (Asm_full_simp_tac 1);
--- a/src/HOL/Hoare/Arith2.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hoare/Arith2.ML Sat Oct 06 00:02:46 2001 +0200
@@ -63,7 +63,7 @@
(*** pow ***)
-Goal "m mod # 2 = 0 ==> ((n::nat)*n)^(m div # 2) = n^m";
+Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
mult_div_cancel]) 1);
qed "sq_pow_div2";
--- a/src/HOL/Hoare/Examples.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hoare/Examples.ML Sat Oct 06 00:02:46 2001 +0200
@@ -50,9 +50,9 @@
Goal "|- VARS a b x y. \
\ {0<A & 0<B & a=A & b=B & x=B & y=A} \
\ WHILE a ~= b \
-\ INV {0<a & 0<b & gcd A B = gcd a b & # 2*A*B = a*x + b*y} \
+\ INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y} \
\ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \
-\ {a = gcd A B & # 2*A*B = a*(x+y)}";
+\ {a = gcd A B & 2*A*B = a*(x+y)}";
by (hoare_tac (K all_tac) 1);
by(Asm_simp_tac 1);
by(asm_simp_tac (simpset() addsimps
@@ -68,9 +68,9 @@
\ c := (1::nat); \
\ WHILE b ~= 0 \
\ INV {A^B = c * a^b} \
-\ DO WHILE b mod # 2 = 0 \
+\ DO WHILE b mod 2 = 0 \
\ INV {A^B = c * a^b} \
-\ DO a := a*a; b := b div # 2 OD; \
+\ DO a := a*a; b := b div 2 OD; \
\ c := c*a; b := b - 1 \
\ OD \
\ {c = A^B}";
@@ -114,7 +114,7 @@
\ x := X; u := 1; w := 1; r := (0::nat); \
\ WHILE w <= x \
\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \
-\ DO r := r + 1; w := w + u + # 2; u := u + # 2 OD \
+\ DO r := r + 1; w := w + u + 2; u := u + 2 OD \
\ {r*r <= X & X < (r+1)*(r+1)}";
by (hoare_tac (SELECT_GOAL Auto_tac) 1);
qed "sqrt_without_multiplication";
--- a/src/HOL/Hyperreal/HyperArith0.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/HyperArith0.ML Sat Oct 06 00:02:46 2001 +0200
@@ -288,34 +288,34 @@
set trace_simp;
fun test s = (Goal s; by (Simp_tac 1));
-test "Numeral0 <= (y::hypreal) * # -2";
-test "# 9*x = # 12 * (y::hypreal)";
-test "(# 9*x) / (# 12 * (y::hypreal)) = z";
-test "# 9*x < # 12 * (y::hypreal)";
-test "# 9*x <= # 12 * (y::hypreal)";
+test "Numeral0 <= (y::hypreal) * -2";
+test "9*x = 12 * (y::hypreal)";
+test "(9*x) / (12 * (y::hypreal)) = z";
+test "9*x < 12 * (y::hypreal)";
+test "9*x <= 12 * (y::hypreal)";
-test "# -99*x = # 123 * (y::hypreal)";
-test "(# -99*x) / (# 123 * (y::hypreal)) = z";
-test "# -99*x < # 123 * (y::hypreal)";
-test "# -99*x <= # 123 * (y::hypreal)";
+test "-99*x = 123 * (y::hypreal)";
+test "(-99*x) / (123 * (y::hypreal)) = z";
+test "-99*x < 123 * (y::hypreal)";
+test "-99*x <= 123 * (y::hypreal)";
-test "# 999*x = # -396 * (y::hypreal)";
-test "(# 999*x) / (# -396 * (y::hypreal)) = z";
-test "# 999*x < # -396 * (y::hypreal)";
-test "# 999*x <= # -396 * (y::hypreal)";
+test "999*x = -396 * (y::hypreal)";
+test "(999*x) / (-396 * (y::hypreal)) = z";
+test "999*x < -396 * (y::hypreal)";
+test "999*x <= -396 * (y::hypreal)";
-test "# -99*x = # -81 * (y::hypreal)";
-test "(# -99*x) / (# -81 * (y::hypreal)) = z";
-test "# -99*x <= # -81 * (y::hypreal)";
-test "# -99*x < # -81 * (y::hypreal)";
+test "-99*x = -81 * (y::hypreal)";
+test "(-99*x) / (-81 * (y::hypreal)) = z";
+test "-99*x <= -81 * (y::hypreal)";
+test "-99*x < -81 * (y::hypreal)";
-test "# -2 * x = # -1 * (y::hypreal)";
-test "# -2 * x = -(y::hypreal)";
-test "(# -2 * x) / (# -1 * (y::hypreal)) = z";
-test "# -2 * x < -(y::hypreal)";
-test "# -2 * x <= # -1 * (y::hypreal)";
-test "-x < # -23 * (y::hypreal)";
-test "-x <= # -23 * (y::hypreal)";
+test "-2 * x = -1 * (y::hypreal)";
+test "-2 * x = -(y::hypreal)";
+test "(-2 * x) / (-1 * (y::hypreal)) = z";
+test "-2 * x < -(y::hypreal)";
+test "-2 * x <= -1 * (y::hypreal)";
+test "-x < -23 * (y::hypreal)";
+test "-x <= -23 * (y::hypreal)";
*)
@@ -516,18 +516,18 @@
qed "hypreal_divide_1";
Addsimps [hypreal_divide_1];
-Goal "x/# -1 = -(x::hypreal)";
+Goal "x/-1 = -(x::hypreal)";
by (Simp_tac 1);
qed "hypreal_divide_minus1";
Addsimps [hypreal_divide_minus1];
-Goal "# -1/(x::hypreal) = - (Numeral1/x)";
+Goal "-1/(x::hypreal) = - (Numeral1/x)";
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
qed "hypreal_minus1_divide";
Addsimps [hypreal_minus1_divide];
Goal "[| (Numeral0::hypreal) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1);
+by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
by (asm_simp_tac (simpset() addsimps [min_def]) 1);
qed "hypreal_lbound_gt_zero";
@@ -644,11 +644,11 @@
(*** Density of the Hyperreals ***)
-Goal "x < y ==> x < (x+y) / (# 2::hypreal)";
+Goal "x < y ==> x < (x+y) / (2::hypreal)";
by Auto_tac;
qed "hypreal_less_half_sum";
-Goal "x < y ==> (x+y)/(# 2::hypreal) < y";
+Goal "x < y ==> (x+y)/(2::hypreal) < y";
by Auto_tac;
qed "hypreal_gt_half_sum";
--- a/src/HOL/Hyperreal/HyperBin.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML Sat Oct 06 00:02:46 2001 +0200
@@ -57,18 +57,18 @@
qed "mult_hypreal_number_of";
Addsimps [mult_hypreal_number_of];
-Goal "(# 2::hypreal) = Numeral1 + Numeral1";
+Goal "(2::hypreal) = Numeral1 + Numeral1";
by (Simp_tac 1);
val lemma = result();
(*For specialist use: NOT as default simprules*)
-Goal "# 2 * z = (z+z::hypreal)";
+Goal "2 * z = (z+z::hypreal)";
by (simp_tac (simpset ()
addsimps [lemma, hypreal_add_mult_distrib,
one_eq_numeral_1 RS sym]) 1);
qed "hypreal_mult_2";
-Goal "z * # 2 = (z+z::hypreal)";
+Goal "z * 2 = (z+z::hypreal)";
by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1);
qed "hypreal_mult_2_right";
@@ -107,11 +107,11 @@
(*** New versions of existing theorems involving 0, 1hr ***)
-Goal "- Numeral1 = (# -1::hypreal)";
+Goal "- Numeral1 = (-1::hypreal)";
by (Simp_tac 1);
qed "minus_numeral_one";
-(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to # -1*)
+(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to -1*)
val hypreal_numeral_ss =
real_numeral_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1,
minus_numeral_one];
@@ -242,14 +242,14 @@
hypreal_add_ac@rel_iff_rel_0_rls) 1);
qed "hypreal_le_add_iff2";
-Goal "(z::hypreal) * # -1 = -z";
+Goal "(z::hypreal) * -1 = -z";
by (stac (minus_numeral_one RS sym) 1);
by (stac (hypreal_minus_mult_eq2 RS sym) 1);
by Auto_tac;
qed "hypreal_mult_minus_1_right";
Addsimps [hypreal_mult_minus_1_right];
-Goal "# -1 * (z::hypreal) = -z";
+Goal "-1 * (z::hypreal) = -z";
by (simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
qed "hypreal_mult_minus_1";
Addsimps [hypreal_mult_minus_1];
@@ -471,7 +471,7 @@
structure CombineNumeralsData =
struct
val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
+ val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
@@ -530,34 +530,34 @@
set trace_simp;
fun test s = (Goal s, by (Simp_tac 1));
-test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::hypreal)";
-test "# 2*u = (u::hypreal)";
-test "(i + j + # 12 + (k::hypreal)) - # 15 = y";
-test "(i + j + # 12 + (k::hypreal)) - # 5 = y";
+test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hypreal)";
+test "2*u = (u::hypreal)";
+test "(i + j + 12 + (k::hypreal)) - 15 = y";
+test "(i + j + 12 + (k::hypreal)) - 5 = y";
test "y - b < (b::hypreal)";
-test "y - (# 3*b + c) < (b::hypreal) - # 2*c";
+test "y - (3*b + c) < (b::hypreal) - 2*c";
-test "(# 2*x - (u*v) + y) - v*# 3*u = (w::hypreal)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::hypreal)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::hypreal)";
-test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::hypreal)";
+test "(2*x - (u*v) + y) - v*3*u = (w::hypreal)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::hypreal)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::hypreal)";
+test "u*v - (x*u*v + (u*v)*4 + y) = (w::hypreal)";
-test "(i + j + # 12 + (k::hypreal)) = u + # 15 + y";
-test "(i + j*# 2 + # 12 + (k::hypreal)) = j + # 5 + y";
+test "(i + j + 12 + (k::hypreal)) = u + 15 + y";
+test "(i + j*2 + 12 + (k::hypreal)) = j + 5 + y";
-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)";
+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)";
test "a + -(b+c) + b = (d::hypreal)";
test "a + -(b+c) - b = (d::hypreal)";
(*negative numerals*)
-test "(i + j + # -2 + (k::hypreal)) - (u + # 5 + y) = zz";
-test "(i + j + # -3 + (k::hypreal)) < u + # 5 + y";
-test "(i + j + # 3 + (k::hypreal)) < u + # -6 + y";
-test "(i + j + # -12 + (k::hypreal)) - # 15 = y";
-test "(i + j + # 12 + (k::hypreal)) - # -15 = y";
-test "(i + j + # -12 + (k::hypreal)) - # -15 = y";
+test "(i + j + -2 + (k::hypreal)) - (u + 5 + y) = zz";
+test "(i + j + -3 + (k::hypreal)) < u + 5 + y";
+test "(i + j + 3 + (k::hypreal)) < u + -6 + y";
+test "(i + j + -12 + (k::hypreal)) - 15 = y";
+test "(i + j + 12 + (k::hypreal)) - -15 = y";
+test "(i + j + -12 + (k::hypreal)) - -15 = y";
*)
--- a/src/HOL/Hyperreal/HyperPow.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/HyperPow.ML Sat Oct 06 00:02:46 2001 +0200
@@ -75,7 +75,7 @@
qed "hrabs_minus_hrealpow_one";
Addsimps [hrabs_minus_hrealpow_one];
-Goal "abs(# -1 ^ n) = (Numeral1::hypreal)";
+Goal "abs(-1 ^ n) = (Numeral1::hypreal)";
by (induct_tac "n" 1);
by Auto_tac;
qed "hrabs_hrealpow_minus_one";
@@ -134,13 +134,13 @@
by Auto_tac;
qed "hrealpow_two_ge_one";
-Goal "(Numeral1::hypreal) <= # 2 ^ n";
+Goal "(Numeral1::hypreal) <= 2 ^ n";
by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
by (rtac hrealpow_le 2);
by Auto_tac;
qed "two_hrealpow_ge_one";
-Goal "hypreal_of_nat n < # 2 ^ n";
+Goal "hypreal_of_nat n < 2 ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),
simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib]));
@@ -149,17 +149,17 @@
qed "two_hrealpow_gt";
Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
-Goal "# -1 ^ (# 2*n) = (Numeral1::hypreal)";
+Goal "-1 ^ (2*n) = (Numeral1::hypreal)";
by (induct_tac "n" 1);
by (Auto_tac);
qed "hrealpow_minus_one";
-Goal "n+n = (# 2*n::nat)";
+Goal "n+n = (2*n::nat)";
by Auto_tac;
qed "double_lemma";
(*ugh: need to get rid fo the n+n*)
-Goal "# -1 ^ (n + n) = (Numeral1::hypreal)";
+Goal "-1 ^ (n + n) = (Numeral1::hypreal)";
by (auto_tac (claset(),
simpset() addsimps [double_lemma, hrealpow_minus_one]));
qed "hrealpow_minus_one2";
@@ -340,7 +340,7 @@
qed "hrabs_minus_hyperpow_one";
Addsimps [hrabs_minus_hyperpow_one];
-Goal "abs(# -1 pow n) = (Numeral1::hypreal)";
+Goal "abs(-1 pow n) = (Numeral1::hypreal)";
by (subgoal_tac "abs((- 1hr) pow n) = 1hr" 1);
by (Asm_full_simp_tac 1);
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
@@ -388,7 +388,7 @@
simpset()));
qed "hyperpow_two_ge_one";
-Goal "(Numeral1::hypreal) <= # 2 pow n";
+Goal "(Numeral1::hypreal) <= 2 pow n";
by (res_inst_tac [("y","Numeral1 pow n")] order_trans 1);
by (rtac hyperpow_le 2);
by Auto_tac;
@@ -397,7 +397,7 @@
Addsimps [simplify (simpset()) realpow_minus_one];
-Goal "# -1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
+Goal "-1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
by (subgoal_tac "(-(1hr)) pow ((1hn + 1hn)*n) = 1hr" 1);
by (Asm_full_simp_tac 1);
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
--- a/src/HOL/Hyperreal/Lim.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML Sat Oct 06 00:02:46 2001 +0200
@@ -29,7 +29,7 @@
Goalw [LIM_def]
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
by (Clarify_tac 1);
-by (REPEAT(dres_inst_tac [("x","r/# 2")] spec 1));
+by (REPEAT(dres_inst_tac [("x","r/2")] spec 1));
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
by (res_inst_tac [("R1.0","s"),("R2.0","sa")]
@@ -1544,15 +1544,15 @@
simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
qed "Bolzano_bisect_Suc_le_snd";
-Goal "((x::real) = y / (# 2 * z)) = (# 2 * x = y/z)";
+Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)";
by Auto_tac;
-by (dres_inst_tac [("f","%u. (Numeral1/# 2)*u")] arg_cong 1);
+by (dres_inst_tac [("f","%u. (Numeral1/2)*u")] arg_cong 1);
by Auto_tac;
qed "eq_divide_2_times_iff";
Goal "a \\<le> b ==> \
\ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
-\ (b-a) / (# 2 ^ n)";
+\ (b-a) / (2 ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),
simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib,
@@ -1604,8 +1604,8 @@
by (rename_tac "l" 1);
by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
by (rewtac LIMSEQ_def);
-by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
-by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
+by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
+by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
by (dtac real_less_half_sum 1);
by Safe_tac;
(*linear arithmetic bug if we just use Asm_simp_tac*)
@@ -2148,12 +2148,12 @@
simpset() addsimps [real_mult_assoc]));
qed "DERIV_const_ratio_const2";
-Goal "((a + b) /# 2 - a) = (b - a)/(# 2::real)";
+Goal "((a + b) /2 - a) = (b - a)/(2::real)";
by Auto_tac;
qed "real_average_minus_first";
Addsimps [real_average_minus_first];
-Goal "((b + a)/# 2 - a) = (b - a)/(# 2::real)";
+Goal "((b + a)/2 - a) = (b - a)/(2::real)";
by Auto_tac;
qed "real_average_minus_second";
Addsimps [real_average_minus_second];
@@ -2161,7 +2161,7 @@
(* Gallileo's "trick": average velocity = av. of end velocities *)
Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
-\ ==> v((a + b)/# 2) = (v a + v b)/# 2";
+\ ==> v((a + b)/2) = (v a + v b)/2";
by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
by Auto_tac;
by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
--- a/src/HOL/Hyperreal/Lim.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Sat Oct 06 00:02:46 2001 +0200
@@ -71,8 +71,8 @@
"Bolzano_bisect P a b 0 = (a,b)"
"Bolzano_bisect P a b (Suc n) =
(let (x,y) = Bolzano_bisect P a b n
- in if P(x, (x+y)/# 2) then ((x+y)/# 2, y)
- else (x, (x+y)/# 2) )"
+ in if P(x, (x+y)/2) then ((x+y)/2, y)
+ else (x, (x+y)/2) )"
end
--- a/src/HOL/Hyperreal/NSA.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/NSA.ML Sat Oct 06 00:02:46 2001 +0200
@@ -260,11 +260,11 @@
qed "Infinitesimal_zero";
AddIffs [Infinitesimal_zero];
-Goal "x/(# 2::hypreal) + x/(# 2::hypreal) = x";
+Goal "x/(2::hypreal) + x/(2::hypreal) = x";
by Auto_tac;
qed "hypreal_sum_of_halves";
-Goal "Numeral0 < r ==> Numeral0 < r/(# 2::hypreal)";
+Goal "Numeral0 < r ==> Numeral0 < r/(2::hypreal)";
by Auto_tac;
qed "hypreal_half_gt_zero";
--- a/src/HOL/Hyperreal/Series.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/Series.ML Sat Oct 06 00:02:46 2001 +0200
@@ -101,7 +101,7 @@
by (Auto_tac);
qed "sumr_shift_bounds";
-Goal "sumr 0 (# 2*n) (%i. (# -1) ^ Suc i) = Numeral0";
+Goal "sumr 0 (2*n) (%i. (-1) ^ Suc i) = Numeral0";
by (induct_tac "n" 1);
by (Auto_tac);
qed "sumr_minus_one_realpow_zero";
--- a/src/HOL/Hyperreal/hypreal_arith0.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith0.ML Sat Oct 06 00:02:46 2001 +0200
@@ -115,7 +115,7 @@
qed "";
Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> # 6*a <= # 5*l+i";
+\ ==> 6*a <= 5*l+i";
by (fast_arith_tac 1);
qed "";
*)
--- a/src/HOL/IMP/Compiler.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMP/Compiler.thy Sat Oct 06 00:02:46 2001 +0200
@@ -39,9 +39,9 @@
"compile (x:==a) = [ASIN x a]"
"compile (c1;c2) = compile c1 @ compile c2"
"compile (IF b THEN c1 ELSE c2) =
- [JMPF b (length(compile c1) + # 2)] @ compile c1 @
+ [JMPF b (length(compile c1) + 2)] @ compile c1 @
[JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
-"compile (WHILE b DO c) = [JMPF b (length(compile c) + # 2)] @ compile c @
+"compile (WHILE b DO c) = [JMPF b (length(compile c) + 2)] @ compile c @
[JMPB (length(compile c)+1)]"
declare nth_append[simp];
--- a/src/HOL/IMP/Examples.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMP/Examples.ML Sat Oct 06 00:02:46 2001 +0200
@@ -34,7 +34,7 @@
val step = resolve_tac evalc.intrs 1;
val simp = Asm_simp_tac 1;
Goalw [factorial_def] "a~=b ==> \
-\ <factorial a b, Mem(a:=# 3)> -c-> Mem(b:=# 6,a:=Numeral0)";
+\ <factorial a b, Mem(a:=3)> -c-> Mem(b:=6,a:=Numeral0)";
by (ftac not_sym 1);
by step;
by step;
--- a/src/HOL/IMPP/EvenOdd.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMPP/EvenOdd.ML Sat Oct 06 00:02:46 2001 +0200
@@ -17,7 +17,7 @@
Addsimps [not_even_1];
Goalw [even_def] "even (Suc (Suc n)) = even n";
-by (subgoal_tac "Suc (Suc n) = n+# 2" 1);
+by (subgoal_tac "Suc (Suc n) = n+2" 1);
by (Simp_tac 2);
by (etac ssubst 1);
by (rtac dvd_reduce 1);
--- a/src/HOL/IMPP/EvenOdd.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy Sat Oct 06 00:02:46 2001 +0200
@@ -9,7 +9,7 @@
EvenOdd = Misc +
constdefs even :: nat => bool
- "even n == # 2 dvd n"
+ "even n == 2 dvd n"
consts
Even, Odd :: pname
--- a/src/HOL/Induct/Mutil.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Induct/Mutil.thy Sat Oct 06 00:02:46 2001 +0200
@@ -29,7 +29,7 @@
constdefs
coloured :: "nat => (nat \<times> nat) set"
- "coloured b == {(i, j). (i + j) mod # 2 = b}"
+ "coloured b == {(i, j). (i + j) mod 2 = b}"
text {* \medskip The union of two disjoint tilings is a tiling *}
@@ -61,14 +61,14 @@
apply auto
done
-lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (# 2 * n) \<in> tiling domino"
+lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (2 * n) \<in> tiling domino"
apply (induct n)
apply (simp_all add: Un_assoc [symmetric])
apply (rule tiling.Un)
apply (auto simp add: sing_Times_lemma)
done
-lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (# 2 * n) \<in> tiling domino"
+lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino"
apply (induct m)
apply auto
done
@@ -78,7 +78,7 @@
lemma coloured_insert [simp]:
"coloured b \<inter> (insert (i, j) t) =
- (if (i + j) mod # 2 = b then insert (i, j) (coloured b \<inter> t)
+ (if (i + j) mod 2 = b then insert (i, j) (coloured b \<inter> t)
else coloured b \<inter> t)"
apply (unfold coloured_def)
apply auto
@@ -125,7 +125,7 @@
theorem gen_mutil_not_tiling:
"t \<in> tiling domino ==>
- (i + j) mod # 2 = 0 ==> (m + n) mod # 2 = 0 ==>
+ (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==>
{(i, j), (m, n)} \<subseteq> t
==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
apply (rule notI)
@@ -140,8 +140,8 @@
text {* Apply the general theorem to the well-known case *}
theorem mutil_not_tiling:
- "t = lessThan (# 2 * Suc m) \<times> lessThan (# 2 * Suc n)
- ==> t - {(0, 0)} - {(Suc (# 2 * m), Suc (# 2 * n))} \<notin> tiling domino"
+ "t = lessThan (2 * Suc m) \<times> lessThan (2 * Suc n)
+ ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} \<notin> tiling domino"
apply (rule gen_mutil_not_tiling)
apply (blast intro!: dominoes_tile_matrix)
apply auto
--- a/src/HOL/Integ/Bin.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/Bin.ML Sat Oct 06 00:02:46 2001 +0200
@@ -160,7 +160,7 @@
(*The correctness of shifting. But it doesn't seem to give a measurable
speed-up.*)
-Goal "(# 2::int) * number_of w = number_of (w BIT False)";
+Goal "(2::int) * number_of w = number_of (w BIT False)";
by (induct_tac "w" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
@@ -250,11 +250,11 @@
by (Simp_tac 1);
qed "zmult_1_right";
-Goal "# -1 * z = -(z::int)";
+Goal "-1 * z = -(z::int)";
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
qed "zmult_minus1";
-Goal "z * # -1 = -(z::int)";
+Goal "z * -1 = -(z::int)";
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
qed "zmult_minus1_right";
--- a/src/HOL/Integ/IntArith.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/IntArith.ML Sat Oct 06 00:02:46 2001 +0200
@@ -168,7 +168,7 @@
by Auto_tac;
qed "pos_zmult_eq_1_iff";
-Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = # -1 & n = # -1))";
+Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = -1 & n = -1))";
by (case_tac "Numeral0<m" 1);
by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
by (case_tac "m=Numeral0" 1);
--- a/src/HOL/Integ/IntDiv.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/IntDiv.ML Sat Oct 06 00:02:46 2001 +0200
@@ -84,8 +84,8 @@
Goal "adjust a b (q,r) = (let diff = r-b in \
-\ if Numeral0 <= diff then (# 2*q + Numeral1, diff) \
-\ else (# 2*q, r))";
+\ if Numeral0 <= diff then (2*q + Numeral1, diff) \
+\ else (2*q, r))";
by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
qed "adjust_eq";
Addsimps [adjust_eq];
@@ -103,7 +103,7 @@
(**use with simproc to avoid re-proving the premise*)
Goal "Numeral0 < b ==> \
\ posDivAlg (a,b) = \
-\ (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, # 2*b)))";
+\ (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, 2*b)))";
by (rtac (posDivAlg_raw_eqn RS trans) 1);
by (Asm_simp_tac 1);
qed "posDivAlg_eqn";
@@ -141,7 +141,7 @@
(**use with simproc to avoid re-proving the premise*)
Goal "Numeral0 < b ==> \
\ negDivAlg (a,b) = \
-\ (if Numeral0<=a+b then (# -1,a+b) else adjust a b (negDivAlg(a, # 2*b)))";
+\ (if Numeral0<=a+b then (-1,a+b) else adjust a b (negDivAlg(a, 2*b)))";
by (rtac (negDivAlg_raw_eqn RS trans) 1);
by (Asm_simp_tac 1);
qed "negDivAlg_eqn";
@@ -179,7 +179,7 @@
qed "posDivAlg_0";
Addsimps [posDivAlg_0];
-Goal "negDivAlg (# -1, b) = (# -1, b-Numeral1)";
+Goal "negDivAlg (-1, b) = (-1, b-Numeral1)";
by (stac negDivAlg_raw_eqn 1);
by Auto_tac;
qed "negDivAlg_minus1";
@@ -272,7 +272,7 @@
by (auto_tac (claset(), simpset() addsimps [quorem_def]));
qed "div_neg_neg_trivial";
-Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a div b = # -1";
+Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a div b = -1";
by (rtac quorem_div 1);
by (auto_tac (claset(), simpset() addsimps [quorem_def]));
qed "div_pos_neg_trivial";
@@ -290,7 +290,7 @@
qed "mod_neg_neg_trivial";
Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a mod b = a+b";
-by (res_inst_tac [("q","# -1")] quorem_mod 1);
+by (res_inst_tac [("q","-1")] quorem_mod 1);
by (auto_tac (claset(), simpset() addsimps [quorem_def]));
qed "mod_pos_neg_trivial";
@@ -411,7 +411,7 @@
by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "zdiv_zero";
-Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
+Goal "(Numeral0::int) < b ==> -1 div b = -1";
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "div_eq_minus1";
@@ -421,11 +421,11 @@
Addsimps [zdiv_zero, zmod_zero];
-Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
+Goal "(Numeral0::int) < b ==> -1 div b = -1";
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "zdiv_minus1";
-Goal "(Numeral0::int) < b ==> # -1 mod b = b-Numeral1";
+Goal "(Numeral0::int) < b ==> -1 mod b = b-Numeral1";
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
qed "zmod_minus1";
@@ -491,15 +491,15 @@
qed "zdiv_1";
Addsimps [zdiv_1];
-Goal "a mod (# -1::int) = Numeral0";
-by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_sign 1);
-by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_bound 2);
+Goal "a mod (-1::int) = Numeral0";
+by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_sign 1);
+by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_bound 2);
by Auto_tac;
qed "zmod_minus1_right";
Addsimps [zmod_minus1_right];
-Goal "a div (# -1::int) = -a";
-by (cut_inst_tac [("a","a"),("b","# -1")] zmod_zdiv_equality 1);
+Goal "a div (-1::int) = -a";
+by (cut_inst_tac [("a","a"),("b","-1")] zmod_zdiv_equality 1);
by Auto_tac;
qed "zdiv_minus1_right";
Addsimps [zdiv_minus1_right];
@@ -861,13 +861,13 @@
(** computing "div" by shifting **)
-Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) div (# 2*a) = b div a";
+Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) div (2*a) = b div a";
by (zdiv_undefined_case_tac "a = Numeral0" 1);
by (subgoal_tac "Numeral1 <= a" 1);
by (arith_tac 2);
-by (subgoal_tac "Numeral1 < a * # 2" 1);
+by (subgoal_tac "Numeral1 < a * 2" 1);
by (arith_tac 2);
-by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
+by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
by (rtac zmult_zle_mono2 2);
by (auto_tac (claset(),
simpset() addsimps [zadd_commute, zmult_commute,
@@ -887,12 +887,12 @@
qed "pos_zdiv_mult_2";
-Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) div (# 2*a) = (b+Numeral1) div a";
-by (subgoal_tac "(Numeral1 + # 2*(-b-Numeral1)) div (# 2 * (-a)) = (-b-Numeral1) div (-a)" 1);
+Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) div (2*a) = (b+Numeral1) div a";
+by (subgoal_tac "(Numeral1 + 2*(-b-Numeral1)) div (2 * (-a)) = (-b-Numeral1) div (-a)" 1);
by (rtac pos_zdiv_mult_2 2);
by (auto_tac (claset(),
simpset() addsimps [zmult_zminus_right]));
-by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
+by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
by (Simp_tac 2);
by (asm_full_simp_tac (HOL_ss
addsimps [zdiv_zminus_zminus, zdiff_def,
@@ -921,13 +921,13 @@
(** computing "mod" by shifting (proofs resemble those for "div") **)
-Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) mod (# 2*a) = Numeral1 + # 2 * (b mod a)";
+Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) mod (2*a) = Numeral1 + 2 * (b mod a)";
by (zdiv_undefined_case_tac "a = Numeral0" 1);
by (subgoal_tac "Numeral1 <= a" 1);
by (arith_tac 2);
-by (subgoal_tac "Numeral1 < a * # 2" 1);
+by (subgoal_tac "Numeral1 < a * 2" 1);
by (arith_tac 2);
-by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
+by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
by (rtac zmult_zle_mono2 2);
by (auto_tac (claset(),
simpset() addsimps [zadd_commute, zmult_commute,
@@ -947,13 +947,13 @@
qed "pos_zmod_mult_2";
-Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) mod (# 2*a) = # 2 * ((b+Numeral1) mod a) - Numeral1";
+Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) mod (2*a) = 2 * ((b+Numeral1) mod a) - Numeral1";
by (subgoal_tac
- "(Numeral1 + # 2*(-b-Numeral1)) mod (# 2*(-a)) = Numeral1 + # 2*((-b-Numeral1) mod (-a))" 1);
+ "(Numeral1 + 2*(-b-Numeral1)) mod (2*(-a)) = Numeral1 + 2*((-b-Numeral1) mod (-a))" 1);
by (rtac pos_zmod_mult_2 2);
by (auto_tac (claset(),
simpset() addsimps [zmult_zminus_right]));
-by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
+by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
by (Simp_tac 2);
by (asm_full_simp_tac (HOL_ss
addsimps [zmod_zminus_zminus, zdiff_def,
@@ -965,9 +965,9 @@
Goal "number_of (v BIT b) mod number_of (w BIT False) = \
\ (if b then \
\ if (Numeral0::int) <= number_of w \
-\ then # 2 * (number_of v mod number_of w) + Numeral1 \
-\ else # 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1 \
-\ else # 2 * (number_of v mod number_of w))";
+\ then 2 * (number_of v mod number_of w) + Numeral1 \
+\ else 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1 \
+\ else 2 * (number_of v mod number_of w))";
by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
by (asm_simp_tac (simpset()
delsimps bin_arith_extra_simps@bin_rel_simps
@@ -981,10 +981,10 @@
(** Quotients of signs **)
Goal "[| a < (Numeral0::int); Numeral0 < b |] ==> a div b < Numeral0";
-by (subgoal_tac "a div b <= # -1" 1);
+by (subgoal_tac "a div b <= -1" 1);
by (Force_tac 1);
by (rtac order_trans 1);
-by (res_inst_tac [("a'","# -1")] zdiv_mono1 1);
+by (res_inst_tac [("a'","-1")] zdiv_mono1 1);
by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
qed "div_neg_pos_less0";
--- a/src/HOL/Integ/IntDiv.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/IntDiv.thy Sat Oct 06 00:02:46 2001 +0200
@@ -15,8 +15,8 @@
(if Numeral0 < b then Numeral0<=r & r<b else b<r & r <= Numeral0)"
adjust :: "[int, int, int*int] => int*int"
- "adjust a b == %(q,r). if Numeral0 <= r-b then (# 2*q + Numeral1, r-b)
- else (# 2*q, r)"
+ "adjust a b == %(q,r). if Numeral0 <= r-b then (2*q + Numeral1, r-b)
+ else (2*q, r)"
(** the division algorithm **)
@@ -25,14 +25,14 @@
recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))"
"posDivAlg (a,b) =
(if (a<b | b<=Numeral0) then (Numeral0,a)
- else adjust a b (posDivAlg(a, # 2*b)))"
+ else adjust a b (posDivAlg(a, 2*b)))"
(*for the case a<0, b>0*)
consts negDivAlg :: "int*int => int*int"
recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
"negDivAlg (a,b) =
- (if (Numeral0<=a+b | b<=Numeral0) then (# -1,a+b)
- else adjust a b (negDivAlg(a, # 2*b)))"
+ (if (Numeral0<=a+b | b<=Numeral0) then (-1,a+b)
+ else adjust a b (negDivAlg(a, 2*b)))"
(*for the general case b~=0*)
--- a/src/HOL/Integ/NatSimprocs.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML Sat Oct 06 00:02:46 2001 +0200
@@ -92,40 +92,40 @@
(** Evens and Odds, for Mutilated Chess Board **)
-(*Case analysis on b<# 2*)
-Goal "(n::nat) < # 2 ==> n = Numeral0 | n = Numeral1";
+(*Case analysis on b<2*)
+Goal "(n::nat) < 2 ==> n = Numeral0 | n = Numeral1";
by (arith_tac 1);
qed "less_2_cases";
-Goal "Suc(Suc(m)) mod # 2 = m mod # 2";
-by (subgoal_tac "m mod # 2 < # 2" 1);
+Goal "Suc(Suc(m)) mod 2 = m mod 2";
+by (subgoal_tac "m mod 2 < 2" 1);
by (Asm_simp_tac 2);
be (less_2_cases RS disjE) 1;
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
qed "mod2_Suc_Suc";
Addsimps [mod2_Suc_Suc];
-Goal "!!m::nat. (0 < m mod # 2) = (m mod # 2 = Numeral1)";
-by (subgoal_tac "m mod # 2 < # 2" 1);
+Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = Numeral1)";
+by (subgoal_tac "m mod 2 < 2" 1);
by (Asm_simp_tac 2);
by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
qed "mod2_gr_0";
Addsimps [mod2_gr_0, rename_numerals mod2_gr_0];
-(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) # 2 **)
+(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **)
-Goal "# 2 + n = Suc (Suc n)";
+Goal "2 + n = Suc (Suc n)";
by (Simp_tac 1);
qed "add_2_eq_Suc";
-Goal "n + # 2 = Suc (Suc n)";
+Goal "n + 2 = Suc (Suc n)";
by (Simp_tac 1);
qed "add_2_eq_Suc'";
Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
(*Can be used to eliminate long strings of Sucs, but not by default*)
-Goal "Suc (Suc (Suc n)) = # 3 + n";
+Goal "Suc (Suc (Suc n)) = 3 + n";
by (Simp_tac 1);
qed "Suc3_eq_add_3";
@@ -136,21 +136,21 @@
We already have some rules to simplify operands smaller than 3.
**)
-Goal "m div (Suc (Suc (Suc n))) = m div (# 3+n)";
+Goal "m div (Suc (Suc (Suc n))) = m div (3+n)";
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
qed "div_Suc_eq_div_add3";
-Goal "m mod (Suc (Suc (Suc n))) = m mod (# 3+n)";
+Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)";
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
qed "mod_Suc_eq_mod_add3";
Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3];
-Goal "(Suc (Suc (Suc m))) div n = (# 3+m) div n";
+Goal "(Suc (Suc (Suc m))) div n = (3+m) div n";
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
qed "Suc_div_eq_add3_div";
-Goal "(Suc (Suc (Suc m))) mod n = (# 3+m) mod n";
+Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n";
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
qed "Suc_mod_eq_add3_mod";
--- a/src/HOL/Integ/int_arith1.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/int_arith1.ML Sat Oct 06 00:02:46 2001 +0200
@@ -279,7 +279,7 @@
structure CombineNumeralsData =
struct
val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
+ val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
@@ -318,35 +318,35 @@
set trace_simp;
fun test s = (Goal s; by (Simp_tac 1));
-test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::int)";
+test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
-test "# 2*u = (u::int)";
-test "(i + j + # 12 + (k::int)) - # 15 = y";
-test "(i + j + # 12 + (k::int)) - # 5 = y";
+test "2*u = (u::int)";
+test "(i + j + 12 + (k::int)) - 15 = y";
+test "(i + j + 12 + (k::int)) - 5 = y";
test "y - b < (b::int)";
-test "y - (# 3*b + c) < (b::int) - # 2*c";
+test "y - (3*b + c) < (b::int) - 2*c";
-test "(# 2*x - (u*v) + y) - v*# 3*u = (w::int)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::int)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::int)";
-test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::int)";
+test "(2*x - (u*v) + y) - v*3*u = (w::int)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
+test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
-test "(i + j + # 12 + (k::int)) = u + # 15 + y";
-test "(i + j*# 2 + # 12 + (k::int)) = j + # 5 + y";
+test "(i + j + 12 + (k::int)) = u + 15 + y";
+test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
-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)";
+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)";
test "a + -(b+c) + b = (d::int)";
test "a + -(b+c) - b = (d::int)";
(*negative numerals*)
-test "(i + j + # -2 + (k::int)) - (u + # 5 + y) = zz";
-test "(i + j + # -3 + (k::int)) < u + # 5 + y";
-test "(i + j + # 3 + (k::int)) < u + # -6 + y";
-test "(i + j + # -12 + (k::int)) - # 15 = y";
-test "(i + j + # 12 + (k::int)) - # -15 = y";
-test "(i + j + # -12 + (k::int)) - # -15 = y";
+test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
+test "(i + j + -3 + (k::int)) < u + 5 + y";
+test "(i + j + 3 + (k::int)) < u + -6 + y";
+test "(i + j + -12 + (k::int)) - 15 = y";
+test "(i + j + 12 + (k::int)) - -15 = y";
+test "(i + j + -12 + (k::int)) - -15 = y";
*)
@@ -455,7 +455,7 @@
(* Some test data
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
by (fast_arith_tac 1);
-Goal "!!a::int. [| a < b; c < d |] ==> a-d+ # 2 <= b+(-c)";
+Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
by (fast_arith_tac 1);
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d";
by (fast_arith_tac 1);
@@ -465,7 +465,7 @@
\ ==> a+a <= j+j";
by (fast_arith_tac 1);
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
-\ ==> a+a - - # -1 < j+j - # 3";
+\ ==> a+a - - -1 < j+j - 3";
by (fast_arith_tac 1);
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
by (arith_tac 1);
@@ -482,6 +482,6 @@
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
by (fast_arith_tac 1);
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> # 6*a <= # 5*l+i";
+\ ==> 6*a <= 5*l+i";
by (fast_arith_tac 1);
*)
--- a/src/HOL/Integ/int_arith2.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/int_arith2.ML Sat Oct 06 00:02:46 2001 +0200
@@ -75,7 +75,7 @@
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
qed "nat_1";
-Goal "nat # 2 = Suc (Suc 0)";
+Goal "nat 2 = Suc (Suc 0)";
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
qed "nat_2";
--- a/src/HOL/Integ/int_factor_simprocs.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Sat Oct 06 00:02:46 2001 +0200
@@ -114,33 +114,33 @@
set trace_simp;
fun test s = (Goal s; by (Simp_tac 1));
-test "# 9*x = # 12 * (y::int)";
-test "(# 9*x) div (# 12 * (y::int)) = z";
-test "# 9*x < # 12 * (y::int)";
-test "# 9*x <= # 12 * (y::int)";
+test "9*x = 12 * (y::int)";
+test "(9*x) div (12 * (y::int)) = z";
+test "9*x < 12 * (y::int)";
+test "9*x <= 12 * (y::int)";
-test "# -99*x = # 132 * (y::int)";
-test "(# -99*x) div (# 132 * (y::int)) = z";
-test "# -99*x < # 132 * (y::int)";
-test "# -99*x <= # 132 * (y::int)";
+test "-99*x = 132 * (y::int)";
+test "(-99*x) div (132 * (y::int)) = z";
+test "-99*x < 132 * (y::int)";
+test "-99*x <= 132 * (y::int)";
-test "# 999*x = # -396 * (y::int)";
-test "(# 999*x) div (# -396 * (y::int)) = z";
-test "# 999*x < # -396 * (y::int)";
-test "# 999*x <= # -396 * (y::int)";
+test "999*x = -396 * (y::int)";
+test "(999*x) div (-396 * (y::int)) = z";
+test "999*x < -396 * (y::int)";
+test "999*x <= -396 * (y::int)";
-test "# -99*x = # -81 * (y::int)";
-test "(# -99*x) div (# -81 * (y::int)) = z";
-test "# -99*x <= # -81 * (y::int)";
-test "# -99*x < # -81 * (y::int)";
+test "-99*x = -81 * (y::int)";
+test "(-99*x) div (-81 * (y::int)) = z";
+test "-99*x <= -81 * (y::int)";
+test "-99*x < -81 * (y::int)";
-test "# -2 * x = # -1 * (y::int)";
-test "# -2 * x = -(y::int)";
-test "(# -2 * x) div (# -1 * (y::int)) = z";
-test "# -2 * x < -(y::int)";
-test "# -2 * x <= # -1 * (y::int)";
-test "-x < # -23 * (y::int)";
-test "-x <= # -23 * (y::int)";
+test "-2 * x = -1 * (y::int)";
+test "-2 * x = -(y::int)";
+test "(-2 * x) div (-1 * (y::int)) = z";
+test "-2 * x < -(y::int)";
+test "-2 * x <= -1 * (y::int)";
+test "-x < -23 * (y::int)";
+test "-x <= -23 * (y::int)";
*)
--- a/src/HOL/Integ/nat_bin.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/nat_bin.ML Sat Oct 06 00:02:46 2001 +0200
@@ -25,7 +25,7 @@
by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def, One_nat_def]) 1);
qed "numeral_1_eq_1";
-Goal "# 2 = Suc 1";
+Goal "2 = Suc 1";
by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def, One_nat_def]) 1);
qed "numeral_2_eq_2";
@@ -77,7 +77,7 @@
by (Simp_tac 1);
qed "Suc_numeral_0_eq_1";
-Goal "Suc Numeral1 = # 2";
+Goal "Suc Numeral1 = 2";
by (Simp_tac 1);
qed "Suc_numeral_1_eq_2";
@@ -384,7 +384,7 @@
qed "power_one";
Addsimps [power_zero, power_one];
-Goal "(p::nat) ^ # 2 = p*p";
+Goal "(p::nat) ^ 2 = p*p";
by (simp_tac numeral_ss 1);
qed "power_two";
@@ -497,7 +497,7 @@
Goal "m+m ~= int (Suc 0) + n + n";
by Auto_tac;
-by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
+by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
val lemma2 = result();
@@ -514,7 +514,7 @@
by (res_inst_tac [("x", "number_of v")] spec 1);
by Safe_tac;
by (ALLGOALS Full_simp_tac);
-by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
+by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
qed "eq_number_of_BIT_Pls";
@@ -524,7 +524,7 @@
[number_of_BIT, number_of_Min, eq_commute]) 1);
by (res_inst_tac [("x", "number_of v")] spec 1);
by Auto_tac;
-by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
+by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
by Auto_tac;
qed "eq_number_of_BIT_Min";
--- a/src/HOL/Integ/nat_simprocs.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Sat Oct 06 00:02:46 2001 +0200
@@ -319,7 +319,7 @@
structure CombineNumeralsData =
struct
val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
+ val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
val dest_sum = restricted_dest_Sucs_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
@@ -504,62 +504,62 @@
fun test s = (Goal s; by (Simp_tac 1));
(*cancel_numerals*)
-test "l +( # 2) + (# 2) + # 2 + (l + # 2) + (oo + # 2) = (uu::nat)";
-test "(# 2*length xs < # 2*length xs + j)";
-test "(# 2*length xs < length xs * # 2 + j)";
-test "# 2*u = (u::nat)";
-test "# 2*u = Suc (u)";
-test "(i + j + # 12 + (k::nat)) - # 15 = y";
-test "(i + j + # 12 + (k::nat)) - # 5 = y";
-test "Suc u - # 2 = y";
-test "Suc (Suc (Suc u)) - # 2 = y";
-test "(i + j + # 2 + (k::nat)) - 1 = y";
+test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)";
+test "(2*length xs < 2*length xs + j)";
+test "(2*length xs < length xs * 2 + j)";
+test "2*u = (u::nat)";
+test "2*u = Suc (u)";
+test "(i + j + 12 + (k::nat)) - 15 = y";
+test "(i + j + 12 + (k::nat)) - 5 = y";
+test "Suc u - 2 = y";
+test "Suc (Suc (Suc u)) - 2 = y";
+test "(i + j + 2 + (k::nat)) - 1 = y";
test "(i + j + Numeral1 + (k::nat)) - 2 = y";
-test "(# 2*x + (u*v) + y) - v*# 3*u = (w::nat)";
-test "(# 2*x*u*v + # 5 + (u*v)*# 4 + y) - v*u*# 4 = (w::nat)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::nat)";
-test "Suc (Suc (# 2*x*u*v + u*# 4 + y)) - u = w";
-test "Suc ((u*v)*# 4) - v*# 3*u = w";
-test "Suc (Suc ((u*v)*# 3)) - v*# 3*u = w";
+test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
+test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
+test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
+test "Suc ((u*v)*4) - v*3*u = w";
+test "Suc (Suc ((u*v)*3)) - v*3*u = w";
-test "(i + j + # 12 + (k::nat)) = u + # 15 + y";
-test "(i + j + # 32 + (k::nat)) - (u + # 15 + y) = zz";
-test "(i + j + # 12 + (k::nat)) = u + # 5 + y";
+test "(i + j + 12 + (k::nat)) = u + 15 + y";
+test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
+test "(i + j + 12 + (k::nat)) = u + 5 + y";
(*Suc*)
-test "(i + j + # 12 + k) = Suc (u + y)";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + # 41 + k)";
-test "(i + j + # 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) - # 5 = v";
-test "(i + j + # 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
-test "# 2*y + # 3*z + # 2*u = Suc (u)";
-test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = Suc (u)";
-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)";
-test "# 6 + # 2*y + # 3*z + # 4*u = Suc (vv + # 2*u + z)";
-test "(# 2*n*m) < (# 3*(m*n)) + (u::nat)";
+test "(i + j + 12 + k) = Suc (u + y)";
+test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
+test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
+test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
+test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
+test "2*y + 3*z + 2*u = Suc (u)";
+test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
+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)";
+test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
+test "(2*n*m) < (3*(m*n)) + (u::nat)";
(*negative numerals: FAIL*)
-test "(i + j + # -23 + (k::nat)) < u + # 15 + y";
-test "(i + j + # 3 + (k::nat)) < u + # -15 + y";
-test "(i + j + # -12 + (k::nat)) - # 15 = y";
-test "(i + j + # 12 + (k::nat)) - # -15 = y";
-test "(i + j + # -12 + (k::nat)) - # -15 = y";
+test "(i + j + -23 + (k::nat)) < u + 15 + y";
+test "(i + j + 3 + (k::nat)) < u + -15 + y";
+test "(i + j + -12 + (k::nat)) - 15 = y";
+test "(i + j + 12 + (k::nat)) - -15 = y";
+test "(i + j + -12 + (k::nat)) - -15 = y";
(*combine_numerals*)
-test "k + # 3*k = (u::nat)";
-test "Suc (i + # 3) = u";
-test "Suc (i + j + # 3 + k) = u";
-test "k + j + # 3*k + j = (u::nat)";
-test "Suc (j*i + i + k + # 5 + # 3*k + i*j*# 4) = (u::nat)";
-test "(# 2*n*m) + (# 3*(m*n)) = (u::nat)";
+test "k + 3*k = (u::nat)";
+test "Suc (i + 3) = u";
+test "Suc (i + j + 3 + k) = u";
+test "k + j + 3*k + j = (u::nat)";
+test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
+test "(2*n*m) + (3*(m*n)) = (u::nat)";
(*negative numerals: FAIL*)
-test "Suc (i + j + # -3 + k) = u";
+test "Suc (i + j + -3 + k) = u";
(*cancel_numeral_factors*)
-test "# 9*x = # 12 * (y::nat)";
-test "(# 9*x) div (# 12 * (y::nat)) = z";
-test "# 9*x < # 12 * (y::nat)";
-test "# 9*x <= # 12 * (y::nat)";
+test "9*x = 12 * (y::nat)";
+test "(9*x) div (12 * (y::nat)) = z";
+test "9*x < 12 * (y::nat)";
+test "9*x <= 12 * (y::nat)";
(*cancel_factor*)
test "x*k = k*(y::nat)";
--- a/src/HOL/Isar_examples/Fibonacci.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Sat Oct 06 00:02:46 2001 +0200
@@ -39,7 +39,7 @@
text {* Alternative induction rule. *}
theorem fib_induct:
- "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + # 2)) ==> P (n::nat)"
+ "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
by (induct rule: fib.induct, simp+)
@@ -56,7 +56,7 @@
show "?P 0" by simp
show "?P 1" by simp
fix n
- have "fib (n + # 2 + k + 1)
+ have "fib (n + 2 + k + 1)
= fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
also assume "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
@@ -65,9 +65,9 @@
= fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
(is " _ = ?R2")
also have "?R1 + ?R2
- = fib (k + 1) * fib (n + # 2 + 1) + fib k * fib (n + # 2)"
+ = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
by (simp add: add_mult_distrib2)
- finally show "?P (n + # 2)" .
+ finally show "?P (n + 2)" .
qed
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
@@ -75,14 +75,14 @@
show "?P 0" by simp
show "?P 1" by simp
fix n
- have "fib (n + # 2 + 1) = fib (n + 1) + fib (n + # 2)"
+ have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
by simp
- also have "gcd (fib (n + # 2), ...) = gcd (fib (n + # 2), fib (n + 1))"
+ also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
by (simp only: gcd_add2')
also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
by (simp add: gcd_commute)
also assume "... = 1"
- finally show "?P (n + # 2)" .
+ finally show "?P (n + 2)" .
qed
lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
--- a/src/HOL/Isar_examples/HoareEx.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy Sat Oct 06 00:02:46 2001 +0200
@@ -39,7 +39,7 @@
*}
lemma
- "|- .{\<acute>(N_update (# 2 * \<acute>N)) : .{\<acute>N = # 10}.}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
+ "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
by (rule assign)
text {*
@@ -49,13 +49,13 @@
``obvious'' consequences as well.
*}
-lemma "|- .{True}. \<acute>N := # 10 .{\<acute>N = # 10}."
+lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
by hoare
-lemma "|- .{# 2 * \<acute>N = # 10}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
+lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
by hoare
-lemma "|- .{\<acute>N = # 5}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
+lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
by hoare simp
lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sat Oct 06 00:02:46 2001 +0200
@@ -76,7 +76,7 @@
by (simp add: below_def less_Suc_eq) blast
lemma Sigma_Suc2:
- "m = n + # 2 ==> A <*> below m =
+ "m = n + 2 ==> A <*> below m =
(A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
by (auto simp add: below_def) arith
@@ -87,10 +87,10 @@
constdefs
evnodd :: "(nat * nat) set => nat => (nat * nat) set"
- "evnodd A b == A Int {(i, j). (i + j) mod # 2 = b}"
+ "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
lemma evnodd_iff:
- "(i, j): evnodd A b = ((i, j): A & (i + j) mod # 2 = b)"
+ "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"
by (simp add: evnodd_def)
lemma evnodd_subset: "evnodd A b <= A"
@@ -112,7 +112,7 @@
by (simp add: evnodd_def)
lemma evnodd_insert: "evnodd (insert (i, j) C) b =
- (if (i + j) mod # 2 = b
+ (if (i + j) mod 2 = b
then insert (i, j) (evnodd C b) else evnodd C b)"
by (simp add: evnodd_def) blast
@@ -128,21 +128,21 @@
vertl: "{(i, j), (i + 1, j)} : domino"
lemma dominoes_tile_row:
- "{i} <*> below (# 2 * n) : tiling domino"
+ "{i} <*> below (2 * n) : tiling domino"
(is "?P n" is "?B n : ?T")
proof (induct n)
show "?P 0" by (simp add: below_0 tiling.empty)
fix n assume hyp: "?P n"
- let ?a = "{i} <*> {# 2 * n + 1} Un {i} <*> {# 2 * n}"
+ let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
have "?B (Suc n) = ?a Un ?B n"
by (auto simp add: Sigma_Suc Un_assoc)
also have "... : ?T"
proof (rule tiling.Un)
- have "{(i, # 2 * n), (i, # 2 * n + 1)} : domino"
+ have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
by (rule domino.horiz)
- also have "{(i, # 2 * n), (i, # 2 * n + 1)} = ?a" by blast
+ also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
finally show "... : domino" .
from hyp show "?B n : ?T" .
show "?a <= - ?B n" by blast
@@ -151,13 +151,13 @@
qed
lemma dominoes_tile_matrix:
- "below m <*> below (# 2 * n) : tiling domino"
+ "below m <*> below (2 * n) : tiling domino"
(is "?P m" is "?B m : ?T")
proof (induct m)
show "?P 0" by (simp add: below_0 tiling.empty)
fix m assume hyp: "?P m"
- let ?t = "{m} <*> below (# 2 * n)"
+ let ?t = "{m} <*> below (2 * n)"
have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
also have "... : ?T"
@@ -170,9 +170,9 @@
qed
lemma domino_singleton:
- "d : domino ==> b < # 2 ==> EX i j. evnodd d b = {(i, j)}"
+ "d : domino ==> b < 2 ==> EX i j. evnodd d b = {(i, j)}"
proof -
- assume b: "b < # 2"
+ assume b: "b < 2"
assume "d : domino"
thus ?thesis (is "?P d")
proof induct
@@ -227,9 +227,9 @@
and at: "a <= - t"
have card_suc:
- "!!b. b < # 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
+ "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
proof -
- fix b :: nat assume "b < # 2"
+ fix b :: nat assume "b < 2"
have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
also obtain i j where e: "?e a b = {(i, j)}"
proof -
@@ -260,15 +260,15 @@
constdefs
mutilated_board :: "nat => nat => (nat * nat) set"
"mutilated_board m n ==
- below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))
- - {(0, 0)} - {(# 2 * m + 1, # 2 * n + 1)}"
+ below (2 * (m + 1)) <*> below (2 * (n + 1))
+ - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
proof (unfold mutilated_board_def)
let ?T = "tiling domino"
- let ?t = "below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))"
+ let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
let ?t' = "?t - {(0, 0)}"
- let ?t'' = "?t' - {(# 2 * m + 1, # 2 * n + 1)}"
+ let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
show "?t'' ~: ?T"
proof
@@ -282,12 +282,12 @@
note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff
have "card (?e ?t'' 0) < card (?e ?t' 0)"
proof -
- have "card (?e ?t' 0 - {(# 2 * m + 1, # 2 * n + 1)})
+ have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
< card (?e ?t' 0)"
proof (rule card_Diff1_less)
from _ fin show "finite (?e ?t' 0)"
by (rule finite_subset) auto
- show "(# 2 * m + 1, # 2 * n + 1) : ?e ?t' 0" by simp
+ show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
qed
thus ?thesis by simp
qed
--- a/src/HOL/Isar_examples/Summation.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Sat Oct 06 00:02:46 2001 +0200
@@ -31,14 +31,14 @@
*}
theorem sum_of_naturals:
- "# 2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
+ "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
next
- fix n have "?S (n + 1) = ?S n + # 2 * (n + 1)" by simp
+ fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
also assume "?S n = n * (n + 1)"
- also have "... + # 2 * (n + 1) = (n + 1) * (n + # 2)" by simp
+ also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
finally show "?P (Suc n)" by simp
qed
@@ -86,14 +86,14 @@
*}
theorem sum_of_odds:
- "(\<Sum>i < n. # 2 * i + 1) = n^Suc (Suc 0)"
+ "(\<Sum>i < n. 2 * i + 1) = n^Suc (Suc 0)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
next
- fix n have "?S (n + 1) = ?S n + # 2 * n + 1" by simp
+ fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
also assume "?S n = n^Suc (Suc 0)"
- also have "... + # 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
+ also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
finally show "?P (Suc n)" by simp
qed
@@ -106,28 +106,28 @@
lemmas distrib = add_mult_distrib add_mult_distrib2
theorem sum_of_squares:
- "# 6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (# 2 * n + 1)"
+ "6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
next
- fix n have "?S (n + 1) = ?S n + # 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
- also assume "?S n = n * (n + 1) * (# 2 * n + 1)"
- also have "... + # 6 * (n + 1)^Suc (Suc 0) =
- (n + 1) * (n + # 2) * (# 2 * (n + 1) + 1)" by (simp add: distrib)
+ fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
+ also assume "?S n = n * (n + 1) * (2 * n + 1)"
+ also have "... + 6 * (n + 1)^Suc (Suc 0) =
+ (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
finally show "?P (Suc n)" by simp
qed
theorem sum_of_cubes:
- "# 4 * (\<Sum>i < n + 1. i^# 3) = (n * (n + 1))^Suc (Suc 0)"
+ "4 * (\<Sum>i < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by (simp add: power_eq_if)
next
- fix n have "?S (n + 1) = ?S n + # 4 * (n + 1)^# 3"
+ fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
by (simp add: power_eq_if distrib)
also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
- also have "... + # 4 * (n + 1)^# 3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
+ also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
by (simp add: power_eq_if distrib)
finally show "?P (Suc n)" by simp
qed
--- a/src/HOL/Lambda/Type.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Lambda/Type.thy Sat Oct 06 00:02:46 2001 +0200
@@ -59,11 +59,11 @@
subsection {* Some examples *}
-lemma "e |- Abs (Abs (Abs (Var 1 $ (Var # 2 $ Var 1 $ Var 0)))) : ?T"
+lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T"
apply force
done
-lemma "e |- Abs (Abs (Abs (Var # 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
+lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
apply force
done
--- a/src/HOL/Library/While_Combinator.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy Sat Oct 06 00:02:46 2001 +0200
@@ -135,14 +135,14 @@
theory.}
*}
-theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + # 2) mod # 6 | n. n \<in> N})) =
- P {Numeral0, # 4, # 2}"
+theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
+ P {Numeral0, 4, 2}"
proof -
have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
apply blast
done
show ?thesis
- apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, # 2, # 3, # 4, # 5}"])
+ apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
apply (rule monoI)
apply blast
apply simp
--- a/src/HOL/NumberTheory/EulerFermat.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Sat Oct 06 00:02:46 2001 +0200
@@ -55,7 +55,7 @@
zcongm :: "int => int => int => bool"
"zcongm m == \<lambda>a b. zcong a b m"
-lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = # -1)"
+lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = -1)"
-- {* LCP: not sure why this lemma is needed now *}
apply (auto simp add: zabs_def)
done
--- a/src/HOL/NumberTheory/Fib.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Sat Oct 06 00:02:46 2001 +0200
@@ -67,14 +67,14 @@
*}
lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
- (if n mod # 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
+ (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
apply (induct n rule: fib.induct)
apply (simp add: fib.Suc_Suc)
apply (simp add: fib.Suc_Suc mod_Suc)
apply (simp add: fib.Suc_Suc
add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
- apply (subgoal_tac "x mod # 2 < # 2", arith)
+ apply (subgoal_tac "x mod 2 < 2", arith)
apply simp
done
--- a/src/HOL/NumberTheory/WilsonBij.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy Sat Oct 06 00:02:46 2001 +0200
@@ -133,15 +133,15 @@
apply auto
done
-lemma aux3: "x \<le> p - # 2 ==> x < (p::int)"
+lemma aux3: "x \<le> p - 2 ==> x < (p::int)"
apply auto
done
-lemma aux4: "x \<le> p - # 2 ==> x < (p::int)-Numeral1"
+lemma aux4: "x \<le> p - 2 ==> x < (p::int)-Numeral1"
apply auto
done
-lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - # 2))"
+lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - 2))"
apply (unfold inj_on_def)
apply auto
apply (rule zcong_zless_imp_eq)
@@ -160,7 +160,7 @@
done
lemma inv_d22set_d22set:
- "p \<in> zprime ==> inv p ` d22set (p - # 2) = d22set (p - # 2)"
+ "p \<in> zprime ==> inv p ` d22set (p - 2) = d22set (p - 2)"
apply (rule endo_inj_surj)
apply (rule d22set_fin)
apply (erule_tac [2] inv_inj)
@@ -173,9 +173,9 @@
done
lemma d22set_d22set_bij:
- "p \<in> zprime ==> (d22set (p - # 2), d22set (p - # 2)) \<in> bijR (reciR p)"
+ "p \<in> zprime ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)"
apply (unfold reciR_def)
- apply (rule_tac s = "(d22set (p - # 2), inv p ` d22set (p - # 2))" in subst)
+ apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst)
apply (simp add: inv_d22set_d22set)
apply (rule inj_func_bijR)
apply (rule_tac [3] d22set_fin)
@@ -187,7 +187,7 @@
apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4)
done
-lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - # 2))"
+lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - 2))"
apply (unfold reciR_def bijP_def)
apply auto
apply (rule d22set_mem)
@@ -217,7 +217,7 @@
apply auto
done
-lemma bijER_d22set: "p \<in> zprime ==> d22set (p - # 2) \<in> bijER (reciR p)"
+lemma bijER_d22set: "p \<in> zprime ==> d22set (p - 2) \<in> bijER (reciR p)"
apply (rule bijR_bijER)
apply (erule d22set_d22set_bij)
apply (erule reciP_bijP)
@@ -245,12 +245,12 @@
apply auto
done
-theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
- apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - # 2)) (# -1 * Numeral1) p")
+theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
+ apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - 2)) (-1 * Numeral1) p")
apply (rule_tac [2] zcong_zmult)
apply (simp add: zprime_def)
apply (subst zfact.simps)
- apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
+ apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
apply auto
apply (simp add: zcong_def)
apply (subst d22set_prod_zfact [symmetric])
--- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Sat Oct 06 00:02:46 2001 +0200
@@ -20,7 +20,7 @@
wset :: "int * int => int set"
defs
- inv_def: "inv p a == (a^(nat (p - # 2))) mod p"
+ inv_def: "inv p a == (a^(nat (p - 2))) mod p"
recdef wset
"measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
@@ -32,7 +32,7 @@
text {* \medskip @{term [source] inv} *}
-lemma aux: "Numeral1 < m ==> Suc (nat (m - # 2)) = nat (m - Numeral1)"
+lemma aux: "Numeral1 < m ==> Suc (nat (m - 2)) = nat (m - Numeral1)"
apply (subst int_int_eq [symmetric])
apply auto
done
@@ -137,8 +137,8 @@
apply (simp add: pos_mod_bound)
done
-lemma aux: "# 5 \<le> p ==>
- nat (p - # 2) * nat (p - # 2) = Suc (nat (p - Numeral1) * nat (p - # 3))"
+lemma aux: "5 \<le> p ==>
+ nat (p - 2) * nat (p - 2) = Suc (nat (p - Numeral1) * nat (p - 3))"
apply (subst int_int_eq [symmetric])
apply (simp add: zmult_int [symmetric])
apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
@@ -154,7 +154,7 @@
done
lemma inv_inv: "p \<in> zprime \<Longrightarrow>
- # 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
+ 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
apply (unfold inv_def)
apply (subst zpower_zmod)
apply (subst zpower_zpower)
@@ -165,7 +165,7 @@
apply (subst zcong_zmod [symmetric])
apply (subst aux)
apply (subgoal_tac [2]
- "zcong (a * a^(nat (p - Numeral1) * nat (p - # 3))) (a * Numeral1) p")
+ "zcong (a * a^(nat (p - Numeral1) * nat (p - 3))) (a * Numeral1) p")
apply (rule_tac [3] zcong_zmult)
apply (rule_tac [4] zcong_zpower_zmult)
apply (erule_tac [4] Little_Fermat)
@@ -256,7 +256,7 @@
done
lemma wset_mem_inv_mem [rule_format]:
- "p \<in> zprime --> # 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
+ "p \<in> zprime --> 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
--> inv p b \<in> wset (a, p)"
apply (induct a p rule: wset_induct)
apply auto
@@ -274,7 +274,7 @@
done
lemma wset_inv_mem_mem:
- "p \<in> zprime \<Longrightarrow> # 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
+ "p \<in> zprime \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
\<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
apply (rule_tac [2] wset_mem_inv_mem)
@@ -292,7 +292,7 @@
lemma wset_zcong_prod_1 [rule_format]:
"p \<in> zprime -->
- # 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
+ 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
apply (induct a p rule: wset_induct)
prefer 2
apply (subst wset.simps)
@@ -314,7 +314,7 @@
apply auto
done
-lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - # 2) = wset (p - # 2, p)"
+lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - 2) = wset (p - 2, p)"
apply safe
apply (erule wset_mem)
apply (rule_tac [2] d22set_g_1)
@@ -323,7 +323,7 @@
apply (erule_tac [4] wset_g_1)
prefer 6
apply (subst zle_add1_eq_le [symmetric])
- apply (subgoal_tac "p - # 2 + Numeral1 = p - Numeral1")
+ apply (subgoal_tac "p - 2 + Numeral1 = p - Numeral1")
apply (simp (no_asm_simp))
apply (erule wset_less)
apply auto
@@ -332,36 +332,36 @@
subsection {* Wilson *}
-lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> # 2 \<Longrightarrow> p \<noteq> # 3 ==> # 5 \<le> p"
+lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
apply (unfold zprime_def dvd_def)
- apply (case_tac "p = # 4")
+ apply (case_tac "p = 4")
apply auto
apply (rule notE)
prefer 2
apply assumption
apply (simp (no_asm))
- apply (rule_tac x = "# 2" in exI)
+ apply (rule_tac x = "2" in exI)
apply safe
- apply (rule_tac x = "# 2" in exI)
+ apply (rule_tac x = "2" in exI)
apply auto
apply arith
done
theorem Wilson_Russ:
- "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
- apply (subgoal_tac "[(p - Numeral1) * zfact (p - # 2) = # -1 * Numeral1] (mod p)")
+ "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
+ apply (subgoal_tac "[(p - Numeral1) * zfact (p - 2) = -1 * Numeral1] (mod p)")
apply (rule_tac [2] zcong_zmult)
apply (simp only: zprime_def)
apply (subst zfact.simps)
- apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
+ apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
apply auto
apply (simp only: zcong_def)
apply (simp (no_asm_simp))
- apply (case_tac "p = # 2")
+ apply (case_tac "p = 2")
apply (simp add: zfact.simps)
- apply (case_tac "p = # 3")
+ apply (case_tac "p = 3")
apply (simp add: zfact.simps)
- apply (subgoal_tac "# 5 \<le> p")
+ apply (subgoal_tac "5 \<le> p")
apply (erule_tac [2] prime_g_5)
apply (subst d22set_prod_zfact [symmetric])
apply (subst d22set_eq_wset)
--- a/src/HOL/Numeral.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Numeral.thy Sat Oct 06 00:02:46 2001 +0200
@@ -24,7 +24,7 @@
syntax
"_constify" :: "num => numeral" ("_")
- "_Numeral" :: "numeral => 'a" ("#_")
+ "_Numeral" :: "numeral => 'a" ("_")
Numeral0 :: 'a
Numeral1 :: 'a
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sat Oct 06 00:02:46 2001 +0200
@@ -86,7 +86,7 @@
by (unfold is_vectorspace_def) simp
lemma negate_eq2a:
- "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> # -1 \<cdot> x = - x"
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
by (unfold is_vectorspace_def) simp
lemma diff_eq2:
--- a/src/HOL/Real/RComplete.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RComplete.ML Sat Oct 06 00:02:46 2001 +0200
@@ -8,7 +8,7 @@
claset_ref() := claset() delWrapper "bspec";
-Goal "x/# 2 + x/# 2 = (x::real)";
+Goal "x/2 + x/2 = (x::real)";
by (Simp_tac 1);
qed "real_sum_of_halves";
--- a/src/HOL/Real/RealArith0.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RealArith0.ML Sat Oct 06 00:02:46 2001 +0200
@@ -276,34 +276,34 @@
set trace_simp;
fun test s = (Goal s; by (Simp_tac 1));
-test "Numeral0 <= (y::real) * # -2";
-test "# 9*x = # 12 * (y::real)";
-test "(# 9*x) / (# 12 * (y::real)) = z";
-test "# 9*x < # 12 * (y::real)";
-test "# 9*x <= # 12 * (y::real)";
+test "Numeral0 <= (y::real) * -2";
+test "9*x = 12 * (y::real)";
+test "(9*x) / (12 * (y::real)) = z";
+test "9*x < 12 * (y::real)";
+test "9*x <= 12 * (y::real)";
-test "# -99*x = # 132 * (y::real)";
-test "(# -99*x) / (# 132 * (y::real)) = z";
-test "# -99*x < # 132 * (y::real)";
-test "# -99*x <= # 132 * (y::real)";
+test "-99*x = 132 * (y::real)";
+test "(-99*x) / (132 * (y::real)) = z";
+test "-99*x < 132 * (y::real)";
+test "-99*x <= 132 * (y::real)";
-test "# 999*x = # -396 * (y::real)";
-test "(# 999*x) / (# -396 * (y::real)) = z";
-test "# 999*x < # -396 * (y::real)";
-test "# 999*x <= # -396 * (y::real)";
+test "999*x = -396 * (y::real)";
+test "(999*x) / (-396 * (y::real)) = z";
+test "999*x < -396 * (y::real)";
+test "999*x <= -396 * (y::real)";
-test "# -99*x = # -81 * (y::real)";
-test "(# -99*x) / (# -81 * (y::real)) = z";
-test "# -99*x <= # -81 * (y::real)";
-test "# -99*x < # -81 * (y::real)";
+test "-99*x = -81 * (y::real)";
+test "(-99*x) / (-81 * (y::real)) = z";
+test "-99*x <= -81 * (y::real)";
+test "-99*x < -81 * (y::real)";
-test "# -2 * x = # -1 * (y::real)";
-test "# -2 * x = -(y::real)";
-test "(# -2 * x) / (# -1 * (y::real)) = z";
-test "# -2 * x < -(y::real)";
-test "# -2 * x <= # -1 * (y::real)";
-test "-x < # -23 * (y::real)";
-test "-x <= # -23 * (y::real)";
+test "-2 * x = -1 * (y::real)";
+test "-2 * x = -(y::real)";
+test "(-2 * x) / (-1 * (y::real)) = z";
+test "-2 * x < -(y::real)";
+test "-2 * x <= -1 * (y::real)";
+test "-x < -23 * (y::real)";
+test "-x <= -23 * (y::real)";
*)
@@ -505,18 +505,18 @@
qed "real_divide_1";
Addsimps [real_divide_1];
-Goal "x/# -1 = -(x::real)";
+Goal "x/-1 = -(x::real)";
by (Simp_tac 1);
qed "real_divide_minus1";
Addsimps [real_divide_minus1];
-Goal "# -1/(x::real) = - (Numeral1/x)";
+Goal "-1/(x::real) = - (Numeral1/x)";
by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
qed "real_minus1_divide";
Addsimps [real_minus1_divide];
Goal "[| (Numeral0::real) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1);
+by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
by (asm_simp_tac (simpset() addsimps [min_def]) 1);
qed "real_lbound_gt_zero";
@@ -647,11 +647,11 @@
(*** Density of the Reals ***)
-Goal "x < y ==> x < (x+y) / (# 2::real)";
+Goal "x < y ==> x < (x+y) / (2::real)";
by Auto_tac;
qed "real_less_half_sum";
-Goal "x < y ==> (x+y)/(# 2::real) < y";
+Goal "x < y ==> (x+y)/(2::real) < y";
by Auto_tac;
qed "real_gt_half_sum";
--- a/src/HOL/Real/RealBin.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RealBin.ML Sat Oct 06 00:02:46 2001 +0200
@@ -58,18 +58,18 @@
Addsimps [mult_real_number_of];
-Goal "(# 2::real) = Numeral1 + Numeral1";
+Goal "(2::real) = Numeral1 + Numeral1";
by (Simp_tac 1);
val lemma = result();
(*For specialist use: NOT as default simprules*)
-Goal "# 2 * z = (z+z::real)";
+Goal "2 * z = (z+z::real)";
by (simp_tac (simpset ()
addsimps [lemma, real_add_mult_distrib,
one_eq_numeral_1 RS sym]) 1);
qed "real_mult_2";
-Goal "z * # 2 = (z+z::real)";
+Goal "z * 2 = (z+z::real)";
by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
qed "real_mult_2_right";
@@ -111,12 +111,12 @@
(*** New versions of existing theorems involving 0, 1r ***)
-Goal "- Numeral1 = (# -1::real)";
+Goal "- Numeral1 = (-1::real)";
by (Simp_tac 1);
qed "minus_numeral_one";
-(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to # -1*)
+(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to -1*)
val real_numeral_ss =
HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1,
minus_numeral_one];
@@ -488,7 +488,7 @@
structure CombineNumeralsData =
struct
val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
+ val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
@@ -548,35 +548,35 @@
set trace_simp;
fun test s = (Goal s; by (Simp_tac 1));
-test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::real)";
+test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::real)";
-test "# 2*u = (u::real)";
-test "(i + j + # 12 + (k::real)) - # 15 = y";
-test "(i + j + # 12 + (k::real)) - # 5 = y";
+test "2*u = (u::real)";
+test "(i + j + 12 + (k::real)) - 15 = y";
+test "(i + j + 12 + (k::real)) - 5 = y";
test "y - b < (b::real)";
-test "y - (# 3*b + c) < (b::real) - # 2*c";
+test "y - (3*b + c) < (b::real) - 2*c";
-test "(# 2*x - (u*v) + y) - v*# 3*u = (w::real)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::real)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::real)";
-test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::real)";
+test "(2*x - (u*v) + y) - v*3*u = (w::real)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::real)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::real)";
+test "u*v - (x*u*v + (u*v)*4 + y) = (w::real)";
-test "(i + j + # 12 + (k::real)) = u + # 15 + y";
-test "(i + j*# 2 + # 12 + (k::real)) = j + # 5 + y";
+test "(i + j + 12 + (k::real)) = u + 15 + y";
+test "(i + j*2 + 12 + (k::real)) = j + 5 + y";
-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)";
+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)";
test "a + -(b+c) + b = (d::real)";
test "a + -(b+c) - b = (d::real)";
(*negative numerals*)
-test "(i + j + # -2 + (k::real)) - (u + # 5 + y) = zz";
-test "(i + j + # -3 + (k::real)) < u + # 5 + y";
-test "(i + j + # 3 + (k::real)) < u + # -6 + y";
-test "(i + j + # -12 + (k::real)) - # 15 = y";
-test "(i + j + # 12 + (k::real)) - # -15 = y";
-test "(i + j + # -12 + (k::real)) - # -15 = y";
+test "(i + j + -2 + (k::real)) - (u + 5 + y) = zz";
+test "(i + j + -3 + (k::real)) < u + 5 + y";
+test "(i + j + 3 + (k::real)) < u + -6 + y";
+test "(i + j + -12 + (k::real)) - 15 = y";
+test "(i + j + 12 + (k::real)) - -15 = y";
+test "(i + j + -12 + (k::real)) - -15 = y";
*)
--- a/src/HOL/Real/RealPow.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RealPow.ML Sat Oct 06 00:02:46 2001 +0200
@@ -76,7 +76,7 @@
qed "realpow_eq_one";
Addsimps [realpow_eq_one];
-Goal "abs((# -1) ^ n) = (Numeral1::real)";
+Goal "abs((-1) ^ n) = (Numeral1::real)";
by (induct_tac "n" 1);
by (auto_tac (claset(), simpset() addsimps [abs_mult]));
qed "abs_realpow_minus_one";
@@ -127,13 +127,13 @@
by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
qed "realpow_ge_one2";
-Goal "(Numeral1::real) <= # 2 ^ n";
+Goal "(Numeral1::real) <= 2 ^ n";
by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
by (rtac realpow_le 2);
by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
qed "two_realpow_ge_one";
-Goal "real (n::nat) < # 2 ^ n";
+Goal "real (n::nat) < 2 ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
by (stac real_mult_2 1);
@@ -142,18 +142,18 @@
qed "two_realpow_gt";
Addsimps [two_realpow_gt,two_realpow_ge_one];
-Goal "(# -1) ^ (# 2*n) = (Numeral1::real)";
+Goal "(-1) ^ (2*n) = (Numeral1::real)";
by (induct_tac "n" 1);
by Auto_tac;
qed "realpow_minus_one";
Addsimps [realpow_minus_one];
-Goal "(# -1) ^ Suc (# 2*n) = -(Numeral1::real)";
+Goal "(-1) ^ Suc (2*n) = -(Numeral1::real)";
by Auto_tac;
qed "realpow_minus_one_odd";
Addsimps [realpow_minus_one_odd];
-Goal "(# -1) ^ Suc (Suc (# 2*n)) = (Numeral1::real)";
+Goal "(-1) ^ Suc (Suc (2*n)) = (Numeral1::real)";
by Auto_tac;
qed "realpow_minus_one_even";
Addsimps [realpow_minus_one_even];
--- a/src/HOL/Real/ex/BinEx.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/ex/BinEx.thy Sat Oct 06 00:02:46 2001 +0200
@@ -15,52 +15,52 @@
text {* \medskip Addition *}
-lemma "(# 1359::real) + # -2468 = # -1109"
+lemma "(1359::real) + -2468 = -1109"
by simp
-lemma "(# 93746::real) + # -46375 = # 47371"
+lemma "(93746::real) + -46375 = 47371"
by simp
text {* \medskip Negation *}
-lemma "- (# 65745::real) = # -65745"
+lemma "- (65745::real) = -65745"
by simp
-lemma "- (# -54321::real) = # 54321"
+lemma "- (-54321::real) = 54321"
by simp
text {* \medskip Multiplication *}
-lemma "(# -84::real) * # 51 = # -4284"
+lemma "(-84::real) * 51 = -4284"
by simp
-lemma "(# 255::real) * # 255 = # 65025"
+lemma "(255::real) * 255 = 65025"
by simp
-lemma "(# 1359::real) * # -2468 = # -3354012"
+lemma "(1359::real) * -2468 = -3354012"
by simp
text {* \medskip Inequalities *}
-lemma "(# 89::real) * # 10 \<noteq> # 889"
+lemma "(89::real) * 10 \<noteq> 889"
by simp
-lemma "(# 13::real) < # 18 - # 4"
+lemma "(13::real) < 18 - 4"
by simp
-lemma "(# -345::real) < # -242 + # -100"
+lemma "(-345::real) < -242 + -100"
by simp
-lemma "(# 13557456::real) < # 18678654"
+lemma "(13557456::real) < 18678654"
by simp
-lemma "(# 999999::real) \<le> (# 1000001 + Numeral1)-# 2"
+lemma "(999999::real) \<le> (1000001 + Numeral1) - 2"
by simp
-lemma "(# 1234567::real) \<le> # 1234567"
+lemma "(1234567::real) \<le> 1234567"
by simp
--- a/src/HOL/Real/ex/Sqrt_Irrational.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/ex/Sqrt_Irrational.thy Sat Oct 06 00:02:46 2001 +0200
@@ -114,15 +114,15 @@
this formally :-).
*}
-theorem "x\<twosuperior> = real (# 2::nat) ==> x \<notin> \<rat>"
+theorem "x\<twosuperior> = real (2::nat) ==> x \<notin> \<rat>"
proof (rule sqrt_prime_irrational)
{
- fix m :: nat assume dvd: "m dvd # 2"
- hence "m \<le> # 2" by (simp add: dvd_imp_le)
+ fix m :: nat assume dvd: "m dvd 2"
+ hence "m \<le> 2" by (simp add: dvd_imp_le)
moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
- ultimately have "m = 1 \<or> m = # 2" by arith
+ ultimately have "m = 1 \<or> m = 2" by arith
}
- thus "# 2 \<in> prime" by (simp add: prime_def)
+ thus "2 \<in> prime" by (simp add: prime_def)
qed
text {*
--- a/src/HOL/Real/real_arith0.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/real_arith0.ML Sat Oct 06 00:02:46 2001 +0200
@@ -118,7 +118,7 @@
qed "";
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> # 6*a <= # 5*l+i";
+\ ==> 6*a <= 5*l+i";
by (fast_arith_tac 1);
qed "";
*)
--- a/src/HOL/UNITY/Simple/Mutex.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.ML Sat Oct 06 00:02:46 2001 +0200
@@ -25,7 +25,7 @@
qed "IV";
(*The safety property: mutual exclusion*)
-Goal "Mutex : Always {s. ~ (m s = # 3 & n s = # 3)}";
+Goal "Mutex : Always {s. ~ (m s = 3 & n s = 3)}";
by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
by Auto_tac;
qed "mutual_exclusion";
@@ -42,33 +42,33 @@
getgoal 1;
-Goal "((Numeral1::int) <= i & i <= # 3) = (i = Numeral1 | i = # 2 | i = # 3)";
+Goal "((Numeral1::int) <= i & i <= 3) = (i = Numeral1 | i = 2 | i = 3)";
by (arith_tac 1);
qed "eq_123";
(*** Progress for U ***)
-Goalw [Unless_def] "Mutex : {s. m s=# 2} Unless {s. m s=# 3}";
+Goalw [Unless_def] "Mutex : {s. m s=2} Unless {s. m s=3}";
by (constrains_tac 1);
qed "U_F0";
-Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = # 2}";
+Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = 2}";
by (ensures_tac "U1" 1);
qed "U_F1";
-Goal "Mutex : {s. ~ p s & m s = # 2} LeadsTo {s. m s = # 3}";
+Goal "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}";
by (cut_facts_tac [IU] 1);
by (ensures_tac "U2" 1);
qed "U_F2";
-Goal "Mutex : {s. m s = # 3} LeadsTo {s. p s}";
-by (res_inst_tac [("B", "{s. m s = # 4}")] LeadsTo_Trans 1);
+Goal "Mutex : {s. m s = 3} LeadsTo {s. p s}";
+by (res_inst_tac [("B", "{s. m s = 4}")] LeadsTo_Trans 1);
by (ensures_tac "U4" 2);
by (ensures_tac "U3" 1);
qed "U_F3";
-Goal "Mutex : {s. m s = # 2} LeadsTo {s. p s}";
+Goal "Mutex : {s. m s = 2} LeadsTo {s. p s}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
@@ -80,7 +80,7 @@
by (Blast_tac 1);
val U_lemma1 = result();
-Goal "Mutex : {s. Numeral1 <= m s & m s <= # 3} LeadsTo {s. p s}";
+Goal "Mutex : {s. Numeral1 <= m s & m s <= 3} LeadsTo {s. p s}";
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
U_lemma1, U_lemma2, U_F3] ) 1);
val U_lemma123 = result();
@@ -95,26 +95,26 @@
(*** Progress for V ***)
-Goalw [Unless_def] "Mutex : {s. n s=# 2} Unless {s. n s=# 3}";
+Goalw [Unless_def] "Mutex : {s. n s=2} Unless {s. n s=3}";
by (constrains_tac 1);
qed "V_F0";
-Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = # 2}";
+Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = 2}";
by (ensures_tac "V1" 1);
qed "V_F1";
-Goal "Mutex : {s. p s & n s = # 2} LeadsTo {s. n s = # 3}";
+Goal "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}";
by (cut_facts_tac [IV] 1);
by (ensures_tac "V2" 1);
qed "V_F2";
-Goal "Mutex : {s. n s = # 3} LeadsTo {s. ~ p s}";
-by (res_inst_tac [("B", "{s. n s = # 4}")] LeadsTo_Trans 1);
+Goal "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}";
+by (res_inst_tac [("B", "{s. n s = 4}")] LeadsTo_Trans 1);
by (ensures_tac "V4" 2);
by (ensures_tac "V3" 1);
qed "V_F3";
-Goal "Mutex : {s. n s = # 2} LeadsTo {s. ~ p s}";
+Goal "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
@@ -126,7 +126,7 @@
by (Blast_tac 1);
val V_lemma1 = result();
-Goal "Mutex : {s. Numeral1 <= n s & n s <= # 3} LeadsTo {s. ~ p s}";
+Goal "Mutex : {s. Numeral1 <= n s & n s <= 3} LeadsTo {s. ~ p s}";
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
V_lemma1, V_lemma2, V_F3] ) 1);
val V_lemma123 = result();
@@ -142,7 +142,7 @@
(** Absence of starvation **)
(*Misra's F6*)
-Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = # 3}";
+Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = 3}";
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
by (rtac U_F2 2);
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
@@ -154,7 +154,7 @@
qed "m1_Leadsto_3";
(*The same for V*)
-Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = # 3}";
+Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = 3}";
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
by (rtac V_F2 2);
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
--- a/src/HOL/UNITY/Simple/Mutex.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy Sat Oct 06 00:02:46 2001 +0200
@@ -25,16 +25,16 @@
"U0 == {(s,s'). s' = s (|u:=True, m:=Numeral1|) & m s = Numeral0}"
U1 :: command
- "U1 == {(s,s'). s' = s (|p:= v s, m:=# 2|) & m s = Numeral1}"
+ "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = Numeral1}"
U2 :: command
- "U2 == {(s,s'). s' = s (|m:=# 3|) & ~ p s & m s = # 2}"
+ "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}"
U3 :: command
- "U3 == {(s,s'). s' = s (|u:=False, m:=# 4|) & m s = # 3}"
+ "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}"
U4 :: command
- "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = # 4}"
+ "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = 4}"
(** The program for process V **)
@@ -42,16 +42,16 @@
"V0 == {(s,s'). s' = s (|v:=True, n:=Numeral1|) & n s = Numeral0}"
V1 :: command
- "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=# 2|) & n s = Numeral1}"
+ "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = Numeral1}"
V2 :: command
- "V2 == {(s,s'). s' = s (|n:=# 3|) & p s & n s = # 2}"
+ "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}"
V3 :: command
- "V3 == {(s,s'). s' = s (|v:=False, n:=# 4|) & n s = # 3}"
+ "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}"
V4 :: command
- "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = # 4}"
+ "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = 4}"
Mutex :: state program
"Mutex == mk_program ({s. ~ u s & ~ v s & m s = Numeral0 & n s = Numeral0},
@@ -62,15 +62,15 @@
(** The correct invariants **)
IU :: state set
- "IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) & (m s = # 3 --> ~ p s)}"
+ "IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
IV :: state set
- "IV == {s. (v s = (Numeral1 <= n s & n s <= # 3)) & (n s = # 3 --> p s)}"
+ "IV == {s. (v s = (Numeral1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
(** The faulty invariant (for U alone) **)
bad_IU :: state set
- "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) &
- (# 3 <= m s & m s <= # 4 --> ~ p s)}"
+ "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) &
+ (3 <= m s & m s <= 4 --> ~ p s)}"
end
--- a/src/HOL/UNITY/Union.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/UNITY/Union.ML Sat Oct 06 00:02:46 2001 +0200
@@ -352,7 +352,7 @@
bind_thm ("ok_sym", ok_commute RS iffD1);
-Goal "OK {(Numeral0::int,F),(Numeral1,G),(# 2,H)} snd = (F ok G & (F Join G) ok H)";
+Goal "OK {(Numeral0::int,F),(Numeral1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
by (asm_full_simp_tac
(simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def,
OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);
--- a/src/HOL/Unix/ROOT.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Unix/ROOT.ML Sat Oct 06 00:02:46 2001 +0200
@@ -1,3 +1,3 @@
-Library.setmp print_mode (! print_mode @ ["no_brackets"])
+Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
use_thy "Unix";
--- a/src/HOL/arith_data.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/arith_data.ML Sat Oct 06 00:02:46 2001 +0200
@@ -438,7 +438,7 @@
[Simplifier.change_simpset_of (op addSolver)
(mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
- Method.add_methods [("arith", (arith_method o # 2) oo Method.syntax Args.bang_facts,
+ Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
"decide linear arithmethic")],
Attrib.add_attributes [("arith_split",
(Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
--- a/src/HOL/ex/BinEx.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/BinEx.thy Sat Oct 06 00:02:46 2001 +0200
@@ -12,75 +12,75 @@
text {* Addition *}
-lemma "(# 13::int) + # 19 = # 32"
+lemma "(13::int) + 19 = 32"
by simp
-lemma "(# 1234::int) + # 5678 = # 6912"
+lemma "(1234::int) + 5678 = 6912"
by simp
-lemma "(# 1359::int) + # -2468 = # -1109"
+lemma "(1359::int) + -2468 = -1109"
by simp
-lemma "(# 93746::int) + # -46375 = # 47371"
+lemma "(93746::int) + -46375 = 47371"
by simp
text {* \medskip Negation *}
-lemma "- (# 65745::int) = # -65745"
+lemma "- (65745::int) = -65745"
by simp
-lemma "- (# -54321::int) = # 54321"
+lemma "- (-54321::int) = 54321"
by simp
text {* \medskip Multiplication *}
-lemma "(# 13::int) * # 19 = # 247"
+lemma "(13::int) * 19 = 247"
by simp
-lemma "(# -84::int) * # 51 = # -4284"
+lemma "(-84::int) * 51 = -4284"
by simp
-lemma "(# 255::int) * # 255 = # 65025"
+lemma "(255::int) * 255 = 65025"
by simp
-lemma "(# 1359::int) * # -2468 = # -3354012"
+lemma "(1359::int) * -2468 = -3354012"
by simp
-lemma "(# 89::int) * # 10 \<noteq> # 889"
+lemma "(89::int) * 10 \<noteq> 889"
by simp
-lemma "(# 13::int) < # 18 - # 4"
+lemma "(13::int) < 18 - 4"
by simp
-lemma "(# -345::int) < # -242 + # -100"
+lemma "(-345::int) < -242 + -100"
by simp
-lemma "(# 13557456::int) < # 18678654"
+lemma "(13557456::int) < 18678654"
by simp
-lemma "(# 999999::int) \<le> (# 1000001 + Numeral1) - # 2"
+lemma "(999999::int) \<le> (1000001 + Numeral1) - 2"
by simp
-lemma "(# 1234567::int) \<le> # 1234567"
+lemma "(1234567::int) \<le> 1234567"
by simp
text {* \medskip Quotient and Remainder *}
-lemma "(# 10::int) div # 3 = # 3"
+lemma "(10::int) div 3 = 3"
by simp
-lemma "(# 10::int) mod # 3 = Numeral1"
+lemma "(10::int) mod 3 = Numeral1"
by simp
text {* A negative divisor *}
-lemma "(# 10::int) div # -3 = # -4"
+lemma "(10::int) div -3 = -4"
by simp
-lemma "(# 10::int) mod # -3 = # -2"
+lemma "(10::int) mod -3 = -2"
by simp
text {*
@@ -88,50 +88,50 @@
convention but not with the hardware of most computers}
*}
-lemma "(# -10::int) div # 3 = # -4"
+lemma "(-10::int) div 3 = -4"
by simp
-lemma "(# -10::int) mod # 3 = # 2"
+lemma "(-10::int) mod 3 = 2"
by simp
text {* A negative dividend \emph{and} divisor *}
-lemma "(# -10::int) div # -3 = # 3"
+lemma "(-10::int) div -3 = 3"
by simp
-lemma "(# -10::int) mod # -3 = # -1"
+lemma "(-10::int) mod -3 = -1"
by simp
text {* A few bigger examples *}
-lemma "(# 8452::int) mod # 3 = Numeral1"
+lemma "(8452::int) mod 3 = Numeral1"
by simp
-lemma "(# 59485::int) div # 434 = # 137"
+lemma "(59485::int) div 434 = 137"
by simp
-lemma "(# 1000006::int) mod # 10 = # 6"
+lemma "(1000006::int) mod 10 = 6"
by simp
text {* \medskip Division by shifting *}
-lemma "# 10000000 div # 2 = (# 5000000::int)"
+lemma "10000000 div 2 = (5000000::int)"
by simp
-lemma "# 10000001 mod # 2 = (Numeral1::int)"
+lemma "10000001 mod 2 = (Numeral1::int)"
by simp
-lemma "# 10000055 div # 32 = (# 312501::int)"
+lemma "10000055 div 32 = (312501::int)"
by simp
-lemma "# 10000055 mod # 32 = (# 23::int)"
+lemma "10000055 mod 32 = (23::int)"
by simp
-lemma "# 100094 div # 144 = (# 695::int)"
+lemma "100094 div 144 = (695::int)"
by simp
-lemma "# 100094 mod # 144 = (# 14::int)"
+lemma "100094 mod 144 = (14::int)"
by simp
@@ -139,65 +139,65 @@
text {* Successor *}
-lemma "Suc # 99999 = # 100000"
+lemma "Suc 99999 = 100000"
by (simp add: Suc_nat_number_of)
-- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
text {* \medskip Addition *}
-lemma "(# 13::nat) + # 19 = # 32"
+lemma "(13::nat) + 19 = 32"
by simp
-lemma "(# 1234::nat) + # 5678 = # 6912"
+lemma "(1234::nat) + 5678 = 6912"
by simp
-lemma "(# 973646::nat) + # 6475 = # 980121"
+lemma "(973646::nat) + 6475 = 980121"
by simp
text {* \medskip Subtraction *}
-lemma "(# 32::nat) - # 14 = # 18"
+lemma "(32::nat) - 14 = 18"
by simp
-lemma "(# 14::nat) - # 15 = Numeral0"
+lemma "(14::nat) - 15 = Numeral0"
by simp
-lemma "(# 14::nat) - # 1576644 = Numeral0"
+lemma "(14::nat) - 1576644 = Numeral0"
by simp
-lemma "(# 48273776::nat) - # 3873737 = # 44400039"
+lemma "(48273776::nat) - 3873737 = 44400039"
by simp
text {* \medskip Multiplication *}
-lemma "(# 12::nat) * # 11 = # 132"
+lemma "(12::nat) * 11 = 132"
by simp
-lemma "(# 647::nat) * # 3643 = # 2357021"
+lemma "(647::nat) * 3643 = 2357021"
by simp
text {* \medskip Quotient and Remainder *}
-lemma "(# 10::nat) div # 3 = # 3"
+lemma "(10::nat) div 3 = 3"
by simp
-lemma "(# 10::nat) mod # 3 = Numeral1"
+lemma "(10::nat) mod 3 = Numeral1"
by simp
-lemma "(# 10000::nat) div # 9 = # 1111"
+lemma "(10000::nat) div 9 = 1111"
by simp
-lemma "(# 10000::nat) mod # 9 = Numeral1"
+lemma "(10000::nat) mod 9 = Numeral1"
by simp
-lemma "(# 10000::nat) div # 16 = # 625"
+lemma "(10000::nat) div 16 = 625"
by simp
-lemma "(# 10000::nat) mod # 16 = Numeral0"
+lemma "(10000::nat) mod 16 = Numeral0"
by simp
--- a/src/HOL/ex/NatSum.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/NatSum.thy Sat Oct 06 00:02:46 2001 +0200
@@ -36,8 +36,8 @@
*}
lemma sum_of_odd_squares:
- "# 3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
- n * (# 4 * n * n - Numeral1)"
+ "3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
+ n * (4 * n * n - Numeral1)"
apply (induct n)
txt {* This removes the @{term "-Numeral1"} from the inductive step *}
apply (case_tac [2] n)
@@ -51,7 +51,7 @@
lemma sum_of_odd_cubes:
"setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
- n * n * (# 2 * n * n - Numeral1)"
+ n * n * (2 * n * n - Numeral1)"
apply (induct "n")
txt {* This removes the @{term "-Numeral1"} from the inductive step *}
apply (case_tac [2] "n")
@@ -63,19 +63,19 @@
@{text "n (n + 1) / 2"}.*}
lemma sum_of_naturals:
- "# 2 * setsum id (atMost n) = n * Suc n"
+ "2 * setsum id (atMost n) = n * Suc n"
apply (induct n)
apply auto
done
lemma sum_of_squares:
- "# 6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (# 2 * n)"
+ "6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (2 * n)"
apply (induct n)
apply auto
done
lemma sum_of_cubes:
- "# 4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
+ "4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
apply (induct n)
apply auto
done
@@ -86,8 +86,8 @@
*}
lemma sum_of_fourth_powers:
- "# 30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
- n * Suc n * Suc (# 2 * n) * (# 3 * n * n + # 3 * n - Numeral1)"
+ "30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
+ n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - Numeral1)"
apply (induct n)
apply auto
txt {* Eliminates the subtraction *}
@@ -107,9 +107,9 @@
zdiff_zmult_distrib2 [simp]
lemma int_sum_of_fourth_powers:
- "# 30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
- int m * (int m - Numeral1) * (int (# 2 * m) - Numeral1) *
- (int (# 3 * m * m) - int (# 3 * m) - Numeral1)"
+ "30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
+ int m * (int m - Numeral1) * (int (2 * m) - Numeral1) *
+ (int (3 * m * m) - int (3 * m) - Numeral1)"
apply (induct m)
apply simp_all
done
@@ -118,12 +118,12 @@
text {*
\medskip Sums of geometric series: 2, 3 and the general case *}
-lemma sum_of_2_powers: "setsum (\<lambda>i. # 2^i) (lessThan n) = # 2^n - (1::nat)"
+lemma sum_of_2_powers: "setsum (\<lambda>i. 2^i) (lessThan n) = 2^n - (1::nat)"
apply (induct n)
apply (auto split: nat_diff_split)
done
-lemma sum_of_3_powers: "# 2 * setsum (\<lambda>i. # 3^i) (lessThan n) = # 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * setsum (\<lambda>i. 3^i) (lessThan n) = 3^n - (1::nat)"
apply (induct n)
apply auto
done
--- a/src/HOL/ex/Primrec.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/Primrec.thy Sat Oct 06 00:02:46 2001 +0200
@@ -159,7 +159,7 @@
text {* PROPERTY A 8 *}
-lemma ack_1 [simp]: "ack (Suc 0, j) = j + # 2"
+lemma ack_1 [simp]: "ack (Suc 0, j) = j + 2"
apply (induct j)
apply simp_all
done
@@ -168,7 +168,7 @@
text {* PROPERTY A 9. The unary @{text 1} and @{text 2} in @{term
ack} is essential for the rewriting. *}
-lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = # 2 * j + # 3"
+lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = 2 * j + 3"
apply (induct j)
apply simp_all
done
@@ -203,7 +203,7 @@
text {* PROPERTY A 10 *}
-lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (# 2 + (i1 + i2), j)"
+lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (2 + (i1 + i2), j)"
apply (simp add: numerals)
apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
apply simp
@@ -215,7 +215,7 @@
text {* PROPERTY A 11 *}
-lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (# 4 + (i1 + i2), j)"
+lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (4 + (i1 + i2), j)"
apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans)
prefer 2
apply (rule ack_nest_bound [THEN less_le_trans])
@@ -231,7 +231,7 @@
used @{text "k + 4"}. Quantified version must be nested @{text
"\<exists>k'. \<forall>i j. ..."} *}
-lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (# 4 + k, j)"
+lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (4 + k, j)"
apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
prefer 2
apply (rule ack_add_bound [THEN less_le_trans])
--- a/src/HOL/ex/Records.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/Records.thy Sat Oct 06 00:02:46 2001 +0200
@@ -182,7 +182,7 @@
constdefs
foo10 :: nat
- "foo10 == getX (| x = # 2, y = 0, colour = Blue |)"
+ "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
subsubsection {* Non-coercive structural subtyping *}
@@ -194,7 +194,7 @@
constdefs
foo11 :: cpoint
- "foo11 == setX (| x = # 2, y = 0, colour = Blue |) 0"
+ "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
subsection {* Other features *}
@@ -207,7 +207,7 @@
text {*
\noindent May not apply @{term getX} to
- @{term [source] "(| x' = # 2, y' = 0 |)"}.
+ @{term [source] "(| x' = 2, y' = 0 |)"}.
*}
text {* \medskip Polymorphic records. *}
--- a/src/HOL/ex/svc_test.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/svc_test.ML Sat Oct 06 00:02:46 2001 +0200
@@ -231,9 +231,9 @@
(** Linear arithmetic **)
-Goal "x ~= # 14 & x ~= # 13 & x ~= # 12 & x ~= # 11 & x ~= # 10 & x ~= # 9 & \
-\ x ~= # 8 & x ~= # 7 & x ~= # 6 & x ~= # 5 & x ~= # 4 & x ~= # 3 & \
-\ x ~= # 2 & x ~= Numeral1 & Numeral0 < x & x < # 16 --> # 15 = (x::int)";
+Goal "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & \
+\ x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & \
+\ x ~= 2 & x ~= Numeral1 & Numeral0 < x & x < 16 --> 15 = (x::int)";
by (svc_tac 1);
qed "";
@@ -244,11 +244,11 @@
(** Natural number examples requiring implicit "non-negative" assumptions*)
-Goal "(# 3::nat)*a <= # 2 + # 4*b + # 6*c & # 11 <= # 2*a + b + # 2*c & \
-\ a + # 3*b <= # 5 + # 2*c --> # 2 + # 3*b <= # 2*a + # 6*c";
+Goal "(3::nat)*a <= 2 + 4*b + 6*c & 11 <= 2*a + b + 2*c & \
+\ a + 3*b <= 5 + 2*c --> 2 + 3*b <= 2*a + 6*c";
by (svc_tac 1);
qed "";
-Goal "(n::nat) < # 2 ==> (n = Numeral0) | (n = Numeral1)";
+Goal "(n::nat) < 2 ==> (n = Numeral0) | (n = Numeral1)";
by (svc_tac 1);
qed "";
--- a/src/HOLCF/FOCUS/Buffer_adm.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML Sat Oct 06 00:02:46 2001 +0200
@@ -110,7 +110,7 @@
Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
\ (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
\ (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
-by (res_inst_tac [("x","%i. # 2*i")] exI 1);
+by (res_inst_tac [("x","%i. 2*i")] exI 1);
by (rtac allI 1);
by (nat_ind_tac "i" 1);
by ( Simp_tac 1);
@@ -129,10 +129,10 @@
\\<lbrakk>f \\<in> BufEq;
\\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
x \\<sqsubseteq> s \\<longrightarrow>
- Fin (# 2 * i) < #x \\<longrightarrow>
+ Fin (2 * i) < #x \\<longrightarrow>
(x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
(s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
- Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (# 2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
+ Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
(ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
\\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
*)
@@ -147,11 +147,11 @@
by (hyp_subst_tac 1);
(*
1. \\<And>i d xa ya t ff ffa.
- \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (# 2 * i) < #ya;
+ \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (2 * i) < #ya;
(ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
\\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
x \\<sqsubseteq> s \\<longrightarrow>
- Fin (# 2 * i) < #x \\<longrightarrow>
+ Fin (2 * i) < #x \\<longrightarrow>
(x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
(s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>