Theory Mojmir_Rabin_Impl

theory Mojmir_Rabin_Impl
imports Mojmir_Rabin

section

theory Mojmir_Rabin_Impl
imports Main
begin

― ‹Ranking functions are stored as lists sorted ascending by the state rank›

fun init ::
where

fun nxt ::
where

― ‹Recompute the rank from the list›

fun rk ::
where

― ‹Instead of computing the whole sets for fail, merge, and succeed, we define filters (a.k.a. characteristic functions)›

fun fail_filt ::
where

fun merge_filt ::
where

fun succeed_filt ::
where

subsubsection

lemma nxt_run_distinct:

by (cases n; simp del: remdups_fwd.simps; metis (no_types) remdups_fwd_distinct)

lemma nxt_run_reverse_step:
fixes Σ δ q0 w
defines
assumes
assumes
shows
using assms(2-3) unfolding r_def run.simps nxt.simps remdups_fwd_set by auto

lemma nxt_run_sink_free:

by (induction n) (simp_all add: semi_mojmir_def.sink_def del: remdups_fwd.simps, blast)

subsubsection

lemma rk_bounded:

by (simp add: Let_def) (metis index_conv_size_if_notin index_less_size_conv option.distinct(1) option.inject)

lemma rk_facts:

using rk_bounded by (simp add: index_size_conv)+

lemma rk_split:

by (induction xs) auto

lemma rk_split_card:

using rk_split by (metis length_remdups_card_conv remdups_id_iff_distinct)

lemma rk_split_card_takeWhile:
assumes
assumes
shows
proof -
obtain ys zs where  and
using assms by (blast dest: split_list_first)
moreover
hence  and
using takeWhile_foo assms by (simp, fast)
ultimately
show ?thesis
using rk_split_card by metis
qed

lemma take_rk:
assumes
shows
(is )
using assms
proof (induction i arbitrary: xs)
case (Suc i)
thus ?case
proof (induction xs)
case (Cons x xs)
have
by simp
also
have
using Cons by simp
finally
show ?case
by force
qed simp
qed simp

lemma drop_rk:
assumes
shows
proof -
have  (is )
using rk_facts(2)[of _ xs] by blast
moreover
have
and
by auto
moreover
have
and
by (metis assms append_take_drop_id inf_sup_aci(1,5) distinct_append set_append)+
ultimately
show ?thesis
using take_rk[OF assms] by blast
qed

subsubsection

lemma (in semi_mojmir) nxt_run_configuration:
defines
shows
proof (induction n arbitrary: q)
case (Suc n)
thus ?case
proof (cases )
case True
{
assume
hence
using r_def nxt_run_sink_free by metis
moreover
obtain q' where  and
using  nxt_run_reverse_step[OF _ ] unfolding r_def by blast
hence  and
unfolding configuration_step_eq[OF True] Suc using True  by auto
}
moreover
{
assume  and
then obtain q' where  and
unfolding configuration_step_eq[OF True] by blast
moreover
hence
using  sink_rev_step assms by blast
ultimately
have
unfolding Suc by blast
hence
using
unfolding r_def run.simps set_filter comp_def remdups_fwd_set set_map set_append image_def
unfolding r_def[symmetric] by auto
}
ultimately
show ?thesis
by blast
qed (insert assms, auto simp add: r_def sink_def)
qed (insert assms, auto simp add: r_def sink_def)

lemma (in semi_mojmir) nxt_run_sorted:
defines
shows
proof (induction n)
case (Suc n)
let ?f_n =
let ?f_Suc_n =
let ?step =

have
proof -
fix q qs p ps
assume
then obtain zs zs' zs'' where step_def:
and
and
and
and
and
unfolding remdups_fwd.simps remdups_fwd_split_exact_iff remdups_fwd_split_exact_iff[where ?ys = , simplified] insert_commute
by auto
hence
and  unfolding remdups_fwd_acc_empty[symmetric] by auto
hence
by simp
hence
using step_def by simp
hence  and
unfolding set_map set_filter by blast+

