[STATEMENT]
lemma [simp]: "a * (1::'a G) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * 1 = a
[PROOF STEP]
apply (simp add: one_def times_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G (Rep_G a - u + Rep_G (Abs_G u) \<squnion> (0::'a)) = a
[PROOF STEP]
apply (cut_tac y = "u::'a" in Abs_G_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. u \<in> G
 2. Rep_G (Abs_G u) = u \<Longrightarrow> Abs_G (Rep_G a - u + Rep_G (Abs_G u) \<squnion> (0::'a)) = a
[PROOF STEP]
apply (simp_all add: diff_minus add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G (Abs_G u) = u \<Longrightarrow> Abs_G (Rep_G a \<squnion> (0::'a)) = a
[PROOF STEP]
apply (subgoal_tac "sup (Rep_G a) (0::'a) = Rep_G a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<squnion> (0::'a) = Rep_G a\<rbrakk> \<Longrightarrow> Abs_G (Rep_G a \<squnion> (0::'a)) = a
 2. Rep_G (Abs_G u) = u \<Longrightarrow> Rep_G a \<squnion> (0::'a) = Rep_G a
[PROOF STEP]
apply (simp add: Rep_G_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G (Abs_G u) = u \<Longrightarrow> Rep_G a \<squnion> (0::'a) = Rep_G a
[PROOF STEP]
apply (cut_tac x = a in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<squnion> (0::'a) = Rep_G a
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<squnion> (0::'a) \<le> Rep_G a
 2. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<le> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
by (simp_all add: G_def)


[STATEMENT]
lemma [simp]: "a l\<rightarrow> a = (1::'a G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> a = 1
[PROOF STEP]
by (simp add: one_def impl_def)


[STATEMENT]
lemma [simp]: "a r\<rightarrow> a = (1::'a G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> a = 1
[PROOF STEP]
by (simp add: one_def impr_def diff_minus add.assoc)


[STATEMENT]
lemma [simp]: "a \<in> G \<Longrightarrow> Rep_G (Abs_G a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> G \<Longrightarrow> Rep_G (Abs_G a) = a
[PROOF STEP]
apply (rule Abs_G_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> G \<Longrightarrow> a \<in> G
[PROOF STEP]
by simp


[STATEMENT]
lemma inf_def_1: "((a::'a G) l\<rightarrow> b) * a = Abs_G (inf (Rep_G a) (Rep_G b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) * a = Abs_G (Rep_G a \<sqinter> Rep_G b)
[PROOF STEP]
apply (simp add: times_def impl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G (Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)) = Abs_G (Rep_G a \<sqinter> Rep_G b)
[PROOF STEP]
apply (subgoal_tac "sup (inf (Rep_G b) (Rep_G a)) 0 = inf (Rep_G a) (Rep_G b)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) = Rep_G a \<sqinter> Rep_G b \<Longrightarrow> Abs_G (Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)) = Abs_G (Rep_G a \<sqinter> Rep_G b)
 2. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) = Rep_G a \<sqinter> Rep_G b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) = Rep_G a \<sqinter> Rep_G b
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) \<le> Rep_G a \<sqinter> Rep_G b
 2. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (cut_tac x = "a" in Rep_G)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<in> G \<Longrightarrow> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) \<le> Rep_G a \<sqinter> Rep_G b
 2. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (cut_tac x = "b" in Rep_G)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_G a \<in> G; Rep_G b \<in> G\<rbrakk> \<Longrightarrow> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) \<le> Rep_G a \<sqinter> Rep_G b
 2. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (subgoal_tac "inf (Rep_G a) (Rep_G b) = inf (Rep_G b) (Rep_G a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<sqinter> Rep_G b = Rep_G b \<sqinter> Rep_G a \<Longrightarrow> Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
 2. Rep_G a \<sqinter> Rep_G b = Rep_G b \<sqinter> Rep_G a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<sqinter> Rep_G b = Rep_G b \<sqinter> Rep_G a
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a
 2. Rep_G b \<sqinter> Rep_G a \<le> Rep_G a \<sqinter> Rep_G b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma inf_def_2: "(a::'a G) * (a r\<rightarrow> b) = Abs_G (inf (Rep_G a) (Rep_G b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (a r\<rightarrow> b) = Abs_G (Rep_G a \<sqinter> Rep_G b)
[PROOF STEP]
apply (simp add: times_def impr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G a - u + (u - Rep_G a + Rep_G b)) \<sqinter> Rep_G a \<squnion> (0::'a)) = Abs_G (Rep_G a \<sqinter> Rep_G b)
[PROOF STEP]
apply (simp add: diff_minus add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G a + - u + u + - Rep_G a + Rep_G b) \<sqinter> Rep_G a \<squnion> (0::'a)) = Abs_G (Rep_G a \<sqinter> Rep_G b)
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G (Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)) = Abs_G (Rep_G a \<sqinter> Rep_G b)
[PROOF STEP]
apply (subgoal_tac "sup (inf (Rep_G b) (Rep_G a)) 0 = inf (Rep_G a) (Rep_G b)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) = Rep_G a \<sqinter> Rep_G b \<Longrightarrow> Abs_G (Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)) = Abs_G (Rep_G a \<sqinter> Rep_G b)
 2. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) = Rep_G a \<sqinter> Rep_G b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) = Rep_G a \<sqinter> Rep_G b
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) \<le> Rep_G a \<sqinter> Rep_G b
 2. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (cut_tac x = "a" in Rep_G)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<in> G \<Longrightarrow> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) \<le> Rep_G a \<sqinter> Rep_G b
 2. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (cut_tac x = "b" in Rep_G)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_G a \<in> G; Rep_G b \<in> G\<rbrakk> \<Longrightarrow> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a) \<le> Rep_G a \<sqinter> Rep_G b
 2. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (subgoal_tac "inf (Rep_G a) (Rep_G b) = inf (Rep_G b) (Rep_G a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<sqinter> Rep_G b = Rep_G b \<sqinter> Rep_G a \<Longrightarrow> Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a \<squnion> (0::'a)
 2. Rep_G a \<sqinter> Rep_G b = Rep_G b \<sqinter> Rep_G a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<sqinter> Rep_G b = Rep_G b \<sqinter> Rep_G a
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<sqinter> Rep_G b \<le> Rep_G b \<sqinter> Rep_G a
 2. Rep_G b \<sqinter> Rep_G a \<le> Rep_G a \<sqinter> Rep_G b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma Rep_G_order: "(a \<le> b) = (Rep_G a \<le> Rep_G b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b) = (Rep_G a \<le> Rep_G b)
[PROOF STEP]
apply (simp add: order_def impl_def one_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u) = (Rep_G a \<le> Rep_G b)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (subgoal_tac "Rep_G (Abs_G (inf (Rep_G b - Rep_G a + u) u)) = Rep_G (Abs_G u)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u; Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)\<rbrakk> \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u); True\<rbrakk> \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (Rep_G b - Rep_G a + u) \<sqinter> u = u \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (subst (asm) less_eq_inf_2 [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. u \<le> Rep_G b - Rep_G a + u \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (simp add: diff_minus)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. u \<le> Rep_G b + - Rep_G a + u \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (drule_tac a = "u" and b = " Rep_G b + - Rep_G a + u" and v = "-u" in add_order_preserving_right)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. u + - u \<le> Rep_G b + - Rep_G a + u + - u \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (0::'a) \<le> Rep_G b + - Rep_G a \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (drule_tac a = "0" and b = " Rep_G b + - Rep_G a" and v = "Rep_G a" in add_order_preserving_right)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (0::'a) + Rep_G a \<le> Rep_G b + - Rep_G a + Rep_G a \<Longrightarrow> Rep_G a \<le> Rep_G b
 2. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 3. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
 2. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (subgoal_tac "Rep_G (Abs_G (inf (Rep_G b - Rep_G a + u) u)) = Rep_G (Abs_G u)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_G a \<le> Rep_G b; Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)\<rbrakk> \<Longrightarrow> Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u) = Abs_G u
 2. Rep_G a \<le> Rep_G b \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> Rep_G (Abs_G ((Rep_G b - Rep_G a + u) \<sqinter> u)) = Rep_G (Abs_G u)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> (Rep_G b - Rep_G a + u) \<sqinter> u = u
[PROOF STEP]
apply (subst less_eq_inf_2 [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> u \<le> Rep_G b - Rep_G a + u
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> u + - u \<le> Rep_G b - Rep_G a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> (0::'a) \<le> Rep_G b - Rep_G a
[PROOF STEP]
apply (simp add: diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> (0::'a) \<le> Rep_G b + - Rep_G a
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<le> Rep_G b \<Longrightarrow> (0::'a) + - (- Rep_G a) \<le> Rep_G b
[PROOF STEP]
by simp


[STATEMENT]
lemma ded_left: "((a::'a G) * b) l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
[PROOF STEP]
apply (simp add: times_def impl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G c - (Rep_G a - u + Rep_G b) + u) \<sqinter> (Rep_G c + u) \<sqinter> u) = Abs_G ((Rep_G c - Rep_G b + u - Rep_G a + u) \<sqinter> (u - Rep_G a + u) \<sqinter> u)
[PROOF STEP]
apply (simp add: diff_minus minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G c + (- Rep_G b + (u + - Rep_G a)) + u) \<sqinter> (Rep_G c + u) \<sqinter> u) = Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> (u + - Rep_G a + u) \<sqinter> u)
[PROOF STEP]
apply (simp add: add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> (Rep_G c + u) \<sqinter> u) = Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> (u + - Rep_G a + u) \<sqinter> u)
[PROOF STEP]
apply (simp add: inf_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> ((Rep_G c + u) \<sqinter> u)) = Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> ((u + - Rep_G a + u) \<sqinter> u))
[PROOF STEP]
apply (subgoal_tac "inf (Rep_G c + u) u = u")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> ((Rep_G c + u) \<sqinter> u)) = Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> ((u + - Rep_G a + u) \<sqinter> u))
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (subgoal_tac "inf (u + - Rep_G a + u) u = u")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(Rep_G c + u) \<sqinter> u = u; (u + - Rep_G a + u) \<sqinter> u = u\<rbrakk> \<Longrightarrow> Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> ((Rep_G c + u) \<sqinter> u)) = Abs_G ((Rep_G c + - Rep_G b + u + - Rep_G a + u) \<sqinter> ((u + - Rep_G a + u) \<sqinter> u))
 2. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> (u + - Rep_G a + u) \<sqinter> u = u
 3. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> (u + - Rep_G a + u) \<sqinter> u = u
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> (u + - Rep_G a + u) \<sqinter> u \<le> u
 2. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> u \<le> (u + - Rep_G a + u) \<sqinter> u
 3. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> u \<le> (u + - Rep_G a + u) \<sqinter> u
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> u \<le> u + - Rep_G a + u
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> u \<le> u + (- Rep_G a + u)
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (rule add_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G c + u) \<sqinter> u = u \<Longrightarrow> (0::'a) \<le> - Rep_G a + u
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (cut_tac x = a in Rep_G)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(Rep_G c + u) \<sqinter> u = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> (0::'a) \<le> - Rep_G a + u
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(Rep_G c + u) \<sqinter> u = u; (0::'a) \<le> Rep_G a \<and> Rep_G a \<le> u\<rbrakk> \<Longrightarrow> (0::'a) \<le> - Rep_G a + u
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (rule left_move_to_left)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(Rep_G c + u) \<sqinter> u = u; (0::'a) \<le> Rep_G a \<and> Rep_G a \<le> u\<rbrakk> \<Longrightarrow> - (- Rep_G a) + (0::'a) \<le> u
 2. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_G c + u) \<sqinter> u = u
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G c + u) \<sqinter> u \<le> u
 2. u \<le> (Rep_G c + u) \<sqinter> u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> (Rep_G c + u) \<sqinter> u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> Rep_G c + u
[PROOF STEP]
apply (rule add_pos_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> Rep_G c
[PROOF STEP]
apply (cut_tac x = c in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G c \<in> G \<Longrightarrow> (0::'a) \<le> Rep_G c
[PROOF STEP]
by (simp add: G_def)


[STATEMENT]
lemma ded_right: "((a::'a G) * b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
[PROOF STEP]
apply (simp add: times_def impr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((u - (Rep_G a - u + Rep_G b) + Rep_G c) \<sqinter> (u + Rep_G c) \<sqinter> u) = Abs_G ((u - Rep_G b + (u - Rep_G a + Rep_G c)) \<sqinter> (u - Rep_G b + u) \<sqinter> u)
[PROOF STEP]
apply (simp add: diff_minus minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((u + (- Rep_G b + (u + - Rep_G a)) + Rep_G c) \<sqinter> (u + Rep_G c) \<sqinter> u) = Abs_G ((u + - Rep_G b + (u + - Rep_G a + Rep_G c)) \<sqinter> (u + - Rep_G b + u) \<sqinter> u)
[PROOF STEP]
apply (simp add: add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> (u + Rep_G c) \<sqinter> u) = Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> (u + - Rep_G b + u) \<sqinter> u)
[PROOF STEP]
apply (simp add: inf_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> ((u + Rep_G c) \<sqinter> u)) = Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> ((u + - Rep_G b + u) \<sqinter> u))
[PROOF STEP]
apply (subgoal_tac "inf (u + Rep_G c) u = u")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> ((u + Rep_G c) \<sqinter> u)) = Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> ((u + - Rep_G b + u) \<sqinter> u))
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (subgoal_tac "inf (u + - Rep_G b + u) u = u")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(u + Rep_G c) \<sqinter> u = u; (u + - Rep_G b + u) \<sqinter> u = u\<rbrakk> \<Longrightarrow> Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> ((u + Rep_G c) \<sqinter> u)) = Abs_G ((u + - Rep_G b + u + - Rep_G a + Rep_G c) \<sqinter> ((u + - Rep_G b + u) \<sqinter> u))
 2. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> (u + - Rep_G b + u) \<sqinter> u = u
 3. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> (u + - Rep_G b + u) \<sqinter> u = u
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> (u + - Rep_G b + u) \<sqinter> u \<le> u
 2. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> u \<le> (u + - Rep_G b + u) \<sqinter> u
 3. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> u \<le> (u + - Rep_G b + u) \<sqinter> u
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> u \<le> u + - Rep_G b + u
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> u \<le> u + (- Rep_G b + u)
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (rule add_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (u + Rep_G c) \<sqinter> u = u \<Longrightarrow> (0::'a) \<le> - Rep_G b + u
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (cut_tac x = b in Rep_G)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(u + Rep_G c) \<sqinter> u = u; Rep_G b \<in> G\<rbrakk> \<Longrightarrow> (0::'a) \<le> - Rep_G b + u
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(u + Rep_G c) \<sqinter> u = u; (0::'a) \<le> Rep_G b \<and> Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'a) \<le> - Rep_G b + u
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (rule left_move_to_left)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(u + Rep_G c) \<sqinter> u = u; (0::'a) \<le> Rep_G b \<and> Rep_G b \<le> u\<rbrakk> \<Longrightarrow> - (- Rep_G b) + (0::'a) \<le> u
 2. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u + Rep_G c) \<sqinter> u = u
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (u + Rep_G c) \<sqinter> u \<le> u
 2. u \<le> (u + Rep_G c) \<sqinter> u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> (u + Rep_G c) \<sqinter> u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> u + Rep_G c
[PROOF STEP]
apply (rule add_pos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> Rep_G c
[PROOF STEP]
apply (cut_tac x = c in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G c \<in> G \<Longrightarrow> (0::'a) \<le> Rep_G c
[PROOF STEP]
by (simp add: G_def)


[STATEMENT]
lemma [simp]: "0 \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'b) \<in> G
[PROOF STEP]
by (simp add: G_def)


[STATEMENT]
lemma [simp]: "0 \<le> (a::'a G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a
[PROOF STEP]
apply (simp add: order_def impl_def zero_def one_def diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G a + u) \<sqinter> u) = Abs_G u
[PROOF STEP]
apply (subgoal_tac "inf (Rep_G a + u) u = u")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G a + u) \<sqinter> u = u \<Longrightarrow> Abs_G ((Rep_G a + u) \<sqinter> u) = Abs_G u
 2. (Rep_G a + u) \<sqinter> u = u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_G a + u) \<sqinter> u = u
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_G a + u) \<sqinter> u \<le> u
 2. u \<le> (Rep_G a + u) \<sqinter> u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> (Rep_G a + u) \<sqinter> u
[PROOF STEP]
apply (cut_tac x = a in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<in> G \<Longrightarrow> u \<le> (Rep_G a + u) \<sqinter> u
[PROOF STEP]
apply (unfold G_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<in> {a. (0::'a) \<le> a \<and> a \<le> u} \<Longrightarrow> u \<le> (Rep_G a + u) \<sqinter> u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> Rep_G a \<and> Rep_G a \<le> u \<Longrightarrow> u \<le> Rep_G a + u
[PROOF STEP]
apply (rule add_pos_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> Rep_G a \<and> Rep_G a \<le> u \<Longrightarrow> (0::'a) \<le> Rep_G a
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_W1: "((a::'a G) l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply (simp add: impl_def impr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((u - (Rep_G b - Rep_G a + u) + Rep_G b \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((u - (Rep_G a - Rep_G b + u) + Rep_G a \<squnion> Rep_G a) \<sqinter> u)
[PROOF STEP]
apply (simp add: diff_minus minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G a + - Rep_G b + Rep_G b \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((Rep_G b + - Rep_G a + Rep_G a \<squnion> Rep_G a) \<sqinter> u)
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G a \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((Rep_G b \<squnion> Rep_G a) \<sqinter> u)
[PROOF STEP]
apply (subgoal_tac "Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a \<Longrightarrow> Abs_G ((Rep_G a \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((Rep_G b \<squnion> Rep_G a) \<sqinter> u)
 2. Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<squnion> Rep_G b \<le> Rep_G b \<squnion> Rep_G a
 2. Rep_G b \<squnion> Rep_G a \<le> Rep_G a \<squnion> Rep_G b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma lemma_W2: "((a::'a G) r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: impl_def impr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G b - (u - Rep_G a + Rep_G b) + u \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((Rep_G a - (u - Rep_G b + Rep_G a) + u \<squnion> Rep_G a) \<sqinter> u)
[PROOF STEP]
apply (simp add: diff_minus minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G a + - u + u \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((Rep_G b + - u + u \<squnion> Rep_G a) \<sqinter> u)
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G ((Rep_G a \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((Rep_G b \<squnion> Rep_G a) \<sqinter> u)
[PROOF STEP]
apply (subgoal_tac "Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a \<Longrightarrow> Abs_G ((Rep_G a \<squnion> Rep_G b) \<sqinter> u) = Abs_G ((Rep_G b \<squnion> Rep_G a) \<sqinter> u)
 2. Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_G a \<squnion> Rep_G b \<le> Rep_G b \<squnion> Rep_G a
 2. Rep_G b \<squnion> Rep_G a \<le> Rep_G a \<squnion> Rep_G b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma [simp]: "A \<in> subgroup \<Longrightarrow> 0 \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> subgroup \<Longrightarrow> (0::'a) \<in> A
[PROOF STEP]
by (simp add: subgroup_def)


[STATEMENT]
lemma [simp]: "A \<in> subgroup \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a + b \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> subgroup; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a + b \<in> A
[PROOF STEP]
apply (subst (asm) subgroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> {A. (0::'a) \<in> A \<and> (\<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> a + b \<in> A \<and> - a \<in> A)}; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a + b \<in> A
[PROOF STEP]
by simp


[STATEMENT]
lemma minus_subgroup: "A \<in> subgroup \<Longrightarrow> -a \<in> A \<Longrightarrow> a \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> subgroup; - a \<in> A\<rbrakk> \<Longrightarrow> a \<in> A
[PROOF STEP]
apply (subst (asm) subgroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> {A. (0::'a) \<in> A \<and> (\<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> a + b \<in> A \<and> - a \<in> A)}; - a \<in> A\<rbrakk> \<Longrightarrow> a \<in> A
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- a \<in> A; (0::'a) \<in> A; \<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> a + b \<in> A \<and> - a \<in> A\<rbrakk> \<Longrightarrow> a \<in> A
[PROOF STEP]
apply (drule_tac x="-a" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- a \<in> A; (0::'a) \<in> A; \<forall>b. - a \<in> A \<and> b \<in> A \<longrightarrow> - a + b \<in> A \<and> - (- a) \<in> A\<rbrakk> \<Longrightarrow> a \<in> A
[PROOF STEP]
by simp


[STATEMENT]
lemma inf_lsubgroup:
  "A \<in> lsubgroup \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> inf a b \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> lsubgroup; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a \<sqinter> b \<in> A
[PROOF STEP]
by (simp add: lsubgroup_def)


[STATEMENT]
lemma sup_lsubgroup:
  "A \<in> lsubgroup \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> sup a b \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> lsubgroup; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a \<squnion> b \<in> A
[PROOF STEP]
by (simp add: lsubgroup_def)


[STATEMENT]
lemma sup_assoc_lgroup: "a \<squnion> b \<squnion> c = a \<squnion> (b \<squnion> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion> b \<squnion> c = a \<squnion> (b \<squnion> c)
[PROOF STEP]
by (rule sup_assoc)