--- a/src/HOL/Hoare/Arith2.ML Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/Hoare/Arith2.ML Tue Jan 30 15:24:36 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Hoare/Arith2.ML
+(* Title: HOL/Hoare/Arith2.ML
ID: $Id$
- Author: Norbert Galm
+ Author: Norbert Galm
Copyright 1995 TUM
More arithmetic lemmas.
@@ -30,16 +30,16 @@
\ !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z) \
\ |] ==> P m n k";
by (res_inst_tac [("x","m")] spec 1);
-br diff_induct 1;
-br allI 1;
-br allI 2;
+by (rtac diff_induct 1);
+by (rtac allI 1);
+by (rtac allI 2);
by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1);
by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4);
-br allI 7;
+by (rtac allI 7);
by (nat_ind_tac "xa" 7);
by (ALLGOALS (resolve_tac prems));
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
by (fast_tac HOL_cs 1);
by (fast_tac HOL_cs 1);
qed "diff_induct3";
@@ -48,33 +48,33 @@
val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
by (cut_facts_tac prems 1);
-br mp 1;
-ba 2;
+by (rtac mp 1);
+by (assume_tac 2);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "diff_not_assoc";
val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)";
by (cut_facts_tac prems 1);
-bd conjI 1;
-ba 1;
+by (dtac conjI 1);
+by (assume_tac 1);
by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
-ba 2;
+by (assume_tac 2);
by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
by (ALLGOALS Asm_simp_tac);
-br impI 1;
+by (rtac impI 1);
by (dres_inst_tac [("P","~x<y")] conjE 1);
-ba 2;
-br (Suc_diff_n RS sym) 1;
-br le_less_trans 1;
-be (not_less_eq RS subst) 2;
-br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
+by (assume_tac 2);
+by (rtac (Suc_diff_n RS sym) 1);
+by (rtac le_less_trans 1);
+by (etac (not_less_eq RS subst) 2);
+by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1);
qed "diff_add_not_assoc";
val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
by (cut_facts_tac prems 1);
-br mp 1;
-ba 2;
+by (rtac mp 1);
+by (assume_tac 2);
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "add_diff_assoc";
@@ -82,12 +82,12 @@
(*** more ***)
val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
-br iffI 1;
+by (rtac iffI 1);
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
by (Asm_full_simp_tac 1);
-be disjE 1;
-be (less_not_refl2 RS not_sym) 1;
-be less_not_refl2 1;
+by (etac disjE 1);
+by (etac (less_not_refl2 RS not_sym) 1);
+by (etac less_not_refl2 1);
qed "not_eq_eq_less_or_gr";
val [prem] = goal Arith.thy "m<n ==> n-m~=0";
@@ -115,7 +115,7 @@
by (res_inst_tac [("n","k")] natE 1);
by (ALLGOALS Asm_full_simp_tac);
by (nat_ind_tac "x" 1);
-be add_less_mono 2;
+by (etac add_less_mono 2);
by (ALLGOALS Asm_full_simp_tac);
qed "mult_less_mono_r";
@@ -124,8 +124,8 @@
by (nat_ind_tac "k" 1);
by (ALLGOALS Simp_tac);
by (fold_goals_tac [le_def]);
-be add_le_mono 1;
-ba 1;
+by (etac add_le_mono 1);
+by (assume_tac 1);
qed "mult_not_less_mono_r";
val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k";
@@ -137,10 +137,10 @@
val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k";
by (cut_facts_tac prems 1);
by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
-br (less_not_refl2 RS not_sym) 2;
-be mult_less_mono_r 2;
-br less_not_refl2 3;
-be mult_less_mono_r 3;
+by (rtac (less_not_refl2 RS not_sym) 2);
+by (etac mult_less_mono_r 2);
+by (rtac less_not_refl2 3);
+by (etac mult_less_mono_r 3);
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
qed "mult_not_eq_mono_r";
@@ -149,18 +149,18 @@
val prems = goal Arith.thy "(m - n)*k = (m*k) - ((n*k)::nat)";
by (res_inst_tac [("P","m*k<n*k")] case_split_thm 1);
by (forward_tac [mult_not_less_mono_r COMP not_imp_swap] 1);
-bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
-bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
-br mp 2;
-ba 3;
+by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
+by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
+by (rtac mp 2);
+by (assume_tac 3);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 2);
by (ALLGOALS Asm_simp_tac);
-br impI 1;
-bd (refl RS iffD1) 1;
+by (rtac impI 1);
+by (dtac (refl RS iffD1) 1);
by (dres_inst_tac [("k","k")] add_not_less_mono_l 1);
-bd (refl RS iffD1) 1;
-bd (refl RS iffD1) 1;
-bd diff_not_assoc 1;
+by (dtac (refl RS iffD1) 1);
+by (dtac (refl RS iffD1) 1);
+by (dtac diff_not_assoc 1);
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_add_inverse]) 1);
qed "diff_mult_distrib_r";
@@ -178,29 +178,29 @@
val prems=goal thy "0<n ==> n mod n = 0";
by (cut_facts_tac prems 1);
-br (mod_def RS wf_less_trans) 1;
+by (rtac (mod_def RS wf_less_trans) 1);
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1);
-be mod_less 1;
+by (etac mod_less 1);
qed "mod_nn_is_0";
val prems=goal thy "0<n ==> m mod n = (m+n) mod n";
by (cut_facts_tac prems 1);
by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1);
-br add_commute 1;
+by (rtac add_commute 1);
by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
-br diff_add_inverse 1;
-br sym 1;
-be mod_geq 1;
+by (rtac diff_add_inverse 1);
+by (rtac sym 1);
+by (etac mod_geq 1);
by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1);
by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
-br le_add1 1;
+by (rtac le_add1 1);
qed "mod_eq_add";
val prems=goal thy "0<n ==> m*n mod n = 0";
by (cut_facts_tac prems 1);
by (nat_ind_tac "m" 1);
by (Simp_tac 1);
-be mod_less 1;
+by (etac mod_less 1);
by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
qed "mod_prod_nn_is_0";
@@ -208,25 +208,25 @@
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
by (cut_facts_tac prems 1);
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
-be mod_div_equality 1;
+by (etac mod_div_equality 1);
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
-be mod_div_equality 1;
+by (etac mod_div_equality 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
-br add_mult_distrib 1;
-be mod_prod_nn_is_0 1;
+by (rtac add_mult_distrib 1);
+by (etac mod_prod_nn_is_0 1);
qed "mod0_sum";
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
by (cut_facts_tac prems 1);
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
-be mod_div_equality 1;
+by (etac mod_div_equality 1);
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
-be mod_div_equality 1;
+by (etac mod_div_equality 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
-br diff_mult_distrib_r 1;
-be mod_prod_nn_is_0 1;
+by (rtac diff_mult_distrib_r 1);
+by (etac mod_prod_nn_is_0 1);
qed "mod0_diff";
@@ -234,11 +234,11 @@
val prems = goal thy "0<n ==> m*n div n = m";
by (cut_facts_tac prems 1);
-br (mult_not_eq_mono_r RS not_imp_swap) 1;
-ba 1;
-ba 1;
+by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1);
+by (assume_tac 1);
+by (assume_tac 1);
by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1);
-ba 1;
+by (assume_tac 1);
by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1);
by (Asm_simp_tac 1);
qed "div_prod_nn_is_m";
@@ -254,32 +254,32 @@
val prems=goalw thy [divides_def] "x divides n ==> x<=n";
by (cut_facts_tac prems 1);
-br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
+by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1);
by (Asm_simp_tac 1);
-br (less_not_refl2 RS not_sym) 1;
+by (rtac (less_not_refl2 RS not_sym) 1);
by (Asm_simp_tac 1);
qed "divides_le";
val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
by (cut_facts_tac prems 1);
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
-br conjI 1;
+by (rtac conjI 1);
by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
-ba 1;
-be conjI 1;
-br mod0_sum 1;
+by (assume_tac 1);
+by (etac conjI 1);
+by (rtac mod0_sum 1);
by (ALLGOALS atac);
qed "divides_sum";
val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
by (cut_facts_tac prems 1);
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
-br conjI 1;
-be less_imp_diff_positive 1;
-be conjI 1;
-br mod0_diff 1;
+by (rtac conjI 1);
+by (etac less_imp_diff_positive 1);
+by (etac conjI 1);
+by (rtac mod0_diff 1);
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def])));
-be less_not_sym 1;
+by (etac less_not_sym 1);
qed "divides_diff";
@@ -288,16 +288,16 @@
val prems=goalw thy [cd_def] "0<n ==> cd n n n";
by (cut_facts_tac prems 1);
-bd divides_nn 1;
+by (dtac divides_nn 1);
by (Asm_simp_tac 1);
qed "cd_nnn";
val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
by (cut_facts_tac prems 1);
-bd conjE 1;
-ba 2;
-bd divides_le 1;
-bd divides_le 1;
+by (dtac conjE 1);
+by (assume_tac 2);
+by (dtac divides_le 1);
+by (dtac divides_le 1);
by (Asm_simp_tac 1);
qed "cd_le";
@@ -307,32 +307,32 @@
val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
by (cut_facts_tac prems 1);
-br iffI 1;
-bd conjE 1;
-ba 2;
-br conjI 1;
-br divides_diff 1;
-bd conjE 5;
-ba 6;
-br conjI 5;
-bd less_not_sym 5;
-bd add_diff_inverse 5;
+by (rtac iffI 1);
+by (dtac conjE 1);
+by (assume_tac 2);
+by (rtac conjI 1);
+by (rtac divides_diff 1);
+by (dtac conjE 5);
+by (assume_tac 6);
+by (rtac conjI 5);
+by (dtac less_not_sym 5);
+by (dtac add_diff_inverse 5);
by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
by (ALLGOALS Asm_full_simp_tac);
qed "cd_diff_l";
val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
by (cut_facts_tac prems 1);
-br iffI 1;
-bd conjE 1;
-ba 2;
-br conjI 1;
-br divides_diff 2;
-bd conjE 5;
-ba 6;
-br conjI 5;
-bd less_not_sym 6;
-bd add_diff_inverse 6;
+by (rtac iffI 1);
+by (dtac conjE 1);
+by (assume_tac 2);
+by (rtac conjI 1);
+by (rtac divides_diff 2);
+by (dtac conjE 5);
+by (assume_tac 6);
+by (rtac conjI 5);
+by (dtac less_not_sym 6);
+by (dtac add_diff_inverse 6);
by (dres_inst_tac [("n","n-m")] divides_sum 6);
by (ALLGOALS Asm_full_simp_tac);
qed "cd_diff_r";
@@ -342,15 +342,15 @@
val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
by (cut_facts_tac prems 1);
-bd cd_nnn 1;
-br (select_equality RS sym) 1;
-be conjI 1;
-br allI 1;
-br impI 1;
-bd cd_le 1;
-bd conjE 2;
-ba 3;
-br le_anti_sym 2;
+by (dtac cd_nnn 1);
+by (rtac (select_equality RS sym) 1);
+by (etac conjI 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (dtac cd_le 1);
+by (dtac conjE 2);
+by (assume_tac 3);
+by (rtac le_anti_sym 2);
by (dres_inst_tac [("x","x")] cd_le 2);
by (dres_inst_tac [("x","n")] spec 3);
by (ALLGOALS Asm_full_simp_tac);
@@ -364,16 +364,16 @@
by (cut_facts_tac prems 1);
by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
by (Asm_simp_tac 1);
-br allI 1;
-be cd_diff_l 1;
+by (rtac allI 1);
+by (etac cd_diff_l 1);
qed "gcd_diff_l";
val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
by (cut_facts_tac prems 1);
by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
by (Asm_simp_tac 1);
-br allI 1;
-be cd_diff_r 1;
+by (rtac allI 1);
+by (etac cd_diff_r 1);
qed "gcd_diff_r";
@@ -392,7 +392,7 @@
by (nat_ind_tac "k" 1);
by (ALLGOALS Asm_simp_tac);
by (fold_goals_tac [pow_def]);
-br (pow_add_reduce RS sym) 1;
+by (rtac (pow_add_reduce RS sym) 1);
qed "pow_pow_reduce";
(*** fac ***)