theory Ex12_Template
imports "../Thys/VC" GCD
begin

section {* A nicer notation for annotated programs *}

notation Askip ("SKIP")
notation Aassign ("_ #= _" [1000, 61] 61)
notation Asemi ("_;;/ _"  [60, 61] 60)
notation Aif ("(IF' _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
notation Awhile ("(WHILE' _/ _/ DO _)"  [0, 61] 61)

section {* Homework *}
text {* A useful abbreviation: *}
abbreviation Eq where "Eq a1 a2 == And (Not (Less a1 a2)) (Not (Less a2 a1))"

definition SUB :: "acom" where
 "SUB=
IF' Less (V 0) (V 1)
THEN 2#=(N 0)
ELSE 
(
 2#= (N 0);;
 WHILE' (Not (Eq (Plus (V 1) (V 2)) (V 0))) 
  (\<lambda>s. (s 2)>= 0 & (s 2)<=(s 0) &  (s 1)<=(s 0) & (s 2)+(s 1)<=(s 0))
 DO
  (
   2#=Plus (V 2) (N 1)
  )
)"
lemma SUB_sound: "vc SUB (\<lambda>s. s 2 = s 0 - s 1) s"
unfolding SUB_def  
apply(auto simp add: SUB_def)
done 

(* a =0 a'=2
   b =1 b'=3  *)
definition EUCLID :: "acom" where
  "EUCLID =
IF' (And (Less (N 0) (V 0)) (Less (N 0) (V 1)))
THEN(
2#=(V 0);;
3#=(V 1);;
12#=(N 0);;
WHILE' (Not (Eq (V 2) (V 3))) 
 (\<lambda>s.  gcd(s 0)(s 1)=gcd(s 2)(s 3) &  0<(s 12)& 0<(s 2) &(s 3)<=(s 1)& 
                                    (s 0)>=0 &(s 0)>=0 & (s 1)>=0 &  0<=(s 2)) 


DO 
(
 IF' (Less (V 2) (V 3))
 THEN (*3=3-2*)
 (
  (* 10#=(V 3);;
   11#=(V 2);; *)
   (*gr=10;kl=11; Diff=12*)
   12#= (N 1);;
   (WHILE' (Not (Eq (Plus (V 2) (V 12)) (V 3))) 
     (\<lambda>s.  (s 3)>=gcd(s 0)(s 1) &  0<(s 12)& 0<(s 2) &(s 3)<=(s 1) &
                       gcd(s 0)(s 1)=gcd(s 2)(s 3) &(s 12) + (s 2) <= (s 3) )
   DO
   (
   12#=Plus (V 12) (N 1)
   ));;
   3#=(V 12)
 )
 ELSE (*2=2-3*)
 ( (*10#=(V 2);;
   11#=(V 3);;*) 
   (*gr=10;kl=11; Diff=12*)
   12#= (N 1);;
   (WHILE' (Not (Eq (Plus (V 3) (V 12)) (V 2))) 
      (\<lambda>s. (s 2)>=gcd(s 0)(s 1) &  0<(s 12)& 0<(s 2) &(s 3)<=(s 1)&
                      gcd(s 0)(s 1)=gcd(s 2)(s 3) & (s 12) + (s 3) <= (s 2))
   DO
   (
   12#=Plus (V 12) (N 1)
   ));;
   2#=(V 12)
 )
))
ELSE
 (2#=(N 0);;
  3#=(N 0))"

lemma EUCLID_sound: "vc EUCLID (\<lambda>s. s 2 = gcd (s 0) (s 1)) s"
unfolding EUCLID_def 
apply (auto)
by (metis One_nat_def_raw gcd_add2_nat gcd_semilattice_nat.inf_commute numeral_2_eq_2 numeral_3_eq_3)

end