Theory ProcParEx

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

Copyright (C) 2006-2008 Norbert Schirmer
*)

section "Examples for Procedures as Parameters"

theory ProcParEx 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 "Γ,Θ⊢⇘/F ⇙P 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



record 'g vars = "'g state" +
  compare_' :: string
  n_'   :: nat
  m_'   :: nat
  b_'   :: bool
  k_'  :: nat



procedures compare(n,m|b) = "NoBody"
print_locale! compare_signature


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


procedures
  LEQ (n,m | b) = "´b :== ´n ≤ ´m"
  LEQ_spec: "∀σ. Γ⊢ {σ}  PROC LEQ(´n,´m,´b) ⦃´b = (⇗σ⇖n ≤ ⇗σ⇖m)⦄"
  LEQ_modifies: "∀σ. Γ⊢ {σ} PROC LEQ(´n,´m,´b) {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
  Max (compare, n, m | k) =
  "´b :== DYNCALL ´compare(´n,´m);;
   IF ´b THEN ´k :== ´n ELSE ´k :== ´m FI"

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


lemma (in Max_impl ) Max_spec1:
shows
"∀σ leq. Γ⊢
  ({σ} ∩ ⦃ (∀τ. Γ⊢{τ} ´b :== PROC ´compare(´n,´m) ⦃´b = (leq ⇗τ⇖n ⇗τ⇖m)⦄) ∧
      (∀τ. Γ⊢ {τ} ´b :== PROC ´compare(´n,´m) {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) vars_scheme" and s::"('a,'b) vars_scheme" and leq
   assume compare_spec:
       "∀τ. Γ⊢{τ} ´b :== PROC ⇗s⇖compare(´n,´m) ⦃´b = leq ⇗τ⇖n ⇗τ⇖m⦄"

  assume compare_modifies:
        "∀τ. Γ⊢{τ} ´b :== PROC ⇗s⇖compare(´n,´m)
                {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. Γ⊢
  ({σ} ∩ ⦃(∀τ. Γ⊢ {τ} ´b :== PROC ´compare(´n,´m) ⦃´b = (leq ⇗τ⇖n ⇗τ⇖m)⦄) ∧
      (∀τ. Γ⊢ {τ} ´b :== PROC ´compare(´n,´m) {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⦄  ∩
   ⦃(∀τ. Γ⊢ {τ} ´b :== PROC ´compare(´n,´m) ⦃´b = (leq ⇗τ⇖n ⇗τ⇖m)⦄) ∧
     (∀τ. Γ⊢ {τ} ´b :== PROC ´compare(´n,´m) {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⦄ ∩ ⦃∀τ. Γ⊢ {τ} ´b :== PROC ´compare(´n,´m) ⦃´b = (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 simp add: mx_def)
done

locale Max_test = Max_spec + 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 [simplified])
    apply (rule LEQ_modifies [simplified])
    done
qed


lemma (in Max_impl) Max_spec5:
shows
"∀n m leq. Γ⊢
  (⦃´n=n ∧ ´m=m⦄ ∩ ⦃∀n' m'. Γ⊢ ⦃´n=n' ∧ ´m=m'⦄ ´b :== PROC ´compare(´n,´m) ⦃´b = (leq n' m')⦄⦄)
    ´k :== PROC Max(´compare,´n,´m)
  ⦃´k = mx leq n m⦄"
term "⦃{s. ⇗s⇖n = n' ∧ ⇗s⇖m = m'} = X⦄"
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. Γ⊢ ⦃´n=n ∧ ´m=m⦄  PROC LEQ(´n,´m,´b) ⦃´b = (n ≤ m)⦄"
  apply vcg
  done


locale Max_test' = Max_impl + 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