Theory PDS_Code

theory PDS_Code
  imports PDS "Deriving.Derive"
begin

global_interpretation pds: PDS_with_P_automata Δ F_ctr_loc F_ctr_loc_st
  for Δ :: "('ctr_loc::{enum, linorder}, 'label::{finite, linorder}) rule set"
  and F_ctr_loc :: "('ctr_loc) set"
  and F_ctr_loc_st :: "('state::finite) set"
  defines pre_star = "PDS_with_P_automata.pre_star_exec Δ"
  and pre_star_check = "PDS_with_P_automata.pre_star_exec_check Δ"
  and inits = "PDS_with_P_automata.inits"
  and finals = "PDS_with_P_automata.finals F_ctr_loc F_ctr_loc_st"
  and accepts = "PDS_with_P_automata.accepts F_ctr_loc F_ctr_loc_st"
  and language = "PDS_with_P_automata.lang F_ctr_loc F_ctr_loc_st"
  and step_starp = "rtranclp (LTS.step_relp (PDS.transition_rel Δ))"
  and accepts_pre_star_check = "PDS_with_P_automata.accept_pre_star_exec_check Δ F_ctr_loc F_ctr_loc_st"
  .

global_interpretation inter: Intersection_P_Automaton
  initial_automaton Init "finals initial_F_ctr_loc initial_F_ctr_loc_st"
  "pre_star Δ final_automaton" "finals final_F_ctr_loc final_F_ctr_loc_st"
  for Δ :: "('ctr_loc::{enum, linorder}, 'label::{finite, linorder}) rule set"
  and initial_automaton :: "(('ctr_loc, 'state::finite, 'label) state, 'label) transition set"
  and initial_F_ctr_loc :: "'ctr_loc set"
  and initial_F_ctr_loc_st :: "'state set"
  and final_automaton :: "(('ctr_loc, 'state, 'label) state, 'label) transition set"
  and final_F_ctr_loc :: "'ctr_loc set"
  and final_F_ctr_loc_st :: "'state set"
  defines nonempty_inter = "P_Automaton.nonempty
    (inters initial_automaton (pre_star Δ final_automaton))
    ((λp. (Init p, Init p)))
    (inters_finals (finals initial_F_ctr_loc initial_F_ctr_loc_st)
                   (finals final_F_ctr_loc final_F_ctr_loc_st))"
  .

definition "check Δ I IF IF_st F FF FF_st =
  (if pds.inits ⊆ LTS.srcs F then Some (nonempty_inter Δ I IF IF_st F FF FF_st) else None)"

lemma check_None: "check Δ I IF IF_st F FF FF_st = None ⟷ ¬ (inits ⊆ LTS.srcs F)"
  unfolding check_def by auto

lemma check_Some: "check Δ I IF IF_st F FF FF_st = Some b ⟷
  (inits ⊆ LTS.srcs F ∧ b = (∃p w p' w'.
     (p, w) ∈ language IF IF_st I ∧
     (p', w') ∈ language FF FF_st F ∧
     step_starp Δ (p, w) (p', w')))"
  unfolding check_def nonempty_inter_def P_Automaton.nonempty_def
    inter.lang_aut_alt inter.inters_lang
    pds.lang_aut_lang
  by (auto 0 5 simp: pds.pre_star_exec_lang_correct pds.pre_star_def image_iff
    elim!: bexI[rotated])

declare P_Automaton.mark.simps[code]

export_code check checking SML

end