Theory ClosureEx

(*
    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⇩0 ∧ (∀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⇩0 + 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 ‹
val 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