Theory Strong_Term
section ‹Term algebra extended with wellformedness›
theory Strong_Term
imports Consts
begin
class pre_strong_term = "term" +
fixes wellformed :: "'a ⇒ bool"
fixes all_frees :: "'a ⇒ name fset"
assumes wellformed_const[simp]: "wellformed (const name)"
assumes wellformed_free[simp]: "wellformed (free name)"
assumes wellformed_app[simp]: "wellformed (app u⇩1 u⇩2) ⟷ wellformed u⇩1 ∧ wellformed u⇩2"
assumes all_frees_const[simp]: "all_frees (const name) = fempty"
assumes all_frees_free[simp]: "all_frees (free name) = {| name |}"
assumes all_frees_app[simp]: "all_frees (app u⇩1 u⇩2) = all_frees u⇩1 |∪| all_frees u⇩2"
begin
abbreviation wellformed_env :: "(name, 'a) fmap ⇒ bool" where
"wellformed_env ≡ fmpred (λ_. wellformed)"
end
context pre_constants begin
definition shadows_consts :: "'a::pre_strong_term ⇒ bool" where
"shadows_consts t ⟷ ¬ fdisjnt all_consts (all_frees t)"
sublocale shadows: simple_syntactic_or shadows_consts
by standard (auto simp: shadows_consts_def fdisjnt_alt_def)
abbreviation not_shadows_consts_env :: "(name, 'a::pre_strong_term) fmap ⇒ bool" where
"not_shadows_consts_env ≡ fmpred (λ_ s. ¬ shadows_consts s)"
end
declare pre_constants.shadows_consts_def[code]
class strong_term = pre_strong_term +
assumes raw_frees_all_frees: "abs_pred (λt. frees t |⊆| all_frees t) t"
assumes raw_subst_wellformed: "abs_pred (λt. wellformed t ⟶ (∀env. wellformed_env env ⟶ wellformed (subst t env))) t"
begin
lemma frees_all_frees: "frees t |⊆| all_frees t"
proof (induction t rule: raw_induct)
case (abs t)
show ?case
by (rule raw_frees_all_frees)
qed auto
lemma subst_wellformed: "wellformed t ⟹ wellformed_env env ⟹ wellformed (subst t env)"
proof (induction t arbitrary: env rule: raw_induct)
case (abs t)
show ?case
by (rule raw_subst_wellformed)
qed (auto split: option.splits)
end
global_interpretation wellformed: subst_syntactic_and "wellformed :: 'a::strong_term ⇒ bool"
by standard (auto simp: subst_wellformed)
instantiation "term" :: strong_term begin
fun all_frees_term :: "term ⇒ name fset" where
"all_frees_term (Free x) = {| x |}" |
"all_frees_term (t⇩1 $ t⇩2) = all_frees_term t⇩1 |∪| all_frees_term t⇩2" |
"all_frees_term (Λ t) = all_frees_term t" |
"all_frees_term _ = {||}"
lemma frees_all_frees_term[simp]: "all_frees t = frees (t::term)"
by (induction t) auto
definition wellformed_term :: "term ⇒ bool" where
[simp]: "wellformed_term t ⟷ Term.wellformed t"
instance proof (standard, goal_cases)
case 8
have *: "abs_pred P t" if "P t" for P and t :: "term"
unfolding abs_pred_term_def using that
by auto
show ?case
apply (rule *)
unfolding wellformed_term_def
by (auto simp: Term.subst_wellformed)
qed (auto simp: const_term_def free_term_def app_term_def abs_pred_term_def)
end
instantiation nterm :: strong_term begin
definition wellformed_nterm :: "nterm ⇒ bool" where
[simp]: "wellformed_nterm t ⟷ True"
fun all_frees_nterm :: "nterm ⇒ name fset" where
"all_frees_nterm (Nvar x) = {| x |}" |
"all_frees_nterm (t⇩1 $⇩n t⇩2) = all_frees_nterm t⇩1 |∪| all_frees_nterm t⇩2" |
"all_frees_nterm (Λ⇩n x. t) = finsert x (all_frees_nterm t)" |
"all_frees_nterm (Nconst _) = {||}"
instance proof (standard, goal_cases)
case (7 t)
show ?case
unfolding abs_pred_nterm_def
by auto
qed (auto simp: const_nterm_def free_nterm_def app_nterm_def abs_pred_nterm_def)
end
lemma (in pre_constants) shadows_consts_frees:
fixes t :: "'a::strong_term"
shows "¬ shadows_consts t ⟹ fdisjnt all_consts (frees t)"
unfolding fdisjnt_alt_def shadows_consts_def
using frees_all_frees
by auto
abbreviation wellformed_clauses :: "_ ⇒ bool" where
"wellformed_clauses cs ≡ list_all (λ(pat, t). linear pat ∧ wellformed t) cs ∧ distinct (map fst cs) ∧ cs ≠ []"
end