theory GTT_RRn_Impl
imports GTT_RRn GTT_Impl TA.Tree_Automata_Autoref_Setup
begin
context begin interpretation autoref_syn .
lemma op_map_lookup_pat: "(m :: 'k ⇀ 'v) k ≡ op_map_lookup $ k $ m" by simp
end
lemma image_impl:
fixes f :: "'a :: compare ⇒ 'b :: compare"
shows "(RBT_Impl.ord.rbt_bulkload (comp2lt compare_res) ∘ map (λx. (f x, ())) ∘ RBT_Impl.keys, λX. f ` X)
∈ ⟨Id⟩comp_rs_rel → ⟨Id⟩comp_rs_rel"
proof -
have bar: "set_to_map ((λx. (x, f x)) ` S) = (λx. if x ∈ S then Some (f x) else None)" for f S
by (fastforce simp: set_to_map_def Eps_Opt_def)
have foo: "map_of (map (λx. (x, f x)) xs) = set_to_map ((λx. (x, f x)) ` set xs)" for f xs
unfolding bar by (induct xs) auto
interpret linorder "comp2le compare_res" "comp2lt compare_res"
using compare_to_eq_linorder eq_linorder_class_conv by blast
show ?thesis using foo[of "λ_. ()" "map f _"]
by (auto simp: map2set_rel_def rbt_map_rel_def rbt_map_rel'_def in_br_conv set_to_map_dom image_def
eq_linorder_class_conv[symmetric] compare_to_eq_linorder inj_on_def comp_def
rbt_lookup_rbt_bulkload rbt_lookup_keys[symmetric] distinct_map
intro!: linorder.is_rbt_rbtreeify[of "comp2le compare_res"] arg_cong[of _ _ set_to_map])
qed
lemma rbt_lookup_into_class: "ord.rbt_lookup (<) = RBT_Impl.rbt_lookup"
by (simp add: ord.rbt_lookup_def RBT_Impl.rbt_lookup_def)
lemma list_to_rbt:
"(RBT_Impl.rbt_bulkload ∘ map (λx :: _ :: compare_order. (x, ())), id) ∈ ⟨Id⟩list_set_rel → ⟨Id⟩comp_rs_rel"
proof -
{ fix xs X assume "(xs, X) ∈ ⟨Id⟩list_set_rel"
then have "map_of (map (λx. (x, ())) xs) x = (if x ∈ X then Some () else None)" for x
by (auto simp: list_set_rel_def in_br_conv comp_def map_of_eq_None_iff)
} note [simp] = ext[OF this]
show ?thesis by (auto simp: map2set_rel_def rbt_map_rel_def rbt_map_rel'_def in_br_conv
rbt_lookup_into_class lt_of_comp_post_simp ord_defs rbt_lookup_rbt_bulkload
intro!: relcompI[of _ "λx. if x ∈ _ then Some () else None"] split: if_splits)
qed
lemma ta_eps_ref':
"((λ(_,_,E,_,_,_,_,_). RBT_Impl.rbt_bulkload (map (λk. (k, ())) E)), ta_eps) ∈ dflt_ta_rel → ⟨Id ×⇩r Id⟩comp_rs_rel"
using list_to_rbt by (auto simp: dflt_ta_rel_def dest: fun_relD)
schematic_goal [autoref_rules]:
notes ta_eps_ref'[autoref_rules]
shows "(?f, ta_states) ∈ dflt_ta_rel → ⟨Id⟩comp_rs_rel"
unfolding ta_states_def r_states_def
by (autoref (trace, keep_goal) phases: id_op rel_inf fix_rel trans)
lemma [autoref_rules]:
"(map_ta_rule, map_ta_rule) ∈ (R → R') → (S → S') → ⟨S, R⟩ta_rule_rel → ⟨S', R'⟩ta_rule_rel"
using param_map[of R R'] by (auto simp: fun_relD ta_rule_rel_def dest: fun_relD)
lemma set_comprehension_aux:
"⋀h X. {h f ps p |f ps p. f ps → p ∈ X} = case_ta_rule h ` X"
"⋀h X Y. {h f ps p g qs q|f ps p g qs q. f ps → p ∈ X ∧ g qs → q ∈ Y} =
(λ(r, r'). case_ta_rule (case_ta_rule h r) r') ` (X × Y)"
"⋀h X. {h p p' |p p'. (p, p') ∈ X} = (λ(p, p'). h p p') ` X"
"⋀h X Y. {h p p' q |p q p'. (p, p') ∈ X ∧ q ∈ Y} = (λ((p, p'), q). h p p' q) ` (X × Y)"
"⋀h X Y. {h p q q' |p q q'. p ∈ X ∧ (q, q') ∈ Y} = (λ(p, (q, q')). h p q q') ` (X × Y)"
"⋀h X. {h q |q. q ∈ X} = h ` X"
by (fastforce intro: rev_image_eqI split: ta_rule.splits)+
lemma param_zip_fill:
"(zip_fill, zip_fill) ∈ ⟨R⟩list_rel → ⟨S⟩list_rel → ⟨⟨R⟩option_rel ×⇩r ⟨S⟩option_rel⟩list_rel"
apply (refine_vcg)
subgoal for xs xs' ys ys'
by (induct xs arbitrary: ys xs' ys'; case_tac ys)
(auto simp: zip_fill_code elim!: list_relE intro!: param_map[THEN fun_relD, THEN fun_relD])
done
schematic_goal GTT_to_RR2_ref:
notes [autoref_rules] = param_replicate param_zip_fill
shows "(?f, (λA. (ta_final A, ta_rules A, ta_eps A)) ∘∘ GTT_to_RR2)
∈ ⟨Id ×⇩r Id⟩comp_rs_rel → dflt_ta_rel ×⇩r dflt_ta_rel →
(⟨⟨⟨Id⟩option_rel ×⇩r ⟨Id⟩option_rel⟩option_rel⟩comp_rs_rel ×⇩r
⟨⟨⟨Id⟩option_rel ×⇩r ⟨Id⟩option_rel,⟨⟨Id⟩option_rel ×⇩r ⟨Id⟩option_rel⟩option_rel⟩ta_rule_rel⟩comp_rs_rel ×⇩r
⟨⟨⟨Id⟩option_rel ×⇩r ⟨Id⟩option_rel⟩option_rel ×⇩r ⟨⟨Id⟩option_rel ×⇩r ⟨Id⟩option_rel⟩option_rel⟩list_set_rel)"
unfolding GTT_to_RR2_def[abs_def] parallel_closure_automaton_def GTT_to_RR2_root_def pair_automaton_def
ta_make_simps ta.simps ta.make_def comp_def map_prod_def
unfolding set_comprehension_aux image_comp comp_def
by autoref
concrete_definition GTT_to_RR2_impl uses GTT_to_RR2_ref
end