Theory LTL_to_GBA_impl
section ‹Refinement to Efficient Code›
theory LTL_to_GBA_impl
imports
LTL_to_GBA
Deriving.Compare_Instances
CAVA_Automata.Automata_Impl
CAVA_Base.CAVA_Code_Target
begin
subsection ‹Parametricity Setup Boilerplate›
subsubsection ‹LTL Formulas›
derive linorder ltlr
inductive_set ltlr_rel for R where
"(True_ltlr, True_ltlr) ∈ ltlr_rel R"
| "(False_ltlr, False_ltlr) ∈ ltlr_rel R"
| "(a,a')∈R ⟹ (Prop_ltlr a,Prop_ltlr a') ∈ ltlr_rel R"
| "(a,a')∈R ⟹ (Nprop_ltlr a,Nprop_ltlr a') ∈ ltlr_rel R"
| "⟦(a,a')∈ltlr_rel R; (b,b')∈ltlr_rel R⟧
⟹ (And_ltlr a b,And_ltlr a' b') ∈ ltlr_rel R"
| "⟦(a,a')∈ltlr_rel R; (b,b')∈ltlr_rel R⟧
⟹ (Or_ltlr a b,Or_ltlr a' b') ∈ ltlr_rel R"
| "⟦(a,a')∈ltlr_rel R⟧ ⟹ (Next_ltlr a,Next_ltlr a') ∈ ltlr_rel R"
| "⟦(a,a')∈ltlr_rel R; (b,b')∈ltlr_rel R⟧
⟹ (Until_ltlr a b,Until_ltlr a' b') ∈ ltlr_rel R"
| "⟦(a,a')∈ltlr_rel R; (b,b')∈ltlr_rel R⟧
⟹ (Release_ltlr a b,Release_ltlr a' b') ∈ ltlr_rel R"
lemmas ltlr_rel_induct[induct set]
= ltlr_rel.induct[simplified relAPP_def[of ltlr_rel, symmetric]]
lemmas ltlr_rel_cases[cases set]
= ltlr_rel.cases[simplified relAPP_def[of ltlr_rel, symmetric]]
lemmas ltlr_rel_intros
= ltlr_rel.intros[simplified relAPP_def[of ltlr_rel, symmetric]]
inductive_simps ltlr_rel_left_simps[simplified relAPP_def[of ltlr_rel, symmetric]]:
"(True_ltlr,z) ∈ ltlr_rel R"
"(False_ltlr,z) ∈ ltlr_rel R"
"(Prop_ltlr p, z) ∈ ltlr_rel R"
"(Nprop_ltlr p, z) ∈ ltlr_rel R"
"(And_ltlr a b, z) ∈ ltlr_rel R"
"(Or_ltlr a b, z) ∈ ltlr_rel R"
"(Next_ltlr a, z) ∈ ltlr_rel R"
"(Until_ltlr a b, z) ∈ ltlr_rel R"
"(Release_ltlr a b, z) ∈ ltlr_rel R"
lemma ltlr_rel_sv[relator_props]:
assumes SV: "single_valued R"
shows "single_valued (⟨R⟩ltlr_rel)"
proof (intro single_valuedI allI impI)
fix x y z
assume "(x, y) ∈ ⟨R⟩ltlr_rel" "(x, z) ∈ ⟨R⟩ltlr_rel"
then show "y=z"
apply (induction arbitrary: z)
apply (simp (no_asm_use) only: ltlr_rel_left_simps
| blast intro: single_valuedD[OF SV])+
done
qed
lemma ltlr_rel_id[relator_props]: "⟦ R = Id ⟧ ⟹ ⟨R⟩ltlr_rel = Id"
proof (intro equalityI subsetI, clarsimp_all)
fix a b
assume "(a,b)∈⟨Id⟩ltlr_rel"
then show "a=b"
by induction auto
next
fix a
show "(a,a)∈⟨Id⟩ltlr_rel"
by (induction a) (auto intro: ltlr_rel_intros)
qed
lemma ltlr_rel_id_simp[simp]: "⟨Id⟩ltlr_rel = Id" by (rule ltlr_rel_id) simp
consts i_ltlr :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of ltlr_rel i_ltlr]
thm ltlr_rel_intros[no_vars]
lemma ltlr_con_param[param, autoref_rules]:
"(True_ltlr, True_ltlr) ∈ ⟨R⟩ltlr_rel"
"(False_ltlr, False_ltlr) ∈ ⟨R⟩ltlr_rel"
"(Prop_ltlr, Prop_ltlr) ∈ R → ⟨R⟩ltlr_rel"
"(Nprop_ltlr, Nprop_ltlr) ∈ R → ⟨R⟩ltlr_rel"
"(And_ltlr, And_ltlr) ∈ ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel"
"(Or_ltlr, Or_ltlr) ∈ ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel"
"(Next_ltlr, Next_ltlr) ∈ ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel"
"(Until_ltlr, Until_ltlr) ∈ ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel"
"(Release_ltlr, Release_ltlr) ∈ ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel"
by (auto intro: ltlr_rel_intros)
lemma case_ltlr_param[param, autoref_rules]:
"(case_ltlr,case_ltlr) ∈ Rv → Rv → (R → Rv)
→ (R → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv)
→ (⟨R⟩ltlr_rel → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv) → ⟨R⟩ltlr_rel → Rv"
apply (clarsimp)
apply (case_tac ai, simp_all add: ltlr_rel_left_simps)
apply (clarsimp_all)
apply parametricity+
done
lemma rec_ltlr_param[param, autoref_rules]:
"(rec_ltlr,rec_ltlr) ∈ Rv → Rv → (R → Rv)
→ (R → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv → Rv → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv → Rv → Rv)
→ (⟨R⟩ltlr_rel → Rv → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv → Rv → Rv)
→ (⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → Rv → Rv → Rv)
→ ⟨R⟩ltlr_rel → Rv"
proof (clarsimp, goal_cases)
case prems: 1
from prems(10)
show ?case
apply (induction)
using prems(1-9)
apply simp_all
apply parametricity+
done
qed
lemma case_ltlr_mono[refine_mono]:
assumes "φ = True_ltlr ⟹ a≤a'"
assumes "φ = False_ltlr ⟹ b≤b'"
assumes "⋀p. φ = Prop_ltlr p ⟹ c p≤c' p"
assumes "⋀p. φ = Nprop_ltlr p ⟹ d p≤d' p"
assumes "⋀μ ν. φ = And_ltlr μ ν ⟹ e μ ν≤e' μ ν"
assumes "⋀μ ν. φ = Or_ltlr μ ν ⟹ f μ ν≤f' μ ν"
assumes "⋀μ. φ = Next_ltlr μ ⟹ g μ≤g' μ"
assumes "⋀μ ν. φ = Until_ltlr μ ν ⟹ h μ ν≤h' μ ν"
assumes "⋀μ ν. φ = Release_ltlr μ ν ⟹ i μ ν≤i' μ ν"
shows "case_ltlr a b c d e f g h i φ ≤ case_ltlr a' b' c' d' e' f' g' h' i' φ"
using assms
apply (cases φ)
apply simp_all
done
primrec ltlr_eq where
"ltlr_eq eq True_ltlr f ⟷ (case f of True_ltlr ⇒ True | _ ⇒ False)"
| "ltlr_eq eq False_ltlr f ⟷ (case f of False_ltlr ⇒ True | _ ⇒ False)"
| "ltlr_eq eq (Prop_ltlr p) f ⟷ (case f of Prop_ltlr p' ⇒ eq p p' | _ ⇒ False)"
| "ltlr_eq eq (Nprop_ltlr p) f ⟷ (case f of Nprop_ltlr p' ⇒ eq p p' | _ ⇒ False)"
| "ltlr_eq eq (And_ltlr μ ν) f
⟷ (case f of And_ltlr μ' ν' ⇒ ltlr_eq eq μ μ' ∧ ltlr_eq eq ν ν' | _ ⇒ False)"
| "ltlr_eq eq (Or_ltlr μ ν) f
⟷ (case f of Or_ltlr μ' ν' ⇒ ltlr_eq eq μ μ' ∧ ltlr_eq eq ν ν' | _ ⇒ False)"
| "ltlr_eq eq (Next_ltlr φ) f
⟷ (case f of Next_ltlr φ' ⇒ ltlr_eq eq φ φ' | _ ⇒ False)"
| "ltlr_eq eq (Until_ltlr μ ν) f
⟷ (case f of Until_ltlr μ' ν' ⇒ ltlr_eq eq μ μ' ∧ ltlr_eq eq ν ν' | _ ⇒ False)"
| "ltlr_eq eq (Release_ltlr μ ν) f
⟷ (case f of
Release_ltlr μ' ν' ⇒ ltlr_eq eq μ μ' ∧ ltlr_eq eq ν ν'
| _ ⇒ False)"
lemma ltlr_eq_autoref[autoref_rules]:
assumes EQP: "(eq,(=)) ∈ R → R → bool_rel"
shows "(ltlr_eq eq, (=)) ∈ ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → bool_rel"
proof (intro fun_relI)
fix μ' μ ν' ν
assume "(μ',μ)∈⟨R⟩ltlr_rel" and "(ν',ν)∈⟨R⟩ltlr_rel"
then show "(ltlr_eq eq μ' ν', μ=ν)∈bool_rel"
apply (induction arbitrary: ν' ν)
apply (erule ltlr_rel_cases, simp_all) []
apply (erule ltlr_rel_cases, simp_all) []
apply (erule ltlr_rel_cases,
simp_all add: EQP[THEN fun_relD, THEN fun_relD, THEN IdD]) []
apply (erule ltlr_rel_cases,
simp_all add: EQP[THEN fun_relD, THEN fun_relD, THEN IdD]) []
apply (rotate_tac -1)
apply (erule ltlr_rel_cases, simp_all) []
apply (rotate_tac -1)
apply (erule ltlr_rel_cases, simp_all) []
apply (rotate_tac -1)
apply (erule ltlr_rel_cases, simp_all) []
apply (rotate_tac -1)
apply (erule ltlr_rel_cases, simp_all) []
apply (rotate_tac -1)
apply (erule ltlr_rel_cases, simp_all) []
done
qed
lemma ltlr_dflt_cmp[autoref_rules_raw]:
assumes "PREFER_id R"
shows
"(dflt_cmp (≤) (<), dflt_cmp (≤) (<))
∈ ⟨R⟩ltlr_rel → ⟨R⟩ltlr_rel → comp_res_rel"
using assms
by simp
type_synonym
node_name_impl = node_name
abbreviation (input) "node_name_rel ≡ Id :: (node_name_impl×node_name) set"
lemma case_ltlr_gtransfer:
assumes
"γ ai ≤ a"
"γ bi ≤ b"
"⋀a. γ (ci a) ≤ c a"
"⋀a. γ (di a) ≤ d a"
"⋀ltlr1 ltlr2. γ (ei ltlr1 ltlr2) ≤ e ltlr1 ltlr2"
"⋀ltlr1 ltlr2. γ (fi ltlr1 ltlr2) ≤ f ltlr1 ltlr2"
"⋀ltlr. γ (gi ltlr) ≤ g ltlr"
"⋀ltlr1 ltlr2. γ (hi ltlr1 ltlr2) ≤ h ltlr1 ltlr2"
"⋀ltlr1 ltlr2. γ (iiv ltlr1 ltlr2) ≤ i ltlr1 ltlr2"
shows "γ (case_ltlr ai bi ci di ei fi gi hi iiv φ)
≤ (case_ltlr a b c d e f g h i φ)"
apply (cases φ)
apply (auto intro: assms)
done
lemmas [refine_transfer]
= case_ltlr_gtransfer[where γ=nres_of] case_ltlr_gtransfer[where γ=RETURN]
lemma [refine_transfer]:
assumes
"ai ≠ dSUCCEED"
"bi ≠ dSUCCEED"
"⋀a. ci a ≠ dSUCCEED"
"⋀a. di a ≠ dSUCCEED"
"⋀ltlr1 ltlr2. ei ltlr1 ltlr2 ≠ dSUCCEED"
"⋀ltlr1 ltlr2. fi ltlr1 ltlr2 ≠ dSUCCEED"
"⋀ltlr. gi ltlr ≠ dSUCCEED"
"⋀ltlr1 ltlr2. hi ltlr1 ltlr2 ≠ dSUCCEED"
"⋀ltlr1 ltlr2. iiv ltlr1 ltlr2 ≠ dSUCCEED"
shows "case_ltlr ai bi ci di ei fi gi hi iiv φ ≠ dSUCCEED"
apply (cases φ)
apply (simp_all add: assms)
done
subsubsection ‹Nodes›
record 'a node_impl =
name_impl :: node_name_impl
incoming_impl :: "(node_name_impl,unit) RBT_Impl.rbt"
new_impl :: "'a frml list"
old_impl :: "'a frml list"
next_impl :: "'a frml list"
definition node_rel where node_rel_def_internal: "node_rel Re R ≡ {(
⦇ name_impl = namei,
incoming_impl = inci,
new_impl = newi,
old_impl = oldi,
next_impl = nexti,
… = morei
⦈,
⦇ name = name,
incoming = inc,
new=new,
old=old,
next = next,
… = more
⦈ ) | namei name inci inc newi new oldi old nexti next morei more.
(namei,name)∈node_name_rel
∧ (inci,inc)∈⟨node_name_rel⟩dflt_rs_rel
∧ (newi,new)∈⟨⟨R⟩ltlr_rel⟩lss.rel
∧ (oldi,old)∈⟨⟨R⟩ltlr_rel⟩lss.rel
∧ (nexti,next)∈⟨⟨R⟩ltlr_rel⟩lss.rel
∧ (morei,more)∈Re
}"
lemma node_rel_def: "⟨Re,R⟩node_rel = {(
⦇ name_impl = namei,
incoming_impl = inci,
new_impl = newi,
old_impl = oldi,
next_impl = nexti,
… = morei
⦈,
⦇ name = name,
incoming = inc,
new=new,
old=old,
next = next,
… = more
⦈ ) | namei name inci inc newi new oldi old nexti next morei more.
(namei,name)∈node_name_rel
∧ (inci,inc)∈⟨node_name_rel⟩dflt_rs_rel
∧ (newi,new)∈⟨⟨R⟩ltlr_rel⟩lss.rel
∧ (oldi,old)∈⟨⟨R⟩ltlr_rel⟩lss.rel
∧ (nexti,next)∈⟨⟨R⟩ltlr_rel⟩lss.rel
∧ (morei,more)∈Re
}" by (simp add: node_rel_def_internal relAPP_def)
lemma node_rel_sv[relator_props]:
"single_valued Re ⟹ single_valued R ⟹ single_valued (⟨Re,R⟩node_rel)"
apply (rule single_valuedI)
apply (simp add: node_rel_def)
apply (auto
dest: single_valuedD lss.rel_sv[OF ltlr_rel_sv] map2set_rel_sv[OF ahm_rel_sv]
dest: single_valuedD[
OF map2set_rel_sv[OF rbt_map_rel_sv[OF single_valued_Id single_valued_Id]]
])
done
consts i_node :: "interface ⇒ interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of node_rel i_node]
lemma [autoref_rules]: "(node_impl_ext, node_ext) ∈
node_name_rel
→ ⟨node_name_rel⟩dflt_rs_rel
→ ⟨⟨R⟩ltlr_rel⟩lss.rel
→ ⟨⟨R⟩ltlr_rel⟩lss.rel
→ ⟨⟨R⟩ltlr_rel⟩lss.rel
→ Re
→ ⟨Re,R⟩node_rel"
unfolding node_rel_def
by auto
lemma [autoref_rules]:
"(node_impl.name_impl_update,node.name_update)
∈ (node_name_rel → node_name_rel) → ⟨Re,R⟩node_rel → ⟨Re,R⟩node_rel"
"(node_impl.incoming_impl_update,node.incoming_update)
∈ (⟨node_name_rel⟩dflt_rs_rel → ⟨node_name_rel⟩dflt_rs_rel)
→ ⟨Re,R⟩node_rel
→ ⟨Re,R⟩node_rel"
"(node_impl.new_impl_update,node.new_update)
∈ (⟨⟨R⟩ltlr_rel⟩lss.rel → ⟨⟨R⟩ltlr_rel⟩lss.rel) → ⟨Re,R⟩node_rel → ⟨Re,R⟩node_rel"
"(node_impl.old_impl_update,node.old_update)
∈ (⟨⟨R⟩ltlr_rel⟩lss.rel → ⟨⟨R⟩ltlr_rel⟩lss.rel) → ⟨Re,R⟩node_rel → ⟨Re,R⟩node_rel"
"(node_impl.next_impl_update,node.next_update)
∈ (⟨⟨R⟩ltlr_rel⟩lss.rel → ⟨⟨R⟩ltlr_rel⟩lss.rel) → ⟨Re,R⟩node_rel → ⟨Re,R⟩node_rel"
"(node_impl.more_update,node.more_update)
∈ (Re → Re) → ⟨Re,R⟩node_rel → ⟨Re,R⟩node_rel"
unfolding node_rel_def
by (auto dest: fun_relD)
term name
lemma [autoref_rules]:
"(node_impl.name_impl,node.name)∈⟨Re,R⟩node_rel → node_name_rel"
"(node_impl.incoming_impl,node.incoming)
∈ ⟨Re,R⟩node_rel → ⟨node_name_rel⟩dflt_rs_rel"
"(node_impl.new_impl,node.new)∈⟨Re,R⟩node_rel → ⟨⟨R⟩ltlr_rel⟩lss.rel"
"(node_impl.old_impl,node.old)∈⟨Re,R⟩node_rel → ⟨⟨R⟩ltlr_rel⟩lss.rel"
"(node_impl.next_impl,node.next)∈⟨Re,R⟩node_rel → ⟨⟨R⟩ltlr_rel⟩lss.rel"
"(node_impl.more, node.more)∈⟨Re,R⟩node_rel → Re"
unfolding node_rel_def by auto
subsection ‹Massaging the Abstract Algorithm›
text ‹
In a first step, we do some refinement steps on the abstract data structures,
with the goal to make the algorithm more efficient.
›
subsubsection ‹Creation of the Nodes›
text ‹
In the expand-algorithm, we replace nested conditionals by case-distinctions,
and slightly stratify the code.
›
abbreviation (input) "expand2 exp n ns φ n1 nx1 n2 ≡ do {
(nm, nds) ← exp (
n⦇
new := insert n1 (new n),
old := insert φ (old n),
next := nx1 ∪ next n ⦈,
ns);
exp (n⦇ name := nm, new := n2 ∪ new n, old := {φ} ∪ old n ⦈, nds)
}"
definition "expand_aimpl ≡ REC⇩T (λexpand (n,ns).
if new n = {} then (
if (∃n'∈ns. old n' = old n ∧ next n' = next n) then
RETURN (name n, upd_incoming n ns)
else do {
ASSERT (n ∉ ns);
ASSERT (name n ∉ name`ns);
expand (⦇
name=expand_new_name (name n),
incoming={name n},
new=next n,
old={},
next={} ⦈,
insert n ns)
}
) else do {
φ ← SPEC (λx. x∈(new n));
let n = n⦇ new := new n - {φ} ⦈;
case φ of
prop⇩r(q) ⇒
if nprop⇩r(q)∈old n then RETURN (name n, ns)
else expand (n⦇ old := {φ} ∪ old n ⦈, ns)
| nprop⇩r(q) ⇒
if prop⇩r(q)∈old n then RETURN (name n, ns)
else expand (n⦇ old := {φ} ∪ old n ⦈, ns)
| true⇩r ⇒ expand (n⦇ old := {φ} ∪ old n ⦈, ns)
| false⇩r ⇒ RETURN (name n, ns)
| ν and⇩r μ ⇒ expand (n⦇
new := insert ν (insert μ (new n)),
old := {φ} ∪ old n,
next := next n ⦈, ns)
| X⇩r ν ⇒ expand
(n⦇ new := new n, old := {φ} ∪ old n, next := insert ν (next n) ⦈, ns)
| μ or⇩r ν ⇒ expand2 expand n ns φ μ {} {ν}
| μ U⇩r ν ⇒ expand2 expand n ns φ μ {φ} {ν}
| μ R⇩r ν ⇒ expand2 expand n ns φ ν {φ} {μ,ν}
}
)"
lemma expand_aimpl_refine:
fixes n_ns :: "('a node × _)"
defines "R ≡ Id ∩ {(_,(n,ns)). ∀n'∈ns. n > name n'}"
defines "R' ≡ Id ∩ {(_,(n,ns)). ∀n'∈ns. name n > name n'}"
assumes [refine]: "(n_ns',n_ns)∈R'"
shows "expand_aimpl n_ns' ≤ ⇓R (expand⇩T n_ns)"
using [[goals_limit = 1]]
proof -
have [relator_props]: "single_valued R"
by (auto simp add: R_def intro: single_valuedI)
have [relator_props]: "single_valued R'"
by (auto simp add: R'_def intro: single_valuedI)
{
fix n :: "'a node" and ns and n' ns'
assume "((n', ns'), (n, ns)) ∈ R'"
then have "(RETURN (name n', ns') ≤ ⇓ R (RETURN (name n, ns)))"
by (auto simp: R_def R'_def pw_le_iff refine_pw_simps)
} note aux = this
show ?thesis
unfolding expand_aimpl_def expand⇩T_def
apply refine_rcg
apply (simp add: R_def R'_def)
apply (simp add: R_def R'_def)
apply (auto simp add: R_def R'_def upd_incoming_def) []
apply (auto simp add: R_def R'_def upd_incoming_def) []
apply (auto simp add: R_def R'_def upd_incoming_def) []
apply rprems
apply (auto simp: R'_def expand_new_name_def) []
apply (simp add: R'_def)
apply (auto split: ltlr.split) []
apply (fastforce simp: R_def R'_def) []
apply (fastforce simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (auto simp: R_def R'_def) []
apply (refine_rcg, rprems, (fastforce simp: R_def R'_def)+) []
apply (fastforce simp: R'_def) []
apply (refine_rcg, rprems, (fastforce simp: R_def R'_def)+) []
apply (refine_rcg, rprems, (fastforce simp: R_def R'_def)+) []
done
qed
thm create_graph_def
definition "create_graph_aimpl φ = do {
(_, nds) ←
expand_aimpl
(⦇name = expand_new_name expand_init, incoming = {expand_init},
new = {φ}, old = {}, next = {}⦈,
{});
RETURN nds
}"
lemma create_graph_aimpl_refine: "create_graph_aimpl φ ≤ ⇓Id (create_graph⇩T φ)"
unfolding create_graph_aimpl_def create_graph⇩T_def
apply (refine_rcg expand_aimpl_refine)
apply auto
done
subsubsection ‹Creation of GBA from Nodes›
text ‹
We summarize creation of the GBA and renaming of the nodes into one step
›
lemma create_name_gba_alt: "create_name_gba φ = do {
nds ← create_graph⇩T φ;
ASSERT (nds_invars nds);
RETURN (gba_rename_ext (λ_. ()) name (create_gba_from_nodes φ nds))
}"
proof -
have [simp]: "⋀nds. g_V (create_gba_from_nodes φ nds) = nds"
by (auto simp: create_gba_from_nodes_def)
show ?thesis
unfolding create_name_gba_def create_gba_def
by simp
qed
text ‹In the following, we implement the componenents of the
renamed GBA separately.
›
text ‹\paragraph{Successor Function}›
definition "build_succ nds =
FOREACH
nds (λq' s.
FOREACH
(incoming q') (λqn s.
if qn=expand_init then
RETURN s
else
RETURN (s(qn ↦ insert (name q') (the_default {} (s qn))))
) s
) Map.empty"
lemma build_succ_aux1:
assumes [simp]: "finite nds"
assumes [simp]: "⋀q. q∈nds ⟹ finite (incoming q)"
shows "build_succ nds ≤ SPEC (λr. r = (λqn.
dflt_None_set {qn'. ∃q'.
q'∈nds ∧ qn' = name q' ∧ qn∈incoming q' ∧ qn≠expand_init
}))"
unfolding build_succ_def
apply (refine_rcg refine_vcg
FOREACH_rule[where
I="λit s. s = (λqn. dflt_None_set {qn'. ∃q'. q'∈nds-it ∧ qn' = name q'
∧ qn∈incoming q' ∧ qn≠expand_init })"])
apply (simp_all add: dflt_None_set_def) [2]
apply (rename_tac q' it s)
apply (rule_tac I="λit2 s. s =
(λqn. dflt_None_set (
{qn'. ∃q'. q'∈nds-it ∧ qn' = name q' ∧ qn∈incoming q' ∧ qn≠expand_init } ∪
{qn' . qn'=name q' ∧ qn∈incoming q' - it2 ∧ qn≠expand_init} ))"
in FOREACH_rule)
apply auto []
apply (simp_all add: dflt_None_set_def)
apply (refine_rcg refine_vcg)
apply (auto simp: dflt_None_set_def intro!: ext) []
apply (rule ext, (auto) [])+
done
lemma build_succ_aux2:
assumes NINIT: "expand_init ∉ name`nds"
assumes CL: "⋀nd. nd∈nds ⟹ incoming nd ⊆ insert expand_init (name`nds)"
shows
"(λqn. dflt_None_set
{qn'. ∃q'. q'∈nds ∧ qn' = name q' ∧ qn∈incoming q' ∧ qn≠expand_init })
= (λqn. dflt_None_set (succ_of_E
(rename_E name {(q, q'). q ∈ nds ∧ q' ∈ nds ∧ name q ∈ incoming q'}) qn))"
(is "(λqn. dflt_None_set (?L qn)) = (λqn. dflt_None_set (?R qn))")
apply (intro ext)
apply (fo_rule arg_cong)
proof (intro ext equalityI subsetI)
fix qn x
assume "x∈?R qn"
then show "x∈?L qn" using NINIT
by (force simp: succ_of_E_def)
next
fix qn x
assume XL: "x∈?L qn"
show "x∈?R qn"
proof (cases "qn = expand_init")
case False
from XL obtain q' where
A: "q'∈nds" "qn∈incoming q'"
and [simp]: "x=name q'"
by auto
from False obtain q where B: "q∈nds" and [simp]: "qn = name q"
using CL A by auto
from A B show "x∈?R qn"
by (auto simp: succ_of_E_def image_def)
next
case [simp]: True
from XL show "x∈?R qn" by simp
qed
qed
lemma build_succ_correct:
assumes NINIT: "expand_init ∉ name`nds"
assumes FIN: "finite nds"
assumes CL: "⋀nd. nd∈nds ⟹ incoming nd ⊆ insert expand_init (name`nds)"
shows "build_succ nds ≤ SPEC (λr.
E_of_succ (λqn. the_default {} (r qn))
= rename_E (λu. name u) {(q, q'). q ∈ nds ∧ q' ∈ nds ∧ name q ∈ incoming q'})"
proof -
from FIN CL have FIN': "⋀q. q∈nds ⟹ finite (incoming q)"
by (metis finite_imageI finite_insert infinite_super)
note build_succ_aux1[OF FIN FIN']
also note build_succ_aux2[OF NINIT CL]
finally show ?thesis
by (rule order_trans) auto
qed
text ‹\paragraph{ Accepting Sets}›
primrec until_frmlsr :: "'a frml ⇒ ('a frml × 'a frml) set" where
"until_frmlsr (μ and⇩r ψ) = (until_frmlsr μ) ∪ (until_frmlsr ψ)"
| "until_frmlsr (X⇩r μ) = until_frmlsr μ"
| "until_frmlsr (μ U⇩r ψ) = insert (μ, ψ) ((until_frmlsr μ) ∪ (until_frmlsr ψ))"
| "until_frmlsr (μ R⇩r ψ) = (until_frmlsr μ) ∪ (until_frmlsr ψ)"
| "until_frmlsr (μ or⇩r ψ) = (until_frmlsr μ) ∪ (until_frmlsr ψ)"
| "until_frmlsr (true⇩r) = {}"
| "until_frmlsr (false⇩r) = {}"
| "until_frmlsr (prop⇩r(_)) = {}"
| "until_frmlsr (nprop⇩r(_)) = {}"
lemma until_frmlsr_correct:
"until_frmlsr φ = {(μ, η). Until_ltlr μ η ∈ subfrmlsr φ}"
by (induct φ) auto
definition "build_F nds φ
≡ (λ(μ,η). name ` {q ∈ nds. (Until_ltlr μ η ∈ old q ⟶ η ∈ old q)}) `
until_frmlsr φ"
lemma build_F_correct: "build_F nds φ =
{name ` A |A. ∃μ η. A = {q ∈ nds. Until_ltlr μ η ∈ old q ⟶ η ∈ old q} ∧
Until_ltlr μ η ∈ subfrmlsr φ}"
proof -
have "{name ` A |A. ∃μ η. A = {q ∈ nds. Until_ltlr μ η ∈ old q ⟶ η ∈ old q} ∧
Until_ltlr μ η ∈ subfrmlsr φ}
= (λ(μ,η). name`{q∈nds. Until_ltlr μ η ∈ old q ⟶ η ∈ old q})
` {(μ, η). Until_ltlr μ η ∈ subfrmlsr φ}"
by auto
also have "… = (λ(μ,η). name`{q∈nds. Until_ltlr μ η ∈ old q ⟶ η ∈ old q})
` until_frmlsr φ"
unfolding until_frmlsr_correct ..
finally show ?thesis
unfolding build_F_def by simp
qed
text ‹\paragraph{ Labeling Function }›
definition "pn_props ps ≡ FOREACHi
(λit (P,N). P = {p. Prop_ltlr p ∈ ps - it} ∧ N = {p. Nprop_ltlr p ∈ ps - it})
ps (λp (P,N).
case p of Prop_ltlr p ⇒ RETURN (insert p P,N)
| Nprop_ltlr p ⇒ RETURN (P, insert p N)
| _ ⇒ RETURN (P,N)
) ({},{})"
lemma pn_props_correct:
assumes [simp]: "finite ps"
shows "pn_props ps ≤ SPEC(λr. r =
({p. Prop_ltlr p ∈ ps}, {p. Nprop_ltlr p ∈ ps}))"
unfolding pn_props_def
apply (refine_rcg refine_vcg)
apply (auto split: ltlr.split)
done
definition "pn_map nds ≡ FOREACH nds
(λnd m. do {
PN ← pn_props (old nd);
RETURN (m(name nd ↦ PN))
}) Map.empty"
lemma pn_map_correct:
assumes [simp]: "finite nds"
assumes FIN': "⋀nd. nd∈nds ⟹ finite (old nd)"
assumes INJ: "inj_on name nds"
shows "pn_map nds ≤ SPEC (λr. ∀qn.
case r qn of
None ⇒ qn ∉ name`nds
| Some (P,N) ⇒ qn ∈ name`nds
∧ P = {p. Prop_ltlr p ∈ old (the_inv_into nds name qn)}
∧ N = {p. Nprop_ltlr p ∈ old (the_inv_into nds name qn)}
)"
unfolding pn_map_def
apply (refine_rcg refine_vcg
FOREACH_rule[where I="λit r. ∀qn.
case r qn of
None ⇒ qn ∉ name`(nds - it)
| Some (P,N) ⇒ qn ∈ name`(nds - it)
∧ P = {p. Prop_ltlr p ∈ old (the_inv_into nds name qn)}
∧ N = {p. Nprop_ltlr p ∈ old (the_inv_into nds name qn)}"]
order_trans[OF pn_props_correct]
)
apply simp_all
apply (blast dest: subsetD[THEN FIN']) []
apply (force
split: option.splits
simp: the_inv_into_f_f[OF INJ] it_step_insert_iff) []
apply (fastforce split: option.splits) []
done
text ‹\paragraph{ Assembling the Implementation }›
definition "cr_rename_gba nds φ ≡ do {
let V = name ` nds;
let V0 = name ` {q ∈ nds. expand_init ∈ incoming q};
succmap ← build_succ nds;
let E = E_of_succ (the_default {} o succmap);
let F = build_F nds φ;
pnm ← pn_map nds;
let L = (λqn l. case pnm qn of
None ⇒ False
| Some (P,N) ⇒ (∀p∈P. p∈(l:::⇩r⟨Id⟩fun_set_rel)) ∧ (∀p∈N. p∉l)
);
RETURN (⦇ g_V = V, g_E=E, g_V0=V0, gbg_F = F, gba_L = L ⦈)
}"
lemma cr_rename_gba_refine:
assumes INV: "nds_invars nds"
assumes REL[simplified]: "(nds',nds)∈Id" "(φ',φ)∈Id"
shows "cr_rename_gba nds' φ'
≤ ⇓Id (RETURN (gba_rename_ext (λ_. ()) name (create_gba_from_nodes φ nds)))"
unfolding RETURN_SPEC_conv
proof (rule Id_SPEC_refine)
from INV have
NINIT: "expand_init ∉ name`nds"
and FIN: "finite nds"
and FIN': "⋀nd. nd∈nds ⟹ finite (old nd)"
and CL: "⋀nd. nd∈nds ⟹ incoming nd ⊆ insert expand_init (name`nds)"
and INJ: "inj_on name nds"
unfolding nds_invars_def by auto
show "cr_rename_gba nds' φ'
≤ SPEC (λx. x = gba_rename_ext (λ_. ()) name (create_gba_from_nodes φ nds))"
unfolding REL
unfolding cr_rename_gba_def
apply (refine_rcg refine_vcg
order_trans[OF build_succ_correct[OF NINIT FIN CL]]
order_trans[OF pn_map_correct[OF FIN FIN' INJ]]
)
unfolding gba_rename_ecnv_def gb_rename_ecnv_def
fr_rename_ext_def create_gba_from_nodes_def
apply simp
apply (intro conjI)
apply (simp add: comp_def)
apply (simp add: build_F_correct)
apply (intro ext)
apply (drule_tac x=qn in spec)
apply (auto simp: the_inv_into_f_f[OF INJ] split: option.split prod.split)
done
qed
definition "create_name_gba_aimpl φ ≡ do {
nds ← create_graph_aimpl φ;
ASSERT (nds_invars nds);
cr_rename_gba nds φ
}"
lemma create_name_gba_aimpl_refine:
"create_name_gba_aimpl φ ≤ ⇓Id (create_name_gba φ)"
unfolding create_name_gba_aimpl_def create_name_gba_alt
apply (refine_rcg create_graph_aimpl_refine cr_rename_gba_refine)
by auto
subsection ‹Refinement to Efficient Data Structures›
subsubsection ‹Creation of GBA from Nodes›
schematic_goal until_frmlsr_impl_aux:
assumes [relator_props, simp]: "R=Id"
shows "(?c,until_frmlsr)
∈ ⟨(R::(_×_::linorder) set)⟩ltlr_rel → ⟨⟨R⟩ltlr_rel ×⇩r ⟨R⟩ltlr_rel⟩dflt_rs_rel"
unfolding until_frmlsr_def
apply (autoref (keep_goal, trace))
done
concrete_definition until_frmlsr_impl uses until_frmlsr_impl_aux
lemmas [autoref_rules] = until_frmlsr_impl.refine[OF PREFER_id_D]
schematic_goal build_succ_impl_aux:
shows "(?c,build_succ) ∈
⟨⟨Rm,R⟩node_rel⟩list_set_rel
→ ⟨⟨nat_rel,⟨nat_rel⟩list_set_rel⟩iam_map_rel⟩nres_rel"
unfolding build_succ_def[abs_def] expand_init_def
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition build_succ_impl uses build_succ_impl_aux
lemmas [autoref_rules] = build_succ_impl.refine
schematic_goal build_succ_code_aux: "RETURN ?c ≤ build_succ_impl x"
unfolding build_succ_impl_def
apply (refine_transfer (post))
done
concrete_definition build_succ_code uses build_succ_code_aux
lemmas [refine_transfer] = build_succ_code.refine
schematic_goal build_F_impl_aux:
assumes [relator_props]: "R = Id"
shows "(?c,build_F) ∈
⟨⟨Rm,R⟩node_rel⟩list_set_rel → ⟨R⟩ltlr_rel → ⟨⟨nat_rel⟩list_set_rel⟩list_set_rel"
unfolding build_F_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition build_F_impl uses build_F_impl_aux
lemmas [autoref_rules] = build_F_impl.refine[OF PREFER_id_D]
schematic_goal pn_map_impl_aux:
shows "(?c,pn_map) ∈
⟨⟨Rm,Id⟩node_rel⟩list_set_rel
→ ⟨⟨nat_rel,⟨Id⟩list_set_rel ×⇩r ⟨Id⟩list_set_rel⟩iam_map_rel⟩nres_rel"
unfolding pn_map_def[abs_def] pn_props_def
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition pn_map_impl uses pn_map_impl_aux
lemma pn_map_impl_autoref[autoref_rules]:
assumes "PREFER_id R"
shows "(pn_map_impl,pn_map) ∈
⟨⟨Rm,R⟩node_rel⟩list_set_rel
→ ⟨⟨nat_rel,⟨R⟩list_set_rel ×⇩r ⟨R⟩list_set_rel⟩iam_map_rel⟩nres_rel"
using assms pn_map_impl.refine by simp
schematic_goal pn_map_code_aux: "RETURN ?c ≤ pn_map_impl x"
unfolding pn_map_impl_def
apply (refine_transfer (post))
done
concrete_definition pn_map_code uses pn_map_code_aux
lemmas [refine_transfer] = pn_map_code.refine
schematic_goal cr_rename_gba_impl_aux:
assumes ID[relator_props]: "R=Id"
notes [autoref_tyrel del] = tyrel_dflt_linorder_set
notes [autoref_tyrel] = ty_REL[of "⟨nat_rel⟩list_set_rel"]
shows "(?c,cr_rename_gba) ∈
⟨⟨Rm,R⟩node_rel⟩list_set_rel → ⟨R⟩ltlr_rel → (?R::(?'c × _) set)"
unfolding ID
unfolding cr_rename_gba_def[abs_def] expand_init_def comp_def
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition cr_rename_gba_impl uses cr_rename_gba_impl_aux
thm cr_rename_gba_impl.refine
lemma cr_rename_gba_autoref[autoref_rules]:
assumes "PREFER_id R"
shows "(cr_rename_gba_impl, cr_rename_gba) ∈
⟨⟨Rm, R⟩node_rel⟩list_set_rel → ⟨R⟩ltlr_rel →
⟨gbav_impl_rel_ext unit_rel nat_rel (⟨R⟩fun_set_rel)⟩nres_rel"
using assms cr_rename_gba_impl.refine[of R Rm] by simp
schematic_goal cr_rename_gba_code_aux: "RETURN ?c ≤ cr_rename_gba_impl x y"
unfolding cr_rename_gba_impl_def
apply (refine_transfer (post))
done
concrete_definition cr_rename_gba_code uses cr_rename_gba_code_aux
lemmas [refine_transfer] = cr_rename_gba_code.refine
subsubsection ‹Creation of Graph›
text ‹
The implementation of the node-set. The relation enforces that there are no
different nodes with the same name. This effectively establishes an additional
invariant, made explicit by an assertion in the refined program. This invariant
allows for a more efficient implementation.
›
definition ls_nds_rel_def_internal:
"ls_nds_rel R ≡ ⟨R⟩list_set_rel ∩ {(_,s). inj_on name s}"
lemma ls_nds_rel_def: "⟨R⟩ls_nds_rel = ⟨R⟩list_set_rel ∩ {(_,s). inj_on name s}"
by (simp add: relAPP_def ls_nds_rel_def_internal)
lemmas [autoref_rel_intf] = REL_INTFI[of ls_nds_rel i_set]
lemma ls_nds_rel_sv[relator_props]:
assumes "single_valued R"
shows "single_valued (⟨R⟩ls_nds_rel)"
using list_set_rel_sv[OF assms]
unfolding ls_nds_rel_def
by (metis inf.cobounded1 single_valued_subset)
context begin interpretation autoref_syn .
lemma lsnds_empty_autoref[autoref_rules]:
assumes "PREFER_id R"
shows "([],{})∈⟨R⟩ls_nds_rel"
using assms
apply (simp add: ls_nds_rel_def)
by autoref
lemma lsnds_insert_autoref[autoref_rules]:
assumes "SIDE_PRECOND (name n ∉ name`ns)"
assumes "(n',n)∈R"
assumes "(ns',ns)∈⟨R⟩ls_nds_rel"
shows "(n'#ns',(OP insert ::: R → ⟨R⟩ls_nds_rel → ⟨R⟩ls_nds_rel)$n$ns)
∈ ⟨R⟩ls_nds_rel"
using assms
unfolding ls_nds_rel_def
apply simp
proof (elim conjE, rule conjI)
assume [autoref_rules]: "(n', n) ∈ R" "(ns', ns) ∈ ⟨R⟩list_set_rel"
assume "name n ∉ name ` ns"
and "inj_on name ns"
then have "n ∉ ns" by (auto)
then show "(n' # ns', insert n ns) ∈ ⟨R⟩list_set_rel"
by autoref
qed auto
lemma ls_nds_image_autoref_aux:
assumes [autoref_rules]: "(fi,f) ∈ Ra → Rb"
assumes "(l,s) ∈ ⟨Ra⟩ls_nds_rel"
assumes [simp]: "∀x. name (f x) = name x"
shows "(map fi l, f`s) ∈ ⟨Rb⟩ls_nds_rel"
proof -
from assms have
[autoref_rules]: "(l,s)∈⟨Ra⟩list_set_rel"
and INJ: "(inj_on name s)"
by (auto simp add: ls_nds_rel_def)
have [simp]: "inj_on f s"
by (rule inj_onI) (metis INJ assms(3) inj_on_eq_iff)
have "(map fi l, f`s) ∈ ⟨Rb⟩list_set_rel"
by (autoref (keep_goal))
moreover have "inj_on name (f`s)"
apply (rule inj_onI)
apply (auto simp: image_iff dest: inj_onD[OF INJ])
done
ultimately show ?thesis
by (auto simp: ls_nds_rel_def)
qed
lemma ls_nds_image_autoref[autoref_rules]:
assumes "(fi,f) ∈ Ra → Rb"
assumes "SIDE_PRECOND (∀x. name (f x) = name x)"
shows "(map fi, (OP (`) ::: (Ra→Rb) → ⟨Ra⟩ls_nds_rel → ⟨Rb⟩ls_nds_rel)$f)
∈ ⟨Ra⟩ls_nds_rel → ⟨Rb⟩ls_nds_rel"
using assms
unfolding autoref_tag_defs
using ls_nds_image_autoref_aux
by blast
lemma list_set_autoref_to_list[autoref_ga_rules]:
shows "is_set_to_sorted_list (λ_ _. True) R ls_nds_rel id"
unfolding is_set_to_list_def is_set_to_sorted_list_def ls_nds_rel_def
it_to_sorted_list_def list_set_rel_def br_def
by auto
end
context begin interpretation autoref_syn .
lemma [autoref_itype]:
"upd_incoming
::⇩i ⟨Im, I⟩⇩ii_node →⇩i ⟨⟨Im', I⟩⇩ii_node⟩⇩ii_set →⇩i ⟨⟨Im', I⟩⇩ii_node⟩⇩ii_set"
by simp
end
term upd_incoming
schematic_goal upd_incoming_impl_aux:
assumes "REL_IS_ID R"
shows "(?c, upd_incoming)∈⟨Rm1,R⟩node_rel
→ ⟨⟨Rm2,R⟩node_rel⟩ls_nds_rel
→ ⟨⟨Rm2,R⟩node_rel⟩ls_nds_rel"
using assms apply simp
unfolding upd_incoming_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal))
done
concrete_definition upd_incoming_impl uses upd_incoming_impl_aux
lemmas [autoref_rules] = upd_incoming_impl.refine[OF PREFER_D[of REL_IS_ID]]
schematic_goal expand_impl_aux: "(?c, expand_aimpl) ∈
⟨unit_rel,Id⟩node_rel ×⇩r ⟨⟨unit_rel,Id⟩node_rel⟩ls_nds_rel
→ ⟨nat_rel ×⇩r ⟨⟨unit_rel,Id⟩node_rel⟩ls_nds_rel⟩nres_rel"
unfolding expand_aimpl_def[abs_def] expand_new_name_def
using [[autoref_trace_failed_id, autoref_trace_intf_unif]]
apply (autoref (trace,keep_goal))
done
concrete_definition expand_impl uses expand_impl_aux
context begin interpretation autoref_syn .
lemma [autoref_itype]: "expand⇩T
::⇩i ⟨⟨i_unit, I⟩⇩ii_node, ⟨⟨i_unit, I⟩⇩ii_node⟩⇩ii_set⟩⇩ii_prod
→⇩i ⟨⟨i_nat,⟨⟨i_unit, I⟩⇩ii_node⟩⇩ii_set⟩⇩ii_prod⟩⇩ii_nres" by simp
lemma expand_autoref[autoref_rules]:
assumes ID: "PREFER_id R"
assumes A: "(n_ns', n_ns)
∈ ⟨unit_rel,R⟩node_rel ×⇩r ⟨⟨unit_rel,R⟩node_rel⟩list_set_rel"
assumes B: "SIDE_PRECOND (
let (n,ns)=n_ns in inj_on name ns ∧ (∀n'∈ns. name n > name n')
)"
shows "(expand_impl n_ns',
(OP expand_aimpl
::: ⟨unit_rel,R⟩node_rel ×⇩r ⟨⟨unit_rel,R⟩node_rel⟩list_set_rel
→ ⟨nat_rel ×⇩r ⟨⟨unit_rel,R⟩node_rel⟩list_set_rel⟩nres_rel)$n_ns)
∈ ⟨nat_rel ×⇩r ⟨⟨unit_rel,R⟩node_rel⟩list_set_rel⟩nres_rel"
proof simp
from ID A B have
1: "(n_ns, n_ns) ∈ Id ∩ {(_,(n,ns)). ∀n'∈ns. name n > name n'}"
and 2: "(n_ns', n_ns)
∈ ⟨unit_rel,Id⟩node_rel ×⇩r ⟨⟨unit_rel,Id⟩node_rel⟩ls_nds_rel"
unfolding ls_nds_rel_def
apply -
apply auto []
apply (cases n_ns')
apply auto []
done
have [simp]: "single_valued (nat_rel ×⇩r ⟨⟨unit_rel, Id⟩node_rel⟩list_set_rel)"
by tagged_solver
have [relator_props]: "⋀R. single_valued (Id ∩ R)"
by (metis IntE single_valuedD single_valuedI single_valued_Id)
have [simp]: "single_valued ((nat_rel ×⇩r ⟨⟨unit_rel, Id⟩node_rel⟩ls_nds_rel) O
(Id ∩ {(_, n, ns). ∀n'∈ns. name n' < n}))"
by (tagged_solver)
from expand_impl.refine[THEN fun_relD, OF 2, THEN nres_relD]
show "(expand_impl n_ns', expand_aimpl n_ns)
∈ ⟨nat_rel ×⇩r ⟨⟨unit_rel, R⟩node_rel⟩list_set_rel⟩nres_rel"
apply -
apply (rule nres_relI)
using ID
apply (simp add: pw_le_iff refine_pw_simps)
apply (fastforce simp: ls_nds_rel_def)
done
qed
end
schematic_goal expand_code_aux: "RETURN ?c ≤ expand_impl n_ns"
unfolding expand_impl_def
by (refine_transfer the_resI)
concrete_definition expand_code uses expand_code_aux
prepare_code_thms expand_code_def
lemmas [refine_transfer] = expand_code.refine
schematic_goal create_graph_impl_aux:
assumes ID: "R=Id"
shows "(?c, create_graph_aimpl)
∈ ⟨R⟩ltlr_rel → ⟨⟨⟨unit_rel,R⟩node_rel⟩list_set_rel⟩nres_rel"
unfolding ID
unfolding create_graph_aimpl_def[abs_def] expand_init_def expand_new_name_def
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal))
done
concrete_definition create_graph_impl uses create_graph_impl_aux
lemmas [autoref_rules] = create_graph_impl.refine[OF PREFER_id_D]
schematic_goal create_graph_code_aux: "RETURN ?c ≤ create_graph_impl φ"
unfolding create_graph_impl_def
by refine_transfer
concrete_definition create_graph_code uses create_graph_code_aux
lemmas [refine_transfer] = create_graph_code.refine
schematic_goal create_name_gba_impl_aux:
"(?c, (create_name_gba_aimpl:: 'a::linorder ltlr ⇒ _))
∈ ⟨Id⟩ltlr_rel → (?R::(?'c×_) set)"
unfolding create_name_gba_aimpl_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition create_name_gba_impl uses create_name_gba_impl_aux
lemma create_name_gba_autoref[autoref_rules]:
assumes "PREFER_id R"
shows
"(create_name_gba_impl, create_name_gba)
∈ ⟨R⟩ltlr_rel → ⟨gbav_impl_rel_ext unit_rel nat_rel (⟨R⟩fun_set_rel)⟩nres_rel"
(is "_:_→⟨?R⟩nres_rel")
proof (intro fun_relI nres_relI)
fix φ φ'
assume A: "(φ,φ')∈⟨R⟩ltlr_rel"
from assms have RID[simp]: "R=Id" by simp
note create_name_gba_impl.refine[THEN fun_relD,THEN nres_relD, OF A[unfolded RID]]
also note create_name_gba_aimpl_refine
finally show "create_name_gba_impl φ ≤ ⇓ ?R (create_name_gba φ')" by simp
qed
schematic_goal create_name_gba_code_aux: "RETURN ?c ≤ create_name_gba_impl φ"
unfolding create_name_gba_impl_def
by (refine_transfer (post))
concrete_definition create_name_gba_code uses create_name_gba_code_aux
lemmas [refine_transfer] = create_name_gba_code.refine
schematic_goal create_name_igba_impl_aux:
assumes RID: "R=Id"
shows "(?c,create_name_igba)∈
⟨R⟩ltlr_rel → ⟨igbav_impl_rel_ext unit_rel nat_rel (⟨R⟩fun_set_rel)⟩nres_rel"
unfolding RID
unfolding create_name_igba_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (trace, keep_goal))
done
concrete_definition create_name_igba_impl uses create_name_igba_impl_aux
lemmas [autoref_rules] = create_name_igba_impl.refine[OF PREFER_id_D]
schematic_goal create_name_igba_code_aux: "RETURN ?c ≤ create_name_igba_impl φ"
unfolding create_name_igba_impl_def
by (refine_transfer (post))
concrete_definition create_name_igba_code uses create_name_igba_code_aux
lemmas [refine_transfer] = create_name_igba_code.refine
export_code create_name_igba_code checking SML
end