--- a/src/HOL/GroupTheory/Exponent.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.ML Tue Aug 07 16:36:52 2001 +0200
@@ -8,11 +8,11 @@
val prime_def = thm "prime_def";
-Goalw [prime_def] "p\\<in>prime ==> 1 < p";
-by (Blast_tac 1);
+Goalw [prime_def] "p\\<in>prime ==> 1' < p";
+by (force_tac (claset(), simpset() addsimps []) 1);
qed "prime_imp_one_less";
-Goal "(p\\<in>prime) = (1<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
+Goal "(p\\<in>prime) = (1'<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
by (auto_tac (claset(), simpset() addsimps [prime_imp_one_less]));
by (blast_tac (claset() addSDs [thm "prime_dvd_mult"]) 1);
by (auto_tac (claset(), simpset() addsimps [prime_def]));
@@ -23,6 +23,7 @@
by (dres_inst_tac [("x","k")] spec 1);
by (asm_full_simp_tac
(simpset() addsimps [dvd_mult_cancel1, dvd_mult_cancel2]) 1);
+by Auto_tac;
qed "prime_iff";
Goal "p\\<in>prime ==> 0 < p^a";
@@ -106,9 +107,7 @@
by (res_inst_tac [("P","%x. x <= b * c")] subst 1);
by (rtac mult_1_right 1);
by (rtac mult_le_mono 1);
-by (assume_tac 1);
-by (stac Suc_le_eq 1);
-by (assume_tac 1);
+by Auto_tac;
qed "le_extend_mult";
@@ -194,15 +193,15 @@
qed_spec_mp "prime_power_dvd_cases";
(*needed in this form in Sylow.ML*)
-Goal "[| p\\<in>prime; ~(p ^ (r+1) dvd n); p ^ (a+r) dvd n * k |] \
+Goal "[| p \\<in> prime; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] \
\ ==> p ^ a dvd k";
-by (dres_inst_tac [("a","r+1"), ("b","a")] prime_power_dvd_cases 1);
+by (dres_inst_tac [("a","Suc r"), ("b","a")] prime_power_dvd_cases 1);
by (assume_tac 1);
by Auto_tac;
qed "div_combine";
(*Lemma for power_dvd_bound*)
-Goal "1 < p ==> Suc n <= p^n";
+Goal "1' < p ==> Suc n <= p^n";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
by (Asm_full_simp_tac 1);
@@ -219,7 +218,7 @@
qed "Suc_le_power";
(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
-Goal "[|p^n dvd a; 1 < p; 0 < a|] ==> n < a";
+Goal "[|p^n dvd a; 1' < p; 0 < a|] ==> n < a";
by (dtac dvd_imp_le 1);
by (dres_inst_tac [("n","n")] Suc_le_power 2);
by Auto_tac;
@@ -254,7 +253,7 @@
by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
by (rtac Greatest_equality 1);
by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addIs [prime_imp_one_less, power_dvd_imp_le]) 1);
+by (asm_simp_tac (simpset() addsimps [prime_imp_one_less, power_dvd_imp_le]) 1);
qed "exponent_power_eq";
Addsimps [exponent_power_eq];
@@ -268,7 +267,7 @@
Addsimps [exponent_eq_0];
-(* exponent_mult_add, easy inclusion. Could weaken p\\<in>prime to 1<p *)
+(* exponent_mult_add, easy inclusion. Could weaken p\\<in>prime to 1'<p *)
Goal "[| 0 < a; 0 < b |] \
\ ==> (exponent p a) + (exponent p b) <= exponent p (a * b)";
by (case_tac "p \\<in> prime" 1);
@@ -313,7 +312,7 @@
by (auto_tac (claset() addDs [dvd_mult_left], simpset()));
qed "not_divides_exponent_0";
-Goal "exponent p 1 = 0";
+Goal "exponent p 1' = 0";
by (case_tac "p \\<in> prime" 1);
by (auto_tac (claset(),
simpset() addsimps [prime_iff, not_divides_exponent_0]));
@@ -358,7 +357,7 @@
Goal "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a";
-by (res_inst_tac [("m","1")] p_fac_forw_lemma 1);
+by (res_inst_tac [("m","1'")] p_fac_forw_lemma 1);
by Auto_tac;
qed "r_le_a_forw";
@@ -423,7 +422,7 @@
qed "p_not_div_choose";
-Goal "0 < m ==> exponent p ((p^a * m - 1) choose (p^a - 1)) = 0";
+Goal "0 < m ==> exponent p ((p^a * m - 1') choose (p^a - 1')) = 0";
by (case_tac "p \\<in> prime" 1);
by (Asm_simp_tac 2);
by (forw_inst_tac [("a","a")] zero_less_prime_power 1);
--- a/src/HOL/GroupTheory/Sylow.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.ML Tue Aug 07 16:36:52 2001 +0200
@@ -127,7 +127,7 @@
le_extend_mult, zero_less_m]) 1);
qed "zero_less_card_calM";
-Goal "~(p ^ (exponent p m+ 1) dvd card(calM))";
+Goal "~ (p ^ Suc(exponent p m) dvd card(calM))";
by (subgoal_tac "exponent p m = exponent p (card calM)" 1);
by (asm_full_simp_tac (simpset() addsimps [card_calM,
zero_less_m RS const_p_fac]) 2);
@@ -140,7 +140,7 @@
by Auto_tac;
qed "finite_calM";
-Goal "\\<exists>M \\<in> calM // RelM. ~(p ^ ((exponent p m)+ 1) dvd card(M))";
+Goal "\\<exists>M \\<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))";
by (rtac (max_p_div_calM RS contrapos_np) 1);
by (asm_full_simp_tac (simpset() addsimps [finite_calM,
RelM_equiv RSN(2, equiv_imp_dvd_card)]) 1);
--- a/src/HOL/GroupTheory/Sylow.thy Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.thy Tue Aug 07 16:36:52 2001 +0200
@@ -36,7 +36,7 @@
M1 :: "'a set"
assumes
M_in_quot "M \\<in> calM // RelM"
- not_dvd_M "~(p ^ (exponent p m + 1) dvd card(M))"
+ not_dvd_M "~(p ^ Suc(exponent p m) dvd card(M))"
M1_in_M "M1 \\<in> M"
defines
H_def "H == {g. g\\<in>carrier G & M1 #> g = M1}"
--- a/src/HOL/Hyperreal/HyperNat.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/HyperNat.ML Tue Aug 07 16:36:52 2001 +0200
@@ -682,7 +682,7 @@
Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def]
"(0::hypnat) < 1hn";
by (res_inst_tac [("x","%n. 0")] exI 1);
-by (res_inst_tac [("x","%n. 1")] exI 1);
+by (res_inst_tac [("x","%n. 1'")] exI 1);
by Auto_tac;
qed "hypnat_zero_less_one";
@@ -806,11 +806,11 @@
by Auto_tac;
qed "hypnat_of_nat_le_iff";
-Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat 1 = 1hn";
+Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat 1' = 1hn";
by (Simp_tac 1);
qed "hypnat_of_nat_one";
-Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat 0 = 0";
+Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat 0 = 0";
by (Simp_tac 1);
qed "hypnat_of_nat_zero";
@@ -903,7 +903,7 @@
qed "SHNat_hypnat_of_nat";
Addsimps [SHNat_hypnat_of_nat];
-Goal "hypnat_of_nat 1 : Nats";
+Goal "hypnat_of_nat 1' : Nats";
by (Simp_tac 1);
qed "SHNat_hypnat_of_nat_one";
--- a/src/HOL/Hyperreal/HyperPow.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/HyperPow.ML Tue Aug 07 16:36:52 2001 +0200
@@ -33,7 +33,7 @@
by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
qed "hrealpow_add";
-Goal "(r::hypreal) ^ 1 = r";
+Goal "(r::hypreal) ^ 1' = r";
by (Simp_tac 1);
qed "hrealpow_one";
Addsimps [hrealpow_one];
--- a/src/HOL/Hyperreal/Lim.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML Tue Aug 07 16:36:52 2001 +0200
@@ -1294,7 +1294,7 @@
qed "NSDERIV_cmult_Id";
Addsimps [NSDERIV_cmult_Id];
-Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
+Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
by (induct_tac "n" 1);
by (dtac (DERIV_Id RS DERIV_mult) 2);
by (auto_tac (claset(),
@@ -1306,7 +1306,7 @@
qed "DERIV_pow";
(* NS version *)
-Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
+Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
qed "NSDERIV_pow";
--- a/src/HOL/Hyperreal/Series.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/Series.ML Tue Aug 07 16:36:52 2001 +0200
@@ -191,28 +191,17 @@
by (Auto_tac);
qed "sumr_zero";
-Goal "Suc N <= n --> N <= n - 1";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed_spec_mp "Suc_le_imp_diff_ge";
-
Goal "ALL n. N <= n --> f (Suc n) = #0 \
\ ==> ALL m n. Suc N <= m --> sumr m n f = #0";
by (rtac sumr_zero 1 THEN Step_tac 1);
-by (subgoal_tac "0 < n" 1);
-by (dtac Suc_le_imp_diff_ge 1);
-by (Auto_tac);
+by (case_tac "n" 1);
+by Auto_tac;
qed "Suc_le_imp_diff_ge2";
-(* proved elsewhere? *)
-Goal "(0 < n) = (EX m. n = Suc m)";
+Goal "sumr 1' n (%n. f(n) * #0 ^ n) = #0";
by (induct_tac "n" 1);
-by (Auto_tac);
-qed "gt_zero_eq_Ex";
-
-Goal "sumr 1 n (%n. f(n) * #0 ^ n) = #0";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [gt_zero_eq_Ex]));
+by (case_tac "n" 2);
+by Auto_tac;
qed "sumr_one_lb_realpow_zero";
Addsimps [sumr_one_lb_realpow_zero];
@@ -220,7 +209,7 @@
by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1);
qed "sumr_diff";
-Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumr m n f = sumr m n g";
+Goal "(ALL p. m <= p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g";
by (induct_tac "n" 1);
by (Auto_tac);
qed_spec_mp "sumr_subst";
@@ -564,7 +553,8 @@
by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
-by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
+by (res_inst_tac [("x","Suc N")] exI 1);
+by (Clarify_tac 1);
by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
qed "ratio_test_lemma2";
--- a/src/HOL/Integ/NatBin.thy Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Integ/NatBin.thy Tue Aug 07 16:36:52 2001 +0200
@@ -18,10 +18,6 @@
"number_of v == nat (number_of v)"
(*::bin=>nat ::bin=>int*)
-axioms
-neg_number_of_bin_pred_iff_0:
- "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
-
use "nat_bin.ML" setup nat_bin_arith_setup
end
--- a/src/HOL/Integ/NatSimprocs.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML Tue Aug 07 16:36:52 2001 +0200
@@ -14,15 +14,12 @@
(*Now just instantiating n to (number_of v) does the right simplification,
but with some redundant inequality tests.*)
-(*
Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
-by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
-by (Asm_simp_tac 1);
+by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1')" 1);
+by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1);
by (stac less_number_of_Suc 1);
by (Simp_tac 1);
qed "neg_number_of_bin_pred_iff_0";
-*)
-val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0";
Goal "neg (number_of (bin_minus v)) ==> \
\ Suc m - (number_of v) = m - (number_of (bin_pred v))";
--- a/src/HOL/NatArith.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NatArith.ML Tue Aug 07 16:36:52 2001 +0200
@@ -96,17 +96,17 @@
(** Lemmas for ex/Factorization **)
-Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
+Goal "!!m::nat. [| 1' < n; 1' < m |] ==> 1' < m*n";
by (case_tac "m" 1);
by Auto_tac;
qed "one_less_mult";
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
+Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<m*n";
by (case_tac "m" 1);
by Auto_tac;
qed "n_less_m_mult_n";
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
+Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<n*m";
by (case_tac "m" 1);
by Auto_tac;
qed "n_less_n_mult_m";
--- a/src/HOL/NumberTheory/Chinese.thy Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Tue Aug 07 16:36:52 2001 +0200
@@ -56,9 +56,9 @@
mhf_def:
"mhf mf n i ==
- if i = 0 then funprod mf 1 (n - 1)
- else if i = n then funprod mf 0 (n - 1)
- else funprod mf 0 (i - 1) * funprod mf (i + 1) (n - 1 - i)"
+ if i = 0 then funprod mf 1' (n - 1')
+ else if i = n then funprod mf 0 (n - 1')
+ else funprod mf 0 (i - 1') * funprod mf (Suc i) (n - 1' - i)"
xilin_sol_def:
"xilin_sol i n kf bf mf ==
--- a/src/HOL/NumberTheory/Factorization.thy Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy Tue Aug 07 16:36:52 2001 +0200
@@ -26,7 +26,7 @@
"nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
primrec
- "prod [] = 1"
+ "prod [] = 1'"
"prod (x # xs) = x * prod xs"
primrec
@@ -40,12 +40,12 @@
subsection {* Arithmetic *}
-lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1 ==> 1 < m"
+lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1' ==> 1' < m"
apply (case_tac m)
apply auto
done
-lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1 < m * k ==> 1 < k"
+lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1' < m * k ==> 1' < k"
apply (case_tac k)
apply auto
done
@@ -54,13 +54,13 @@
apply auto
done
-lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1"
+lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1'"
apply (case_tac n)
apply auto
done
lemma prod_mn_less_k:
- "(0::nat) < n ==> 0 < k ==> 1 < m ==> m * n = k ==> n < k"
+ "(0::nat) < n ==> 0 < k ==> 1' < m ==> m * n = k ==> n < k"
apply (induct m)
apply auto
done
@@ -88,7 +88,7 @@
apply auto
done
-lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1"
+lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1'"
apply (unfold prime_def dvd_def)
apply auto
done
@@ -115,13 +115,13 @@
apply auto
done
-lemma primel_one_empty: "primel xs ==> prod xs = 1 ==> xs = []"
+lemma primel_one_empty: "primel xs ==> prod xs = 1' ==> xs = []"
apply (unfold primel_def prime_def)
apply (case_tac xs)
apply simp_all
done
-lemma prime_g_one: "p \<in> prime ==> 1 < p"
+lemma prime_g_one: "p \<in> prime ==> 1' < p"
apply (unfold prime_def)
apply auto
done
@@ -132,7 +132,7 @@
done
lemma primel_nempty_g_one [rule_format]:
- "primel xs --> xs \<noteq> [] --> 1 < prod xs"
+ "primel xs --> xs \<noteq> [] --> 1' < prod xs"
apply (unfold primel_def prime_def)
apply (induct xs)
apply (auto elim: one_less_mult)
@@ -223,8 +223,8 @@
done
lemma not_prime_ex_mk:
- "1 < n \<and> n \<notin> prime ==>
- \<exists>m k. 1 < m \<and> 1 < k \<and> m < n \<and> k < n \<and> n = m * k"
+ "1' < n \<and> n \<notin> prime ==>
+ \<exists>m k. 1' < m \<and> 1' < k \<and> m < n \<and> k < n \<and> n = m * k"
apply (unfold prime_def dvd_def)
apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
done
@@ -237,7 +237,7 @@
apply (simp add: primel_append)
done
-lemma factor_exists [rule_format]: "1 < n --> (\<exists>l. primel l \<and> prod l = n)"
+lemma factor_exists [rule_format]: "1' < n --> (\<exists>l. primel l \<and> prod l = n)"
apply (induct n rule: nat_less_induct)
apply (rule impI)
apply (case_tac "n \<in> prime")
@@ -247,7 +247,7 @@
apply (auto intro!: split_primel)
done
-lemma nondec_factor_exists: "1 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
+lemma nondec_factor_exists: "1' < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
apply (erule factor_exists [THEN exE])
apply (blast intro!: ex_nondec_lemma)
done
@@ -349,7 +349,7 @@
done
lemma unique_prime_factorization [rule_format]:
- "\<forall>n. 1 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
+ "\<forall>n. 1' < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
apply safe
apply (erule nondec_factor_exists)
apply (rule perm_nondec_unique)
--- a/src/HOL/NumberTheory/Fib.thy Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Tue Aug 07 16:36:52 2001 +0200
@@ -18,8 +18,8 @@
consts fib :: "nat => nat"
recdef fib less_than
- zero: "fib 0 = 0"
- one: "fib 1 = 1"
+ zero: "fib 0 = 0"
+ one: "fib 1' = 1'"
Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)"
text {*
@@ -81,7 +81,7 @@
text {* \medskip Towards Law 6.111 of Concrete Mathematics *}
-lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1"
+lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1'"
apply (induct n rule: fib.induct)
prefer 3
apply (simp add: gcd_commute fib_Suc3)