src/HOL/Algebra/abstract/RingHomo.thy

standard headers;

(*  Author: Clemens Ballarin, started 15 April 1997

Ring homomorphism.
*)

header {* Ring homomorphism *}

theory RingHomo
imports Ring2
begin

definition
  homo :: "('a::ring => 'b::ring) => bool" where
  "homo f \<longleftrightarrow> (ALL a b. f (a + b) = f a + f b &
                                   f (a * b) = f a * f b) &
                                   f 1 = 1"


lemma homoI:
  "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b;  
            f 1 = 1 |] ==> homo f"
  unfolding homo_def by blast

lemma homo_add [simp]: "!! f. homo f ==> f (a + b) = f a + f b"
  unfolding homo_def by blast

lemma homo_mult [simp]: "!! f. homo f ==> f (a * b) = f a * f b"
  unfolding homo_def by blast

lemma homo_one [simp]: "!! f. homo f ==> f 1 = 1"
  unfolding homo_def by blast

lemma homo_zero [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0"
  apply (rule_tac a = "f 0" in a_lcancel)
  apply (simp (no_asm_simp) add: homo_add [symmetric])
  done

lemma homo_uminus [simp]:
  "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a"
  apply (rule_tac a = "f a" in a_lcancel)
  apply (frule homo_zero)
  apply (simp (no_asm_simp) add: homo_add [symmetric])
  done

lemma homo_power [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n"
  apply (induct_tac n)
   apply (drule homo_one)
   apply simp
  apply (drule_tac a = "a^n" and b = "a" in homo_mult)
  apply simp
  done

lemma homo_SUM [simp]:
  "!! f::('a::ring=>'b::ring).  
    homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}"
  apply (induct_tac n)
   apply simp
  apply simp
  done

lemma id_homo [simp]: "homo (%x. x)"
  by (blast intro!: homoI)

end