Rel 12 (e)

theory Hoare_anotado_ejercicios

imports "VCG_b" "Hoare_Total_b"

begin

definition
    "MUL ≡
    ''z''::=N 0;;
    ''c''::=N 0;;
    WHILE (Less (V ''c'') (V ''y'')) DO (
      ''z''::=Plus (V ''z'') (V ''x'');;
      ''c''::=Plus (V ''c'') (N 1))"

abbreviation MUL_invar :: "state ⇒ state ⇒ bool" where
    "MUL_invar sorig s ≡ 
      s ''z'' = s ''x'' * s ''c'' 
    ∧ s ''c'' ≤ s ''y''
    ∧ (∀v. v∉{''z'', ''c''} ⟶ s v = sorig v )"

definition
    "MUL_annot sorig ≡
    ''z''::=N 0;;
    ''c''::=N 0;;
    {MUL_invar sorig} WHILE (Less (V ''c'') (V ''y'')) DO (
      ''z''::=Plus (V ''z'') (V ''x'');;
      ''c''::=Plus (V ''c'') (N 1))"

lemma MUL_strip: "MUL = strip (MUL_annot sorig)"
oops 

lemma "⊢
  {λs. 0 ≤ s ''y'' ∧ prod = s ''y'' * s ''x''}
  MUL
  {λs. s ''z'' = prod}"
  oops (* Comentario *)

lemma "⊢
  {λs. 0 ≤ s ''y'' ∧ s=sorig}
  MUL
  {λs. s ''z'' = s ''x'' * s ''y'' ∧ (∀v. v∉{''z'', ''c''} ⟶ s v = sorig v )}"
oops


definition "SQRT ≡
    ''r'' ::= N 0 ;;
    ''s'' ::= N 1 ;;
    WHILE (Not (Less (V ''x'') (V ''s''))) DO (
    ''r'' ::= Plus (V ''r'') (N 1 );;
    ''s'' ::= Plus (V ''s'' ) (V ''r'' );;
    ''s'' ::= Plus (V ''s'' ) (V ''r'' );;
    ''s'' ::= Plus (V ''s'' ) (N 1 )
  )"

context fixes sorig :: state 
begin
    
abbreviation "SQRT_invar s ≡ 
        s ''s'' = (s ''r'' + 1) ^ 2
      ∧ (s ''r'') ^ 2 ≤ s ''x''  
      ∧ (∀v . v ∉ {''s'' , ''r'' } ⟶ s v = sorig v)"

definition "SQRT_annot ≡
    ''r'' ::= N 0 ;;
    ''s'' ::= N 1 ;;
    {SQRT_invar} WHILE (Not (Less (V ''x'') (V ''s''))) DO (
      ''r'' ::= Plus (V ''r'') (N 1 );;
      ''s'' ::= Plus (V ''s'' ) (V ''r'' );;
      ''s'' ::= Plus (V ''s'' ) (V ''r'' );;
      ''s'' ::= Plus (V ''s'' ) (N 1 )
    )"

lemma SQRT_strip: "SQRT = strip SQRT_annot"
oops
    
lemma "⊢
    {λs. s=sorig ∧ s ''x'' ≥ 0 }
    SQRT
    {λs. (s ''r'')^2 ≤ s ''x'' 
      ∧ s ''x'' < (s ''r'' + 1)^2 
      ∧ (∀v . v ∉ {''s'' , ''r'' } ⟶ s v = sorig v )}"  
oops      

thm power2_eq_square    


lemmas Seq_bwd = Seq[rotated]

thm If

text{*
Modificamos el lema:
*}

lemma IfT :
    assumes "⊢⇩t {P1} c1 {Q}" and "⊢⇩t {P2} c2 {Q}"
    shows "⊢⇩t 
      {λs. (bval b s ⟶ P1 s) ∧ (¬ bval b s ⟶ P2 s)} 
        IF b THEN c1 ELSE c2 
      {Q}"
    apply (rule If)    
    apply (rule strengthen_pre[where P=P1])
    apply (auto simp: assms)
    apply (rule strengthen_pre[where P=P2])
    apply (auto simp: assms)
    done


lemma 
  assumes "⊢⇩t {P1} c1 {Q}" and "⊢⇩t {P2} c2 {Q}"
  shows "⊢⇩t 
      {λs. (bval b s ⟶ P1 s) ∧ (¬ bval b s ⟶ P2 s)} 
        IF b THEN c1 ELSE c2 
      {Q}"
oops

lemmas hoareT_rule[intro? ] = Seq_bwd Hoare_Total_b.Assign Hoare_Total_b.Assign' IfT

lemma "⊢⇩t
  {λs. 0 ≤ s ''y'' ∧ s=sorig}
  MUL
  {λs. s ''z'' = s ''x'' * s ''y'' ∧ (∀v. v∉{''z'', ''c''} ⟶ s v = sorig v )}"
oops

lemma "⊢⇩t
    {λs. s=sorig ∧ s ''x'' ≥ 0 }
    SQRT
    {λs. (s ''r'')^2 ≤ s ''x'' 
      ∧ s ''x'' < (s ''r'' + 1)^2 
      ∧ (∀v . v ∉ {''s'' , ''r'' } ⟶ s v = sorig v )}"  
oops

end

end