show
proof (cases )
case True
hence  and q_def:
using step_def unfolding sink_def by simp+
hence
using   unfolding  sink_def by simp
hence
using nxt_run_configuration bounded_w unfolding set_map set_filter r_def sink_def init.simps by blast
hence  using assms
unfolding  using configuration_step_eq_q0 by blast
hence
using assms  by force
moreover
have
using   image_set unfolding filter_map_split_iff[of  ]
by (metis (no_types, lifting) Un_insert_right    append_Nil2 insert_iff insert_subset list.simps(15) mem_Collect_eq set_append set_filter)
hence
using nxt_run_configuration unfolding r_def by auto
hence
using configuration_step assms by blast
hence
using assms oldest_token_bounded[of q ]
by (simp del: configuration.simps)
ultimately
show
by presburger
next
case False
hence X:
using step_def unfolding map_append filter_append sink_def apply simp
by (metis (no_types, lifting) butlast.simps(2) list.distinct(1) butlast_append append_is_Nil_conv butlast_snoc)
obtain qs' sq' sp' ps' ps'' where r_def':
and 1:
and 2:
and 3:
and
and
using X  unfolding filter_map_split_iff by (blast)
hence 21:
and 41:
by (metis filter_set image_set list.set(1) list.simps(15))+
from 21 obtain q' where  and  and
using sink_rev_step(2)[OF , of _ n] by fastforce
from 41 obtain p' where  and  and
using sink_rev_step(2)[OF , of _ n] by fastforce
from Suc have
unfolding r_def' map_append sorted_append set_append set_map using   by auto
moreover
{
have
using nxt_run_configuration option.distinct(1) r_def r_def'    set_append
unfolding init.simps oldest_token.simps by (metis UnCI)
moreover
hence
using  by (metis oldest_token.simps option.distinct(1) configuration_step_non_empty)
ultimately
obtain x y where x_def:
and y_def:
by blast
moreover
hence  and
using oldest_token_bounded push_down_oldest_token_token_run assms by blast+
moreover
hence
using  by (rule token_run_step)
ultimately
have
using oldest_token_monotonic_Suc assms by blast
moreover
{
have
using  unfolding [symmetric] set_map set_filter apply simp using  by blast
moreover
{
obtain us vs where 1:  and  and
using    unfolding filter_eq_Cons_iff by auto
moreover
hence
by (metis UnE filter_empty_conv)
hence
using  by blast
ultimately
have
using 1   by (fastforce dest: split_list elim: map_splitE)
}
ultimately
have
using nxt_run_configuration[of _ n]  sink_rev_step
unfolding r_def'[unfolded r_def] set_append
by blast
moreover
have
using x_def using Suc unfolding r_def' map_append sorted_append set_append set_map  using
apply (simp del: oldest_token.simps) by fastforce
moreover
have
using x_def by simp
moreover
have
using assms by auto
ultimately
have
by fastforce
}
hence
unfolding configuration_step_eq_unified using
by (cases ; auto)
hence
using y_def Min.boundedI configuration_finite using push_down_oldest_token_configuration by presburger
ultimately
have
using x_def y_def by fastforce
}
moreover
{
have
using nxt_run_configuration oldest_token.simps option.distinct(1) r_def r_def'    set_append
unfolding init.simps by (metis UnCI)
moreover
hence
using  by (metis oldest_token.simps option.distinct(1) configuration_step_non_empty)
ultimately
obtain x y where x_def:
and y_def:
by blast
moreover
hence  and
using oldest_token_bounded push_down_oldest_token_token_run assms by blast+
moreover
hence
using  assms token_run_step by simp
ultimately
have
using oldest_token_monotonic_Suc assms by blast
moreover
{
have
using   unfolding 1[symmetric] 2[symmetric] 3[symmetric] set_map set_filter by blast
moreover
{
obtain us vs where 1:  and  and
using  unfolding filter_eq_Cons_iff by auto
moreover
hence
by (metis UnE filter_empty_conv)
hence
using  by blast
ultimately
have
using 1   by (fastforce dest: split_list elim: map_splitE)
}
ultimately
have
using nxt_run_configuration[of _ n]  [THEN sink_rev_step(2)] unfolding r_def'[unfolded r_def] set_append
by blast
moreover
have
using x_def using Suc unfolding r_def' map_append sorted_append set_append set_map  using
apply (simp del: oldest_token.simps)  by fastforce
moreover
have
using x_def by simp
moreover
have
using assms  by auto
ultimately
have
by fastforce
}
hence
unfolding configuration_step_eq_unified using
by (cases ; auto)
hence
using y_def Min.boundedI configuration_finite using push_down_oldest_token_configuration  by presburger
ultimately
have
using x_def y_def by fastforce
}
ultimately
show ?thesis
by presburger
qed
qed
hence
by (auto elim: map_splitE simp del: remdups_fwd.simps)
hence
using sorted_pre by metis
thus ?case
by (simp add: r_def sink_def)
qed (simp add: r_def)

