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