theory Horn_Autoref
imports Horn_List Collections.Refine_Dflt Refine_Iterator
begin
lemma color_rel_Id:
"color_rel = Id"
apply (intro equalityI subrelI)
subgoal using color_rel.cases by blast
subgoal using color.exhaust color_rel.simps by auto
done
lemma rbt_rel_Id [simp]:
"⟨Id, Id⟩rbt_rel = Id"
unfolding rbt_rel_def relAPP_def
apply (intro equalityI subrelI)
subgoal for x y by (induct rule: rbt_rel_aux.induct) (auto elim: color_rel.cases)
subgoal for x y by (induct x arbitrary: y) (auto intro: rbt_rel_aux.intros simp: color_rel_Id)
done
text ‹automatic refinement setup for horn datatype›
definition horn_rel :: "_ ⇒ 'a horn rel" where
horn_rel_def': "horn_rel R ≡ {(as →⇩h a, bs →⇩h b) |as a bs b. (as, bs) ∈ ⟨R⟩list_rel ∧ (a, b) ∈ R}"
lemma horn_rel_def [refine_rel_defs]:
"⟨R⟩horn_rel ≡ {(as →⇩h a, bs →⇩h b) |as a bs b. (as, bs) ∈ ⟨R⟩list_rel ∧ (a, b) ∈ R}"
by (simp add: horn_rel_def' relAPP_def)
lemma horn_autoref [autoref_rules, param]:
"((→⇩h), (→⇩h)) ∈ ⟨R⟩list_rel → R → ⟨R⟩horn_rel"
"(case_horn, case_horn) ∈ (⟨R⟩list_rel → R → X) → ⟨R⟩horn_rel → X"
by (auto simp: horn_rel_def dest!: fun_relD)
lemma foldl_nop:
"(⋀x. f s x = s) ⟹ foldl f s xs = s"
by (induct xs) auto
lemma foldli_conv_foldl [code_unfold]:
"foldli xs (case_dres False False (λ_. True)) (λx s. s ⤜ f x) s =
foldl (λs x. s ⤜ f x) s xs"
by (induct xs arbitrary: s) (auto split: dres.splits simp: foldl_nop)
context horn
begin
definition saturate_impl_loop :: "'a set nres" where
"saturate_impl_loop = do {
let G = infer0; let B = {};
(G, B) ← WHILE (λ(G, B). G ≠ {}) (λ(G, B). do {
x ← SPEC (λx. x ∈ G);
RETURN (G - {x} ∪ infer1 x B, B ∪ {x})
}) (G, B);
RETURN B
}"
lemma saturate_impl_loop_spec:
"saturate_impl_loop ≤ SPEC ((=) saturate)"
unfolding saturate_impl_loop_def Let_def using trans[OF _ propagate]
by (refine_vcg WHILE_rule[where I = "λ(G, B). (infer0, {}) ⊢ (G, B)"])
(auto dest: step_sound intro: refl simp: insert_absorb)
definition saturate_rec :: "('a × 'a set ⇒ 'a set nres) ⇒ 'a × 'a set ⇒ 'a set nres" where
"saturate_rec = (λf (x, B). if x ∈ B then RETURN B else FOREACH_it (infer1 x B) (curry f) (insert x B))"
definition saturate_impl :: "'a set nres" where
"saturate_impl = FOREACH_it infer0 (curry (REC saturate_rec)) {}"
lemma trimono_saturate_rec [simp]:
"trimono saturate_rec"
unfolding saturate_rec_def curry_def FOREACH_it_def LIST_FOREACH_def FOREACH_cond_def FOREACH_body_def
by refine_mono
lemma saturate_rec_spec:
"REC saturate_rec (x, B) ≤ SPEC (λB'. ({x}, B) ⊢ ({}, B'))"
proof (intro REC_rule[of _ "λ_. True" "(x, B)" "λ(x, B). SPEC (λB'. ({x}, B) ⊢ ({}, B'))",
unfolded prod.case] trimono_saturate_rec TrueI, goal_cases)
case (1 f xB)
obtain x B where xB: "xB = (x, B)" by (cases xB)
{ fix G' B' x' assume *: "({x}, B) ⊢ (insert x' G', B')"
have "f (x', B') ≤ SPEC (λB'. ({x}, B) ⊢ (G', B'))" using step.trans[OF *(1)]
by (auto intro!: order.trans[OF 1(1)] dest!: step_mono[of "{x'}" _ _ _ "G'"] simp: insert_absorb)
}
then show ?case
unfolding saturate_rec_def xB using propagate[where G = "{}"]
by (refine_vcg FOREACH_it_rule[where I = "λG' B'. ({x}, B) ⊢ (G', B')"])
(auto split: list.splits simp: hd_def intro: delete)
qed
lemma saturate_impl_sound:
"saturate_impl ≤ SPEC ((=) saturate)"
proof -
let ?G = "infer0"
have "saturate_impl ≤ SPEC (λB'. (?G, {}) ⊢ ({}, B'))"
unfolding saturate_impl_def
by (refine_vcg FOREACH_it_rule[where I = "λG' B'. (?G, {}) ⊢ (G', B')"])
(auto intro!: order.trans[OF saturate_rec_spec] intro: refl simp: insert_absorb hd_def
split: list.splits dest: trans[OF _ step_mono[of "{_}" _ "{}" _ _], simplified])
also have "... ≤ SPEC ((=) saturate)" using step_sound by auto
finally show ?thesis .
qed
end
schematic_goal (in horn) saturate_impl_list:
defines "infer0'' ≡ infer0" and "infer1'' ≡ infer1"
assumes i0 [autoref_rules]: "(infer0', infer0'') ∈ ⟨Id⟩it_set_rel"
assumes i1 [autoref_rules]: "(infer1', infer1'') ∈ Id → ⟨Id⟩list_set_rel → ⟨Id⟩it_set_rel"
shows "(nres_of ?f, saturate_impl) ∈ ⟨⟨Id⟩list_set_rel⟩nres_rel"
unfolding saturate_impl_def curry_def saturate_rec_def
infer0''_def[symmetric] infer1''_def[symmetric] FOREACH_it_def LIST_FOREACH'_eq LIST_FOREACH'_def
by (autoref_monadic (plain))
concrete_definition saturate_list uses horn.saturate_impl_list
prepare_code_thms saturate_list_def
locale horn_list' = horn +
fixes infer0_impl :: "'a list" and infer1_impl :: "'a ⇒ 'a list ⇒ 'a list"
assumes infer0: "infer0 = set infer0_impl"
and infer1: "⋀x bs. distinct bs ⟹ infer1 x (set bs) = set (infer1_impl x bs)"
begin
lemma infer0_rel:
"(infer0_impl, infer0) ∈ ⟨Id⟩it_set_rel"
using infer0 unfolding it_set_rel_def list_set_rel_def br_def by simp
lemma infer1_rel:
"(infer1_impl, infer1) ∈ Id → ⟨Id⟩list_set_rel → ⟨Id⟩it_set_rel"
using infer1 unfolding it_set_rel_def list_set_rel_def br_def by auto
lemma saturate_list_sound:
"nres_of (saturate_list infer0_impl infer1_impl) ≤ ⇓ (⟨Id⟩list_set_rel) (SPEC ((=) saturate))"
using saturate_impl_list[OF infer0_rel infer1_rel, folded saturate_list_def]
by (intro ref_two_step[OF _ saturate_impl_sound]) (auto simp: nres_rel_def)
end
locale horn_linorder = horn ℋ for ℋ :: "('a :: linorder) horn set"
begin
schematic_goal saturate_impl_rbt:
defines "infer0'' ≡ infer0" and "infer1'' ≡ infer1"
assumes i0 [autoref_rules]: "(infer0', infer0'') ∈ ⟨Id⟩it_set_rel"
assumes i1 [autoref_rules]: "(infer1', infer1'') ∈ Id → ⟨Id⟩dflt_rs_rel → ⟨Id⟩it_set_rel"
notes [autoref_rules] = dflt_cmp_id and [simp] = class_to_eq_linorder
shows "(nres_of ?f, saturate_impl) ∈ ⟨⟨Id⟩dflt_rs_rel⟩nres_rel"
unfolding saturate_impl_def curry_def saturate_rec_def
infer0''_def[symmetric] infer1''_def[symmetric] FOREACH_it_def LIST_FOREACH'_eq LIST_FOREACH'_def
by (autoref_monadic (plain))
end
concrete_definition saturate_rbt uses horn_linorder.saturate_impl_rbt
prepare_code_thms saturate_rbt_def
locale horn_rbt = horn_linorder +
fixes infer0_impl :: "'a list" and infer1_impl :: "'a ⇒ ('a, unit) rbt ⇒ 'a list"
assumes infer0: "infer0 = set infer0_impl"
and infer1: "⋀x bs. infer1 x (set (RBT_Impl.keys bs)) = set (infer1_impl x bs)"
begin
lemma infer0_rel:
"(infer0_impl, infer0) ∈ ⟨Id⟩it_set_rel"
using infer0 unfolding it_set_rel_def br_def by simp
lemma infer1_rel:
"(infer1_impl, infer1) ∈ Id → ⟨Id⟩dflt_rs_rel → ⟨Id⟩it_set_rel"
apply (intro fun_relI, elim map2set_relE)
subgoal for a' a B'' B B' using fun_relD[OF rbt_map_impl(3), of B'' B'] infer1
linorder.rbt_lookup_keys[OF linorder_class.linorder_axioms ord.is_rbt_rbt_sorted, of B'']
by (auto simp: rbt_map_rel_def rbt_map_rel'_def br_def it_set_rel_def)
done
lemma saturate_rbt_sound:
"nres_of (saturate_rbt infer0_impl infer1_impl) ≤ ⇓ (⟨Id⟩dflt_rs_rel) (SPEC ((=) saturate))"
using saturate_impl_rbt[OF infer0_rel infer1_rel, folded saturate_rbt_def]
by (intro ref_two_step[OF _ saturate_impl_sound]) (auto simp: nres_rel_def)
end
end