Theory Nominal_Wellfounded

theory Nominal_Wellfounded

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"
  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

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)