[STATEMENT]
lemma normal_2: "K \<in> normal \<Longrightarrow> K \<in> convex \<Longrightarrow> K \<in> lsubgroup \<Longrightarrow> x \<in> F K ** {a} \<Longrightarrow> x \<in> {a} ** F K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subst (asm) times_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {aa. \<exists>x\<in>F K. \<exists>y\<in>{a}. aa = x * y}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; \<exists>xa\<in>F K. x = xa * a\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; xa \<in> F K; x = xa * a\<rbrakk> \<Longrightarrow> xa * a \<in> {a} ** F K
[PROOF STEP]
apply (subst (asm) F_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; xa \<in> {a. u - Rep_G a \<in> K}; x = xa * a\<rbrakk> \<Longrightarrow> xa * a \<in> {a} ** F K
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G xa \<in> K; x = xa * a\<rbrakk> \<Longrightarrow> xa * a \<in> {a} ** F K
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> x * a \<in> {a} ** F K
[PROOF STEP]
apply (subgoal_tac "Rep_G x - u \<in> K")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> x * a \<in> {a} ** F K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K\<rbrakk> \<Longrightarrow> x * a \<in> {a} ** F K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst (asm) add_set_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; Rep_G x - u + Rep_G a \<in> {c. \<exists>a\<in>{Rep_G a}. \<exists>b\<in>K. c = a + b}\<rbrakk> \<Longrightarrow> x * a \<in> {a} ** F K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; \<exists>b\<in>K. Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> x * a \<in> {a} ** F K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> x * a \<in> {a} ** F K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: times_set_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> \<exists>y\<in>F K. x * a = a * y
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule_tac x = "Abs_G (inf (sup (u + b) 0) u)" in bexI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> x * a = a * Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "b =  - Rep_G a + Rep_G x - u + Rep_G a")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b; b = - Rep_G a + Rep_G x - u + Rep_G a\<rbrakk> \<Longrightarrow> x * a = a * Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "inf (sup (u + b) 0) u \<in> G")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b; b = - Rep_G a + Rep_G x - u + Rep_G a; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> x * a = a * Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b; b = - Rep_G a + Rep_G x - u + Rep_G a\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a); (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> x * a = a * Abs_G ((u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a); (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> x * a = a * Abs_G ((u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: times_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a); (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Abs_G (Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) = Abs_G ((Rep_G a - u + (u + (- Rep_G a + Rep_G x - u + Rep_G a)) \<squnion> (Rep_G a - u)) \<sqinter> Rep_G a \<squnion> (0::'a))
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: diff_minus add.assoc)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + (Rep_G x + (- u + Rep_G a)) \<in> K; (u + (- Rep_G a + (Rep_G x + (- u + Rep_G a))) \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Abs_G (Rep_G x + (- u + Rep_G a) \<squnion> (0::'a)) = Abs_G ((Rep_G x + (- u + Rep_G a) \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<squnion> (0::'a))
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Abs_G (Rep_G x + - u + Rep_G a \<squnion> (0::'a)) = Abs_G ((Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<squnion> (0::'a))
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "sup (Rep_G x + - u + Rep_G a) 0 = sup (inf (sup (Rep_G x + - u + Rep_G a) (Rep_G a + - u)) (Rep_G a)) 0")
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; Rep_G x + - u + Rep_G a \<squnion> (0::'a) = (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<squnion> (0::'a)\<rbrakk> \<Longrightarrow> Abs_G (Rep_G x + - u + Rep_G a \<squnion> (0::'a)) = Abs_G ((Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<squnion> (0::'a))
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (0::'a) = (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<squnion> (0::'a)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (0::'a) = (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<squnion> (0::'a)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "inf (sup (Rep_G x + - u + Rep_G a) (Rep_G a + - u)) (Rep_G a) = sup (Rep_G x + - u + Rep_G a) (Rep_G a + - u)")
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (0::'a) = (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<squnion> (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (0::'a) = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u) \<squnion> (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
(*apply (subst sup_assoc) - why it does not work*)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (0::'a) = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u) \<squnion> (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst sup_assoc_lgroup)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (0::'a) = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u \<squnion> (0::'a))
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "(sup (Rep_G a + - u) (0::'a)) = 0")
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u); Rep_G a + - u \<squnion> (0::'a) = (0::'a)\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (0::'a) = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u \<squnion> (0::'a))
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G a + - u \<squnion> (0::'a) = (0::'a)
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 6. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 8. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G a + - u \<squnion> (0::'a) = (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G a + - u \<squnion> (0::'a) \<le> (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> (0::'a) \<le> Rep_G a + - u \<squnion> (0::'a)
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 6. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 8. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> (0::'a) \<le> Rep_G a + - u \<squnion> (0::'a)
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 6. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 8. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G a \<le> (0::'a) + - (- u)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> (0::'a) \<le> Rep_G a + - u \<squnion> (0::'a)
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 6. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 8. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> Rep_G a \<le> u
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> (0::'a) \<le> Rep_G a + - u \<squnion> (0::'a)
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 6. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 8. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (cut_tac x = a in Rep_G)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u); Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<le> u
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> (0::'a) \<le> Rep_G a + - u \<squnion> (0::'a)
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 6. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 8. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)\<rbrakk> \<Longrightarrow> (0::'a) \<le> Rep_G a + - u \<squnion> (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a = Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a \<le> Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u) \<le> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u) \<le> (Rep_G x + - u + Rep_G a \<squnion> (Rep_G a + - u)) \<sqinter> Rep_G a
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<le> Rep_G a \<and> Rep_G a + - u \<le> Rep_G a
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u + Rep_G a \<le> Rep_G a
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u \<le> Rep_G a + - Rep_G a
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x + - u \<le> (0::'a)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x \<le> (0::'a) + - (- u)
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G x \<le> u
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (cut_tac x = x in Rep_G)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G; Rep_G x \<in> G\<rbrakk> \<Longrightarrow> Rep_G x \<le> u
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> Rep_G a
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<le> Rep_G a + - (- u)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<le> Rep_G a + u
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule left_move_to_left)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; - Rep_G a + Rep_G x + - u + Rep_G a \<in> K; (u + - Rep_G a + Rep_G x + - u + Rep_G a \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> - Rep_G a + Rep_G a \<le> u
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; - Rep_G a + Rep_G x - u + Rep_G a \<in> K; Rep_G x - u + Rep_G a = Rep_G a + (- Rep_G a + Rep_G x - u + Rep_G a)\<rbrakk> \<Longrightarrow> (u + (- Rep_G a + Rep_G x - u + Rep_G a) \<squnion> (0::'a)) \<sqinter> u \<in> G
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x - u + Rep_G a
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: diff_minus)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> b = - Rep_G a + Rep_G x + - u + Rep_G a
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u) \<in> F K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: F_def2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> - Rep_G (Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u)) + u \<in> K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "inf (sup (u + b) (0::'a)) u \<in> G")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> - Rep_G (Abs_G ((u + b \<squnion> (0::'a)) \<sqinter> u)) + u \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (- (u + b) + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: diff_minus minus_add add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst (asm) convex_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> {A. \<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> |[ a , b ]| \<subseteq> A}; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; \<forall>a b. a \<in> K \<and> b \<in> K \<longrightarrow> |[ a , b ]| \<subseteq> K; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (drule_tac x = 0 in spec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; \<forall>b. (0::'a) \<in> K \<and> b \<in> K \<longrightarrow> |[ 0::'a , b ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (drule_tac x = "sup (- b) 0" in spec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (0::'a) \<in> K \<and> - b \<squnion> (0::'a) \<in> K \<longrightarrow> |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - b \<squnion> (0::'a) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst (asm) lsubgroup_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> {A \<in> subgroup. \<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> a \<sqinter> b \<in> A \<and> a \<squnion> b \<in> A}; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - b \<squnion> (0::'a) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - b \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule sup_lsubgroup)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> K \<in> lsubgroup
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - b \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - b \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule minus_subgroup)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> K \<in> subgroup
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - (- b) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst (asm) lsubgroup_def)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> {A \<in> subgroup. \<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> a \<sqinter> b \<in> A \<and> a \<squnion> b \<in> A}; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> K \<in> subgroup
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - (- b) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 5. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 7. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> - (- b) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 4. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 6. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst (asm) lsubgroup_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> {A \<in> subgroup. \<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> a \<sqinter> b \<in> A \<and> a \<squnion> b \<in> A}; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<notin> K\<rbrakk> \<Longrightarrow> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + - u + Rep_G a = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (- b + - u + u) \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - b \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac "sup (inf (- b) u) (0::'a) \<in> |[ 0::'a , sup (-b) 0]|")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K; - b \<sqinter> u \<squnion> (0::'a) \<in> |[ 0::'a , - b \<squnion> (0::'a) ]|\<rbrakk> \<Longrightarrow> - b \<sqinter> u \<squnion> (0::'a) \<in> K
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - b \<sqinter> u \<squnion> (0::'a) \<in> |[ 0::'a , - b \<squnion> (0::'a) ]|
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - b \<sqinter> u \<squnion> (0::'a) \<in> |[ 0::'a , - b \<squnion> (0::'a) ]|
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst closed_interval_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - b \<sqinter> u \<squnion> (0::'a) \<in> {c. (0::'a) \<le> c \<and> c \<le> - b \<squnion> (0::'a)}
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (0::'a) \<le> - b \<sqinter> u \<squnion> (0::'a)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - b \<sqinter> u \<squnion> (0::'a) \<le> - b \<squnion> (0::'a)
 3. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 5. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; u + - Rep_G x \<in> K; Rep_G x + - u \<in> K; b \<in> K; Rep_G x + (- u + Rep_G a) = Rep_G a + b; (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G; |[ 0::'a , - b \<squnion> (0::'a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - b \<sqinter> u \<squnion> (0::'a) \<le> - b \<squnion> (0::'a)
 2. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 4. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
(*
  apply (rule_tac y = "-b" in order_trans)
  apply simp
  apply simp
*)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; b \<in> K; Rep_G x - u + Rep_G a = Rep_G a + b\<rbrakk> \<Longrightarrow> (u + b \<squnion> (0::'a)) \<sqinter> u \<in> G
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subgoal_tac  "{Rep_G a} +++ K = K +++ {Rep_G a}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; {Rep_G a} +++ K = K +++ {Rep_G a}\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> {Rep_G a} +++ K
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> {Rep_G a} +++ K = K +++ {Rep_G a}
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K; {Rep_G a} +++ K = K +++ {Rep_G a}\<rbrakk> \<Longrightarrow> Rep_G x - u + Rep_G a \<in> K +++ {Rep_G a}
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> {Rep_G a} +++ K = K +++ {Rep_G a}
 3. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (simp add: add_set_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> {Rep_G a} +++ K = K +++ {Rep_G a}
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (subst (asm) normal_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>K \<in> {A. \<forall>a. A +++ {a} = {a} +++ A}; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K; Rep_G x - u \<in> K\<rbrakk> \<Longrightarrow> {Rep_G a} +++ K = K +++ {Rep_G a}
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> Rep_G x - u \<in> K
[PROOF STEP]
apply (rule minus_subgroup)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> K \<in> subgroup
 2. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> - (Rep_G x - u) \<in> K
[PROOF STEP]
apply (simp add: lsubgroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; u - Rep_G x \<in> K\<rbrakk> \<Longrightarrow> - (Rep_G x - u) \<in> K
[PROOF STEP]
by (simp add: diff_minus minus_add)