<commit_before>(*  Title:      HOL/Hoare/Examples.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   1995 TUM

Various arithmetic examples.
*)

open Examples;

(*** multiplication by successive addition ***)

Goal
 "{m=0 & s=0} \
\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
\ {s = a*b}";
by (hoare_tac 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
qed "multiply_by_add";


(*** Euclid's algorithm for GCD ***)

Goal
" {0<A & 0<B & a=A & b=B}   \
\ WHILE a ~= b  \
\ DO  {0<a & 0<b & gcd A B = gcd a b} \
\      IF a<b   \
\      THEN   \
\           b:=b-a   \
\      ELSE   \
\           a:=a-b   \
\      END   \
\ END   \
\ {a = gcd A B}";

by (hoare_tac 1);
(*Now prove the verification conditions*)
by Safe_tac;
by (etac less_imp_diff_positive 1);
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";


(*** Power by interated squaring and multiplication ***)

Goal
" {a=A & b=B}   \
\ c:=1;   \
\ WHILE b~=0   \
\ DO {A^B = c * a^b}   \
\      WHILE b mod 2=0   \
\      DO  {A^B = c * a^b}  \
\           a:=a*a;   \<commit_msg>Tidied, removing uses of less_imp_diff_positive<commit_after>(*  Title:      HOL/Hoare/Examples.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   1995 TUM

Various arithmetic examples.
*)

open Examples;

(*** multiplication by successive addition ***)

Goal
 "{m=0 & s=0} \
\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
\ {s = a*b}";
by (hoare_tac 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
qed "multiply_by_add";


(*** Euclid's algorithm for GCD ***)

Goal
" {0<A & 0<B & a=A & b=B}   \
\ WHILE a ~= b  \
\ DO  {0<a & 0<b & gcd A B = gcd a b} \
\      IF a<b   \
\      THEN   \
\           b:=b-a   \
\      ELSE   \
\           a:=a-b   \
\      END   \
\ END   \
\ {a = gcd A B}";

by (hoare_tac 1);
(*Now prove the verification conditions*)
by Auto_tac;
by (etac gcd_nnn 4);
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
by (force_tac (claset(),
	       simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
qed "Euclid_GCD";


(*** Power by interated squaring and multiplication ***)

Goal
" {a=A & b=B}   \
\ c:=1;   \
\ WHILE b~=0   \
\ DO {A^B = c * a^b}   \
\      WHILE b mod 2=0   \
\      DO  {A^B = c * a^b}  \
\           a:=a*a;   \
{'fraction_non_alphanumeric': 0.17571644042232276, 'fraction_numerical': 0.01583710407239819, 'mean_word_length': 2.358227848101266, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2852133', 'n_tokens_mistral': 1269, 'n_tokens_neox': 1204, 'n_words': 297}