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)


text {* A convenient loop construct: *}

abbreviation Afor :: "name => aexp => aexp => assn => acom => acom"
  ("(FOR _/ FROM _/ TO _/ _/ DO _)"  [0, 0, 0, 0, 61] 61) where
  "FOR v FROM a1 TO a2 b DO c ==
     (v #= a1 ;; WHILE' (Less (V v) a2) b DO (c ;; v #= Plus (V v) (N 1)))"



section {* Exercise 1 *}

definition MAX :: "acom" where
  "MAX = SKIP"  (* provide a definition *)

lemma MAX_sound: "vc MAX (\<lambda>s. s 2 = max (s 0) (s 1)) s"
  oops  (* provide a proof *)



section {* Exercise 2 *}

definition MULTIPLY :: "acom" where
  "MULTIPLY = SKIP"  (* provide a definition *)

lemma MULTIPLY_sound: "vc MULTIPLY (\<lambda>s. s 2 = s 0 * s 1) s"
  oops  (* provide a proof *)



section {* Exercise 3 *}

fun factorial :: "nat => nat" where
  "factorial 0 = 1"
| "factorial (Suc n) = factorial n * Suc n"


definition FACTORIAL :: "acom" where
  "FACTORIAL =( 
    1#= N 1;;
    IF' (Less ( V 0 ) (N 1)) THEN 
       SKIP
ELSE(
FOR 2 FROM (N 1) TO  (V 0)  
(*\<lambda>s. False*)
(\<lambda>s.  (s 2)<= (s 0)& (s 1)= factorial (s 2)) 
DO
( 
 3#= N 0;;
 (FOR 4 FROM (N 0) TO (Plus (V 2) (N 1)) 
 (\<lambda>s. s 1 = factorial (s 2) & s 2 < s 0 & s 3 = s 4 * s 1 & s 4 <= s 2 + 1)
  DO 3#= (Plus (V 3) (V 1))
 );;
 1#= V 3
 )
))
"  
lemma FACTORIAL_sound: "vc FACTORIAL (\<lambda>s. s 1 = factorial (s 0)) s"
 apply(auto simp add: FACTORIAL_def)
done


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)\<ge> 0 & (s 2) \<le> (s 0) &  (s 1) \<le> (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
b =1
a'=2
b'=3
*)
definition EUCLID :: "acom" where
  "EUCLID =
2#=(V 0);;
3#=(V 1);;
WHILE' (Not (Eq (V 2) (V 3))) 
   (\<lambda>s. (s 2)>= gcd (s 0) (s 1)  & (s 3)>=gcd (s 0) (s 1) & (s 2)<= (s 0) & (s 3) <= (s 1))
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 12) < (s 3) &  (s 2) < (s 3) & (s 12) + (s 2) <= (s 3)& 
                   0 < (s 12)& 0 < ( s 3)& 1 < (s 2 )& 
                   (s 2)>= gcd (s 0) (s 1) & (s 3)>=gcd (s 0) (s 1) & (s 2)<= (s 0) & (s 3) <= (s 1)) 
   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 12) < (s 2) &  (s 3) < (s 2) & (s 12) + (s 3) <= (s 2) &
                  0< (s 12) & 0 < (s 3) & 1 < (s 2)&
                (s 2)>= gcd (s 0) (s 1) & (s 3)>=gcd (s 0) (s 1) & (s 2)<= (s 0) & (s 3) <= (s 1))
   DO
   (
   12#=Plus (V 12) (N 1)
   ));;
   2#=(V 12)
 )
)
"

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