theory TA_Simplify_Impl
imports GTT_RRn_Impl GTT_Compose_Impl
begin
notation fun_rel_syn (infixr "→⇩r" 60)
notation rel_ANNOT (infix ":::⇩r" 10)
definition ta_nat :: "('q :: compare_order, 'f) ta ⇒ (nat, 'f) ta nres" where
"ta_nat A = do {
qs ← op_set_to_list (ta_states A);
let qm = (map_of (zip qs [0..<length qs]) :::⇩r ⟨Id, Id⟩comp_rm_rel);
RETURN (fmap_states_ta (the ∘ qm) A)
}"
lemma ta_nat_sound:
"ta_nat A ≤ SPEC (λA'. gta_lang A = gta_lang A')"
proof -
have [simp]: "gta_lang (fmap_states_ta ((the ∘∘ map_of) (zip qs [0..<length qs])) A) = gta_lang A"
if "ta_states A = set qs" "distinct qs" for qs
using that unfolding gta_lang_def
by (subst fmap_ta) (auto simp: gta_lang_def_sym inj_on_def in_set_conv_nth)
show ?thesis unfolding ta_nat_def Let_def by refine_vcg auto
qed
lemma ta_nat_sound2:
"ta_nat A ≤ SPEC (λA'. RR2_spec A X ⟷ RR2_spec A' X)"
by (rule order.trans[OF ta_nat_sound]) (auto simp: RR2_spec_def)
lemma ta_nat_soundn:
"ta_nat A ≤ SPEC (λA'. RRn_spec n A X ⟷ RRn_spec n A' X)"
by (rule order.trans[OF ta_nat_sound]) (auto simp: RRn_spec_def)
lemma (in ord) rbt_bulkload_conv_aux:
"id ord.rbt_bulkload (<) = rbt_bulkload" by simp
lemmas rbt_bulkload_conv = rbt_bulkload_conv_aux[unfolded id_def]
lemma rbt_bulkload_autoref [autoref_rules]:
assumes "PREFER_id (K :: (_ :: compare_order) rel)"
assumes "PREFER_id V"
shows "(rbt_comp_bulkload compare, map_of) ∈ ⟨K ×⇩r V⟩list_rel →⇩r ⟨K, V⟩comp_rm_rel"
using assms by (refine_vcg) (auto simp: rbt_map_rel_def rbt_map_rel'_def lt_of_comp_post_simp
compare_order_class.ord_defs rbt_lookup_into_class br_def rbt_lookup_rbt_bulkload rbt_comp_bulkload
comparator_compare rbt_bulkload_conv)
schematic_goal ta_nat_impl:
assumes [autoref_rules]: "(A', A) ∈ dflt_ta_rel"
notes [autoref_rules] = ta_eps_ref' FORCE_id[of _ the] FORCE_id[of _ upt] FORCE_id[of _ zip]
shows "(?f, ta_nat A) ∈ ⟨dflt_ta_rel⟩nres_rel"
unfolding ta_nat_def fmap_states_ta_def[folded ta.make_def] push_in_let_conv comp_def
by (autoref_monadic (plain))
concrete_definition ta_nat_impl uses ta_nat_impl
end