(*
    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) =
"\<acute>p :== NEW 1 [\<acute>cnt :== 0];;
 \<acute>c :== ([(''p'',\<acute>p)],Inc_'proc)"


locale NewCounter_impl' = NewCounter_impl + Inc_impl
lemma (in NewCounter_impl')
shows
  "\<forall>alloc. \<Gamma>\<turnstile> \<lbrace>1 \<le> \<acute>free\<rbrace> \<acute>c :== PROC NewCounter()
          \<lbrace>\<exists>p. p\<rightarrow>\<acute>cnt = 0 \<and>
               (\<forall>i. \<Gamma>\<turnstile> \<lbrace>p\<rightarrow>\<acute>cnt = i\<rbrace> callClosure upd \<acute>c \<lbrace>\<acute>r=i+1 \<and> p\<rightarrow>\<acute>cnt = i+1\<rbrace>)\<rbrace>"
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
  "\<forall>alloc. \<Gamma>\<turnstile> \<lbrace>1 \<le> \<acute>free\<rbrace> \<acute>c :== PROC NewCounter()
          \<lbrace>\<exists>p. p\<rightarrow>\<acute>cnt = 0 \<and>
               (\<forall>i. \<Gamma>\<turnstile> \<lbrace>p\<rightarrow>\<acute>cnt = i\<rbrace> callClosure upd \<acute>c \<lbrace>\<acute>r=i+1 \<and> p\<rightarrow>\<acute>cnt = i+1\<rbrace>)\<rbrace>"
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:
  "\<forall>alloc. \<Gamma>\<turnstile> \<lbrace>1 \<le> \<acute>free \<and> \<acute>alloc=alloc\<rbrace> \<acute>c :== PROC NewCounter()
          \<lbrace>\<exists>p. p \<notin> set alloc \<and> p \<in> set \<acute>alloc \<and> p \<noteq> Null \<and> p\<rightarrow>\<acute>cnt = 0 \<and>
               (\<forall>i. \<Gamma>\<turnstile> \<lbrace>p\<rightarrow>\<acute>cnt = i\<rbrace> callClosure upd \<acute>c \<lbrace>\<acute>r=i+1 \<and> p\<rightarrow>\<acute>cnt = i+1\<rbrace>)\<rbrace>"
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 "\<Gamma>\<turnstile>\<lbrace>\<exists>p. p \<noteq> Null \<and> p\<rightarrow>\<acute>cnt = i \<and>
              (\<forall>i. \<Gamma>\<turnstile> \<lbrace>p\<rightarrow>\<acute>cnt = i\<rbrace> callClosure upd \<acute>c \<lbrace>\<acute>r=i+1 \<and> p\<rightarrow>\<acute>cnt = i+1\<rbrace>)\<rbrace>
           dynCallClosure (\<lambda>s. s) upd c_' (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                         (\<lambda>s t. Basic (\<lambda>u. u\<lparr>r_' := r_' t\<rparr>))
           \<lbrace>\<acute>r=i+1\<rbrace>"
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 \<open>
val hoare_tacs = #hoare_tacs (Hoare.get_data @{context});
\<close>
lemma (in NewCounter_impl')
 shows "\<Gamma>\<turnstile> \<lbrace>1 \<le> \<acute>free\<rbrace>
             \<acute>c :== CALL NewCounter ();;
             dynCallClosure (\<lambda>s. s) upd c_' (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                         (\<lambda>s t. Basic (\<lambda>u. u\<lparr>r_' := r_' t\<rparr>))
           \<lbrace>\<acute>r=1\<rbrace>"
  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 "\<Gamma>\<turnstile> \<lbrace>1 \<le> \<acute>free\<rbrace>
             \<acute>c :== CALL NewCounter ();;
             dynCallClosure (\<lambda>s. s) upd c_' (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                         (\<lambda>s t. Basic (\<lambda>u. u\<lparr>r_' := r_' t\<rparr>));;
             dynCallClosure (\<lambda>s. s) upd c_' (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                         (\<lambda>s t. Basic (\<lambda>u. u\<lparr>r_' := r_' t\<rparr>))
           \<lbrace>\<acute>r=2\<rbrace>"
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 "\<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


lemma (in NewCounter_impl')
 shows "\<Gamma>\<turnstile> \<lbrace>1 \<le> \<acute>free\<rbrace>
             \<acute>c :== CALL NewCounter ();;
             \<acute>d :== \<acute>c;;
             dynCallClosure (\<lambda>s. s) upd c_' (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                         (\<lambda>s t. Basic (\<lambda>u. u\<lparr>n_' := r_' t\<rparr>));;
             dynCallClosure (\<lambda>s. s) upd d_' (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                         (\<lambda>s t. Basic (\<lambda>u. u\<lparr>m_' := r_' t\<rparr>));;
             \<acute>r :== \<acute>n + \<acute>m
           \<lbrace>\<acute>r=3\<rbrace>"

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