[STATEMENT]
lemma list_exhaust3:
  obtains "xs = []" | x where "xs = [x]" | x y ys where "xs = x # y # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x. xs = [x] \<Longrightarrow> thesis; \<And>x y ys. xs = x # y # ys \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis list.exhaust)


[STATEMENT]
lemma card_Ex_subset:
  "k \<le> card M \<Longrightarrow> \<exists>N. N \<subseteq> M \<and> card N = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> card M \<Longrightarrow> \<exists>N\<subseteq>M. card N = k
[PROOF STEP]
by (induct rule: inc_induct) (auto simp: card_Suc_eq)


[STATEMENT]
lemma eventually_le_le:
  fixes P :: "'a => ('b :: preorder)"
  assumes "eventually (\<lambda>x. P x \<le> Q x) net"
  assumes "eventually (\<lambda>x. Q x \<le> R  x) net"
  shows "eventually (\<lambda>x. P x \<le> R x) net"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in net. P x \<le> R x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in net. P x \<le> Q x
\<forall>\<^sub>F x in net. Q x \<le> R x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in net. P x \<le> R x
[PROOF STEP]
by eventually_elim (rule order_trans)


[STATEMENT]
lemma LIMSEQ_neg_powr:
  assumes s: "s < 0"
  shows "(%x. (real x) powr s) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real x powr s) \<longlonglongrightarrow> 0
[PROOF STEP]
by (rule tendsto_neg_powr[OF assms filterlim_real_sequentially])


[STATEMENT]
lemma LIMSEQ_inv_powr:
  assumes "0 < c" "0 < d"
  shows "(\<lambda>n :: nat. (c / n) powr d) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (c / real n) powr d) \<longlonglongrightarrow> 0
[PROOF STEP]
proof (rule tendsto_zero_powrI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lambda>x. c / real x) \<longlonglongrightarrow> 0
 2. (\<lambda>x. d) \<longlonglongrightarrow> ?b
 3. \<forall>\<^sup>\<infinity>n. 0 \<le> c / real n
 4. 0 < ?b
[PROOF STEP]
from \<open>0 < c\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < c
[PROOF STEP]
have "\<And>x. 0 < x \<Longrightarrow> 0 < c / x"
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. \<And>x. 0 < x \<Longrightarrow> 0 < c / x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < ?x \<Longrightarrow> 0 < c / ?x

goal (4 subgoals):
 1. (\<lambda>x. c / real x) \<longlonglongrightarrow> 0
 2. (\<lambda>x. d) \<longlonglongrightarrow> ?b
 3. \<forall>\<^sup>\<infinity>n. 0 \<le> c / real n
 4. 0 < ?b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?x \<Longrightarrow> 0 < c / ?x
[PROOF STEP]
show "\<forall>\<^sup>\<infinity>n. 0 \<le> c / real n"
[PROOF STATE]
proof (prove)
using this:
0 < ?x \<Longrightarrow> 0 < c / ?x

goal (1 subgoal):
 1. \<forall>\<^sup>\<infinity>n. 0 \<le> c / real n
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
0 < ?x \<Longrightarrow> 0 < c / ?x
0 < c

goal (1 subgoal):
 1. \<forall>\<^sup>\<infinity>n. 0 \<le> c / real n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sup>\<infinity>n. 0 \<le> c / real n

goal (3 subgoals):
 1. (\<lambda>x. c / real x) \<longlonglongrightarrow> 0
 2. (\<lambda>x. d) \<longlonglongrightarrow> ?b
 3. 0 < ?b
[PROOF STEP]
show "(\<lambda>x. c / real x) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. c / real x) \<longlonglongrightarrow> 0
[PROOF STEP]
by (intro tendsto_divide_0[OF tendsto_const] filterlim_at_top_imp_at_infinity
              filterlim_real_sequentially tendsto_divide_0)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. c / real x) \<longlonglongrightarrow> 0

goal (2 subgoals):
 1. (\<lambda>x. d) \<longlonglongrightarrow> ?b
 2. 0 < ?b
[PROOF STEP]
show "0 < d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < d
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
this:
0 < d

goal (1 subgoal):
 1. (\<lambda>x. d) \<longlonglongrightarrow> d
[PROOF STEP]
show "(\<lambda>x. d) \<longlonglongrightarrow> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. d) \<longlonglongrightarrow> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. d) \<longlonglongrightarrow> d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in aGroup) ag_carrier_carrier:"carrier (b_ag A) = carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier (b_ag A) = carrier A
[PROOF STEP]
by (simp add:b_ag_def)


