[STATEMENT]
lemma ring_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      A ===> 
      (A ===> A ===> A) ===> 
      (A ===> A) ===> 
      (A ===> A ===> A) ===> 
      (=)
    ) 
    (ring_ow (Collect (Domainp A))) class.ring"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (A ===> A ===> A) ===> (=)) (ring_ow (Collect (Domainp A))) class.ring
[PROOF STEP]
unfolding ring_ow_def class.ring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (A ===> A ===> A) ===> (=)) (\<lambda>plus zero minus uminus times. semiring_ow (Collect (Domainp A)) plus times \<and> ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus) (\<lambda>plus zero minus uminus times. class.ab_group_add plus zero minus uminus \<and> class.semiring plus times)
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Transfer.Rel ((A ===> A ===> A) ===> (A ===> A ===> A) ===> ?Ri11) ?ab11 class.semiring
 2. Transfer.Rel ((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> ?Rh11) ?aa11 class.ab_group_add
 3. Transfer.Rel (?Rh11 ===> ?Ri11 ===> (=)) ?a11 (\<and>)
 4. (\<lambda>plus zero minus uminus times. semiring_ow (Collect (Domainp A)) plus times \<and> ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus) = (\<lambda>plus zero minus uminus times. ?a11 (?aa11 plus zero minus uminus) (?ab11 plus times))
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>plus zero minus uminus times. semiring_ow (Collect (Domainp A)) plus times \<and> ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus) = (\<lambda>plus zero minus uminus times. ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus \<and> semiring_ow (Collect (Domainp A)) plus times)
[PROOF STEP]
by blast