Quelle  ClosureEx.thy

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

Copyright (C) 2006-2008 Norbert Schirmer
*)

theory ClosureEx
imports "../Vcg" "../Simpl_Heap" Closure
begin


record globals =
 cnt_' :: "ref ==> nat"
 alloc_' :: "ref list"
 free_' :: "nat"
record 'g vars = "'g state" +
 p_':: ref
 r_':: nat
 n_':: nat
 m_':: nat
 c_':: "(string × ref) list × string"
 d_':: "(string × ref) list × string"
 e_':: "(string × nat) list × string"


definition "var_n = [''n''↦ (λx. n_'_update (λ_. x)),
                    ''m''↦ (λx. m_'_update (λ_. x))]"
definition "upd_n = gen_upd var_n"

lemma upd_{n_ap}: "upd_n (fst (ap es (es',p))) = upd_n es' ∘ upd_n es"
  by (simp add: upd_{n_def} gen_upd_ap)


lemma
"Γ⊨{🍋n=n₀ ∧ (∀i j. Γ⊨ {🍋n=i ∧ 🍋m=j} callClosure upd_n 🍋e {🍋r=i + j})}
      🍋e :== (ap [(''n'',🍋n)] 🍋e)
   {∀j. Γ⊨ {🍋m=j} callClosure upd_n 🍋e {🍋r=n₀ + j}}"
apply vcg_step
apply clarify
apply (rule ap_closure [where var=var_n, folded upd_{n_def}])
apply clarsimp
apply (rename_tac s s')
apply (erule_tac x="n_' s" in allE)
apply (erule_tac x="m_' s'" in allE)
apply (rule exI)
apply (rule exI)
apply (rule conjI)
apply (assumption)
apply (simp add: upd_{n_def} gen_upd_def var_{n_def})
done


definition "var = [''p''↦ (λx. p_'_update (λ_. x))]"
definition "upd = gen_upd var"

procedures Inc(p|r) =
 "🍋p→🍋cnt :== 🍋p→🍋cnt + 1;;
  🍋r :== 🍋p→🍋cnt"

lemma (in Inc_impl)
 "∀i p. Γ⊨ {🍋p→🍋cnt = i} 🍋r :== PROC Inc(🍋p) {🍋r=i+1 ∧ 🍋p→🍋cnt = i+1}"
  apply vcg
  apply simp
  done

procedures (imports Inc_signature) NewCounter(|c) =
"🍋p :== NEW 1 [🍋cnt :== 0];;
 🍋c :== ([(''p'',🍋p)],Inc_'proc)"


locale NewCounter_impl' = NewCounter_impl + Inc_impl
lemma (in NewCounter_impl')
shows
  "∀alloc. Γ⊨ {1 ≤ 🍋free} 🍋c :== PROC NewCounter()
          {∃p. p→🍋cnt = 0 ∧
               (∀i. Γ⊨ {p→🍋cnt = i} callClosure upd 🍋c {🍋r=i+1 ∧ p→🍋cnt = i+1})}"
apply vcg
apply simp
apply (rule_tac x="new (set alloc)" in exI)
apply simp
apply (simp add: callClosure_def)
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply (simp add: upd_def var_def gen_upd_def)
done

lemma (in NewCounter_impl')

shows
  "∀alloc. Γ⊨ {1 ≤ 🍋free} 🍋c :== PROC NewCounter()
          {∃p. p→🍋cnt = 0 ∧
               (∀i. Γ⊨ {p→🍋cnt = i} callClosure upd 🍋c {🍋r=i+1 ∧ p→🍋cnt = i+1})}"
apply vcg
apply simp
apply (rule_tac x="new (set alloc)" in exI)
apply simp
apply (simp add: callClosure_def)
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply (simp add: upd_def var_def gen_upd_def)
done

lemma (in NewCounter_impl')
shows NewCounter_spec:
  "∀alloc. Γ⊨ {1 ≤ 🍋free ∧ 🍋alloc=alloc} 🍋c :== PROC NewCounter()
          {∃p. p ∉ set alloc ∧ p ∈ set 🍋alloc ∧ p ≠ Null ∧ p→🍋cnt = 0 ∧
               (∀i. Γ⊨ {p→🍋cnt = i} callClosure upd 🍋c {🍋r=i+1 ∧ p→🍋cnt = i+1})}"
apply vcg
apply clarsimp
apply (rule_tac x="new (set alloc)" in exI)
apply simp
apply (simp add: callClosure_def)
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply (simp add: upd_def var_def gen_upd_def)
done



lemma "Γ⊨{∃p. p ≠ Null ∧ p→🍋cnt = i ∧
              (∀i. Γ⊨ {p→🍋cnt = i} callClosure upd 🍋c {🍋r=i+1 ∧ p→🍋cnt = i+1})}
           dynCallClosure (λs. s) upd c_' (λs t. s(globals := globals t))
                         (λs t. Basic (λu. u(r_' := r_' t)))
           {🍋r=i+1}"
apply (rule conseq_extract_pre)
apply clarify
apply (rule dynCallClosureFix)
apply (simp only: Ball_def)
prefer 3
apply (assumption)
prefer 2
apply vcg_step
apply vcg_step
apply (simp only: simp_thms)
apply clarsimp
done

declare [[hoare_trace = 1]]

ML ‹
  hoare_tacs = #hoare_tacs (Hoare.get_data @{context});
 ›
lemma (in NewCounter_impl')
 shows "Γ⊨ {1 ≤ 🍋free}
             🍋c :== CALL NewCounter ();;
             dynCallClosure (λs. s) upd c_' (λs t. s(globals := globals t))
                         (λs t. Basic (λu. u(r_' := r_' t)))
           {🍋r=1}"
  apply vcg_step
apply (rule dynCallClosure)
prefer 2
apply vcg_step
apply vcg_step
apply vcg_step
apply clarsimp
apply (erule_tac x=0 in allE)
apply (rule exI)
apply (rule exI)
apply (rule conjI)
apply (assumption)
apply simp
done


lemma (in NewCounter_impl')
 shows "Γ⊨ {1 ≤ 🍋free}
             🍋c :== CALL NewCounter ();;
             dynCallClosure (λs. s) upd c_' (λs t. s(globals := globals t))
                         (λs t. Basic (λu. u(r_' := r_' t)));;
             dynCallClosure (λs. s) upd c_' (λs t. s(globals := globals t))
                         (λs t. Basic (λu. u(r_' := r_' t)))
           {🍋r=2}"
apply vcg_step
apply (rule dynCallClosure)
prefer 2
apply vcg_step
apply vcg_step
apply vcg_step
apply (rule dynCallClosure)
apply vcg_step
apply vcg_step
apply vcg_step

apply clarsimp
apply (subgoal_tac "Γ⊨ {p→🍋cnt = 0} callClosure upd (c_' t) {🍋r = Suc 0 ∧ p→🍋cnt = Suc 0}")
apply (rule exI)
apply (rule exI)
apply (rule conjI)
apply assumption
apply clarsimp
apply (erule_tac x=1 in allE)
apply (rule exI)
apply (rule exI)
apply (rule conjI)
apply assumption
apply clarsimp
apply (erule allE)
apply assumption
done


lemma (in NewCounter_impl')
 shows "Γ⊨ {1 ≤ 🍋free}
             🍋c :== CALL NewCounter ();;
             🍋d :== 🍋c;;
             dynCallClosure (λs. s) upd c_' (λs t. s(globals := globals t))
                         (λs t. Basic (λu. u(n_' := r_' t)));;
             dynCallClosure (λs. s) upd d_' (λs t. s(globals := globals t))
                         (λs t. Basic (λu. u(m_' := r_' t)));;
             🍋r :== 🍋n + 🍋m
           {🍋r=3}"

apply vcg_step
apply vcg_step
apply (rule dynCallClosure)
prefer 2
apply vcg_step
apply vcg_step
apply vcg_step
apply (rule dynCallClosure)
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply clarsimp
apply (subgoal_tac "Γ⊨ {p→🍋cnt = 0} callClosure upd (c_' t) {🍋r = Suc 0 ∧ p→🍋cnt = Suc 0}")
apply (rule exI)
apply (rule exI)
apply (rule conjI)
apply assumption
apply clarsimp
apply (erule_tac x=1 in allE)
apply (rule exI)
apply (rule exI)
apply (rule conjI)
apply assumption
apply clarsimp
apply (erule allE)
apply assumption
done

end