Theory Idempotent

header {* Idempotents *}

theory Idempotent
imports Main
begin

subsection {* Definition and basic properties *}

constdefs
  idempotent :: "('a => 'a) => bool"
  "idempotent p ≡ ∀x. p (p x) = p x"

lemma idempotent: "idempotent p ==> p (p x) = p x"
by (simp add: idempotent_def)

lemma idempotent_id: "idempotent id"
by (simp add: idempotent_def)

lemma idempotent_const: "idempotent (λx. c)"
by (simp add: idempotent_def)

lemma idempotent_functor:
assumes F2: "!!f g xs. m f (m g xs) = m (λx. f (g x)) xs"
shows "idempotent p ==> idempotent (m p)"
by (simp add: idempotent_def F2)

text {*
  The composition of two idempotents is equal to
  the lesser of the two (if they are comparable).
*}

lemma idempotent_less_comp1:
  "[|idempotent f; idempotent g; range f ⊆ range g|] ==> f (g x) = f x"
oops (* true for projections, but not for idempotents in general *)

lemma idempotent_less_comp2:
  "[|idempotent f; idempotent g; range f ⊆ range g|] ==> g (f x) = f x"
apply (subgoal_tac "f x ∈ range g")
apply clarify
apply (simp add: idempotent_def)
apply (erule subsetD)
apply simp
done


subsection {* Composing idempotents *}

lemma idempotent_fun:
  "[|idempotent p1; idempotent p2|]
    ==> idempotent (λf. p2 o f o p1)"
by (simp add: idempotent_def expand_fun_eq)

lemma idempotent_prod:
  "[|idempotent p1; idempotent p2|]
    ==> idempotent (λ(x,y). (p1 x, p2 y))"
by (simp add: idempotent_def)

lemma idempotent_sum:
  "[|idempotent p1; idempotent p2|]
    ==> idempotent (sum_case (Inl o p1) (Inr o p2))"
by (simp add: idempotent_def split: sum.split)


subsection {* A type of idempotents *}

typedef (open) 'a idem = "{p::'a => 'a. idempotent p}"
by (rule exI, auto intro: idempotent_id)

subsection {* Operations on idempotents *}

subsubsection {* Casting values into an idempotent *}

constdefs
  cast :: "'a idem => 'a => 'a"
  "cast ≡ Rep_idem"

lemma idempotent_cast: "idempotent (cast A)"
by (simp add: cast_def Rep_idem [simplified])

lemma Abs_idem_cast: "Abs_idem (cast A) = A"
by (simp add: cast_def Rep_idem_inverse)

lemma cast_Abs_idem: "idempotent f ==> cast (Abs_idem f) = f"
by (simp add: cast_def Abs_idem_inverse)

lemma cast_idem [simp]: "cast A (cast A x) = cast A x"
by (simp add: idempotent_cast idempotent)

lemma cast_idem2 [simp]: "cast A o cast A = cast A"
by (rule ext, simp)

lemma idempotent_equality: "cast A = cast B ==> A = B"
by (simp add: cast_def Rep_idem_inject)

subsubsection {* Ordering of idempotents *}

instance idem :: (type) ord ..
defs (overloaded)
  le_idem_def:
    "A ≤ B ≡ range (cast A) ⊆ range (cast B)"
(* not antisymmetric! *)

lemma idem_le_refl [simp, intro!]: "(A::'a idem) ≤ A"
by (simp add: le_idem_def)

subsubsection {* Membership in a idempotent *}

constdefs
  in_idem :: "'a => 'a idem => bool" (infixl ":::" 50)
  "x ::: A ≡ cast A x = x"

lemma in_idemI: "cast A x = x ==> x ::: A"
by (simp add: in_idem_def)

lemma in_idemD: "x ::: A ==> ∃y. x = cast A y"
by (unfold in_idem_def, rule exI, erule sym)

lemma in_idemE: "[|x ::: A; !!y. x = cast A y ==> R|] ==> R"
by (drule in_idemD, auto)

lemma cast_in_idem [simp]: "cast A x ::: A"
by (simp add: in_idemI)

lemma cast_fixed: "x ::: A ==> cast A x = x"
by (simp only: in_idem_def)

lemma subidemD: "[|A ≤ B; x ::: A|] ==> x ::: B"
 apply (unfold in_idem_def)
 apply (unfold le_idem_def)
 apply (subgoal_tac "x ∈ range (cast B)")
  apply clarsimp
 apply (erule subsetD)
 apply (erule subst)
 apply simp
done

lemma rev_subidemD: "[|x ::: A; A ≤ B|] ==> x ::: B"
by (rule subidemD)

lemma subidemI: "[|!!x. x ::: A ==> x ::: B|] ==> A ≤ B"
 apply atomize
 apply (simp add: le_idem_def)
 apply (rule subsetI)
 apply (drule_tac x=x in spec)
 apply clarsimp
 apply (simp add: in_idem_def)
 apply (erule subst, simp)
done

lemma nonempty_idem: "∃x. x ::: A"
 apply (unfold in_idem_def)
 apply (rule_tac x="cast A x" in exI)
 apply simp
done


subsubsection {* The identity idempotent *}

lemma cast_id_idem [simp]: "cast (Abs_idem id) = id"
by (simp add: cast_Abs_idem idempotent_id)

lemma in_idem_id_idem [simp, intro]: "x ::: Abs_idem id"
by (simp add: in_idemI)

lemma less_id_idemp [simp, intro]: "A ≤ Abs_idem id"
by (simp add: subidemI)

end