# Theory Nominal_Wellfounded

```theory Nominal_Wellfounded
imports
Nominal2.Nominal2
begin

section ‹Lemmas about Well-Foundedness and Permutations›

definition less_bool_rel :: "bool rel" where
"less_bool_rel ≡ {(x,y). x<y}"

lemma less_bool_rel_iff [simp]:
"(a,b) ∈ less_bool_rel ⟷ ¬ a ∧ b"
by (metis less_bool_def less_bool_rel_def mem_Collect_eq split_conv)

lemma wf_less_bool_rel: "wf less_bool_rel"
by (metis less_bool_rel_iff wfUNIVI)

subsection ‹Hull and well-foundedness›

inductive_set hull_rel where
"(p ∙ x, x) ∈ hull_rel"

lemma hull_relp_reflp: "reflp hull_relp"
by (metis hull_relp.intros permute_zero reflpI)

lemma hull_relp_symp: "symp hull_relp"
by (metis (poly_guards_query) hull_relp.simps permute_minus_cancel(2) sympI)

lemma hull_relp_transp: "transp hull_relp"
by (metis (full_types) hull_relp.simps permute_plus transpI)

lemma hull_relp_equivp: "equivp hull_relp"
by (metis equivpI hull_relp_reflp hull_relp_symp hull_relp_transp)

lemma hull_rel_relcomp_subset:
assumes "eqvt R"
shows "R O hull_rel ⊆ hull_rel O R"
proof
fix x
assume "x ∈ R O hull_rel"
then obtain x1 x2 y where x: "x = (x1,x2)" and R: "(x1,y) ∈ R" and "(y,x2) ∈ hull_rel"
by auto
then obtain p where "y = p ∙ x2"
by (metis hull_rel.simps)
then have "-p ∙ y = x2"
by (metis permute_minus_cancel(2))
then have "(-p ∙ x1, x2) ∈ R"
using R assms by (metis Pair_eqvt eqvt_def mem_permute_iff)
moreover have "(x1, -p ∙ x1) ∈ hull_rel"
by (metis hull_rel.intros permute_minus_cancel(2))
ultimately show "x ∈ hull_rel O R"
using x by auto
qed

lemma wf_hull_rel_relcomp:
assumes "wf R" and "eqvt R"
shows "wf (hull_rel O R)"
using assms by (metis hull_rel_relcomp_subset wf_relcomp_compatible)

lemma hull_rel_relcompI [simp]:
assumes "(x, y) ∈ R"
shows "(p ∙ x, y) ∈ hull_rel O R"
using assms by (metis hull_rel.intros relcomp.relcompI)

lemma hull_rel_relcomp_trivialI [simp]:
assumes "(x, y) ∈ R"
shows "(x, y) ∈ hull_rel O R"
using assms by (metis hull_rel_relcompI permute_zero)

end
```