Theory Closure

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

Copyright (C) 2006-2008 Norbert Schirmer
*)

section "Experiments with Closures"

theory Closure
imports "../Hoare"
begin


definition
"callClosure upd cl = Seq (Basic (upd (fst cl))) (Call (snd cl))"


definition
"dynCallClosure init upd cl return c =
  DynCom (λs. call (upd (fst (cl s)) ∘ init) (snd (cl s)) return c)"





lemma dynCallClosure_sound:
assumes adapt:
  "P ⊆ {s. ∃P' Q' A'. ∀n. Γ,Θ⊨n:⇘/F ⇙ P' (callClosure upd (cl s)) Q',A' ∧
                  init s ∈ P' ∧
                  (∀t ∈ Q'. return s t ∈ R s t) ∧
                  (∀t ∈ A'. return s t ∈ A)}"
assumes res: "∀s t n. Γ,Θ⊨n:⇘/F⇙ (R s t) (c s t) Q,A"
shows
"Γ,Θ⊨n:⇘/F ⇙P (dynCallClosure init upd cl return c) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P Call p Q,A"
  assume exec: "Γ⊢ ⟨dynCallClosure init upd cl return c,Normal s⟩ =n⇒ t"
  from execn.Basic [where f="(upd (fst (cl s)))" and s="(init s)"]
  have exec_upd: "Γ⊢⟨Basic (upd (fst (cl s))),Normal (init s)⟩ =n⇒
             Normal (((upd (fst (cl s))) ∘ init) s)"
      by auto
  assume P: "s ∈ P"
  from P adapt obtain P' Q' A'
      where
      valid: "∀n. Γ,Θ⊨n:⇘/F ⇙ P' (callClosure upd (cl s)) Q',A'" and
      init_P': "init s ∈ P'"  and
      R: "(∀t ∈ Q'. return s t ∈ R s t)" and
      A: "(∀t ∈ A'. return s t ∈ A)"
      by auto
  assume t_notin_F: "t ∉ Fault ` F"
  from exec [simplified dynCallClosure_def]
  have exec_call:
      "Γ⊢⟨call (upd (fst (cl s)) ∘ init) (snd (cl s)) return c,Normal s⟩ =n⇒ t"
    by cases
  then
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases rule: execn_call_Normal_elim)
    fix bdy m t'
    assume bdy: "Γ (snd (cl s)) = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal ((upd (fst (cl s)) ∘ init) s)⟩ =m⇒ Normal t'"
    assume exec_c: "Γ⊢⟨c s t',Normal (return s t')⟩ =Suc m⇒ t"
    assume n: "n = Suc m"
    have "Γ⊢⟨Basic init,Normal s⟩ =m⇒ Normal (init s)"
      by (rule execn.Basic)
    from bdy exec_body
    have exec_callC:
      "Γ⊢⟨Call (snd (cl s)),Normal ((upd (fst (cl s)) ∘ init) s)⟩ =Suc m⇒ Normal t'"
      by (rule execn.Call)
    from execn.Seq [OF exec_upd [simplified n]exec_callC]
    have exec_closure: "Γ⊢ ⟨callClosure upd (cl s),Normal (init s)⟩ =n⇒ Normal t'"
      by (simp add: callClosure_def n)
    from cnvalidD [OF valid [rule_format] ctxt exec_closure init_P']
    have "t' ∈ Q'"
      by auto
    with R have "return s t' ∈ R s t'"
      by auto
    from cnvalidD [OF res [rule_format] ctxt exec_c [simplified n[symmetric]] this
         t_notin_F]
    show ?thesis
      by auto
  next
    fix bdy m t'
    assume bdy: "Γ (snd (cl s)) = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal ((upd (fst (cl s)) ∘ init) s)⟩ =m⇒ Abrupt t'"
    assume t: "t=Abrupt (return s t')"
    assume n: "n = Suc m"
    from bdy exec_body
    have exec_callC:
      "Γ⊢⟨Call (snd (cl s)),Normal ((upd (fst (cl s)) ∘ init) s)⟩ =Suc m⇒ Abrupt t'"
      by (rule execn.Call)
    from execn.Seq [OF exec_upd [simplified n] exec_callC]
    have exec_closure: "Γ⊢ ⟨callClosure upd (cl s),Normal (init s)⟩ =n⇒ Abrupt t'"
      by (simp add: callClosure_def n)

    from cnvalidD [OF valid [rule_format] ctxt exec_closure init_P']
    have "t' ∈ A'"
      by auto
    with A have "return s t' ∈ A"
      by auto
    with t show ?thesis
      by auto
  next
    fix bdy m f
    assume bdy: "Γ (snd (cl s)) = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal ((upd (fst (cl s)) ∘ init) s)⟩ =m⇒ Fault f"
    assume t: "t=Fault f"
    assume n: "n = Suc m"
    from bdy exec_body
    have exec_callC:
      "Γ⊢⟨Call (snd (cl s)),Normal ((upd (fst (cl s)) ∘ init) s)⟩ =Suc m⇒ Fault f"
      by (rule execn.Call)
    from execn.Seq [OF exec_upd [simplified n] exec_callC]
    have exec_closure: "Γ⊢ ⟨callClosure upd (cl s),Normal (init s)⟩ =n⇒ Fault f"
      by (simp add: callClosure_def n)
    from cnvalidD [OF valid [rule_format] ctxt exec_closure init_P'] t_notin_F t
    have False
      by auto
    thus ?thesis ..
  next
    fix bdy m
    assume bdy: "Γ (snd (cl s)) = Some bdy"
    assume exec_body: "Γ⊢⟨bdy,Normal ((upd (fst (cl s)) ∘ init) s)⟩ =m⇒ Stuck"
    assume t: "t=Stuck"
    assume n: "n = Suc m"
    from execn.Basic [where f="(upd (fst (cl s)))" and s="(init s)"]
    have exec_upd: "Γ⊢⟨Basic (upd (fst (cl s))),Normal (init s)⟩ =Suc m⇒
             Normal (((upd (fst (cl s))) ∘ init) s)"
      by auto
    from bdy exec_body
    have exec_callC:
      "Γ⊢⟨Call (snd (cl s)),Normal ((upd (fst (cl s)) ∘ init) s)⟩ =Suc m⇒ Stuck"
      by (rule execn.Call)
    from execn.Seq [OF exec_upd [simplified n] exec_callC]
    have exec_closure: "Γ⊢ ⟨callClosure upd (cl s),Normal (init s)⟩ =n⇒ Stuck"
      by (simp add: callClosure_def n)
    from cnvalidD [OF valid [rule_format] ctxt exec_closure init_P'] t_notin_F t
    have False
      by auto
    thus ?thesis ..
  next
    fix m
    assume no_bdy: "Γ (snd (cl s)) = None"
    assume t: "t=Stuck"
    assume n: "n = Suc m"
    from no_bdy
    have exec_callC:
      "Γ⊢⟨Call (snd (cl s)),Normal ((upd (fst (cl s)) ∘ init) s)⟩ =Suc m⇒ Stuck"
      by (rule execn.CallUndefined)
    from execn.Seq [OF exec_upd [simplified n]exec_callC]
    have exec_closure: "Γ⊢ ⟨callClosure upd (cl s),Normal (init s)⟩ =n⇒ Stuck"
      by (simp add: callClosure_def n)
    from cnvalidD [OF valid [rule_format] ctxt exec_closure init_P'] t_notin_F t
    have False
      by auto
    thus ?thesis ..
  qed
qed


lemma dynCallClosure:
assumes adapt: "P ⊆ {s. ∃P' Q' A'. Γ,Θ⊢⇘/F ⇙ P' (callClosure upd (cl s)) Q',A' ∧
                  init s ∈ P' ∧
                  (∀t ∈ Q'. return s t ∈ R s t) ∧
                  (∀t ∈ A'. return s t ∈ A)}"
assumes res: "∀s t. Γ,Θ⊢⇘/F⇙ (R s t) (c s t) Q,A"
shows
"Γ,Θ⊢⇘/F ⇙P (dynCallClosure init upd cl return c) Q,A"
  apply (rule hoare_complete')
  apply (rule allI)
  apply (rule dynCallClosure_sound [where R=R])
  using adapt
  apply (blast intro: hoare_cnvalid)
  using res
  apply (blast intro: hoare_cnvalid)
  done

lemma in_subsetD: "⟦P ⊆ P'; x ∈ P⟧ ⟹ x ∈ P'"
  by blast

lemma dynCallClosureFix:
assumes adapt: "P ⊆ {s. ∃Z. cl'=cl s ∧
                  init s ∈ P' Z ∧
                  (∀t ∈ Q' Z. return s t ∈ R s t) ∧
                  (∀t ∈ A' Z. return s t ∈ A)}"
assumes res: "∀s t. Γ,Θ⊢⇘/F⇙ (R s t) (c s t) Q,A"
assumes spec: "∀Z. Γ,Θ⊢⇘/F ⇙ (P' Z) (callClosure upd cl') (Q' Z),(A' Z)"
shows
"Γ,Θ⊢⇘/F ⇙P (dynCallClosure init upd cl return c) Q,A"
  apply (rule dynCallClosure [OF _ res])
  using adapt spec
  apply clarsimp
  apply (drule (1) in_subsetD)
  apply clarsimp
  apply (rule_tac x="P' Z" in exI)
  apply (rule_tac x="Q' Z" in exI)
  apply (rule_tac x="A' Z" in exI)
  apply blast
  done


lemma conseq_extract_pre:
             "⟦∀s ∈ P. Γ,Θ⊢⇘/F⇙ ({s}) c Q,A⟧
              ⟹
              Γ,Θ⊢⇘/F⇙ P c Q,A"
  apply (rule hoarep.Conseq)
  apply clarify
  apply (rule_tac x="{s}" in exI)
  apply (rule_tac x="Q" in exI)
  apply (rule_tac x="A" in exI)
  by simp



lemma app_closure_sound:
  assumes adapt: "P ⊆ {s. ∃P' Q' A'. ∀n. Γ,Θ⊨n:⇘/F⇙ P' (callClosure upd (e',p)) Q',A' ∧
                           upd x s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A}"
  assumes ap: "upd e = upd e' ∘ upd x"
  shows "Γ,Θ⊨n:⇘/F⇙ P (callClosure upd (e,p)) Q,A"
proof (rule cnvalidI)
  fix s t
  assume ctxt: "∀(P, p, Q, A)∈Θ. Γ⊨n:⇘/F⇙ P Call p Q,A"
  assume exec_e: "Γ⊢ ⟨callClosure upd (e, p),Normal s⟩ =n⇒ t"
  assume P: "s ∈ P"
  assume t: "t ∉ Fault ` F"
  from P adapt obtain P' Q' A'
    where
    valid: "∀n. Γ,Θ⊨n:⇘/F ⇙ P' (callClosure upd (e',p)) Q',A'" and
    init_P': "upd x s ∈ P'"  and
    Q: "Q' ⊆ Q" and
    A: "A' ⊆ A"
    by auto
  from exec_e [simplified callClosure_def] obtain s'
    where
    exec_e: "Γ⊢ ⟨Basic (upd (fst (e, p))),Normal s⟩ =n⇒ s'"and
    exec_p: "Γ⊢ ⟨Call (snd (e, p)),s'⟩ =n⇒ t"
    by cases
  from exec_e [simplified]
  have s': "s'=Normal (upd e s)"
    by cases simp
  from ap obtain s'' where
   s'': "upd x s = s''" and upd_e': "upd e' s''=upd e s"
    by auto
  from ap s' execn.Basic [where f="(upd (fst (e', p)))" and s="upd x s" and Γ=Γ]
  have exec_e': "Γ⊢ ⟨Basic (upd (fst (e', p))),Normal (upd x s)⟩ =n⇒ s'"
    by simp
  with exec_p
  have "Γ⊢ ⟨callClosure upd (e', p),Normal (upd x s)⟩ =n⇒ t"
    by (auto simp add: callClosure_def intro: execn.Seq)
  from cnvalidD [OF valid [rule_format] ctxt this init_P'] t Q A
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
    by auto
qed

lemma app_closure:
  assumes adapt: "P ⊆ {s. ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' (callClosure upd (e',p)) Q',A' ∧
                           upd x s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A}"
  assumes ap: "upd e = upd e' ∘ upd x"
  shows "Γ,Θ⊢⇘/F⇙ P (callClosure upd (e,p)) Q,A"
  apply (rule hoare_complete')
  apply (rule allI)
  apply (rule app_closure_sound [where x=x and e'=e', OF _ ap])
  using adapt
  apply (blast intro: hoare_cnvalid)
  done

lemma app_closure_spec:
  assumes adapt: "P ⊆ {s. ∃Z. upd x s ∈ P' Z ∧ Q' Z ⊆ Q ∧ A' Z ⊆ A}"
  assumes ap: "upd e = upd e' ∘ upd x"
  assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙ (P' Z) (callClosure upd (e',p)) (Q' Z),(A' Z)"
  shows "Γ,Θ⊢⇘/F⇙ P (callClosure upd (e,p)) Q,A"
  apply (rule app_closure [OF _ ap])
  apply clarsimp
  using adapt spec
  apply -
  apply (drule (1) in_subsetD)
  apply clarsimp
  apply (rule_tac x="P' Z" in exI)
  apply (rule_tac x="Q' Z" in exI)
  apply (rule_tac x="A' Z" in exI)
  apply blast
  done

text ‹Implementation of closures as association lists.›

definition "gen_upd var es s = foldl (λs (x,i). the (var x) i s) s es"
definition "ap es c ≡ (es@fst c,snd c)"

lemma gen_upd_app: "⋀es'. gen_upd var (es@es') = gen_upd var es' ∘ gen_upd var es"
  apply (induct es)
  apply  (rule ext)
  apply  (simp add: gen_upd_def)
  apply (rule ext)
  apply (simp add: gen_upd_def)
  done

lemma gen_upd_ap:
  "gen_upd var (fst (ap es (es',p))) = gen_upd var es' ∘ gen_upd var es"
  by (simp add: gen_upd_app ap_def)

lemma ap_closure:
  assumes adapt: "P ⊆ {s. ∃P' Q' A'. Γ,Θ⊢⇘/F⇙ P' (callClosure (gen_upd var) c) Q',A' ∧
                           gen_upd var es s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A}"
  shows "Γ,Θ⊢⇘/F⇙ P (callClosure (gen_upd var) (ap es c)) Q,A"
proof -
  obtain es' p where c: "c=(es',p)"
    by (cases c)
  have "gen_upd var (fst (ap es (es',p))) = gen_upd var es' ∘ gen_upd var es"
    by (simp add: gen_upd_ap)
  from app_closure [OF adapt [simplified c] this]
  show ?thesis
    by (simp add: c ap_def)
qed


lemma ap_closure_spec:
  assumes adapt: "P ⊆ {s. ∃Z. gen_upd var es s ∈ P' Z ∧ Q' Z ⊆ Q ∧ A' Z ⊆ A}"
  assumes spec: "∀Z. Γ,Θ⊢⇘/F⇙ (P' Z) (callClosure (gen_upd var) c) (Q' Z),(A' Z)"
  shows "Γ,Θ⊢⇘/F⇙ P (callClosure (gen_upd var) (ap es c)) Q,A"
proof -
  obtain es' p where c: "c=(es',p)"
    by (cases c)
  have "gen_upd var (fst (ap es (es',p))) = gen_upd var es' ∘ gen_upd var es"
    by (simp add: gen_upd_ap)
  from app_closure_spec [OF adapt [simplified c] this spec [simplified c]]
  show ?thesis
    by (simp add: c ap_def)
qed

end