Quelle  ComposeEx.thy

(*
    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\<^sub>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 "N p' p = (if p=''Rev'' then p' else '''')"


procedures RevStr(str|q) = "rename (N 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) N_ok:
"∀p bdy. (lift_e [''Rev'' ↦ Rev_body.Rev_body]) p = Some bdy ⟶
     Γ (N RevStr_'proc p) = Some (rename (N RevStr_'proc) bdy)"
apply (insert RevStr_impl)
apply (auto simp add: RevStr_body_def lift_{e_def} N_def)
done

context RevStr_impl
begin
 thm hoare_to_hoare_rename'[OF _ Rev_lift_spec'', OF N_ok,
  simplified N_def, simplified ]
end

lemmas (in RevStr_impl) RevStr_spec =
  hoare_to_hoare_rename' [OF _ Rev_lift_spec'', OF N_ok,
  simplified N_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 N_ok, of "''Rev''", simplified N_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