# HG changeset patch
# User paulson
# Date 864998481 -7200
# Node ID 6e472c8f001130599845f80ce27551bbf7d7f0f9
# Parent  80f0d0b2f4044c499a6ef81886cc4a37f00770ef
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs

diff -r 80f0d0b2f404 -r 6e472c8f0011 src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Fri May 30 15:20:41 1997 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Fri May 30 15:21:21 1997 +0200
@@ -18,254 +18,59 @@
 val not_imp_swap=result();
 
 
-(*** analogue of diff_induct, for simultaneous induction over 3 vars ***)
-
-val prems = goal Nat.thy
-    "[| !!x. P x 0 0;  \
-\       !!y. P 0 (Suc y) 0;  \
-\       !!z. P 0 0 (Suc z);  \
-\       !!x y. [| P x y 0 |] ==> P (Suc x) (Suc y) 0;  \
-\       !!x z. [| P x 0 z |] ==> P (Suc x) 0 (Suc z);  \
-\       !!y z. [| P 0 y z |] ==> P 0 (Suc y) (Suc z);  \
-\       !!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);
-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);
-by (rtac allI 7);
-by (nat_ind_tac "xa" 7);
-by (ALLGOALS (resolve_tac prems));
-by (assume_tac 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
-qed "diff_induct3";
-
-(*** interaction of + and - ***)
-
-val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
-by (cut_facts_tac prems 1);
-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);
-by (dtac conjI 1);
-by (assume_tac 1);
-by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
-by (assume_tac 2);
-by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
-by (ALLGOALS Asm_simp_tac);
-by (rtac impI 1);
-by (dres_inst_tac [("P","~x<y")] conjE 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 Suc_leI] 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);
-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";
-
-(*** more ***)
-
-val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
-by (rtac iffI 1);
-by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
-by (Asm_full_simp_tac 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";
-by (rtac (prem RS rev_mp) 1);
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "less_imp_diff_not_0";
-
-(*******************************************************************)
-
-val prems = goal Arith.thy "(i::nat)<j ==> k+i<k+j";
-by (cut_facts_tac prems 1);
-by (nat_ind_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_less_mono_l";
-
-val prems = goal Arith.thy "~(i::nat)<j ==> ~k+i<k+j";
-by (cut_facts_tac prems 1);
-by (nat_ind_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_not_less_mono_l";
-
-(******************************************************************)
-
-(*** mod ***)
-
-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);
-by (etac mod_div_equality 1);
-by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 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);
-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);
-by (etac mod_div_equality 1);
-by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 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);
-by (rtac diff_mult_distrib 1);
-by (etac mod_prod_nn_is_0 1);
-qed "mod0_diff";
-
-
-(*** divides ***)
-
-val prems=goalw thy [divides_def] "0<n ==> n divides n";
-by (cut_facts_tac prems 1);
-by (forward_tac [mod_nn_is_0] 1);
-by (Asm_simp_tac 1);
-qed "divides_nn";
-
-val prems=goalw thy [divides_def] "x divides n ==> x<=n";
-by (cut_facts_tac prems 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);
-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)));
-by (rtac conjI 1);
-by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 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)));
-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 addsimps [le_def])));
-by (etac less_not_sym 1);
-qed "divides_diff";
-
 
 (*** cd ***)
 
 
 val prems=goalw thy [cd_def] "0<n ==> cd n n n";
 by (cut_facts_tac prems 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";
+val prems=goalw thy [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n";
 by (cut_facts_tac prems 1);
-by (dtac conjE 1);
-by (assume_tac 2);
-by (dtac divides_le 1);
-by (dtac divides_le 1);
-by (Asm_simp_tac 1);
+by (blast_tac (!claset addIs [dvd_imp_le]) 1);
 qed "cd_le";
 
 val prems=goalw thy [cd_def] "cd x m n = cd x n m";
 by (Fast_tac 1);
 qed "cd_swap";
 
-val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
+val prems=goalw thy [cd_def] "n<=m ==> cd x m n = cd x (m-n) n";
 by (cut_facts_tac prems 1);
-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);
+by (blast_tac (!claset addIs [dvd_diff] addDs [dvd_diffD]) 1);
 qed "cd_diff_l";
 
-val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
+val prems=goalw thy [cd_def] "m<=n ==> cd x m n = cd x m (n-m)";
 by (cut_facts_tac prems 1);
-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);
+by (blast_tac (!claset addIs [dvd_diff] addDs [dvd_diffD]) 1);
 qed "cd_diff_r";
 
 
 (*** gcd ***)
 
-val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
-by (cut_facts_tac prems 1);
-by (dtac cd_nnn 1);
+goalw thy [gcd_def] "!!n. 0<n ==> n = gcd n n";
+by (forward_tac [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);
+by (blast_tac (!claset addDs [cd_le]) 1);
+by (blast_tac (!claset addIs [le_anti_sym] addDs [cd_le]) 1);
 qed "gcd_nnn";
 
 val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
 by (simp_tac (!simpset addsimps [cd_swap]) 1);
 qed "gcd_swap";
 
-val prems=goalw thy [gcd_def] "n<m ==> gcd m n = gcd (m-n) n";
+val prems=goalw thy [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n";
 by (cut_facts_tac prems 1);
-by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
+by (subgoal_tac "n<=m ==> !x.cd x m n = cd x (m-n) n" 1);
 by (Asm_simp_tac 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)";
+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 (subgoal_tac "m<=n ==> !x.cd x m n = cd x m (n-m)" 1);
 by (Asm_simp_tac 1);
 by (rtac allI 1);
 by (etac cd_diff_r 1);
diff -r 80f0d0b2f404 -r 6e472c8f0011 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Fri May 30 15:20:41 1997 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Fri May 30 15:21:21 1997 +0200
@@ -3,17 +3,14 @@
     Author:     Norbert Galm
     Copyright   1995 TUM
 
-More arithmetic.
+More arithmetic.  Much of this duplicates ex/Primes.
 *)
 
-Arith2 = Arith +
+Arith2 = Divides +
 
 constdefs
-  divides :: [nat, nat] => bool                             (infixl 70)
-  "x divides n == 0<n & 0<x & (n mod x) = 0"
-
   cd      :: [nat, nat, nat] => bool
-  "cd x m n  == x divides m & x divides n"
+  "cd x m n  == x dvd m & x dvd n"
 
   gcd     :: [nat, nat] => nat
   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
diff -r 80f0d0b2f404 -r 6e472c8f0011 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Fri May 30 15:20:41 1997 +0200
+++ b/src/HOL/Hoare/Examples.ML	Fri May 30 15:21:21 1997 +0200
@@ -35,21 +35,14 @@
 \ {a = gcd A B}";
 
 by (hoare_tac 1);
-
+(*Now prove the verification conditions*)
 by (safe_tac (!claset));
-
 by (etac less_imp_diff_positive 1);
-by (etac gcd_diff_r 1);
-
-by (cut_facts_tac [less_linear] 1);
-by (cut_facts_tac [less_linear] 2);
-by (rtac less_imp_diff_positive 1);
-by (rtac gcd_diff_l 2);
-
-by (dtac gcd_nnn 3);
-
-by (ALLGOALS (Fast_tac));
-
+by (asm_simp_tac (!simpset addsimps [less_imp_le, gcd_diff_r]) 1);
+by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, gcd_diff_l]) 2);
+by (etac gcd_nnn 2);
+by (full_simp_tac (!simpset addsimps [not_less_iff_le, le_eq_less_or_eq]) 1);
+by (blast_tac (!claset addIs [less_imp_diff_positive]) 1);
 qed "Euclid_GCD";