Theory ComposeEx

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

Copyright (C) 2006-2008 Norbert Schirmer
*)
theory ComposeEx imports Compose "../Vcg" "../HeapList" begin


record globals_list =
  next_' :: "ref ⇒ ref"

record state_list = "globals_list state" +
  p_'    :: "ref"
  sl_q_'    :: "ref"
  r_'    :: "ref"


procedures Rev(p|sl_q) =
      "´sl_q :== Null;;
       WHILE ´p ≠ Null
       DO
         ´r :== ´p;; ⦃´p ≠ Null⦄⟼ ´p :== ´p→´next;;
         ⦃´r ≠ Null⦄⟼ ´r→´next :== ´sl_q;; ´sl_q :== ´r
       OD"
print_theorems



lemma (in Rev_impl)
 Rev_modifies:
  "∀σ. Γ⊢⇘/UNIV ⇙{σ} ´sl_q :== PROC Rev(´p) {t. t may_only_modify_globals σ in [next]}"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (vcg spec=modifies)
done

lemma (in Rev_impl) shows
 Rev_spec:
  "∀Ps. Γ⊢ ⦃List ´p ´next Ps⦄ ´sl_q :== PROC Rev(´p) ⦃List ´sl_q ´next (rev Ps)⦄"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (hoare_rule anno =
       "´sl_q :== Null;;
       WHILE ´p ≠ Null INV ⦃∃Ps' Qs'. List ´p ´next Ps' ∧ List ´sl_q ´next Qs' ∧
                             set Ps' ∩ set Qs' = {} ∧
                             rev Ps' @ Qs' = rev Ps⦄
        DO
         ´r :== ´p;; ⦃´p ≠ Null⦄⟼´p :== ´p→´next;;
         ⦃´r ≠ Null⦄⟼ ´r→´next :== ´sl_q;; ´sl_q :== ´r
       OD" in HoarePartial.annotateI)
apply vcg
apply   clarsimp
apply  fastforce
apply clarsimp
done

declare [[names_unique = false]]

record globals =
  strnext_'   :: "ref ⇒ ref"
  chr_'    :: "ref ⇒ char"

  qnext_' :: "ref ⇒ ref"
  cont_'   :: "ref ⇒ int"
record state = "globals state" +
  str_'  :: "ref"
  queue_':: "ref"
  q_'    :: "ref"
  r_'    :: "ref"


definition project_globals_str:: "globals ⇒ globals_list"
  where "project_globals_str g = ⦇next_' = strnext_' g⦈"

definition project_str:: "state ⇒ state_list"
where
"project_str s =
  ⦇globals = project_globals_str (globals s),
   state_list.p_' = str_' s, sl_q_' = q_' s, state_list.r_' = r_' s⦈"

definition inject_globals_str::
  "globals ⇒ globals_list ⇒ globals"
where
  "inject_globals_str G g =
   G⦇strnext_' := next_' g⦈"

definition "inject_str"::"state ⇒ state_list ⇒ state" where
"inject_str S s = S⦇globals := inject_globals_str (globals S) (globals s),
                str_' := state_list.p_' s, q_' := sl_q_' s,
                r_' := state_list.r_' s⦈"

lemma globals_inject_project_str_commutes:
  "inject_globals_str G (project_globals_str G) = G"
  by (simp add: inject_globals_str_def project_globals_str_def)

lemma inject_project_str_commutes: "inject_str S (project_str S) = S"
  by (simp add: inject_str_def project_str_def globals_inject_project_str_commutes)

lemma globals_project_inject_str_commutes:
  "project_globals_str (inject_globals_str G g) = g"
  by (simp add: inject_globals_str_def project_globals_str_def)

lemma project_inject_str_commutes: "project_str (inject_str S s) = s"
  by (simp add: inject_str_def project_str_def globals_project_inject_str_commutes)

lemma globals_inject_str_last:
  "inject_globals_str (inject_globals_str G g) g' = inject_globals_str G g'"
  by (simp add: inject_globals_str_def)

lemma inject_str_last:
  "inject_str (inject_str S s) s' = inject_str S s'"
  by (simp add: inject_str_def globals_inject_str_last)

definition
  "lift⇩e = (λΓ p. map_option (lift⇩c project_str inject_str) (Γ p))"
print_locale lift_state_space
interpretation ex: lift_state_space project_str inject_str
  "xstate_map project_str" lift⇩e "lift⇩c project_str inject_str"
  "lift⇩f project_str inject_str" "lift⇩s project_str"
  "lift⇩r project_str inject_str"
  apply -
  apply       (rule lift_state_space.intro)
  apply       (rule project_inject_str_commutes)
  apply      simp
  apply     simp
  apply    (simp add: lift⇩e_def)
  apply   simp
  apply  simp
  apply simp
  done

interpretation ex: lift_state_space_ext project_str inject_str
  "xstate_map project_str" lift⇩e "lift⇩c project_str inject_str"
  "lift⇩f project_str inject_str" "lift⇩s project_str"
  "lift⇩r project_str inject_str"

(*  project_str "inject_str" _ lift⇩e *)
apply -
apply intro_locales [1]
  apply (rule lift_state_space_ext_axioms.intro)
  apply  (rule inject_project_str_commutes)
  apply (rule inject_str_last)
apply (simp_all add: lift⇩e_def)
  done

(*
  apply (intro_locales)
  apply (rule lift_state_space_ext_axioms.intro)
  apply  (rule inject_project_str_commutes)
  apply (rule inject_str_last)
  done
*)

(*
declare lift_set_def [simp] project_def [simp] project_globals_def [simp]
*)
lemmas Rev_lift_spec = ex.lift_hoarep' [OF Rev_impl.Rev_spec,simplified lift⇩s_def
 project_str_def project_globals_str_def,simplified, of _ "''Rev''"]
