Theory SM.SM_Visible

section ‹Preparing Partial Order Reduction›
theory SM_Visible
imports "../RefPoint/SM_LTL" Rename_Cfg
begin

  section ‹Visible Part of State›

  locale visible_prog = well_typed_prog +
    fixes is_vis_var :: "ident  bool"
  begin
    abbreviation "vis_vars  Collect is_vis_var"

    definition interp_gs :: "global_state  exp set" where
      "interp_gs gs  sm_props (global_state.variables gs |` vis_vars)"
  
    definition interp_gc :: "global_config  exp set" where
      "interp_gc gc  interp_gs (global_config.state gc)"
    
    sublocale lv: Gen_Scheduler'_linit
      cfgc la_en' la_ex' 
      "{init_gc}" interp_gc .

    lemma lv_accept_conv: "lv.sa.accept w 
       (w'. w=interp_gs o w'  ref_accept prog w')"
      unfolding lih'_accept_eq[symmetric]
      unfolding lih'.sa.accept_def lv.sa.accept_def
      unfolding lih'.sa.is_run_def
      unfolding lv.sa.is_run_def
      apply simp
      unfolding interp_gc_def[abs_def]
      by fastforce

  end
end