Theory SML_Relations
section‹Relativization of the results about relations›
theory SML_Relations
imports Main
begin
subsection‹Definitions and common properties›
context
notes [[inductive_internals]]
begin
inductive_set trancl_on :: "['a set, ('a × 'a) set] ⇒ ('a × 'a) set"
(‹on _/ (_⇧+)› [1000, 1000] 999)
for U :: "'a set" and r :: "('a × 'a) set"
where
r_into_trancl[intro, Pure.intro]:
"⟦ a ∈ U; b ∈ U; (a, b) ∈ r ⟧ ⟹ (a, b) ∈ on U r⇧+"
| trancl_into_trancl[Pure.intro]:
"
⟦ a ∈ U; b ∈ U; c ∈ U; (a, b) ∈ on U r⇧+; (b, c) ∈ r ⟧ ⟹
(a, c) ∈ on U r⇧+
"
abbreviation tranclp_on (‹on _/ (_⇧+⇧+)› [1000, 1000] 1000) where
"tranclp_on ≡ trancl_onp"
declare trancl_on_def[nitpick_unfold del]
lemmas tranclp_on_def = trancl_onp_def
end
definition transp_on :: "['a set, ['a, 'a] ⇒ bool] ⇒ bool"
where "transp_on U = (λr. (∀x∈U. ∀y∈U. ∀z∈U. r x y ⟶ r y z ⟶ r x z))"
definition acyclic_on :: "['a set, ('a × 'a) set] ⇒ bool"
where "acyclic_on U = (λr. (∀x∈U. (x, x) ∉ on U r⇧+))"
lemma trancl_on_eq_tranclp_on:
"on P (λx y. (x, y) ∈ r)⇧+⇧+ x y = ((x, y) ∈ on (Collect P) r⇧+)"
unfolding trancl_on_def tranclp_on_def Set.mem_Collect_eq by simp
lemma trancl_on_imp_U: "(x, y) ∈ on U r⇧+ ⟹ (x, y) ∈ U × U"
by (auto dest: trancl_on.cases)
lemmas tranclp_on_imp_P = trancl_on_imp_U[to_pred, simplified]
lemma trancl_on_imp_trancl: "(x, y) ∈ on U r⇧+ ⟹ (x, y) ∈ r⇧+"
by (induction rule: trancl_on.induct) auto
lemmas tranclp_on_imp_tranclp = trancl_on_imp_trancl[to_pred]
lemma tranclp_eq_tranclp_on: "r⇧+⇧+ = on (λx. True) r⇧+⇧+"
unfolding tranclp_def tranclp_on_def by simp
lemma trancl_eq_trancl_on: "r⇧+ = on UNIV r⇧+"
unfolding trancl_def trancl_on_def by (simp add: tranclp_eq_tranclp_on)
lemma transp_on_empty[simp]: "transp_on {} r" unfolding transp_on_def by simp
lemma transp_eq_transp_on: "transp = transp_on UNIV"
unfolding transp_def transp_on_def by simp
lemma acyclic_on_empty[simp]: "acyclic_on {} r" unfolding acyclic_on_def by simp
lemma acyclic_eq_acyclic_on: "acyclic = acyclic_on UNIV"
unfolding acyclic_def acyclic_on_def
unfolding trancl_def tranclp_def trancl_on_def tranclp_on_def
by simp
subsection‹Transfer rules I: \<^const>‹lfp› transfer›
text‹
The following context contains code from \<^cite>‹"immler_re_2019"›.
›
context
includes lifting_syntax
begin
lemma Inf_transfer[transfer_rule]:
"(rel_set (A ===> (=)) ===> A ===> (=)) Inf Inf"
unfolding Inf_fun_def by transfer_prover
lemma less_eq_pred_transfer[transfer_rule]:
assumes [transfer_rule]: "right_total A"
shows
"((A ===> (=)) ===> (A ===> (=)) ===> (=))
(λf g. ∀x∈Collect(Domainp A). f x ≤ g x) (≤)"
unfolding le_fun_def by transfer_prover
lemma lfp_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
defines "R ≡ (((A ===> (=)) ===> (A ===> (=))) ===> (A ===> (=)))"
shows "R (λf. lfp (λu x. if Domainp A x then f u x else bot)) lfp"
proof -
have "R (λf. Inf {u. ∀x∈Collect (Domainp A). f u x ≤ u x}) lfp"
unfolding R_def lfp_def by transfer_prover
thus ?thesis by (auto simp: le_fun_def lfp_def)
qed
lemma Inf2_transfer[transfer_rule]:
"(rel_set (T ===> T ===> (=)) ===> T ===> T ===> (=)) Inf Inf"
unfolding Inf_fun_def by transfer_prover
lemma less_eq2_pred_transfer[transfer_rule]:
assumes [transfer_rule]: "right_total T"
shows
"((T ===> T ===> (=)) ===> (T ===> T ===> (=)) ===> (=))
(λf g. ∀x∈Collect(Domainp T). ∀y∈Collect(Domainp T). f x y ≤ g x y) (≤)"
unfolding le_fun_def by transfer_prover
lemma lfp2_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
defines
"R ≡
(((A ===> A ===> (=)) ===> (A ===> A ===> (=))) ===> (A ===> A ===> (=)))"
shows
"R
(
λf. lfp
(
λu x y.
if Domainp A x
then if Domainp A y then (f u) x y else bot
else bot
)
)
lfp"
proof -
have
"R
(
λf.
Inf
{
u.
∀x∈Collect (Domainp A). ∀y∈Collect (Domainp A).
(f u) x y ≤ u x y
}
)
lfp"
unfolding R_def lfp_def by transfer_prover
thus ?thesis by (auto simp: le_fun_def lfp_def)
qed
end
subsection‹Transfer rules II: application-specific rules›
context
includes lifting_syntax
begin
lemma transp_rt_transfer[transfer_rule]:
assumes[transfer_rule]: "right_total A"
shows
"((A ===> A ===> (=)) ===> (=)) (transp_on (Collect (Domainp A))) transp"
unfolding transp_def transp_on_def by transfer_prover
lemma tranclp_rt_bu_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> (=)) ===> (A ===> A ===> (=)))
(tranclp_on (Domainp A)) tranclp"
unfolding tranclp_on_def tranclp_def
apply transfer_prover_start
apply transfer_step+
proof
fix r
have
"(
λp x y.
(∃a b. x = a ∧ y = b ∧ Domainp A a ∧ Domainp A b ∧ r a b) ∨
(
∃a b c.
x = a ∧ y = c ∧
Domainp A a ∧ Domainp A b ∧ Domainp A c ∧
p a b ∧ r b c
)
) =
(
λp x y.
if Domainp A x
then if Domainp A y
then
(
∃a∈Collect (Domainp A). ∃b∈Collect (Domainp A).
x = a ∧ y = b ∧ r a b) ∨
(
∃a∈Collect (Domainp A).
∃b∈Collect (Domainp A).
∃c∈Collect (Domainp A).
x = a ∧ y = c ∧ p a b ∧ r b c
)
else bot
else bot
)"
(is "?lhs = ?rhs")
by (intro ext) simp
thus "lfp ?lhs = lfp ?rhs" by clarsimp
qed
lemma trancl_rt_bu_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"(rel_set (rel_prod A A) ===> rel_set (rel_prod A A))
(trancl_on (Collect (Domainp A))) trancl"
unfolding trancl_on_def trancl_def
apply transfer_prover_start
apply transfer_step+
by (auto simp: tranclp_on_imp_P[where U="Domainp A"])
lemma acyclic_rt_bu_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"((rel_set (rel_prod A A)) ===> (=))
(acyclic_on (Collect (Domainp A))) acyclic"
unfolding acyclic_on_def acyclic_def by transfer_prover
end
text‹\newpage›
end