Theory ProcParExSP

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2007-2008 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.

*)

section "Examples for Procedures as Parameters using Statespaces"
theory ProcParExSP imports "../Vcg" begin


lemma DynProcProcPar':
 assumes adapt: "P  {s. p s = q 
         (Z. init s  P' Z 
              (t  Q' Z. return s t  R s t) 
              (t  A' Z. return s t  A))}"
 assumes result: "s t. Γ,Θ⊢⇘/F(R s t) result s t Q,A"
 assumes q: "Z. Γ,Θ⊢⇘/F(P' Z) Call q (Q' Z),(A' Z)"
 shows "Γ,Θ⊢⇘/FP dynCall init p return result Q,A"
apply (rule HoarePartial.DynProcProcPar [OF _ result q])
apply (insert adapt)
apply fast
done




lemma conseq_exploit_pre':
             "s  S. Γ,Θ  ({s}  P) c Q,A
              
              Γ,Θ (P  S)c Q,A"
  apply (rule HoarePartialDef.Conseq)
  apply clarify
  by (metis IntI insertI1 subset_refl)

lemma conseq_exploit_pre'':
             "Z. s  S Z.  Γ,Θ  ({s}  P Z) c (Q Z),(A Z)
              
              Z. Γ,Θ (P Z  S Z)c (Q Z),(A Z)"
  apply (rule allI)
  apply (rule conseq_exploit_pre')
  apply blast
  done

lemma conseq_exploit_pre''':
             "s  S. Z. Γ,Θ  ({s}  P Z) c (Q Z),(A Z)
              
              Z. Γ,Θ (P Z  S)c (Q Z),(A Z)"
  apply (rule allI)
  apply (rule conseq_exploit_pre')
  apply blast
  done


procedures compare(i::nat,j::nat|r::bool) "NoBody"


print_locale! compare_signature


context compare_impl
begin
declare [[hoare_use_call_tr' = false]]
term "´r :== CALL compare(´i,´j)"
declare [[hoare_use_call_tr' = true]]
end


(* fixme: typing issue with modifies locale*)
procedures
  LEQ (i::nat,j::nat | r::bool) "´r :== ´i ≤ ´j"
  LEQ_spec: "∀σ. Γ⊢ {σ}  PROC LEQ(´i,´j,´r) ⦃´r = (σi ≤ σj)⦄"

  LEQ_modifies: "∀σ. Γ⊢ {σ} PROC LEQ(´i,´j,´r) {t. t may_only_modify_globals σ in []}"



definition mx:: "('a  'a  bool)  'a  'a  'a"
  where "mx leq a b = (if leq a b then a else b)"

procedures (imports compare_signature)
  Max (compare::string, n::nat, m::nat | k::nat)
  where b::bool
  in
  "´b :== DYNCALL ´compare(´n,´m);;
   IF ´b THEN ´k :== ´n ELSE ´k :== ´m FI"

  Max_spec: "⋀leq. ∀σ. Γ⊢
  ({σ} ∩ {s. (∀τ. Γ⊢ {τ} ´r :== PROC scompare(´i,´j) ⦃´r = (leq τi τj)⦄) ∧
              (∀τ. Γ⊢ {τ} ´r :== PROC scompare(´i,´j) {t. t may_only_modify_globals τ in []})})
    PROC Max(´compare,´n,´m,´k)
  ⦃´k = mx leq σn σm⦄"

context Max_spec
begin
thm Max_spec
end
context Max_impl
begin
term "´b :== DYNCALL ´compare(´n,´m)"
declare [[hoare_use_call_tr' = false]]
term "´b :== DYNCALL ´compare(´n,´m)"
declare [[hoare_use_call_tr' = true]]
end



lemma (in Max_impl ) Max_spec1:
shows
"σ leq. Γ
  ({σ}   (τ. Γ{τ} ´r :== PROC ´compare(´i,´j) ´r = (leq τi τj)) 
      (τ. Γ {τ} ´r :== PROC ´compare(´i,´j) {t. t may_only_modify_globals τ in []}))
    ´k :== PROC Max(´compare,´n,´m)
  ´k = mx leq σn σm"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (intro allI)
apply (rule conseq_exploit_pre')
apply (rule)
apply clarify
proof -
  fix σ:: "('a, 'b, 'c, 'd) stateSP_scheme" and s::"('a, 'b, 'c, 'd) stateSP_scheme" and leq
   assume compare_spec:
       "τ. Γ{τ} ´r :== PROC scompare(´i,´j) ´r = leq τi τj"

  assume compare_modifies:
        "τ. Γ{τ} ´r :== PROC scompare(´i,´j)
                {t. t may_only_modify_globals τ in []}"

   show "Γ({s}  {σ})
            ´b :== DYNCALL ´compare (´n,´m);;
            IF ´b THEN ´k :== ´n ELSE ´k :== ´m FI
            ´k = mx leq σn σm"
     apply vcg
     apply (clarsimp simp add: mx_def)
     done
 qed


lemma (in Max_impl) Max_spec2:
shows
"σ leq. Γ
  ({σ}  (τ. Γ {τ} ´r :== PROC ´compare(´i,´j) ´r = (leq τi τj)) 
      (τ. Γ {τ} ´r :== PROC ´compare(´i,´j) {t. t may_only_modify_globals τ in []}))
    ´k :== PROC Max(´compare,´n,´m)
  ´k = mx leq σn σm"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (intro allI)
apply (rule conseq_exploit_pre')
apply (rule)
apply clarify
apply vcg
apply (clarsimp simp add: mx_def)
done

lemma (in Max_impl) Max_spec3:
shows
"n m leq. Γ
  (´n=n  ´m=m  
   (τ. Γ {τ} ´r :== PROC ´compare(´i,´j) ´r = (leq τi τj)) 
     (τ. Γ {τ} ´r :== PROC ´compare(´i,´j) {t. t may_only_modify_globals τ in []}))
    ´k :== PROC Max(´compare,´n,´m)
  ´k = mx leq n m"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (intro allI)
apply (rule conseq_exploit_pre')
apply (rule)
apply clarify
apply vcg
apply (clarsimp simp add: mx_def)
done

lemma (in Max_impl) Max_spec4:
shows
"n m leq. Γ
  (´n=n  ´m=m  τ. Γ {τ} ´r :== PROC ´compare(´i,´j) ´r = (leq τi τj))
    ´k :== PROC Max(´compare,´n,´m)
  ´k = mx leq n m"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (intro allI)
apply (rule conseq_exploit_pre')
apply (rule)
apply clarify
apply vcg
apply (clarsimp simp add: mx_def)
done

print_locale Max_spec

(* We have to rename the parameters of the compare procedure to match the LEQ procedure *)
locale Max_test = Max_spec where
        i_'compare_' = i_'LEQ_' and
        j_'compare_' = j_'LEQ_' and
        r_'compare_' = r_'LEQ_'
       + LEQ_spec + LEQ_modifies

lemma (in Max_test)
  shows
  "Γ {σ} ´k :== CALL Max(LEQ_'proc,´n,´m) ´k = mx (≤) σn σm"
proof -
  note Max_spec = Max_spec [where leq="(≤)"]
  show ?thesis
    apply vcg
    apply (clarsimp)
    apply (rule conjI)
    apply (rule LEQ_spec)
    apply (rule LEQ_modifies)
    done
qed






lemma (in Max_impl) Max_spec5:
shows
"n m leq. Γ
  (´n=n  ´m=m  n' m'. Γ ´i=n'  ´j=m' ´r :== PROC ´compare(´i,´j) ´r = (leq n' m'))
    ´k :== PROC Max(´compare,´n,´m)
  ´k = mx leq n m"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (intro allI)
apply (rule conseq_exploit_pre')
apply (rule)
apply clarify
apply vcg
apply clarsimp
apply (clarsimp simp add: mx_def)
done

lemma (in LEQ_impl)
 LEQ_spec: "n m. Γ ´i=n  ´j=m  PROC LEQ(´i,´j,´r) ´r = (n  m)"
  apply vcg
  apply simp
  done


print_locale Max_impl
locale Max_test' = Max_impl where
        i_'compare_' = i_'LEQ_' and
        j_'compare_' = j_'LEQ_' and
        r_'compare_' = r_'LEQ_'
        + LEQ_impl
lemma (in Max_test')
  shows
  "n m. Γ ´n=n  ´m=m ´k :== CALL Max(LEQ_'proc,´n,´m) ´k = mx (≤) n m"
proof -
  note Max_spec = Max_spec5
  show ?thesis
    apply vcg
    apply (rule_tac x="(≤)" in exI)
    apply clarsimp
    apply (rule LEQ_spec [rule_format])
    done
qed

end