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. (s 3)>=gcd (s 0)(s 1)& gcd(s 0)(s 1)=gcd(s 2)(s 3)  & (s 3)<=(s 1)
  & (s 0)>= gcd (s 0)(s 1) & (s 0)>0 & (s 1)>0 & gcd(s 0)(s 1)=(s 2) & 0<(s 2)) 
               (*Wirkung von gcd ((s 0) (s 1) = (s 2)) überprüfen *)
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. 0<(s 12)& 0<(s 2) & gcd(s 0)(s 1)=gcd(s 2)(s 3) & (s 3)<=(s 1)
      &(s 0)>=gcd(s 0)(s 1) & (s 0)>0 & (s 1)>0 & gcd(s 0)(s 1)=(s 2)) 
   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. 0<(s 12) & (s 3)>=gcd(s 0)(s 1) & gcd(s 0)(s 1)=gcd(s 2)(s 3)
        &(s 3)<=(s 1) & (s 0)>0 & (s 1)>0 & gcd(s 0)(s 1)=(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 simp add: EUCLID_def)
done
end

 (IF' (Less (V 2) (V 3))
 THEN (*3=3-2*)
 (
  12#=(V 2);;
  2#=(V 3);;
  3#=(V 12);;
 )
 ELSE (*2=2-3*
)

 ( SKIP));;

goal (1 subgoal):
 1. [| 0 < s 12; gcd (s 0) (s (Suc 0)) = gcd (s 3 + s 12) (s 3); s 3 <= s (Suc 0); 0 < s 0; 0 < s 3; s 2 = s 3 + s 12 |] ==> gcd (s 3 + s 12) (s 3) = gcd (s 12) (s 3)