Theory Gabow_GBG_Code
section ‹Code Generation for GBG Lasso Finding Algorithm\label{sec:gbg_code}›
theory Gabow_GBG_Code
imports
Gabow_GBG
Gabow_Skeleton_Code
CAVA_Automata.Automata_Impl
Find_Path_Impl
CAVA_Base.CAVA_Code_Target
begin
section ‹Autoref Setup›
locale impl_lasso_loc = igb_fr_graph G
+ fr_graph_impl_loc "⟨mrel,node_rel⟩igbg_impl_rel_eext" node_rel node_eq_impl node_hash_impl node_def_hash_size G_impl G
for mrel and node_rel and node_eq_impl node_hash_impl node_def_hash_size and G_impl and G :: "('q,'more) igb_graph_rec_scheme"
begin
lemma locale_this: "impl_lasso_loc mrel node_rel node_eq_impl node_hash_impl node_def_hash_size G_impl G"
by unfold_locales
context begin interpretation autoref_syn .
lemma [autoref_op_pat]:
"goinitial_impl ≡ OP goinitial_impl"
"ginitial_impl ≡ OP ginitial_impl"
"gpath_is_empty_impl ≡ OP gpath_is_empty_impl"
"gselect_edge_impl ≡ OP gselect_edge_impl"
"gis_on_stack_impl ≡ OP gis_on_stack_impl"
"gcollapse_impl ≡ OP gcollapse_impl"
"last_is_acc_impl ≡ OP last_is_acc_impl"
"ce_impl ≡ OP ce_impl"
"gis_done_impl ≡ OP gis_done_impl"
"gpush_impl ≡ OP gpush_impl"
"gpop_impl ≡ OP gpop_impl"
"goBrk_impl ≡ OP goBrk_impl"
"gto_outer_impl ≡ OP gto_outer_impl"
"go_is_done_impl ≡ OP go_is_done_impl"
"is_done_oimpl ≡ OP is_done_oimpl"
"go_is_no_brk_impl ≡ OP go_is_no_brk_impl"
by simp_all
end
abbreviation "gGSi_rel ≡ ⟨⟨nat_rel⟩bs_set_rel⟩as_rel ×⇩r GSi_rel"
abbreviation (in -) "ce_rel node_rel ≡ ⟨⟨node_rel⟩fun_set_rel ×⇩r ⟨node_rel⟩fun_set_rel⟩option_rel"
abbreviation "goGSi_rel ≡ ce_rel node_rel ×⇩r oGSi_rel"
end
section ‹Automatic Refinement›
context impl_lasso_loc
begin
schematic_goal goinitial_code_aux: "(?c,goinitial_impl)∈goGSi_rel"
unfolding goinitial_impl_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) goinitial_code
uses impl_lasso_loc.goinitial_code_aux
lemmas [autoref_rules] = goinitial_code.refine[OF locale_this]
term ginitial_impl
schematic_goal ginitial_code_aux:
"(?c,ginitial_impl)∈node_rel → goGSi_rel → gGSi_rel"
unfolding ginitial_impl_def[abs_def] initial_impl_def GS_initial_impl_def
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) ginitial_code uses impl_lasso_loc.ginitial_code_aux
lemmas [autoref_rules] = ginitial_code.refine[OF locale_this]
schematic_goal gpath_is_empty_code_aux:
"(?c,gpath_is_empty_impl)∈gGSi_rel→bool_rel"
unfolding gpath_is_empty_impl_def[abs_def] path_is_empty_impl_def
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gpath_is_empty_code
uses impl_lasso_loc.gpath_is_empty_code_aux
lemmas [autoref_rules] = gpath_is_empty_code.refine[OF locale_this]
term goBrk
schematic_goal goBrk_code_aux: "(?c,goBrk_impl)∈goGSi_rel→ce_rel node_rel"
unfolding goBrk_impl_def[abs_def] goBrk_impl_def
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) goBrk_code uses impl_lasso_loc.goBrk_code_aux
lemmas [autoref_rules] = goBrk_code.refine[OF locale_this]
thm autoref_itype(1)
term gto_outer_impl
schematic_goal gto_outer_code_aux:
"(?c,gto_outer_impl)∈ce_rel node_rel → gGSi_rel→goGSi_rel"
unfolding gto_outer_impl_def[abs_def] gto_outer_impl_def
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gto_outer_code
uses impl_lasso_loc.gto_outer_code_aux
lemmas [autoref_rules] = gto_outer_code.refine[OF locale_this]
term go_is_done_impl
schematic_goal go_is_done_code_aux:
"(?c,go_is_done_impl)∈node_rel → goGSi_rel → bool_rel"
unfolding go_is_done_impl_def[abs_def] is_done_oimpl_def
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) go_is_done_code
uses impl_lasso_loc.go_is_done_code_aux
lemmas [autoref_rules] = go_is_done_code.refine[OF locale_this]
schematic_goal go_is_no_brk_code_aux:
"(?c,go_is_no_brk_impl)∈goGSi_rel→bool_rel"
unfolding go_is_no_brk_impl_def[abs_def] go_is_no_brk_impl_def
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) go_is_no_brk_code
uses impl_lasso_loc.go_is_no_brk_code_aux
lemmas [autoref_rules] = go_is_no_brk_code.refine[OF locale_this]
schematic_goal gselect_edge_code_aux: "(?c,gselect_edge_impl)
∈ gGSi_rel → ⟨⟨node_rel⟩option_rel ×⇩r gGSi_rel⟩nres_rel"
unfolding gselect_edge_impl_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gselect_edge_code
uses impl_lasso_loc.gselect_edge_code_aux
lemmas [autoref_rules] = gselect_edge_code.refine[OF locale_this]
term gis_on_stack_impl
schematic_goal gis_on_stack_code_aux:
"(?c,gis_on_stack_impl)∈node_rel → gGSi_rel → bool_rel"
unfolding gis_on_stack_impl_def[abs_def] is_on_stack_impl_def[abs_def]
GS.is_on_stack_impl_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gis_on_stack_code
uses impl_lasso_loc.gis_on_stack_code_aux
lemmas [autoref_rules] = gis_on_stack_code.refine[OF locale_this]
term gcollapse_impl
schematic_goal gcollapse_code_aux: "(?c,gcollapse_impl)∈node_rel → gGSi_rel
→ ⟨gGSi_rel⟩nres_rel"
unfolding gcollapse_impl_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gcollapse_code
uses impl_lasso_loc.gcollapse_code_aux
lemmas [autoref_rules] = gcollapse_code.refine[OF locale_this]
schematic_goal last_is_acc_code_aux:
"(?c,last_is_acc_impl)∈gGSi_rel→⟨bool_rel⟩nres_rel"
unfolding last_is_acc_impl_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) last_is_acc_code
uses impl_lasso_loc.last_is_acc_code_aux
lemmas [autoref_rules] = last_is_acc_code.refine[OF locale_this]
schematic_goal ce_code_aux: "(?c,ce_impl)
∈gGSi_rel→⟨ce_rel node_rel ×⇩r gGSi_rel⟩nres_rel"
unfolding ce_impl_def[abs_def] on_stack_less_def[abs_def]
on_stack_ge_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) ce_code uses impl_lasso_loc.ce_code_aux
lemmas [autoref_rules] = ce_code.refine[OF locale_this]
schematic_goal gis_done_code_aux:
"(?c,gis_done_impl)∈node_rel→gGSi_rel→bool_rel"
unfolding gis_done_impl_def[abs_def] is_done_impl_def GS.is_done_impl_def
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gis_done_code uses impl_lasso_loc.gis_done_code_aux
lemmas [autoref_rules] = gis_done_code.refine[OF locale_this]
schematic_goal gpush_code_aux:
"(?c,gpush_impl)∈node_rel → gGSi_rel→gGSi_rel"
unfolding gpush_impl_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gpush_code uses impl_lasso_loc.gpush_code_aux
lemmas [autoref_rules] = gpush_code.refine[OF locale_this]
schematic_goal gpop_code_aux: "(?c,gpop_impl)∈gGSi_rel→⟨gGSi_rel⟩nres_rel"
unfolding gpop_impl_def[abs_def]
using [[autoref_trace_failed_id]]
by (autoref (trace,keep_goal))
concrete_definition (in -) gpop_code uses impl_lasso_loc.gpop_code_aux
lemmas [autoref_rules] = gpop_code.refine[OF locale_this]
schematic_goal find_ce_code_aux: "(?c,find_ce_impl)∈⟨ce_rel node_rel⟩nres_rel"
unfolding find_ce_impl_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (trace,keep_goal))
done
concrete_definition (in -) find_ce_code
uses impl_lasso_loc.find_ce_code_aux
lemmas [autoref_rules] = find_ce_code.refine[OF locale_this]
schematic_goal find_ce_tr_aux: "RETURN ?c ≤ find_ce_code node_eq_impl node_hash_impl node_def_hash_size G_impl"
unfolding
find_ce_code_def
ginitial_code_def
gpath_is_empty_code_def
gselect_edge_code_def
gis_on_stack_code_def
gcollapse_code_def
last_is_acc_code_def
ce_code_def
gis_done_code_def
gpush_code_def
gpop_code_def
apply refine_transfer
done
concrete_definition (in -) find_ce_tr for G_impl
uses impl_lasso_loc.find_ce_tr_aux
lemmas [refine_transfer] = find_ce_tr.refine[OF locale_this]
context begin interpretation autoref_syn .
lemma [autoref_op_pat]:
"find_ce_spec ≡ OP find_ce_spec"
by auto
end
theorem find_ce_autoref[autoref_rules]:
shows "(find_ce_code node_eq_impl node_hash_impl node_def_hash_size G_impl, find_ce_spec) ∈ ⟨ce_rel node_rel⟩nres_rel"
proof -
note find_ce_code.refine[OF locale_this, THEN nres_relD]
also note find_ce_impl_refine
also note find_ce_refine
also note find_ce_correct
finally show ?thesis by (auto intro: nres_relI)
qed
end
context impl_lasso_loc
begin
context begin interpretation autoref_syn .
lemma [autoref_op_pat]:
"reconstruct_reach ≡ OP reconstruct_reach"
"reconstruct_lasso ≡ OP reconstruct_lasso"
by auto
end
schematic_goal reconstruct_reach_code_aux:
shows "(?c, reconstruct_reach)∈⟨node_rel⟩fun_set_rel →
⟨node_rel⟩fun_set_rel →
⟨⟨node_rel⟩list_rel ×⇩r node_rel⟩nres_rel"
unfolding reconstruct_lasso_def[abs_def] reconstruct_reach_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition (in -) reconstruct_reach_code
uses impl_lasso_loc.reconstruct_reach_code_aux
lemmas [autoref_rules] = reconstruct_reach_code.refine[OF locale_this]
schematic_goal reconstruct_lasso_code_aux:
shows "(?c, reconstruct_lasso)∈⟨node_rel⟩fun_set_rel →
⟨node_rel⟩fun_set_rel →
⟨⟨node_rel⟩list_rel ×⇩r ⟨node_rel⟩list_rel⟩nres_rel"
unfolding reconstruct_lasso_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition (in -) reconstruct_lasso_code
uses impl_lasso_loc.reconstruct_lasso_code_aux
lemmas [autoref_rules] = reconstruct_lasso_code.refine[OF locale_this]
schematic_goal reconstruct_lasso_tr_aux:
"RETURN ?c ≤ reconstruct_lasso_code eqi hi dszi G_impl Vr Vl"
unfolding reconstruct_lasso_code_def reconstruct_reach_code_def
apply (refine_transfer (post))
done
concrete_definition (in -) reconstruct_lasso_tr for G_impl
uses impl_lasso_loc.reconstruct_lasso_tr_aux
lemmas [refine_transfer] = reconstruct_lasso_tr.refine[OF locale_this]
schematic_goal find_lasso_code_aux:
shows "(?c::?'c, find_lasso)∈?R"
unfolding find_lasso_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition (in -) find_lasso_code
uses impl_lasso_loc.find_lasso_code_aux
lemmas [autoref_rules] = find_lasso_code.refine[OF locale_this]
schematic_goal find_lasso_tr_aux:
"RETURN ?c ≤ find_lasso_code node_eq_impl node_hash_impl node_def_hash_size G_impl"
unfolding find_lasso_code_def
apply (refine_transfer (post))
done
concrete_definition (in -) find_lasso_tr for G_impl
uses impl_lasso_loc.find_lasso_tr_aux
lemmas [refine_transfer] = find_lasso_tr.refine[OF locale_this]
end
export_code find_lasso_tr checking SML
section ‹Main Correctness Theorem›
abbreviation fl_rel :: "_ ⇒ (_ × ('a list × 'a list) option) set" where
"fl_rel node_rel ≡ ⟨⟨node_rel⟩list_rel ×⇩r ⟨node_rel⟩list_rel⟩Relators.option_rel"
theorem find_lasso_tr_correct:
fixes Re and node_rel :: "('vi × 'v) set"
assumes A: "(G_impl,G)∈igbg_impl_rel_ext Re node_rel"
and node_eq_refine: "(node_eq_impl, (=)) ∈ node_rel → node_rel → bool_rel"
and node_hash: "is_bounded_hashcode node_rel node_eq_impl node_hash_impl"
and node_hash_def_size: "(is_valid_def_hm_size TYPE('vi) node_def_hash_size)"
assumes B: "igb_fr_graph G"
shows "RETURN (find_lasso_tr node_eq_impl node_hash_impl node_def_hash_size G_impl)
≤ ⇓(fl_rel node_rel) (igb_graph.find_lasso_spec G)"
proof -
from B interpret igb_fr_graph G .
have I: "impl_lasso_loc Re node_rel node_eq_impl node_hash_impl node_def_hash_size G_impl G"
apply unfold_locales
by fact+
then interpret impl_lasso_loc Re node_rel node_eq_impl node_hash_impl node_def_hash_size G_impl G .
note find_lasso_tr.refine[OF I]
also note find_lasso_code.refine[OF I, THEN nres_relD]
also note find_lasso_correct
finally show ?thesis .
qed
section ‹Autoref Setup for ‹igb_graph.find_lasso_spec››
text ‹Setup for Autoref, such that ‹igb_graph.find_lasso_spec›
can be used›
definition [simp]: "op_find_lasso_spec ≡ igb_graph.find_lasso_spec"
context begin interpretation autoref_syn .
lemma [autoref_op_pat]: "igb_graph.find_lasso_spec ≡ op_find_lasso_spec"
by simp
term op_find_lasso_spec
lemma [autoref_itype]:
"op_find_lasso_spec
::⇩i i_igbg Ie I →⇩i ⟨⟨⟨⟨I⟩⇩ii_list, ⟨I⟩⇩ii_list⟩⇩ii_prod⟩⇩ii_option⟩⇩ii_nres"
by simp
lemma find_lasso_spec_autoref[autoref_rules_raw]:
fixes Re and node_rel :: "('vi × 'v) set"
assumes GR: "SIDE_PRECOND (igb_fr_graph G)"
assumes eq: "GEN_OP node_eq_impl (=) (node_rel→node_rel→bool_rel)"
assumes hash: "SIDE_GEN_ALGO (is_bounded_hashcode node_rel node_eq_impl node_hash_impl)"
assumes hash_dsz: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('vi) node_def_hash_size)"
assumes Gi: "(G_impl,G)∈igbg_impl_rel_ext Re node_rel"
shows "(RETURN (find_lasso_tr node_eq_impl node_hash_impl node_def_hash_size G_impl),
(OP op_find_lasso_spec
::: igbg_impl_rel_ext Re node_rel → ⟨fl_rel node_rel⟩nres_rel)$G) ∈ ⟨fl_rel node_rel⟩nres_rel"
using find_lasso_tr_correct[OF Gi GEN_OP_D[OF eq] SIDE_GEN_ALGO_D[OF hash] SIDE_GEN_ALGO_D[OF hash_dsz]] using GR
apply (fastforce intro!: nres_relI)
done
end
end