SSL ClosureEx.thy   Interaktion und
PortierbarkeitIsabelle

(*
    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 "\<Gamma>\<turnstile> \<lbrace>p\<rightarrow>\<acute>cnt = 0\<rbrace> callClosure upd (c_' t) \<lbrace>\<acute>r = Suc 0 \<and> p\<rightarrow>\<acute>cnt = Suc 0\<rbrace>")
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