(******************************************************************************
 * Clean
 *
 * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

(*
 * IsPrime-Test 
 *
 * Authors : Burkhart Wolff, Frédéric Tuong
 *)

chapter ‹ Clean Semantics : Another Clean Example›


theory IsPrime
  imports (* "../src/Clean"
             "../src/Hoare_Clean"
              "../src/Clean_Symbex"
              "HOL-Computational_Algebra.Primes"
           *)
          Clean.Clean
          Clean.Hoare_MonadSE
          Clean.Clean_Symbex 
          "HOL-Computational_Algebra.Primes"
begin

section‹The Primality-Test Example at a Glance›

definition "SQRT_UINT_MAX = (65536::nat)"
definition "UINT_MAX = (2^32::nat) - 1"


function_spec isPrime(n :: nat) returns bool
pre          "‹n ≤ SQRT_UINT_MAX›"
post "‹λres. res ⟷ prime n ›"
local_vars   i :: nat
defines " if_C ‹n < 2›
            then return_{.result_value_update} ‹False›
            else skip_SE
          fi ;-
          ‹i := 2› ;-
          while_C ‹i < SQRT_UINT_MAX ∧ i*i ≤ n ›
            do if_C ‹n mod i = 0›
                  then return_{.result_value_update} ‹False›
                  else skip_SE
                fi ;-
                ‹i := i + 1 ›
            od ;-
         return_{.result_value_update} ‹True›"


find_theorems name:isPrime name:core
term‹isPrime_core›

lemma XXX :
"isPrime_core n ≡
     if_C (λσ. n < 2) then (return (λσ. False)) 
                     else skip_SE fi;-
     i_update :==_L (λσ. 2) ;-
     while_C (λσ. (hd∘i)σ < SQRT_UINT_MAX ∧ (hd∘i)σ * (hd∘i)σ ≤ n) 
     do
        (if_C (λσ. n mod (hd ∘ i) σ = 0) 
         then (return (λσ. False)) 
         else skip_SE fi ;-
        i_update :==_L (λσ. (hd ∘ i) σ + 1)) 
     od ;-
     return (λσ. True)"

  by(simp add: isPrime_core_def)

lemma YYY:
"isPrime n ≡ block_C push_local_isPrime_state 
                    (isPrime_core n) 
                    pop_local_isPrime_state"
  by(simp add: isPrime_def)

lemma isPrime_correct :
  "{λσ.   ▹ σ ∧ isPrime_pre (n)(σ) ∧ σ = σ_pre } 
     isPrime n 
   {λr σ. ▹ σ ∧ isPrime_post(n) (σ_pre)(σ)(r) }"
   oops



end