theory F_Algebra
imports TRS.Term_More
begin
section ‹F-Algebras›
locale algebra = fixes I :: "'f ⇒ 'a list ⇒ 'a"
begin
fun eval :: "('f,'v) term ⇒ ('v ⇒ 'a) ⇒ 'a"
where "eval (Var x) α = α x"
| "eval (Fun f ss) α = I f (map (λs. eval s α) ss)"
notation eval ("⟦(_)⟧")
lemma eval_same_vars[intro]: "(⋀x. x ∈ vars_term t ⟹ α x = β x) ⟹ ⟦t⟧ α = ⟦t⟧ β"
by(induct t, auto intro!:map_cong[OF refl] cong[of "I _"])
lemma subset_range_eval: "range α ⊆ range (λs. ⟦s⟧α)" (is "?l ⊆ ?r")
proof
fix a assume "a ∈ ?l"
then obtain v where "α v = a" by auto
then show "a ∈ ?r" by (auto intro!: range_eqI[of _ _ "Var v"])
qed
definition constant_at where "constant_at f n i ≡
∀as b. i < n ⟶ length as = n ⟶ I f (as[i:=b]) = I f as"
lemma constant_atI:
assumes "⋀as b. i < n ⟹ length as = n ⟹ I f (as[i:=b]) = I f as"
shows "constant_at f n i" using assms by (auto simp: constant_at_def)
lemma constant_atD:
"constant_at f n i ⟹ length as = n ⟹ I f (as[i:=b]) = I f as"
by (auto simp: constant_at_def)
definition "constant_term_on s x ≡ ∀α a. ⟦s⟧(α(x:=a)) = ⟦s⟧α"
lemma constant_term_onI: assumes "⋀α a. ⟦s⟧(α(x:=a)) = ⟦s⟧α" shows "constant_term_on s x"
using assms by (auto simp: constant_term_on_def)
lemma constant_term_onD:
assumes "constant_term_on s x" shows "⟦s⟧(α(x:=a)) = ⟦s⟧α"
using assms by (auto simp: constant_term_on_def)
lemma constant_term_onE:
assumes "constant_term_on s x" and "(⋀α a. ⟦s⟧(α(x:=a)) = ⟦s⟧α) ⟹ thesis"
shows thesis using assms by (auto simp: constant_term_on_def)
lemma constant_term_on_extra_var: "x ∉ vars_term s ⟹ constant_term_on s x"
by (auto intro!: constant_term_onI)
lemma constant_term_on_eq:
assumes "⟦s⟧ = ⟦t⟧" and "constant_term_on s x" shows "constant_term_on t x"
using assms by (simp add: constant_term_on_def)
definition "constant_term s ≡ ∀x. constant_term_on s x"
lemma constant_termI: assumes "⋀x. constant_term_on s x" shows "constant_term s"
using assms by (auto simp: constant_term_def)
lemma ground_imp_constant: "ground s ⟹ constant_term s"
by (auto intro!: constant_termI constant_term_on_extra_var simp: ground_vars_term_empty)
end
declare algebra.eval.simps[code,simp]
lemma eval_map_term:
"algebra.eval I (map_term ff fv t) α = algebra.eval (I ∘ ff) t (α ∘ fv)"
by (induct t, auto intro: cong[of "I _"])
text ‹In the term algebra, evaluation is substitution.›
interpretation term_algebra: algebra Fun
rewrites term_algebra_eval: "term_algebra.eval = (⋅)"
proof (intro ext)
show "algebra.eval Fun s σ = s⋅σ" for s σ by (induct s, unfold algebra.eval.simps, auto)
qed
subsection ‹Homomorphism›
locale algebra_hom = source: algebra I + target: algebra I'
for hom :: "'a ⇒ 'b" and I :: "'f ⇒ 'a list ⇒ 'a" and I' :: "'f ⇒ 'b list ⇒ 'b" +
assumes hom: "⋀f as. hom (I f as) = I' f (map hom as)"
begin
lemma hom_eval: "hom (source.eval s α) = target.eval s (λx. hom (α x))"
by (induct s, auto simp: hom intro: arg_cong[OF list.map_cong0])
end
context algebra begin
text ‹Evaluation is a homomophism from the term algebra.›
sublocale eval_hom: algebra_hom "(λs. ⟦s⟧α)" Fun I
rewrites "algebra.eval Fun = (⋅)"
by (unfold_locales, auto simp: term_algebra_eval)
lemmas subst_eval = eval_hom.hom_eval
end
thm term_algebra.subst_eval[folded subst_compose_def]
locale algebra_epim = algebra_hom +
assumes surj: "surj hom"
text ‹An algebra where every element has a representation:›
locale algebra_constant = algebra I
for I :: "'f ⇒ 'a list ⇒ 'a"
and const :: "'a ⇒ ('f,'v) term" +
assumes vars_term_const[simp]: "⋀d. vars_term (const d) = {}"
and eval_const[simp]: "⋀d α. ⟦const d⟧ α = d"
text ‹
Here we ``encode'' an $F$-algebra into a $G$-algebra, where $G$ is supposed to be established
small signature like the semiring signature.
Each function symbol $f \in F$ of arity $n$ is encoded as a term in $T(G,{0..<n})$.
›
subsubsection ‹Syntactic Encodings›
locale pre_encoding =
fixes E :: "'f ⇒ nat ⇒ ('g, nat) term"
begin
text ‹These "pre" locales are needed only for (unconditional) cord equations.›
abbreviation(input) I where "I f ss ≡ E f (length ss) ⋅ (nth ss)"
sublocale algebra I.
end
locale pre_encoded_algebra = target: algebra I + encoder: pre_encoding E
for I :: "'g ⇒ 'a list ⇒ 'a"
and E :: "'f ⇒ nat ⇒ ('g, nat) term"
begin
abbreviation encode :: "('f,'v) term ⇒ ('g,'v) term" where "encode s ≡ encoder.eval s Var"
abbreviation IE :: "'f ⇒ 'a list ⇒ 'a" where "IE f vs ≡ target.eval (E f (length vs)) (nth vs)"
sublocale algebra IE.
lemma constant_at_via_encoding:
assumes "target.constant_term_on (E f n) i"
shows "constant_at f n i"
proof (intro constant_atI)
fix as :: "'a list" and b
assume 1: "i < n" and 2: "length as = n"
then have [simp]: "(!) (as [i := b]) = (λj. if i = j then b else as ! j)" by auto
from target.constant_term_onD[OF assms, of "λj. as ! j" b, symmetric]
show "target.eval (E f (length (as[i := b]))) ((!) (as[i := b])) =
target.eval (E f (length as)) ((!) as)" by (auto simp: fun_upd_def 2)
qed
definition "constant_positions f n ≡ [i ← [0..<n]. i ∉ vars_term (E f n)]"
lemma constant_positions: "i ∈ set (constant_positions f n) ⟹ constant_at f n i"
apply (rule constant_at_via_encoding)
apply (rule target.constant_term_on_extra_var)
by (auto simp: constant_positions_def)
end
subsubsection ‹Well-Formed Encodings›
locale encoding = pre_encoding +
assumes var_domain: "i ∈ vars_term (E f n) ⟹ i < n"
locale encoded_algebra = pre_encoded_algebra + encoder: encoding
begin
sublocale algebra_hom "λt. target.eval t α" "encoder.I" IE
apply unfold_locales
by (auto simp: target.eval_hom.hom_eval encoder.var_domain)
lemma eval_via_encoding [simp]: "target.eval (encode s) = ⟦s⟧"
by (intro ext, induct s, auto simp: target.eval_hom.hom_eval encoder.var_domain)
end
end