[STATEMENT]
lemma ring_of_integers:"Ring Zr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring Zr
[PROOF STEP]
apply (simp add:Ring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<plusminus>\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> c = a \<plusminus>\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b = b \<plusminus>\<^bsub>Zr\<^esub> a)) \<and> mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<plusminus>\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr
 2. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> c = a \<plusminus>\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b = b \<plusminus>\<^bsub>Zr\<^esub> a)) \<and> mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> c = a \<plusminus>\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b = b \<plusminus>\<^bsub>Zr\<^esub> a)) \<and> mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> c = a \<plusminus>\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c)))
 2. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b = b \<plusminus>\<^bsub>Zr\<^esub> a)) \<and> mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b = b \<plusminus>\<^bsub>Zr\<^esub> a)) \<and> mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b = b \<plusminus>\<^bsub>Zr\<^esub> a)
 2. mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> carrier Zr; b \<in> carrier Zr\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>Zr\<^esub> b = b \<plusminus>\<^bsub>Zr\<^esub> a
 2. mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mop Zr \<in> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mop Zr \<in> carrier Zr \<rightarrow> carrier Zr
 2. (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier Zr \<longrightarrow> -\<^sub>a\<^bsub>Zr\<^esub> a \<plusminus>\<^bsub>Zr\<^esub> a = \<zero>\<^bsub>Zr\<^esub>) \<and> \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI,
       rule allI, rule impI, simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero>\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI, simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier Zr \<longrightarrow> \<zero>\<^bsub>Zr\<^esub> \<plusminus>\<^bsub>Zr\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI,
       rule allI, rule impI, simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<cdot>\<^sub>r\<^bsub>Zr\<^esub>) \<in> carrier Zr \<rightarrow> carrier Zr \<rightarrow> carrier Zr
 2. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI,
       (rule allI, rule impI)+, simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI,
       (rule allI, rule impI)+, simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr
 2. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier Zr \<longrightarrow> (\<forall>b. b \<in> carrier Zr \<longrightarrow> (\<forall>c. c \<in> carrier Zr \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (b \<plusminus>\<^bsub>Zr\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> b \<plusminus>\<^bsub>Zr\<^esub> a \<cdot>\<^sub>r\<^bsub>Zr\<^esub> c))) \<and> (\<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a)