print_theorems


definition "𝒩 p' p = (if p=''Rev'' then p' else '''')"


procedures RevStr(str|q) = "rename (𝒩 RevStr_'proc)
                (lift⇩c project_str inject_str (Rev_body.Rev_body))"


lemmas Rev_lift_spec' =
  Rev_lift_spec [of "[''Rev''↦Rev_body.Rev_body]" ,
     simplified Rev_impl_def Rev_clique_def,simplified]
thm Rev_lift_spec'


lemma Rev_lift_spec'':
  "∀Ps. lift⇩e [''Rev'' ↦ Rev_body.Rev_body]
       ⊢ ⦃List ´str ´strnext Ps⦄ Call ''Rev'' ⦃List ´q ´strnext (rev Ps)⦄"
  by (rule Rev_lift_spec')

lemma (in RevStr_impl) 𝒩_ok:
"∀p bdy. (lift⇩e [''Rev'' ↦ Rev_body.Rev_body]) p = Some bdy ⟶
     Γ (𝒩 RevStr_'proc p) = Some (rename (𝒩 RevStr_'proc) bdy)"
apply (insert RevStr_impl)
apply (auto simp add: RevStr_body_def lift⇩e_def 𝒩_def)
done

context RevStr_impl
begin
 thm hoare_to_hoare_rename'[OF _ Rev_lift_spec'', OF 𝒩_ok,
  simplified 𝒩_def, simplified ]
end

lemmas (in RevStr_impl) RevStr_spec =
  hoare_to_hoare_rename' [OF _ Rev_lift_spec'', OF 𝒩_ok,
  simplified 𝒩_def, simplified ]


lemma (in RevStr_impl) RevStr_spec':
"∀Ps. Γ⊢ ⦃List ´str ´strnext Ps⦄ ´q :== PROC RevStr(´str)
          ⦃List ´q ´strnext (rev Ps)⦄"
  by (rule RevStr_spec)

lemmas Rev_modifies' =
  Rev_impl.Rev_modifies [of "[''Rev''↦Rev_body.Rev_body]", simplified Rev_impl_def,
   simplified]
thm Rev_modifies'

context RevStr_impl
begin
lemmas RevStr_modifies' =
  hoare_to_hoare_rename' [OF _ ex.hoare_lift_modifies' [OF Rev_modifies'],
         OF 𝒩_ok, of "''Rev''", simplified 𝒩_def Rev_clique_def,simplified]
end


lemma (in RevStr_impl) RevStr_modifies:
"∀σ. Γ⊢⇘/UNIV ⇙{σ} ´str :== PROC RevStr(´str)
  {t. t may_only_modify_globals σ in [strnext]}"
apply (rule allI)
apply (rule HoarePartialProps.ConseqMGT [OF RevStr_modifies'])
apply (clarsimp simp add:
  lift⇩s_def mex_def meq_def
  project_str_def inject_str_def project_globals_str_def inject_globals_str_def)
apply blast
done

end