equal
deleted
inserted
replaced
34 \ END \ |
34 \ END \ |
35 \ {a = gcd A B}"; |
35 \ {a = gcd A B}"; |
36 |
36 |
37 by (hoare_tac 1); |
37 by (hoare_tac 1); |
38 (*Now prove the verification conditions*) |
38 (*Now prove the verification conditions*) |
39 by Safe_tac; |
39 by Auto_tac; |
40 by (etac less_imp_diff_positive 1); |
40 by (etac gcd_nnn 4); |
|
41 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3); |
|
42 by (force_tac (claset(), |
|
43 simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2); |
41 by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1); |
44 by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1); |
42 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2); |
|
43 by (etac gcd_nnn 2); |
|
44 by (full_simp_tac (simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 1); |
|
45 by (blast_tac (claset() addIs [less_imp_diff_positive]) 1); |
|
46 qed "Euclid_GCD"; |
45 qed "Euclid_GCD"; |
47 |
46 |
48 |
47 |
49 (*** Power by interated squaring and multiplication ***) |
48 (*** Power by interated squaring and multiplication ***) |
50 |
49 |