theory Abstract_Rewriting_Impl
imports
"Abstract-Rewriting.Abstract_Rewriting"
begin
partial_function (option) compute_NF :: "('a ⇒ 'a option) ⇒ 'a ⇒ 'a option"
where [simp,code]: "compute_NF f a = (case f a of None ⇒ Some a | Some b ⇒ compute_NF f b)"
lemma compute_NF_sound: assumes res: "compute_NF f a = Some b"
and f_sound: "⋀ a b. f a = Some b ⟹ (a,b) ∈ r"
shows "(a,b) ∈ r^*"
proof (induct rule: compute_NF.raw_induct[OF _ res, of "λ g a b. g = f ⟶ (a,b) ∈ r^*", THEN mp[OF _ refl]])
case (1 cnf g a b)
show ?case
proof
assume "g = f"
note 1 = 1[unfolded this]
show "(a,b) ∈ r^*"
proof (cases "f a")
case None
with 1(2) show ?thesis by simp
next
case (Some c)
from 1(2)[unfolded this] have "cnf f c = Some b" by simp
from 1(1)[OF this] have "(c,b) ∈ r^*" by auto
with f_sound[OF Some] show ?thesis by auto
qed
qed
qed
lemma compute_NF_complete: assumes res: "compute_NF f a = Some b"
and f_complete: "⋀ a. f a = None ⟹ a ∈ NF r"
shows "b ∈ NF r"
proof (induct rule: compute_NF.raw_induct[OF _ res, of "λ g a b. g = f ⟶ b ∈ NF r", THEN mp[OF _ refl]])
case (1 cnf g a b)
show ?case
proof
assume "g = f"
note 1 = 1[unfolded this]
show "b ∈ NF r"
proof (cases "f a")
case None
with f_complete[OF None] 1(2)
show ?thesis by simp
next
case (Some c)
from 1(2)[unfolded this] have "cnf f c = Some b" by simp
from 1(1)[OF this] show ?thesis by simp
qed
qed
qed
lemma compute_NF_SN: assumes SN: "SN r"
and f_sound: "⋀ a b. f a = Some b ⟹ (a,b) ∈ r"
shows "∃ b. compute_NF f a = Some b" (is "?P a")
proof -
let ?r = "{(a,b). f a = Some b}"
have "?r ⊆ r" using f_sound by auto
from SN_subset[OF SN this] have SNr: "SN ?r" .
show ?thesis
proof (induct rule: SN_induct[OF SNr, of "λ a. ?P a"])
case (1 a)
show ?case
proof (cases "f a")
case None then show ?thesis by auto
next
case (Some b)
then have "(a,b) ∈ ?r" by simp
from 1[OF this] f_sound[OF Some] show ?thesis
using Some by auto
qed
qed
qed
definition "compute_trancl A R = R^+ `` A"
lemma compute_trancl_rtrancl[code_unfold]: "{b. (a,b) ∈ R^*} = insert a (compute_trancl {a} R)"
proof -
have id: "R^* = (Id ∪ R^+)" by regexp
show ?thesis unfolding id compute_trancl_def by auto
qed
lemma [code]: "compute_trancl A R = (let B = R `` A in
if B ⊆ {} then {} else B ∪ compute_trancl B { ab ∈ R . fst ab ∉ A ∧ snd ab ∉ B})"
proof -
have R: "R^+ = R O R^*" by regexp
define B where "B = R `` A"
define R' where "R' = {ab ∈ R. fst ab ∉ A ∧ snd ab ∉ B}"
note d = compute_trancl_def
show ?thesis unfolding Let_def B_def[symmetric] R'_def[symmetric] d
proof (cases "B ⊆ {}")
case True
then show "R⇧+ `` A = (if B ⊆ {} then {} else B ∪ R'^+ `` B)" unfolding B_def R by auto
next
case False
have "R' ⊆ R" unfolding R'_def by auto
then have "R'^+ ⊆ R^+" by (rule trancl_mono_set)
also have "… ⊆ R^*" by auto
finally have mono: "R'^+ ⊆ R^*" .
have "B ∪ R'⇧+ `` B = R⇧+ `` A"
proof
show "B ∪ R'⇧+ `` B ⊆ R^+ `` A" unfolding B_def R using mono
by blast
next
show "R^+ `` A ⊆ B ∪ R'^+ `` B"
proof
fix x
assume "x ∈ R^+ `` A"
then obtain a where a: "a ∈ A" and ax: "(a,x) ∈ R^+" by auto
from ax a show "x ∈ B ∪ R'^+ `` B"
proof (induct)
case base
then show ?case unfolding B_def by auto
next
case (step x y)
from step(3)[OF step(4)] have x: "x ∈ B ∪ R'^+ `` B" .
show ?case
proof (cases "y ∈ B")
case False note y = this
show ?thesis
proof (cases "x ∈ A")
case True
with y step(2) show ?thesis unfolding B_def by auto
next
case False
with y step(2) have "(x,y) ∈ R'" unfolding R'_def by auto
with x have "y ∈ (R' ∪ (R'^+ O R')) `` B" by blast
also have "R' ∪ (R'^+ O R') = R'^+" by regexp
finally show ?thesis by blast
qed
qed auto
qed
qed
qed
with False show "R⇧+ `` A = (if B ⊆ {} then {} else B ∪ R'^+ `` B)" by auto
qed
qed
lemma [code_unfold]: "R^+ `` A = compute_trancl A R" unfolding compute_trancl_def by auto
lemma compute_rtrancl[code_unfold]: "R^* `` A = A ∪ compute_trancl A R"
proof -
have id: "R^* = (Id ∪ R^+)" by regexp
show ?thesis unfolding id compute_trancl_def by auto
qed
lemma [code_unfold]: "(a,b) ∈ R^+ ⟷ b ∈ compute_trancl {a} R" unfolding compute_trancl_def by auto
lemma [code_unfold]: "(a,b) ∈ R^* ⟷ b = a ∨ b ∈ compute_trancl {a} R"
using compute_rtrancl[of R "{a}"] by auto
end