Theory SM_Wrapup

theory SM_Wrapup
imports SM_Ample_Impl Stuttering_Equivalence.PLTL
begin

  export_code ty_program ltlc_next_free checking SML

  definition "vars_of_aprop e ≡ udvars_of_exp e ∪ gvars_of_exp e"
  definition "vars_of_ltlc φ ≡ ⋃ (vars_of_aprop ` atoms_ltlc φ)"

  lemma test_aprop_vars_cong:
    assumes "e ∈ atoms_ltlc φ"
    shows "test_aprop e (v |` vars_of_ltlc φ) ⟷ test_aprop e v"
  proof -
    have 1: "eval_exp e (⦇ local_state.variables = Map.empty ⦈,
      ⦇ global_state.variables = v |` vars_of_ltlc φ ⦈) =
      eval_exp e (⦇ local_state.variables = Map.empty ⦈, ⦇ global_state.variables = v ⦈)"
    proof (rule eval_dep_vars)
      show "gs_eq_on (vars_of_ltlc φ) ⦇ global_state.variables = v |` vars_of_ltlc φ ⦈
        ⦇ global_state.variables = v ⦈" by (simp add: eq_on_def)
      show "udvars_of_exp e ⊆ vars_of_ltlc φ"
        using assms vars_of_aprop_def vars_of_ltlc_def by blast
      show "gvars_of_exp e ⊆ vars_of_ltlc φ"
        using assms vars_of_aprop_def vars_of_ltlc_def by blast
    qed
    show ?thesis unfolding test_aprop_def 1 by rule
  qed

  context cprog
  begin

    sublocale ample_impl: sa "⦇ g_V = UNIV,
      g_E = ample_step_impl4_impl prog (comp_info_of prog) is_vis_var,
      g_V0 = {pid_init_gc_impl_impl prog (comp_info_of prog)},
      sa_L = pid_interp_gc_impl is_vis_var ⦈"
      for is_vis_var by unfold_locales auto

    theorem ample_reduction_correct: 
      assumes "ty_program prog"
      assumes NF: "ltlc_next_free φ"
      shows "
        (Collect (SM_LTL.ap_accept prog) ⊆ language_ltlc φ)
        ⟷
        (Collect (ample_impl.accept (λx. x∈vars_of_ltlc φ)) ⊆ language_ltlc φ)"
    proof safe
      interpret visible_prog prog "(λx. x∈vars_of_ltlc φ)"
        apply unfold_locales
        by fact
        
      {  
        fix w  
        assume 1: "(Collect (SM_LTL.ap_accept prog) ⊆ language_ltlc φ)"
        and 2: "ample_impl.accept (λx. x∈vars_of_ltlc φ) w"
        note t2 = 2[unfolded pid_init_gc_impl_impl ample_step_impl4_impl]
        from impl4_accept_subset[OF t2] obtain w' where 
          WEQ: "w=interp_gs o w'" and "ref_accept prog w'" 
          unfolding lv_accept_conv
          by blast
        hence "ap_accept prog (sm_props o global_state.variables o w')" 
          (is "ap_accept prog ?ww")
          unfolding ap_accept_def interp_gs_def[abs_def]
          by auto
        with 1 have "?ww ∈ language_ltlc φ" by blast
        moreover have "pw_eq_on (atoms_ltlc φ) w ?ww"
          apply (simp add: WEQ)
          unfolding pw_eq_on_def interp_gs_def[abs_def]
          unfolding sm_props_def[abs_def]
          by (auto simp: test_aprop_vars_cong)
        ultimately show "w ∈ language_ltlc φ" 
          unfolding language_ltlc_def
          by (auto simp: ltlc_eq_on)
      }
  
      {
        fix w
        assume 1: "Collect (ample_impl.accept (λx. x∈vars_of_ltlc φ)) ⊆ language_ltlc φ"
        and 2: "SM_LTL.ap_accept prog w"
        from 2 obtain w' where 
          WEQ: "w = (sm_props o global_state.variables o w')" 
          and ACC: "ref_accept prog w'"
          unfolding ap_accept_def by auto
        with lv_accept_conv[THEN iffD2] have ACC': "lv.sa.accept (interp_gs o w')"
          by (auto simp: interp_gs_def[abs_def])
          
        from impl4_accept_stuttering[OF ACC'] obtain ww where 
          E2: "interp_gs o w' ≈ ww" and "ample_impl.accept (λx. x∈vars_of_ltlc φ) ww"
          unfolding pid_init_gc_impl_impl ample_step_impl4_impl
          unfolding lv_accept_conv
          by blast
        hence L: "ww ∈ language_ltlc φ" using 1 by blast
        
        have E1: "pw_eq_on (atoms_ltlc φ) w (interp_gs o w')"
          apply (simp add: WEQ)
          unfolding pw_eq_on_def interp_gs_def[abs_def]
          unfolding sm_props_def[abs_def]
          by (auto simp: test_aprop_vars_cong)

        from ltlc_next_free_stutter_invariant[OF NF E2] L 
        have "interp_gs o w' ∈ language_ltlc φ" by (auto simp: language_ltlc_def)
        with ltlc_eq_on[OF E1] show "w∈language_ltlc φ" by (auto simp: language_ltlc_def)
      }
    qed

  end

end