lemma (in semi_mojmir) nxt_run_senior_states:
defines
assumes
assumes
shows
(is )
proof (rule set_eqI, rule)
fix q' assume q'_def:
then obtain x y where  and  and
using senior_states.simps using assms by blast
hence
by fastforce
moreover
hence  and
using q'_def option.distinct(1)
oldest_token.simps using assms by (force, metis)
hence  and
using nxt_run_configuration assms by blast+
moreover
have
unfolding r_def using nxt_run_distinct by fast
ultimately
obtain r' r'' r''' where r_alt_def:
using sorted_list[OF _ _ nxt_run_sorted] assms unfolding r_def by presburger
hence
by simp
thus
using  takeWhile_distinct[of  q r''' q'] unfolding r_alt_def by simp
next
fix q' assume q'_def:
moreover
hence
by (blast dest: set_takeWhileD)+
hence 5:
using nxt_run_configuration assms by simp
have
using nxt_run_configuration assms by blast+
ultimately
obtain  r' r'' r''' where r_alt_def:
using takeWhile_split by metis
have
unfolding r_def using nxt_run_distinct by fast
have 1:
using nxt_run_sorted[of n, unfolded r_def[symmetric]] assms
unfolding r_alt_def map_append list.map
unfolding sorted_append by (simp del: oldest_token.simps)
have
using  r_alt_def by auto
moreover
have 2:  and 3:
using assms  nxt_run_configuration by force+
ultimately
have 4:
by (metis oldest_token_equal option.collapse)

show
using 1 2 3 4 5 assms by fastforce
qed

lemma (in semi_mojmir) nxt_run_state_rank:

by (cases , unfold state_rank.simps)
(metis nxt_run_senior_states rk_split_card_takeWhile nxt_run_distinct nxt_run_configuration, metis nxt_run_configuration rk_facts(1))

lemma (in semi_mojmir) nxt_foldl_state_rank:

unfolding nxt_run_state_rank run_foldl ..

lemma (in semi_mojmir) nxt_run_step_run:

using nxt_run_state_rank state_rank_step_foldl[unfolded run_foldl[symmetric]] unfolding comp_def by presburger

definition (in semi_mojmir_def) QE
where

lemma (in semi_mojmir) finite_Q:

proof -
{
fix i fix w ::
assume
then interpret : semi_mojmir Σ δ q0 w
using finite_reach finite_Σ by (unfold_locales, blast)
have  (is )
using ℌ.nxt_run_configuration by auto
also
have  (is )
unfolding reach_def token_run.simps using  by fastforce
finally
have  .
}
hence
unfolding QE_def reach_def by blast
hence
using finite_reach by (blast dest: finite_subset)
moreover
have
unfolding QE_def reach_def using nxt_run_distinct by fastforce
ultimately
show
using set_list by auto
qed

lemma (in mojmir_to_rabin_def) filt_equiv:

by (simp add: failR_def succeedR_def mergeR_def del: rk.simps; metis (no_types, lifting) option.sel rk_facts(2))+

lemma fail_filt_eq:

unfolding mojmir_to_rabin_def.filt_equiv(1)[where y' = y] by simp

lemma merge_filt_eq:

unfolding mojmir_to_rabin_def.filt_equiv(3)[where y' = y] by simp

lemma succeed_filt_eq:

unfolding mojmir_to_rabin_def.filt_equiv(2)[where y' = y] by simp

theorem (in mojmir_to_rabin) rabin_accept_iff_rabin_list_accept_rank:

(is )
proof -
have
using wellformed_ℛ finite_Σ finite_reacht by fast
moreover
have
using finite_Q finite_Σ finite_reacht by (auto simp add: QE_def)
moreover
have
using nxt_run_step_run by auto
moreover
note bounded_w filt_equiv
ultimately
show ?thesis
by (intro accepting_pairR_abstract) auto
qed

subsection

fun mojmir_to_rabin_exec
where

subsection

― ‹Setup missing equations for code generator›
declare semi_mojmir_def.sink_def [code]

― ‹Drop computation of length by different code equation›
fun index_option ::
where

|

declare rk.simps [code del]

lemma rk_eq_index_option [code]:

proof -
have A:
and B:
by (induction xs) (auto, metis add_Suc_right)
thus ?thesis
proof (cases )
case True
moreover
hence
using A[OF True, of 0] by simp
ultimately
show ?thesis
unfolding rk.simps by (metis (mono_tags, lifting) B True index_less_size_conv less_irrefl option.collapse)
qed simp
qed

― ‹Check Code Export›
export_code init nxt fail_filt succeed_filt merge_filt mojmir_to_rabin_exec checking

lemma (in mojmir) max_rank_card:
assumes
shows
unfolding max_rank_def QL_reach[OF finite_reach[unfolded ]]
by (simp add: Set.filter_def set_diff_eq assms(1))

theorem (in mojmir_to_rabin) exec_correct:
assumes
shows  (is )
proof -
have F1:
using finite_Q by (simp add: QE_def)
hence F2:
using finite_Σ by (rule finite_reacht)

let ?δ' =
have δ'_Def:
using δL_reach[OF F2[unfolded assms]] unfolding  assms  by simp

have 3:
unfolding assms mojmir_to_rabin_exec.simps Let_def fst_conv snd_conv set_map δ'_Def[unfolded assms] max_rank_card[OF assms, symmetric]
unfolding assms[symmetric] Set.filter_def by auto

have
using mojmir_accept_iff_rabin_accept by blast

moreover

have
unfolding acceptR_def fst_conv snd_conv using rabin_accept_iff_rabin_list_accept_rank by blast

moreover

have
apply (subst acceptR_restrict[OF bounded_w])
unfolding 3[unfolded mojmir_to_rabin_exec.simps Let_def snd_conv, symmetric] assms[symmetric] mojmir_to_rabin_exec.simps Let_def unfolding assms δ'_Def[unfolded assms]
unfolding acceptR_LTS[OF bounded_w[unfolded assms], symmetric, unfolded assms] by simp

ultimately

show ?thesis
by blast
qed

end