[PROOF STEP]
apply (rule conjI,
       (rule allI, rule impI)+, simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. a * (c + b) = a * c + a * b
 2. \<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a
[PROOF STEP]
apply (simp add: distrib_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. a \<in> carrier Zr \<longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> carrier Zr \<Longrightarrow> 1\<^sub>r\<^bsub>Zr\<^esub> \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a = a
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Zr_zero:"\<zero>\<^bsub>Zr\<^esub> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero>\<^bsub>Zr\<^esub> = 0
[PROOF STEP]
by (simp add:Zr_def)


[STATEMENT]
lemma Zr_one:"1\<^sub>r\<^bsub>Zr\<^esub> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r\<^bsub>Zr\<^esub> = 1
[PROOF STEP]
by (simp add:Zr_def)


[STATEMENT]
lemma Zr_minus:"-\<^sub>a\<^bsub>Zr\<^esub> n = - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. -\<^sub>a\<^bsub>Zr\<^esub> n = - n
[PROOF STEP]
by (simp add:Zr_def Zset_def)


[STATEMENT]
lemma Zr_add:"n \<plusminus>\<^bsub>Zr\<^esub> m = n + m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<plusminus>\<^bsub>Zr\<^esub> m = n + m
[PROOF STEP]
by (simp add:Zr_def Zset_def)


[STATEMENT]
lemma Zr_times:"n \<cdot>\<^sub>r\<^bsub>Zr\<^esub> m = n * m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<cdot>\<^sub>r\<^bsub>Zr\<^esub> m = n * m
[PROOF STEP]
by (simp add:Zr_def Zset_def)


[STATEMENT]
lemma Zr_gen_Zleast:"\<lbrakk>ideal Zr I; I \<noteq> {0::int}\<rbrakk> \<Longrightarrow>
                       Rxa Zr (lev I) = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (cut_tac ring_of_integers)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (simp add:lev_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p Zleast {n \<in> I. 0 < n} = I
[PROOF STEP]
apply (subgoal_tac "{n. n \<in> I \<and> 0 < n} \<noteq> {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p Zleast {n \<in> I. 0 < n} = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
[PROOF STEP]
apply (subgoal_tac "{n. n \<in> I \<and> 0 < n} \<subseteq> Zset")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p Zleast {n \<in> I. 0 < n} = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<subseteq> Zset
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
[PROOF STEP]
apply (subgoal_tac "LB {n. n \<in> I \<and> 0 < n} 0")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p Zleast {n \<in> I. 0 < n} = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset\<rbrakk> \<Longrightarrow> LB {n \<in> I. 0 < n} 0
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<subseteq> Zset
 4. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
[PROOF STEP]
apply (frule_tac A = "{n. n \<in> I \<and> 0 < n}" and n = 0 in Zleast, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; Zleast {n \<in> I. 0 < n} \<in> {n \<in> I. 0 < n} \<and> (\<forall>x\<in>{n \<in> I. 0 < n}. Zleast {n \<in> I. 0 < n} \<le> x)\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p Zleast {n \<in> I. 0 < n} = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset\<rbrakk> \<Longrightarrow> LB {n \<in> I. 0 < n} 0
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<subseteq> Zset
 4. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; Zleast {n \<in> I. 0 < n} \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. Zleast {n \<in> I. 0 < n} \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p Zleast {n \<in> I. 0 < n} = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset\<rbrakk> \<Longrightarrow> LB {n \<in> I. 0 < n} 0
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<subseteq> Zset
 4. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
[PROOF STEP]
apply (fold lev_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset\<rbrakk> \<Longrightarrow> LB {n \<in> I. 0 < n} 0
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<subseteq> Zset
 4. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset\<rbrakk> \<Longrightarrow> LB {n \<in> I. 0 < n} 0
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<subseteq> Zset
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
 4. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (simp add:LB_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<subseteq> Zset
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (simp add:Zset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr\<rbrakk> \<Longrightarrow> {n \<in> I. 0 < n} \<noteq> {}
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (frule Ring.ideal_zero[of "Zr" "I"], assumption+, simp add:Zr_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; 0 \<in> I\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (frule singleton_sub[of "0" "I"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; 0 \<in> I; {0} \<subseteq> I\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (frule sets_not_eq[of "I" "{0}"], assumption+, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; 0 \<in> I; a \<in> I; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (case_tac "0 < a", blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; 0 \<in> I; a \<in> I; a \<noteq> 0; \<not> 0 < a\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (frule Ring.ring_one[of "Zr"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; 0 \<in> I; a \<in> I; a \<noteq> 0; \<not> 0 < a; 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "Zr"],
         frule aGroup.ag_mOp_closed[of "Zr" "1\<^sub>r\<^bsub>Zr\<^esub>"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; 0 \<in> I; a \<in> I; a \<noteq> 0; \<not> 0 < a; 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr; aGroup Zr; -\<^sub>a\<^bsub>Zr\<^esub> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (frule_tac x = a in Ring.ideal_ring_multiple[of "Zr" "I" _ "-\<^sub>a\<^bsub>Zr\<^esub> 1\<^sub>r\<^bsub>Zr\<^esub>"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; 0 \<in> I; a \<in> I; a \<noteq> 0; \<not> 0 < a; 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr; aGroup Zr; -\<^sub>a\<^bsub>Zr\<^esub> 1\<^sub>r\<^bsub>Zr\<^esub> \<in> carrier Zr; (-\<^sub>a\<^bsub>Zr\<^esub> 1\<^sub>r\<^bsub>Zr\<^esub>) \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a \<in> I\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (simp add:Zr_one Zr_minus,
        thin_tac "ideal Zr I", thin_tac "Ring Zr", thin_tac "1 \<in> carrier Zr",
        thin_tac "-1 \<in> carrier Zr", thin_tac "aGroup Zr")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>I \<noteq> {0}; 0 \<in> I; a \<in> I; a \<noteq> 0; \<not> 0 < a; - 1 \<cdot>\<^sub>r\<^bsub>Zr\<^esub> a \<in> I\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>I \<noteq> {0}; 0 \<in> I; a \<in> I; a \<noteq> 0; \<not> 0 < a; - a \<in> I\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> 0 < x
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (subgoal_tac "0 < - a", blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>I \<noteq> {0}; 0 \<in> I; a \<in> I; a \<noteq> 0; \<not> 0 < a; - a \<in> I\<rbrakk> \<Longrightarrow> 0 < - a
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; {n \<in> I. 0 < n} \<noteq> {}; {n \<in> I. 0 < n} \<subseteq> Zset; LB {n \<in> I. 0 < n} 0; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (thin_tac "{n \<in> I. 0 < n} \<noteq> {}", thin_tac "{n \<in> I. 0 < n} \<subseteq> Zset",
        thin_tac "LB {n \<in> I. 0 < n} 0")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; lev I \<in> {n \<in> I. 0 < n}; \<forall>x\<in>{n \<in> I. 0 < n}. lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; lev I \<in> I \<and> 0 < lev I; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (frule Ring.ideal_cont_Rxa[of "Zr" "I" "lev I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; Zr \<diamondsuit>\<^sub>p lev I \<subseteq> I\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p lev I = I
[PROOF STEP]
apply (rule equalityI, assumption,
        thin_tac "Rxa Zr (lev I) \<subseteq> I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I\<rbrakk> \<Longrightarrow> I \<subseteq> Zr \<diamondsuit>\<^sub>p lev I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I\<rbrakk> \<Longrightarrow> x \<in> Zr \<diamondsuit>\<^sub>p lev I
[PROOF STEP]
apply (simp add:Rxa_def, simp add:Zr_times)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier Zr. x = r * lev I
[PROOF STEP]
apply (cut_tac t = x and b = "lev I" in mult_div_mod_eq [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier Zr. x = r * lev I
[PROOF STEP]
apply (subgoal_tac "x = (x div lev I) * (lev I)",
        subgoal_tac "x div lev I \<in> carrier Zr", blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I; x = x div lev I * lev I\<rbrakk> \<Longrightarrow> x div lev I \<in> carrier Zr
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x = x div lev I * lev I
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x = x div lev I * lev I
[PROOF STEP]
apply (subgoal_tac "x mod lev I = 0", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I); x mod lev I = 0\<rbrakk> \<Longrightarrow> x = x div lev I * lev I
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I = 0
[PROOF STEP]
apply (subst mult.commute, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I = 0
[PROOF STEP]
apply (subgoal_tac "x mod lev I \<in> I")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I; x mod lev I \<in> I\<rbrakk> \<Longrightarrow> x mod lev I = 0
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (thin_tac "x = lev I * (x div lev I) + x mod lev I")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x mod lev I \<in> I\<rbrakk> \<Longrightarrow> x mod lev I = 0
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (frule_tac a = x in Divides.pos_mod_conj[of "lev I"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x mod lev I \<in> I; 0 \<le> x mod lev I \<and> x mod lev I < lev I\<rbrakk> \<Longrightarrow> x mod lev I = 0
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; x \<in> I; x mod lev I \<in> I; 0 \<le> x mod lev I \<and> x mod lev I < lev I; x mod lev I \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; x \<in> I; x mod lev I \<in> I; x mod lev I \<noteq> 0; 0 \<le> x mod lev I; x mod lev I < lev I\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (frule_tac a = "x mod (lev I)" in forall_spec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; x \<in> I; x mod lev I \<in> I; x mod lev I \<noteq> 0; 0 \<le> x mod lev I; x mod lev I < lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I \<and> 0 < x mod lev I
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; x \<in> I; x mod lev I \<in> I; x mod lev I \<noteq> 0; 0 \<le> x mod lev I; x mod lev I < lev I; lev I \<le> x mod lev I\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; x \<in> I; x mod lev I \<in> I; x mod lev I \<noteq> 0; 0 \<le> x mod lev I; x mod lev I < lev I; lev I \<le> x mod lev I\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (frule_tac r = "x div (lev I)" in
          Ring.ideal_ring_multiple1[of "Zr" "I" "lev I"], assumption+,
          simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; x = lev I * (x div lev I) + x mod lev I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (frule sym, thin_tac "x = lev I * (x div lev I) + x mod lev I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> x mod lev I \<in> I
[PROOF STEP]
apply (rule_tac a = "lev I * (x div lev I)" and b = "x mod lev I " in
         Ring.ideal_ele_sumTr1[of "Zr" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<in> carrier Zr
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> x mod lev I \<in> carrier Zr
 3. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<plusminus>\<^bsub>Zr\<^esub> x mod lev I \<in> I
 4. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<in> I
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> x mod lev I \<in> carrier Zr
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<plusminus>\<^bsub>Zr\<^esub> x mod lev I \<in> I
 3. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<in> I
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<plusminus>\<^bsub>Zr\<^esub> x mod lev I \<in> I
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<in> I
[PROOF STEP]
apply (subst Zr_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) + x mod lev I \<in> I
 2. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal Zr I; I \<noteq> {0}; Ring Zr; \<forall>x. x \<in> I \<and> 0 < x \<longrightarrow> lev I \<le> x; lev I \<in> I; 0 < lev I; x \<in> I; lev I \<cdot>\<^sub>r\<^bsub>Zr\<^esub> (x div lev I) \<in> I; lev I * (x div lev I) + x mod lev I = x\<rbrakk> \<Longrightarrow> lev I * (x div lev I) \<in> I
[PROOF STEP]
apply (simp add:Zr_times)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Zr_pir:"ideal Zr I \<Longrightarrow> \<exists>n. Rxa Zr n = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal Zr I \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
(** principal ideal ring *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal Zr I \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (case_tac "I = {(0::int)}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (subgoal_tac "Rxa Zr 0 = I")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal Zr I; I = {0}; Zr \<diamondsuit>\<^sub>p 0 = I\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
 2. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p 0 = I
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p 0 = I
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> Zr \<diamondsuit>\<^sub>p 0 \<subseteq> I
 2. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> I \<subseteq> Zr \<diamondsuit>\<^sub>p 0
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I = {0}; x \<in> Zr \<diamondsuit>\<^sub>p 0\<rbrakk> \<Longrightarrow> x \<in> I
 2. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> I \<subseteq> Zr \<diamondsuit>\<^sub>p 0
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (simp add:Rxa_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr {0}; I = {0}; \<exists>r\<in>carrier Zr. x = r \<cdot>\<^sub>r\<^bsub>Zr\<^esub> 0\<rbrakk> \<Longrightarrow> x = 0
 2. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> I \<subseteq> Zr \<diamondsuit>\<^sub>p 0
 3. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (simp add:Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal Zr I; I = {0}\<rbrakk> \<Longrightarrow> I \<subseteq> Zr \<diamondsuit>\<^sub>p 0
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal Zr I; I = {0}; x \<in> I\<rbrakk> \<Longrightarrow> x \<in> Zr \<diamondsuit>\<^sub>p 0
 2. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (simp add:Rxa_def Zr_def Zset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply (frule Zr_gen_Zleast [of "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal Zr I; I \<noteq> {0}; Zr \<diamondsuit>\<^sub>p lev I = I\<rbrakk> \<Longrightarrow> \<exists>n. Zr \<diamondsuit>\<^sub>p n = I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) mem_set_ar_cos:"\<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow>
                                         a \<uplus>\<^bsub>R\<^esub> I \<in> set_ar_cos R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I \<in> set_ar_cos R I
[PROOF STEP]
by (simp add:set_ar_cos_def, blast)


[STATEMENT]
lemma (in Ring) I_in_set_ar_cos:"ideal R I \<Longrightarrow> I \<in> set_ar_cos R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<in> set_ar_cos R I
[PROOF STEP]
apply (cut_tac ring_is_ag,
       frule ideal_asubg[of "I"],
       rule aGroup.unit_in_set_ar_cos, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_same1:"\<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R;
       b \<plusminus> (-\<^sub>a a) \<in> I \<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; b \<plusminus> -\<^sub>a a \<in> I\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; b \<plusminus> -\<^sub>a a \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule aGroup.b_ag_group[of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:ideal_def asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier R; b \<in> carrier R; b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule aGroup.ag_carrier_carrier[THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; carrier R = carrier (b_ag R)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; \<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; carrier R = carrier (b_ag R)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule Group.rcs_eq[of "b_ag R" "I" "a" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; \<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; carrier R = carrier (b_ag R); (b \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I) = (I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule aGroup.agop_gop [of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; \<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; carrier R = carrier (b_ag R); (b \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I) = (I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b); (\<cdot>\<^bsub>b_ag R\<^esub>) = (\<plusminus>)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule aGroup.agiop_giop[of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; \<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; carrier R = carrier (b_ag R); (b \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I) = (I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b); (\<cdot>\<^bsub>b_ag R\<^esub>) = (\<plusminus>); iop (b_ag R) = mop R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); b \<plusminus> -\<^sub>a a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; \<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; carrier R = carrier (b_ag R); I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; (\<cdot>\<^bsub>b_ag R\<^esub>) = (\<plusminus>); iop (b_ag R) = mop R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:ar_coset_def rcs_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_same2:"\<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R;
                                  a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow>  b \<plusminus> (-\<^sub>a a) \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; a \<uplus>\<^bsub>R\<^esub> I = b \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
[PROOF STEP]
apply (frule aGroup.b_ag_group[of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
[PROOF STEP]
apply (simp add:ideal_def asubGroup_def, frule conjunct1, fold asubGroup_def,
        fold ideal_def, simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
[PROOF STEP]
apply (subgoal_tac "a \<in> carrier (b_ag R)",
         subgoal_tac "b \<in> carrier (b_ag R)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 3. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
[PROOF STEP]
apply (simp add:Group.rcs_eq[THEN sym, of "b_ag R" "I" "a" "b"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; b \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 3. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
[PROOF STEP]
apply (frule aGroup.agop_gop [of "R"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; b \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); (\<cdot>\<^bsub>b_ag R\<^esub>) = (\<plusminus>)\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 3. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
[PROOF STEP]
apply (frule aGroup.agiop_giop[of "R"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; b \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); (\<cdot>\<^bsub>b_ag R\<^esub>) = (\<plusminus>); iop (b_ag R) = mop R\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 3. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I ; a \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> b; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
[PROOF STEP]
apply (simp add:b_ag_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_same3:"\<lbrakk>ideal R I; a \<in> carrier R; a \<uplus>\<^bsub>R\<^esub> I = I\<rbrakk> \<Longrightarrow>
                               a\<in>I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<uplus>\<^bsub>R\<^esub> I = I\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<uplus>\<^bsub>R\<^esub> I = I; aGroup R\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (rule Group.rcs_fixed [of "b_ag R" "I" "a" ])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> Group (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 3. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 4. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> a = I
[PROOF STEP]
apply (rule aGroup.b_ag_group, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 3. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> a = I
[PROOF STEP]
apply (simp add:ideal_def asubGroup_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> a = I
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; I \<bullet>\<^bsub>b_ag R\<^esub> a = I; aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> a = I
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_same3_1:"\<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I\<rbrakk> \<Longrightarrow>
                                                    a \<uplus>\<^bsub>R\<^esub> I \<noteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I \<noteq> I
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; a \<uplus>\<^bsub>R\<^esub> I = I\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:ar_coset_same3)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_same4:"\<lbrakk>ideal R I; a \<in> I\<rbrakk> \<Longrightarrow>
                                     a \<uplus>\<^bsub>R\<^esub> I = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> I\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = I
[PROOF STEP]
apply (frule ideal_subset[of "I" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = I
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> a = I
[PROOF STEP]
apply (rule Group.rcs_Unit2 [of "b_ag R" "I""a"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> Group (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 3. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (rule aGroup.b_ag_group, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 2. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (simp add:ideal_def asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> I; aGroup R; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_same4_1:"\<lbrakk>ideal R I; a \<uplus>\<^bsub>R\<^esub> I \<noteq> I\<rbrakk> \<Longrightarrow> a \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<uplus>\<^bsub>R\<^esub> I \<noteq> I\<rbrakk> \<Longrightarrow> a \<notin> I
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<uplus>\<^bsub>R\<^esub> I \<noteq> I; a \<in> I\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:ar_coset_same4)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) belong_ar_coset1:"\<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R;
                 x \<plusminus> (-\<^sub>a a) \<in> I\<rbrakk> \<Longrightarrow>  x \<in> a \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I\<rbrakk> \<Longrightarrow> x \<in> a \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule ar_coset_same1 [of "I" "a" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> x \<in> a \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (subgoal_tac "x \<in> x \<uplus>\<^bsub>R\<^esub> I")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; x \<in> x \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> x \<in> a \<uplus>\<^bsub>R\<^esub> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> x \<in> x \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> x \<in> x \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> x \<in> x \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (subgoal_tac "carrier R = carrier (b_ag R)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R; carrier R = carrier (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> x \<uplus>\<^bsub>R\<^esub> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (frule aGroup.agop_gop[THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> x \<uplus>\<^bsub>R\<^esub> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (frule aGroup.agiop_giop [THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> x \<uplus>\<^bsub>R\<^esub> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> x
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add:ideal_def asubGroup_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> x
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (rule Group.a_in_rcs [of "b_ag R" "I" "x"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> Group (b_ag R)
 2. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 3. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> carrier (b_ag R)
 4. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add: aGroup.b_ag_group)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 2. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> carrier (b_ag R)
 3. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> carrier (b_ag R); x \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> a \<in> I; I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> x; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> carrier (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> carrier R; x \<plusminus> -\<^sub>a a \<in> I; a \<uplus>\<^bsub>R\<^esub> I = x \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) a_in_ar_coset:"\<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<in> a \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<in> a \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (rule belong_ar_coset1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a a \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a a \<in> I
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<zero> \<in> I
[PROOF STEP]
apply (simp add:ideal_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_subsetD:"\<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I \<rbrakk> \<Longrightarrow>
                           x \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> x \<in> carrier R
[PROOF STEP]
apply (subgoal_tac "carrier R = carrier (b_ag R)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; carrier R = carrier (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; carrier R = carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (frule aGroup.agop_gop [THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (frule aGroup.agiop_giop [THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> carrier (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add:ideal_def asubGroup_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> carrier (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (rule Group.rcs_subset_elem[of "b_ag R" "I" "a" "x"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> Group (b_ag R)
 2. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 3. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 4. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a
 5. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add:aGroup.b_ag_group)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> b_ag R \<guillemotright> I
 2. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 3. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a
 4. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 2. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; carrier R = carrier (b_ag R); aGroup R; (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a
 3. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> carrier R = carrier (b_ag R)
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done