Theory SM.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