[STATEMENT]
lemma (in aGroup) ag_pOp_closed:"\<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow>
                                     pop A x y \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> carrier A
[PROOF STEP]
apply (cut_tac pop_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; (\<plusminus>) \<in> carrier A \<rightarrow> carrier A \<rightarrow> carrier A\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> carrier A
[PROOF STEP]
apply (frule funcset_mem[of "(\<plusminus>) " "carrier A" "carrier A \<rightarrow> carrier A" "x"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; (\<plusminus>) \<in> carrier A \<rightarrow> carrier A \<rightarrow> carrier A; (\<plusminus>) x \<in> carrier A \<rightarrow> carrier A\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> carrier A
[PROOF STEP]
apply (rule funcset_mem[of "(\<plusminus>) x" "carrier A" "carrier A" "y"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_mOp_closed:"x \<in> carrier A \<Longrightarrow> (-\<^sub>a x)  \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier A \<Longrightarrow> -\<^sub>a x \<in> carrier A
[PROOF STEP]
apply (cut_tac mop_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; mop A \<in> carrier A \<rightarrow> carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> carrier A
[PROOF STEP]
apply (rule funcset_mem[of "mop A" "carrier A" "carrier A" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_subset:"A +> H \<Longrightarrow> H \<subseteq> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> H \<subseteq> carrier A
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_ag A \<guillemotright> H  \<Longrightarrow> H \<subseteq> carrier A
[PROOF STEP]
apply (simp add:sg_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<noteq> {}; H \<subseteq> carrier (b_ag A); \<forall>a\<in>H. \<forall>b\<in>H. a \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> b \<in> H\<rbrakk> \<Longrightarrow> H \<subseteq> carrier A
[PROOF STEP]
apply (simp add:ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_pOp_commute:"\<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk>  \<Longrightarrow>
           pop A x y = pop A y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow> x \<plusminus> y = y \<plusminus> x
[PROOF STEP]
by (simp add:pop_commute)


[STATEMENT]
lemma (in aGroup) b_ag_group:"Group (b_ag A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group (b_ag A)
[PROOF STEP]
apply (unfold Group_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<cdot>\<^bsub>b_ag A\<^esub>) \<in> carrier (b_ag A) \<rightarrow> carrier (b_ag A) \<rightarrow> carrier (b_ag A) \<and> (\<forall>a b c. a \<in> carrier (b_ag A) \<longrightarrow> b \<in> carrier (b_ag A) \<longrightarrow> c \<in> carrier (b_ag A) \<longrightarrow> a \<cdot>\<^bsub>b_ag A\<^esub> b \<cdot>\<^bsub>b_ag A\<^esub> c = a \<cdot>\<^bsub>b_ag A\<^esub> (b \<cdot>\<^bsub>b_ag A\<^esub> c)) \<and> iop (b_ag A) \<in> carrier (b_ag A) \<rightarrow> carrier (b_ag A)) \<and> (\<forall>a. a \<in> carrier (b_ag A) \<longrightarrow> \<rho>\<^bsub>b_ag A\<^esub> a \<cdot>\<^bsub>b_ag A\<^esub> a = \<one>\<^bsub>b_ag A\<^esub>) \<and> \<one>\<^bsub>b_ag A\<^esub> \<in> carrier (b_ag A) \<and> (\<forall>a. a \<in> carrier (b_ag A) \<longrightarrow> \<one>\<^bsub>b_ag A\<^esub> \<cdot>\<^bsub>b_ag A\<^esub> a = a)
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<plusminus>) \<in> carrier A \<rightarrow> carrier A \<rightarrow> carrier A \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> (\<forall>b. b \<in> carrier A \<longrightarrow> (\<forall>c. c \<in> carrier A \<longrightarrow> a \<plusminus> b \<plusminus> c = a \<plusminus> (b \<plusminus> c)))) \<and> mop A \<in> carrier A \<rightarrow> carrier A \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>) \<and> \<zero> \<in> carrier A \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a)
[PROOF STEP]
apply (simp add:pop_closed mop_closed ex_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier A \<longrightarrow> (\<forall>b. b \<in> carrier A \<longrightarrow> (\<forall>c. c \<in> carrier A \<longrightarrow> a \<plusminus> b \<plusminus> c = a \<plusminus> (b \<plusminus> c)))) \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>) \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>a. a \<in> carrier A \<longrightarrow> (\<forall>b. b \<in> carrier A \<longrightarrow> (\<forall>c. c \<in> carrier A \<longrightarrow> a \<plusminus> b \<plusminus> c = a \<plusminus> (b \<plusminus> c)))
 2. (\<forall>a. a \<in> carrier A \<longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>) \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> c = a \<plusminus> (b \<plusminus> c)
 2. (\<forall>a. a \<in> carrier A \<longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>) \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a)
[PROOF STEP]
apply (simp add:aassoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. a \<in> carrier A \<longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>) \<and> (\<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>a. a \<in> carrier A \<longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>
 2. \<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> carrier A \<Longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>
 2. \<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a
[PROOF STEP]
apply (simp add:l_m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. a \<in> carrier A \<longrightarrow> \<zero> \<plusminus> a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> carrier A \<Longrightarrow> \<zero> \<plusminus> a = a
[PROOF STEP]
apply (simp add:l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) agop_gop:"top (b_ag A) = pop A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<cdot>\<^bsub>b_ag A\<^esub>) = (\<plusminus>)
[PROOF STEP]
(*agpop_gtop*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<cdot>\<^bsub>b_ag A\<^esub>) = (\<plusminus>)
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) agiop_giop:"iop (b_ag A) = mop A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iop (b_ag A) = mop A
[PROOF STEP]
(*agmop_giop*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iop (b_ag A) = mop A
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) agunit_gone:"one (b_ag A) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>b_ag A\<^esub> = \<zero>
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_pOp_add_r:"\<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A;
                 a = b\<rbrakk>  \<Longrightarrow> a \<plusminus> c =  b \<plusminus> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; a = b\<rbrakk> \<Longrightarrow> a \<plusminus> c = b \<plusminus> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_add_commute:"\<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow>
                                                  a \<plusminus> b = b \<plusminus> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b = b \<plusminus> a
[PROOF STEP]
by (simp add:pop_commute)


[STATEMENT]
lemma (in aGroup) ag_pOp_add_l:"\<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A;
                 a = b\<rbrakk>  \<Longrightarrow> c \<plusminus> a =  c \<plusminus> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; a = b\<rbrakk> \<Longrightarrow> c \<plusminus> a = c \<plusminus> b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_pOp_closed:"\<lbrakk>asubGroup A H; x \<in> H; y \<in> H\<rbrakk>
                                   \<Longrightarrow> pop A x y \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> H
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> H
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H; y \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> H
[PROOF STEP]
apply (frule Group.sg_mult_closed [of "b_ag A" "H" "x" "y"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H; y \<in> H; Group (b_ag A); x \<cdot>\<^bsub>b_ag A\<^esub> y \<in> H\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> H
[PROOF STEP]
apply (simp only:agop_gop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_mOp_closed:"\<lbrakk>asubGroup A H; x \<in> H\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; x \<in> H\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> H
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> H
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> H
[PROOF STEP]
apply (frule Group.sg_i_closed[of "b_ag A" "H" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H; Group (b_ag A); \<rho>\<^bsub>b_ag A\<^esub> x \<in> H\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> H
[PROOF STEP]
apply (simp add:agiop_giop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_subset1:"\<lbrakk>asubGroup A H; x \<in> H\<rbrakk> \<Longrightarrow> x \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; x \<in> H\<rbrakk> \<Longrightarrow> x \<in> carrier A
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H\<rbrakk> \<Longrightarrow> x \<in> carrier A
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> x \<in> carrier A
[PROOF STEP]
apply (frule Group.sg_subset_elem[of "b_ag A" "H" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; x \<in> H; Group (b_ag A); x \<in> carrier (b_ag A)\<rbrakk> \<Longrightarrow> x \<in> carrier A
[PROOF STEP]
apply (simp add:ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_inc_zero:"asubGroup A H \<Longrightarrow> \<zero> \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> \<zero> \<in> H
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_ag A \<guillemotright> H  \<Longrightarrow> \<zero> \<in> H
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A)\<rbrakk> \<Longrightarrow> \<zero> \<in> H
[PROOF STEP]
apply (frule Group.sg_unit_closed[of "b_ag A" "H"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); \<one>\<^bsub>b_ag A\<^esub> \<in> H\<rbrakk> \<Longrightarrow> \<zero> \<in> H
[PROOF STEP]
apply (simp add:b_ag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_inc_zero:"\<zero> \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> carrier A
[PROOF STEP]
by (simp add:ex_zero)


[STATEMENT]
lemma (in aGroup) ag_l_zero:"x \<in> carrier A \<Longrightarrow> \<zero> \<plusminus> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier A \<Longrightarrow> \<zero> \<plusminus> x = x
[PROOF STEP]
by (simp add:l_zero)


[STATEMENT]
lemma (in aGroup) ag_r_zero:"x \<in> carrier A \<Longrightarrow> x \<plusminus> \<zero> = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier A \<Longrightarrow> x \<plusminus> \<zero> = x
[PROOF STEP]
apply (cut_tac ex_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; \<zero> \<in> carrier A\<rbrakk> \<Longrightarrow> x \<plusminus> \<zero> = x
[PROOF STEP]
apply (subst pop_commute, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; \<zero> \<in> carrier A\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> x = x
[PROOF STEP]
apply (rule ag_l_zero, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_l_inv1:"x \<in> carrier A \<Longrightarrow> (-\<^sub>a x) \<plusminus> x = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier A \<Longrightarrow> -\<^sub>a x \<plusminus> x = \<zero>
[PROOF STEP]
by (simp add:l_m)


[STATEMENT]
lemma (in aGroup) ag_r_inv1:"x \<in> carrier A \<Longrightarrow> x \<plusminus> (-\<^sub>a x) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier A \<Longrightarrow> x \<plusminus> -\<^sub>a x = \<zero>
[PROOF STEP]
by (frule ag_mOp_closed[of "x"],
       subst ag_pOp_commute, assumption+,
       simp add:ag_l_inv1)


[STATEMENT]
lemma (in aGroup) ag_pOp_assoc:"\<lbrakk>x \<in> carrier A; y \<in> carrier A; z \<in> carrier A\<rbrakk>
                \<Longrightarrow> (x \<plusminus> y) \<plusminus> z = x \<plusminus> (y \<plusminus> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; z \<in> carrier A\<rbrakk> \<Longrightarrow> x \<plusminus> y \<plusminus> z = x \<plusminus> (y \<plusminus> z)
[PROOF STEP]
by (simp add:aassoc)


[STATEMENT]
lemma (in aGroup) ag_inv_unique:"\<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<plusminus> y = \<zero>\<rbrakk> \<Longrightarrow>
                                     y = -\<^sub>a x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<plusminus> y = \<zero>\<rbrakk> \<Longrightarrow> y = -\<^sub>a x
[PROOF STEP]
apply (frule ag_mOp_closed[of "x"],
       frule aassoc[of "-\<^sub>a x" "x" "y"], assumption+,
       simp add:l_m l_zero ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_inv_inj:"\<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<noteq> y\<rbrakk> \<Longrightarrow>
                                          (-\<^sub>a x) \<noteq> (-\<^sub>a y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<noteq> y\<rbrakk> \<Longrightarrow> -\<^sub>a x \<noteq> -\<^sub>a y
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<noteq> y; -\<^sub>a x = -\<^sub>a y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule ag_mOp_closed[of "y"],
       frule aassoc[of "y" "-\<^sub>a y" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<noteq> y; -\<^sub>a x = -\<^sub>a y; -\<^sub>a y \<in> carrier A; y \<plusminus> -\<^sub>a y \<plusminus> x = y \<plusminus> (-\<^sub>a y \<plusminus> x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp only:ag_r_inv1,
       frule sym, thin_tac "-\<^sub>a x = -\<^sub>a y", simp add:l_m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<noteq> y; -\<^sub>a x \<in> carrier A; \<zero> \<plusminus> x = y \<plusminus> \<zero>; -\<^sub>a y = -\<^sub>a x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:l_zero ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) pOp_assocTr41:"\<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A;
 d \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> c \<plusminus> d = a \<plusminus> b \<plusminus> (c \<plusminus> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; d \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> c \<plusminus> d = a \<plusminus> b \<plusminus> (c \<plusminus> d)
[PROOF STEP]
by (frule ag_pOp_closed[of "a" "b"], assumption+,
    rule aassoc[of "a \<plusminus> b" "c" "d"], assumption+)


[STATEMENT]
lemma (in aGroup) pOp_assocTr42:"\<lbrakk>a \<in> carrier A; b \<in> carrier A;
 c \<in> carrier A; d \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> c \<plusminus> d = a \<plusminus> (b \<plusminus> c) \<plusminus> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; d \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> c \<plusminus> d = a \<plusminus> (b \<plusminus> c) \<plusminus> d
[PROOF STEP]
by (simp add:aassoc[THEN sym, of "a" "b" "c"])


[STATEMENT]
lemma (in aGroup) pOp_assocTr43:"\<lbrakk>a \<in> carrier A; b \<in> carrier A;
 c \<in> carrier A; d \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> (c \<plusminus> d) = a \<plusminus> (b \<plusminus> c) \<plusminus> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; d \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> (c \<plusminus> d) = a \<plusminus> (b \<plusminus> c) \<plusminus> d
[PROOF STEP]
by (subst  pOp_assocTr41[THEN sym], assumption+,
       rule pOp_assocTr42, assumption+)


[STATEMENT]
lemma (in aGroup) pOp_assoc_cancel:"\<lbrakk>a \<in> carrier A; b \<in> carrier A;
 c \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a b \<plusminus> (b \<plusminus> -\<^sub>a c) = a \<plusminus> -\<^sub>a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a b \<plusminus> (b \<plusminus> -\<^sub>a c) = a \<plusminus> -\<^sub>a c
[PROOF STEP]
apply (subst pOp_assocTr43, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a b \<in> carrier A
 2. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A\<rbrakk> \<Longrightarrow> b \<in> carrier A
 3. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a c \<in> carrier A
 4. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> (-\<^sub>a b \<plusminus> b) \<plusminus> -\<^sub>a c = a \<plusminus> -\<^sub>a c
[PROOF STEP]
apply (simp add:ag_l_inv1 ag_mOp_closed)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> \<zero> \<plusminus> -\<^sub>a c = a \<plusminus> -\<^sub>a c
[PROOF STEP]
apply (simp add:ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_p_inv:"\<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow>
                                     (-\<^sub>a (x \<plusminus> y)) = (-\<^sub>a x) \<plusminus> (-\<^sub>a y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a (x \<plusminus> y) = -\<^sub>a x \<plusminus> -\<^sub>a y
[PROOF STEP]
apply (frule ag_mOp_closed[of "x"], frule ag_mOp_closed[of "y"],
       frule ag_pOp_closed[of "x" "y"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; -\<^sub>a x \<in> carrier A; -\<^sub>a y \<in> carrier A; x \<plusminus> y \<in> carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a (x \<plusminus> y) = -\<^sub>a x \<plusminus> -\<^sub>a y
[PROOF STEP]
apply (frule aassoc[of "x \<plusminus> y" "-\<^sub>a x" "-\<^sub>a y"], assumption+,
       simp add:pOp_assocTr43, simp add:pop_commute[of "y" "-\<^sub>a x"],
       simp add:aassoc[THEN sym, of "x" "-\<^sub>a x" "y"],
       simp add:ag_r_inv1 l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; -\<^sub>a x \<in> carrier A; -\<^sub>a y \<in> carrier A; x \<plusminus> y \<in> carrier A; x \<plusminus> y \<plusminus> -\<^sub>a x \<plusminus> -\<^sub>a y = \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a (x \<plusminus> y) = -\<^sub>a x \<plusminus> -\<^sub>a y
[PROOF STEP]
apply (frule ag_pOp_closed[of "-\<^sub>a x" "-\<^sub>a y"], assumption+,
       simp add:pOp_assocTr41,
       rule ag_inv_unique[THEN sym, of "x \<plusminus> y" "-\<^sub>a x \<plusminus> -\<^sub>a y"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) gEQAddcross: "\<lbrakk>l1 \<in> carrier A; l2 \<in> carrier A;
      r1 \<in> carrier A; r1 \<in> carrier A; l1 = r2; l2 = r1\<rbrakk> \<Longrightarrow>
                          l1 \<plusminus> l2 = r1 \<plusminus> r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l1 \<in> carrier A; l2 \<in> carrier A; r1 \<in> carrier A; r1 \<in> carrier A; l1 = r2; l2 = r1\<rbrakk> \<Longrightarrow> l1 \<plusminus> l2 = r1 \<plusminus> r2
[PROOF STEP]
apply (simp add:ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_eq_sol1:"\<lbrakk>a \<in> carrier A; x\<in> carrier A; b\<in> carrier A;
                               a \<plusminus> x = b\<rbrakk> \<Longrightarrow> x = (-\<^sub>a a) \<plusminus> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; x \<in> carrier A; b \<in> carrier A; a \<plusminus> x = b\<rbrakk> \<Longrightarrow> x = -\<^sub>a a \<plusminus> b
[PROOF STEP]
apply (frule ag_mOp_closed[of "a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; x \<in> carrier A; b \<in> carrier A; a \<plusminus> x = b; -\<^sub>a a \<in> carrier A\<rbrakk> \<Longrightarrow> x = -\<^sub>a a \<plusminus> b
[PROOF STEP]
apply (frule aassoc[of "-\<^sub>a a" "a" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; x \<in> carrier A; b \<in> carrier A; a \<plusminus> x = b; -\<^sub>a a \<in> carrier A; -\<^sub>a a \<plusminus> a \<plusminus> x = -\<^sub>a a \<plusminus> (a \<plusminus> x)\<rbrakk> \<Longrightarrow> x = -\<^sub>a a \<plusminus> b
[PROOF STEP]
apply (simp add:l_m l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_eq_sol2:"\<lbrakk>a \<in> carrier A; x\<in> carrier A; b\<in> carrier A;
                                x \<plusminus> a = b\<rbrakk> \<Longrightarrow> x = b \<plusminus> (-\<^sub>a a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; x \<in> carrier A; b \<in> carrier A; x \<plusminus> a = b\<rbrakk> \<Longrightarrow> x = b \<plusminus> -\<^sub>a a
[PROOF STEP]
apply (frule ag_mOp_closed[of "a"],
       frule aassoc[of "x" "a" "-\<^sub>a a"], assumption+,
       simp add:ag_r_inv1 ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_add4_rel:"\<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A;
 d \<in> carrier A \<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> (c \<plusminus> d) =  a \<plusminus> c \<plusminus> (b \<plusminus> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; d \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> (c \<plusminus> d) = a \<plusminus> c \<plusminus> (b \<plusminus> d)
[PROOF STEP]
apply (simp add:pOp_assocTr43[of "a" "b" "c" "d"],
       simp add:ag_pOp_commute[of "b" "c"],
       simp add:pOp_assocTr43[THEN sym, of "a" "c" "b" "d"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_inv_inv:"x \<in> carrier A \<Longrightarrow> -\<^sub>a (-\<^sub>a x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier A \<Longrightarrow> -\<^sub>a (-\<^sub>a x) = x
[PROOF STEP]
by (frule ag_l_inv1[of "x"], frule ag_mOp_closed[of "x"],
       rule  ag_inv_unique[THEN sym, of "-\<^sub>a x" "x"], assumption+)


[STATEMENT]
lemma (in aGroup) ag_inv_zero:"-\<^sub>a \<zero> = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. -\<^sub>a \<zero> = \<zero>
[PROOF STEP]
apply (cut_tac ex_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> carrier A \<Longrightarrow> -\<^sub>a \<zero> = \<zero>
[PROOF STEP]
apply (frule l_zero[of "\<zero>"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<zero> \<in> carrier A; \<zero> \<plusminus> \<zero> = \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a \<zero> = \<zero>
[PROOF STEP]
apply (rule ag_inv_unique[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_diff_minus:"\<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A;
                   a \<plusminus> (-\<^sub>a b) = c\<rbrakk> \<Longrightarrow> b \<plusminus> (-\<^sub>a a) = (-\<^sub>a c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; a \<plusminus> -\<^sub>a b = c\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a = -\<^sub>a c
[PROOF STEP]
apply (frule sym, thin_tac "a \<plusminus> -\<^sub>a b = c", simp, thin_tac "c = a \<plusminus> -\<^sub>a b")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b \<in> carrier A\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a = -\<^sub>a (a \<plusminus> -\<^sub>a b)
[PROOF STEP]
apply (frule ag_mOp_closed[of "b"], frule ag_mOp_closed[of "a"],
       subst ag_p_inv, assumption+, subst ag_inv_inv, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b \<in> carrier A; -\<^sub>a b \<in> carrier A; -\<^sub>a a \<in> carrier A\<rbrakk> \<Longrightarrow> b \<plusminus> -\<^sub>a a = -\<^sub>a a \<plusminus> b
[PROOF STEP]
apply (simp add:ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) pOp_cancel_l:"\<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A;                    c \<plusminus> a =  c \<plusminus> b \<rbrakk> \<Longrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; c \<plusminus> a = c \<plusminus> b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (frule ag_mOp_closed[of "c"],
       frule aassoc[of "-\<^sub>a c" "c" "a"], assumption+,
       simp only:l_m l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>-\<^sub>a c \<plusminus> (c \<plusminus> b) \<in> carrier A; b \<in> carrier A; c \<in> carrier A; c \<plusminus> (-\<^sub>a c \<plusminus> (c \<plusminus> b)) = c \<plusminus> b; -\<^sub>a c \<in> carrier A; a = -\<^sub>a c \<plusminus> (c \<plusminus> b)\<rbrakk> \<Longrightarrow> -\<^sub>a c \<plusminus> (c \<plusminus> b) = b
[PROOF STEP]
apply (simp only:aassoc[THEN sym, of "-\<^sub>a c" "c" "b"],
        simp only:l_m l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) pOp_cancel_r:"\<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A;               a \<plusminus> c =  b \<plusminus> c \<rbrakk> \<Longrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; c \<in> carrier A; a \<plusminus> c = b \<plusminus> c\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
by (simp add:ag_pOp_commute pOp_cancel_l)


[STATEMENT]
lemma (in aGroup) ag_eq_diffzero:"\<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow>
                       (a = b) = (a \<plusminus> (-\<^sub>a b) = \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> (a = b) = (a \<plusminus> -\<^sub>a b = \<zero>)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a = b\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a b = \<zero>
 2. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b = \<zero>\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (simp add:ag_r_inv1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b = \<zero>\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (frule ag_mOp_closed[of "b"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b = \<zero>; -\<^sub>a b \<in> carrier A\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (simp add:ag_pOp_commute[of "a" "-\<^sub>a b"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; -\<^sub>a b \<plusminus> a = \<zero>; -\<^sub>a b \<in> carrier A\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (subst ag_inv_unique[of "-\<^sub>a b" "a"], assumption+,
        simp add:ag_inv_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_eq_diffzero1:"\<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow>
                       (a = b) = ((-\<^sub>a a) \<plusminus> b = \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> (a = b) = (-\<^sub>a a \<plusminus> b = \<zero>)
[PROOF STEP]
apply (frule ag_mOp_closed[of a],
       simp add:ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; -\<^sub>a a \<in> carrier A\<rbrakk> \<Longrightarrow> (a = b) = (b \<plusminus> -\<^sub>a a = \<zero>)
[PROOF STEP]
apply (subst ag_eq_diffzero[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; -\<^sub>a a \<in> carrier A\<rbrakk> \<Longrightarrow> (a = b) = (b = a)
[PROOF STEP]
apply (rule iffI, rule sym, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; -\<^sub>a a \<in> carrier A; b = a\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (rule sym, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_neq_diffnonzero:"\<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow>
         (a \<noteq> b) = (a \<plusminus> (-\<^sub>a b) \<noteq>  \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> (a \<noteq> b) = (a \<plusminus> -\<^sub>a b \<noteq> \<zero>)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a b \<noteq> \<zero>
 2. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<noteq> b
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<noteq> b; a \<plusminus> -\<^sub>a b = \<zero>\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<noteq> b
[PROOF STEP]
apply (simp add:ag_eq_diffzero[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus> -\<^sub>a b \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a \<noteq> b
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<in> carrier A; b \<plusminus> -\<^sub>a b \<noteq> \<zero>; a = b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:ag_r_inv1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_plus_zero:"\<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow>
                     (x = -\<^sub>a y)  = (x \<plusminus> y = \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow> (x = -\<^sub>a y) = (x \<plusminus> y = \<zero>)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x = -\<^sub>a y\<rbrakk> \<Longrightarrow> x \<plusminus> y = \<zero>
 2. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<plusminus> y = \<zero>\<rbrakk> \<Longrightarrow> x = -\<^sub>a y
[PROOF STEP]
apply (simp add:ag_l_inv1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; x \<plusminus> y = \<zero>\<rbrakk> \<Longrightarrow> x = -\<^sub>a y
[PROOF STEP]
apply (simp add:ag_pOp_commute[of "x" "y"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier A; y \<in> carrier A; y \<plusminus> x = \<zero>\<rbrakk> \<Longrightarrow> x = -\<^sub>a y
[PROOF STEP]
apply (rule ag_inv_unique[of "y" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_nsubg:"A +> H \<Longrightarrow>  (b_ag A) \<triangleright> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> b_ag A \<triangleright> H
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> b_ag A \<triangleright> H
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A)\<rbrakk> \<Longrightarrow> b_ag A \<triangleright> H
[PROOF STEP]
apply (rule Group.cond_nsg[of "b_ag A" "H"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (b_ag A). \<forall>h\<in>H. a \<cdot>\<^bsub>b_ag A\<^esub> h \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> a \<in> H
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); a \<in> carrier (b_ag A); h \<in> H\<rbrakk> \<Longrightarrow> a \<cdot>\<^bsub>b_ag A\<^esub> h \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> a \<in> H
[PROOF STEP]
apply(simp add:agop_gop agiop_giop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); a \<in> carrier (b_ag A); h \<in> H\<rbrakk> \<Longrightarrow> a \<plusminus> h \<plusminus> -\<^sub>a a \<in> H
[PROOF STEP]
apply (frule Group.sg_subset[of "b_ag A" "H"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); a \<in> carrier (b_ag A); h \<in> H; H \<subseteq> carrier (b_ag A)\<rbrakk> \<Longrightarrow> a \<plusminus> h \<plusminus> -\<^sub>a a \<in> H
[PROOF STEP]
apply (simp add:ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); a \<in> carrier A; h \<in> H; H \<subseteq> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> h \<plusminus> -\<^sub>a a \<in> H
[PROOF STEP]
apply (frule_tac c = h in subsetD[of "H" "carrier A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); a \<in> carrier A; h \<in> H; H \<subseteq> carrier A; h \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus> h \<plusminus> -\<^sub>a a \<in> H
[PROOF STEP]
apply (subst ag_pOp_commute, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); a \<in> carrier A; h \<in> H; H \<subseteq> carrier A; h \<in> carrier A\<rbrakk> \<Longrightarrow> h \<plusminus> a \<plusminus> -\<^sub>a a \<in> H
[PROOF STEP]
apply (frule_tac x = a in ag_mOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A); a \<in> carrier A; h \<in> H; H \<subseteq> carrier A; h \<in> carrier A; -\<^sub>a a \<in> carrier A\<rbrakk> \<Longrightarrow> h \<plusminus> a \<plusminus> -\<^sub>a a \<in> H
[PROOF STEP]
apply (subst aassoc, assumption+, simp add:ag_r_inv1 ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) subg_asubg:"b_ag G \<guillemotright> H \<Longrightarrow> G +> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_ag G \<guillemotright> H  \<Longrightarrow> G +> H
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_test:"\<lbrakk>H \<subseteq> carrier A; H \<noteq> {};
               \<forall>a\<in>H. \<forall>b\<in>H. (a \<plusminus> (-\<^sub>a b) \<in> H)\<rbrakk> \<Longrightarrow> A +> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H\<rbrakk> \<Longrightarrow> A +> H
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H\<rbrakk> \<Longrightarrow> b_ag A \<guillemotright> H
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> b_ag A \<guillemotright> H
[PROOF STEP]
apply (rule Group.sg_condition [of "b_ag A" "H"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<subseteq> carrier (b_ag A)
 2. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<noteq> {}
 3. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> \<forall>a b. a \<in> H \<and> b \<in> H \<longrightarrow> a \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> b \<in> H
[PROOF STEP]
apply (simp add:ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<noteq> {}
 2. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> \<forall>a b. a \<in> H \<and> b \<in> H \<longrightarrow> a \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> b \<in> H
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> \<forall>a b. a \<in> H \<and> b \<in> H \<longrightarrow> a \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> b \<in> H
[PROOF STEP]
apply (rule allI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> a \<in> H \<and> b \<in> H \<longrightarrow> a \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> b \<in> H
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>H \<subseteq> carrier A; H \<noteq> {}; \<forall>a\<in>H. \<forall>b\<in>H. a \<plusminus> -\<^sub>a b \<in> H; Group (b_ag A); a \<in> H \<and> b \<in> H\<rbrakk> \<Longrightarrow> a \<cdot>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> b \<in> H
[PROOF STEP]
apply (simp add:agop_gop agiop_giop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_zero:"A +> {\<zero>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> {\<zero>}
[PROOF STEP]
apply (rule asubg_test[of "{\<zero>}"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {\<zero>} \<subseteq> carrier A
 2. {\<zero>} \<noteq> {}
 3. \<forall>a\<in>{\<zero>}. \<forall>b\<in>{\<zero>}. a \<plusminus> -\<^sub>a b \<in> {\<zero>}
[PROOF STEP]
apply (simp add:ag_inc_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {\<zero>} \<noteq> {}
 2. \<forall>a\<in>{\<zero>}. \<forall>b\<in>{\<zero>}. a \<plusminus> -\<^sub>a b \<in> {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>{\<zero>}. \<forall>b\<in>{\<zero>}. a \<plusminus> -\<^sub>a b \<in> {\<zero>}
[PROOF STEP]
apply (simp, cut_tac ag_inc_zero, simp add:ag_r_inv1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_whole:"A +> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> carrier A
[PROOF STEP]
apply (rule asubg_test[of "carrier A"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. carrier A \<subseteq> carrier A
 2. carrier A \<noteq> {}
 3. \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. a \<plusminus> -\<^sub>a b \<in> carrier A
[PROOF STEP]
apply (simp,
       cut_tac ag_inc_zero, simp add:nonempty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. a \<plusminus> -\<^sub>a b \<in> carrier A
[PROOF STEP]
apply ((rule ballI)+,
       rule ag_pOp_closed, assumption,
       rule_tac x = b in ag_mOp_closed, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) Ag_ind_carrier:"bij_to f (carrier A) (D::'d set) \<Longrightarrow>
               carrier (Ag_ind A f) = f ` (carrier A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_to f (carrier A) D \<Longrightarrow> carrier (Ag_ind A f) = f ` carrier A
[PROOF STEP]
by (simp add:Ag_ind_def)