Theory PhiTest_Arithmetic

theory PhiTest_Arithmetic
  imports
    Phi_Semantics.PhiSem_CF_Routine
    Phi_Semantics.PhiSem_CF_Breakable
    Phi_Semantics.PhiSem_Variable
    Phi_Semantics.PhiSem_Int_ArbiPrec
    "HOL-Computational_Algebra.Primes"
begin

proc test_prime:
  input  ‹𝗏𝖺𝗅 x ⦂ β„•β€Ί
  output ‹𝗏𝖺𝗅 prime x ⦂ 𝔹› ― β€Ήtermβ€Ήprime :: nat => boolβ€Ί is a predicate checking primesβ€Ί
  is [routine]
❴
  if β€Ή$x ≀ 1β€Ί  ❴
    return (False)
  ❡
  ❴
    β€Ή2 ⦂ β„•β€Ί β†’ var v ;;

    while β€Ήi ⦂ 𝗏𝖺𝗋[v] β„• π—Œπ—Žπ–»π—ƒ i.
            Inv: (1 < i ∧ i ≀ x ∧ (βˆ€j. 1 < j ∧ j < i ⟢ Β¬ j dvd x)) ∧
            Guard: (i β‰  x) ∧
            End: (i = x)β€Ί ― β€ΉSpecification of the loopβ€Ί
          ( β€Ή$v β‰  $xβ€Ί ) ― β€ΉCode for loop guardβ€Ί
    ❴                   ― β€ΉCode for loop bodyβ€Ί
      if β€Ή$x mod $v = 0β€Ί ❴
        return (False)
      ❡
      ❴
        β€Ή$v + 1β€Ί β†’ $v
      ❡
    ❡
    return (True)
  ❡
❡.

thm test_prime_def ― β€ΉSemantic definitionβ€Ί
thm test_prime_Ο†app ― β€ΉSpecification theoremβ€Ί


proc test_prime':
  input  ‹𝗏𝖺𝗅 x ⦂ β„•β€Ί
  output ‹𝗏𝖺𝗅 prime x ⦂ 𝔹›
  is [routine]
❴
  if β€Ή$x ≀ 1β€Ί ❴
    return (False)
  ❡
  ❴
    β€Ή2 ⦂ β„•β€Ί β†’ var v ;;
    (* In the previous example, the loop iterates from 2 to x, here we apply an optimization
       where the loop only needs to iterate to sqrt(x). *)
    while β€Ήi ⦂ 𝗏𝖺𝗋[v] β„• π—Œπ—Žπ–»π—ƒ i.
          Inv: (1 < i ∧ i ≀ x ∧ (βˆ€j ∈ {1<..<i}. Β¬ j dvd x)) ∧
          Guard: (i * i ≀ x) ∧
          End: (x < i * i)β€Ί
        ( β€Ή$v * $v ≀ $xβ€Ί )
    ❴
      if β€Ή$x mod $v = 0β€Ί ❴
        return (False)  
      ❡
      ❴
        β€Ή$v + 1β€Ί β†’ $v 
      ❡
    ❡

    return (True) (*with this optimization, the final obligation fails to be solved
                    automatically, but the manual proof is intuitive and semi-automated.*)
      certified proof simp
        have β€ΉFalseβ€Ί if assm: β€ΉΒ¬ prime xβ€Ί
          proof -
            obtain k where β€Ήk dvd x ∧ 1 < k ∧ k < xβ€Ί by auto_sledgehammer
            then have β€Ήk < ib ∨ x div k < ibβ€Ί by auto_sledgehammer
            then show False by auto_sledgehammer
          qed
        then show β€Ήprime xβ€Ί
          by fastforce
      qed
  ❡ ― β€ΉClose the top branchβ€Ί
❡ ― β€ΉClose the function bodyβ€Ί .


proc GCD:
  input  β€Ήx ⦂ 𝗏𝖺𝗅 β„•βŸ y ⦂ 𝗏𝖺𝗅 β„•β€Ί
  output β€Ήgcd x y ⦂ 𝗏𝖺𝗅 β„•β€Ί 
  is [recursive x y] ― β€Ήx, y are variable through recursive callingsβ€Ί
❴
  if β€Ή$x > $yβ€Ί ❴ GCD ($y, $x) ❡
  ❴
    β€Ή$y mod $xβ€Ί β†’ val t
    if β€Ή$t = 0β€Ί ❴ $x ❡ ❴ GCD ($t, $x) ❡
  ❡
❡.

declare GCD_Ο†app[Ο†synthesis add] ― β€ΉSo that we can use abstract spec β€Ήgcdβ€Ί in synthesisβ€Ί

proc Coprime:
  input  β€Ήx ⦂ 𝗏𝖺𝗅 β„•βŸ y ⦂ 𝗏𝖺𝗅 β„•β€Ί
  output β€Ήcoprime x y ⦂ 𝗏𝖺𝗅 𝔹›
❴
  β€Ήgcd $x $y = 1β€Ί
❡.


proc binary_search:
  requires F: β€Ήβˆ€i v. π—‰π—‹π—ˆπ–Ό F v ⦃ i ⦂ 𝗏𝖺𝗅[v] β„€ ⟼ f i ⦂ 𝗏𝖺𝗅 𝔹 ⦄› ― β€Ήv: raw valueβ€Ί
  premises β€Ήmono fβ€Ί
  input  β€Ήlower ⦂ 𝗏𝖺𝗅 β„€βŸ upper ⦂ 𝗏𝖺𝗅 β„€β€Ί
  premises β€Ήf upperβ€Ί and β€Ήlower < upperβ€Ί
  output β€Ή(LEAST i. lower ≀ i ∧ i ≀ upper ∧ f i) ⦂ 𝗏𝖺𝗅 β„€β€Ί
  is [routine]
❴
  pure_fact β€Ήi ≀ j ⟹ f i ⟹ f jβ€Ί for i j ;;

  if ( F($lower) ) ❴ return ($lower) ❡
  ❴  
    $lower, $upper β†’ var $l, $u ;;
    while β€Ήl ⦂ 𝗏𝖺𝗋[l] β„€βŸ u ⦂ 𝗏𝖺𝗋[u] β„€ π—Œπ—Žπ–»π—ƒ l u.
            Inv: (lower ≀ l ∧ l < u ∧ u ≀ upper ∧ Β¬ f l ∧ f u) ∧
            Guard: (l + 1 < u) ∧
            End: (l + 1 = u)β€Ί
          ( β€Ή$l + 1 < $uβ€Ί )
    ❴
      β€Ή($l + $u) div 2β€Ί β†’ val m ;;
      if ( F($m) ) ❴ $m β†’ $u ❡ ❴ $m β†’ $l ❡
    ❡
    return ($u)
  ❡
❡.

end