[STATEMENT]
lemma WHILET_unfold:
  "WHILET b f s = (if b s then bind (f s) (WHILET b f) else return s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILET b f s = (if b s then bind (f s) (WHILET b f) else return s)
[PROOF STEP]
unfolding WHILET_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEIT (\<lambda>_. True) b f s = (if b s then bind (f s) (WHILEIT (\<lambda>_. True) b f) else return s)
[PROOF STEP]
apply (subst WHILEIT_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if True then if b s then bind (f s) (WHILEIT (\<lambda>_. True) b f) else return s else top) = (if b s then bind (f s) (WHILEIT (\<lambda>_. True) b f) else return s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma transfer_WHILEIT_esc[refine_transfer]:
  assumes REF: "\<And>x. return (f x) \<le> F x"
  shows "return (while b f x) \<le> WHILEIT I b F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return (while b f x) \<le> WHILEIT I b F x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return (while b f x) \<le> WHILEIT I b F x
[PROOF STEP]
interpret transfer return
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return (while b f x) \<le> WHILEIT I b F x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return (while b f x) \<le> WHILEIT I b F x
[PROOF STEP]
unfolding WHILEIT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return (while b f x) \<le> REC\<^sub>T (WHILEI_body bind return I b F) x
[PROOF STEP]
apply (rule transfer_RECT'[where fr="while b f"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. while b f x = ?b (while b f) x
 2. \<And>Fa f x. (\<And>x. return (f x) \<le> Fa x) \<Longrightarrow> return (?b f x) \<le> WHILEI_body bind return I b F Fa x
[PROOF STEP]
apply (rule while_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Fa fa x. (\<And>x. return (fa x) \<le> Fa x) \<Longrightarrow> return (if b x then fa (f x) else x) \<le> WHILEI_body bind return I b F Fa x
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Fa fa x. (\<And>x. return (fa x) \<le> Fa x) \<Longrightarrow> return (if b x then fa (f x) else x) \<le> (if I x then if b x then bind (F x) Fa else return x else top)
[PROOF STEP]
apply (split if_split, intro allI impI conjI)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Fa fa x. \<lbrakk>\<And>x. return (fa x) \<le> Fa x; I x; b x; b x\<rbrakk> \<Longrightarrow> return (fa (f x)) \<le> bind (F x) Fa
 2. \<And>Fa f x. \<lbrakk>\<And>x. return (f x) \<le> Fa x; I x; b x; \<not> b x\<rbrakk> \<Longrightarrow> return x \<le> bind (F x) Fa
 3. \<And>F fa x. \<lbrakk>\<And>x. return (fa x) \<le> F x; I x; \<not> b x\<rbrakk> \<Longrightarrow> return (if b x then fa (f x) else x) \<le> return x
 4. \<And>F fa x. \<lbrakk>\<And>x. return (fa x) \<le> F x; \<not> I x\<rbrakk> \<Longrightarrow> return (if b x then fa (f x) else x) \<le> top
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Fa fa x. \<lbrakk>\<And>x. return (fa x) \<le> Fa x; I x; b x\<rbrakk> \<Longrightarrow> return (fa (f x)) \<le> bind (F x) Fa
[PROOF STEP]
apply (rule order_trans[OF _ ibind_mono[OF REF order_refl]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>F fa x. \<lbrakk>\<And>x. return (fa x) \<le> F x; I x; b x\<rbrakk> \<Longrightarrow> return (fa (f x)) \<le> bind (return (f x)) F
[PROOF STEP]
apply (simp add: imonad_laws)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
return (while b f x) \<le> WHILEIT I b F x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_WHILET_esc[refine_transfer]:
  assumes REF: "\<And>x. return (f x) \<le> F x"
  shows "return (while b f x) \<le> WHILET b F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return (while b f x) \<le> WHILET b F x
[PROOF STEP]
unfolding WHILET_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return (while b f x) \<le> WHILEIT (\<lambda>_. True) b F x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
return (f ?x) \<le> F ?x

goal (1 subgoal):
 1. return (while b f x) \<le> WHILEIT (\<lambda>_. True) b F x
[PROOF STEP]
by (rule transfer_WHILEIT_esc)


[STATEMENT]
lemma WHILE_mono_prover_rule[refine_mono]:
  "\<lbrakk>\<And>x. f x \<le> f' x\<rbrakk> \<Longrightarrow> WHILE b f s0 \<le> WHILE b f' s0"
  "\<lbrakk>\<And>x. f x \<le> f' x\<rbrakk> \<Longrightarrow> WHILEI I b f s0 \<le> WHILEI I b f' s0"
  "\<lbrakk>\<And>x. f x \<le> f' x\<rbrakk> \<Longrightarrow> WHILET b f s0 \<le> WHILET b f' s0"
  "\<lbrakk>\<And>x. f x \<le> f' x\<rbrakk> \<Longrightarrow> WHILEIT I b f s0 \<le> WHILEIT I b f' s0"

  "\<lbrakk>\<And>x. flat_ge (f x) (f' x)\<rbrakk> \<Longrightarrow> flat_ge (WHILET b f s0) (WHILET b f' s0)"
  "\<lbrakk>\<And>x. flat_ge (f x) (f' x)\<rbrakk> \<Longrightarrow> flat_ge (WHILEIT I b f s0) (WHILEIT I b f' s0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>x. f x \<le> f' x) \<Longrightarrow> WHILE b f s0 \<le> WHILE b f' s0) &&& ((\<And>x. f x \<le> f' x) \<Longrightarrow> WHILEI I b f s0 \<le> WHILEI I b f' s0) &&& ((\<And>x. f x \<le> f' x) \<Longrightarrow> WHILET b f s0 \<le> WHILET b f' s0)) &&& ((\<And>x. f x \<le> f' x) \<Longrightarrow> WHILEIT I b f s0 \<le> WHILEIT I b f' s0) &&& ((\<And>x. flat_ge (f x) (f' x)) \<Longrightarrow> flat_ge (WHILET b f s0) (WHILET b f' s0)) &&& ((\<And>x. flat_ge (f x) (f' x)) \<Longrightarrow> flat_ge (WHILEIT I b f s0) (WHILEIT I b f' s0))
[PROOF STEP]
unfolding WHILE_def WHILEI_def WHILEI_body_def
    WHILET_def WHILEIT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>x. f x \<le> f' x) \<Longrightarrow> REC (\<lambda>W s. if True then if b s then bind (f s) W else return s else top) s0 \<le> REC (\<lambda>W s. if True then if b s then bind (f' s) W else return s else top) s0) &&& ((\<And>x. f x \<le> f' x) \<Longrightarrow> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) s0 \<le> REC (\<lambda>W s. if I s then if b s then bind (f' s) W else return s else top) s0) &&& ((\<And>x. f x \<le> f' x) \<Longrightarrow> REC\<^sub>T (\<lambda>W s. if True then if b s then bind (f s) W else return s else top) s0 \<le> REC\<^sub>T (\<lambda>W s. if True then if b s then bind (f' s) W else return s else top) s0)) &&& ((\<And>x. f x \<le> f' x) \<Longrightarrow> REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) s0 \<le> REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f' s) W else return s else top) s0) &&& ((\<And>x. flat_ge (f x) (f' x)) \<Longrightarrow> flat_ge (REC\<^sub>T (\<lambda>W s. if True then if b s then bind (f s) W else return s else top) s0) (REC\<^sub>T (\<lambda>W s. if True then if b s then bind (f' s) W else return s else top) s0)) &&& ((\<And>x. flat_ge (f x) (f' x)) \<Longrightarrow> flat_ge (REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) s0) (REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f' s) W else return s else top) s0))
[PROOF STEP]
by refine_mono+


[STATEMENT]
lemma transfer_WHILEIT[refine_transfer]:
  assumes REF: "\<And>x. \<alpha> (f x) \<le> F x"
  shows "\<alpha> (cWHILEIT I b f x) \<le> aWHILEIT I b F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (cWHILEIT I b f x) \<le> aWHILEIT I b F x
[PROOF STEP]
unfolding c.WHILEIT_def a.WHILEIT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (REC\<^sub>T (WHILEI_body cbind creturn I b f) x) \<le> REC\<^sub>T (WHILEI_body abind areturn I b F) x
[PROOF STEP]
apply (rule transfer_RECT[OF _ c.WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Fa fa x. (\<And>x. \<alpha> (fa x) \<le> Fa x) \<Longrightarrow> \<alpha> (WHILEI_body cbind creturn I b f fa x) \<le> WHILEI_body abind areturn I b F Fa x
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Fa fa x. (\<And>x. \<alpha> (fa x) \<le> Fa x) \<Longrightarrow> \<alpha> (if I x then if b x then cbind (f x) fa else creturn x else top) \<le> (if I x then if b x then abind (F x) Fa else areturn x else top)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Fa fa x. \<lbrakk>\<And>x. \<alpha> (fa x) \<le> Fa x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (cbind (f x) fa) \<le> abind (F x) Fa
 2. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply (rule transfer_bind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Fa fa x. \<lbrakk>\<And>x. \<alpha> (fa x) \<le> Fa x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (f x) \<le> F x
 2. \<And>F f x xa. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (f xa) \<le> F xa
 3. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply (rule REF)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>F f x xa. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (f xa) \<le> F xa
 2. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply (rule transfer_return)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma transfer_WHILEI[refine_transfer]:
  assumes REF: "\<And>x. \<alpha> (f x) \<le> F x"
  shows "\<alpha> (cWHILEI I b f x) \<le> aWHILEI I b F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (cWHILEI I b f x) \<le> aWHILEI I b F x
[PROOF STEP]
unfolding c.WHILEI_def a.WHILEI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (REC (WHILEI_body cbind creturn I b f) x) \<le> REC (WHILEI_body abind areturn I b F) x
[PROOF STEP]
apply (rule transfer_REC[OF _ c.WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Fa fa x. (\<And>x. \<alpha> (fa x) \<le> Fa x) \<Longrightarrow> \<alpha> (WHILEI_body cbind creturn I b f fa x) \<le> WHILEI_body abind areturn I b F Fa x
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Fa fa x. (\<And>x. \<alpha> (fa x) \<le> Fa x) \<Longrightarrow> \<alpha> (if I x then if b x then cbind (f x) fa else creturn x else top) \<le> (if I x then if b x then abind (F x) Fa else areturn x else top)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Fa fa x. \<lbrakk>\<And>x. \<alpha> (fa x) \<le> Fa x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (cbind (f x) fa) \<le> abind (F x) Fa
 2. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply (rule transfer_bind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Fa fa x. \<lbrakk>\<And>x. \<alpha> (fa x) \<le> Fa x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (f x) \<le> F x
 2. \<And>F f x xa. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (f xa) \<le> F xa
 3. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply (rule REF)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>F f x xa. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (f xa) \<le> F xa
 2. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>F f x. \<lbrakk>\<And>x. \<alpha> (f x) \<le> F x; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<alpha> (creturn x) \<le> areturn x
[PROOF STEP]
apply (rule transfer_return)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma transfer_WHILE[refine_transfer]:
  assumes REF: "\<And>x. \<alpha> (f x) \<le> F x"
  shows "\<alpha> (cWHILE b f x) \<le> aWHILE b F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (cWHILE b f x) \<le> aWHILE b F x
[PROOF STEP]
unfolding c.WHILE_def a.WHILE_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (cWHILEI (\<lambda>_. True) b f x) \<le> aWHILEI (\<lambda>_. True) b F x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> (f ?x) \<le> F ?x

goal (1 subgoal):
 1. \<alpha> (cWHILEI (\<lambda>_. True) b f x) \<le> aWHILEI (\<lambda>_. True) b F x
[PROOF STEP]
by (rule transfer_WHILEI)


[STATEMENT]
lemma transfer_WHILET[refine_transfer]:
  assumes REF: "\<And>x. \<alpha> (f x) \<le> F x"
  shows "\<alpha> (cWHILET b f x) \<le> aWHILET b F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (cWHILET b f x) \<le> aWHILET b F x
[PROOF STEP]
unfolding c.WHILET_def a.WHILET_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (cWHILEIT (\<lambda>_. True) b f x) \<le> aWHILEIT (\<lambda>_. True) b F x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> (f ?x) \<le> F ?x

goal (1 subgoal):
 1. \<alpha> (cWHILEIT (\<lambda>_. True) b f x) \<le> aWHILEIT (\<lambda>_. True) b F x
[PROOF STEP]
by (rule transfer_WHILEIT)


[STATEMENT]
lemma ireturn_eq: "return x = SPEC ((=) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return x = SPEC ((=) x)
[PROOF STEP]
unfolding iSPEC_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return x = Sup {return xa |xa. x = xa}
[PROOF STEP]
by auto


[STATEMENT]
lemma iSPEC_rule: "(\<And>x. \<Phi> x \<Longrightarrow> \<Psi> x) \<Longrightarrow> SPEC \<Phi> \<le> SPEC \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<Phi> x \<Longrightarrow> \<Psi> x) \<Longrightarrow> SPEC \<Phi> \<le> SPEC \<Psi>
[PROOF STEP]
unfolding iSPEC_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<Phi> x \<Longrightarrow> \<Psi> x) \<Longrightarrow> Sup {return x |x. \<Phi> x} \<le> Sup {return x |x. \<Psi> x}
[PROOF STEP]
by (auto intro: Sup_mono)


[STATEMENT]
lemma ireturn_rule: "\<Phi> x \<Longrightarrow> return x \<le> SPEC \<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> x \<Longrightarrow> return x \<le> SPEC \<Phi>
[PROOF STEP]
unfolding ireturn_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> x \<Longrightarrow> SPEC ((=) x) \<le> SPEC \<Phi>
[PROOF STEP]
by (auto intro: iSPEC_rule)


[STATEMENT]
lemma WHILEI_rule:
  assumes I0: "I s"
  assumes ISTEP: "\<And>s. \<lbrakk>I s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC I"
  assumes CONS: "\<And>s. \<lbrakk> I s; \<not> b s \<rbrakk> \<Longrightarrow> \<Phi> s"
  shows "WHILEI I b f s \<le> SPEC \<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI I b f s \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule order_trans[where y="SPEC (\<lambda>s. I s \<and> \<not> b s)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. WHILEI I b f s \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 2. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (unfold WHILEI_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. REC (WHILEI_body bind return I b f) s \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 2. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule REC_rule[OF WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?pre3 s
 2. \<And>fa x. \<lbrakk>\<And>x. ?pre3 x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); ?pre3 x; fa \<le> REC (WHILEI_body bind return I b f)\<rbrakk> \<Longrightarrow> WHILEI_body bind return I b f fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 3. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule I0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); I x; fa \<le> REC (WHILEI_body bind return I b f)\<rbrakk> \<Longrightarrow> WHILEI_body bind return I b f fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 2. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); I x; fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top)\<rbrakk> \<Longrightarrow> (if I x then if b x then bind (f x) fa else return x else top) \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 2. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (split if_split)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); I x; fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top)\<rbrakk> \<Longrightarrow> (b x \<longrightarrow> (I x \<longrightarrow> bind (f x) fa \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)) \<and> (\<not> I x \<longrightarrow> top \<le> SPEC (\<lambda>s. I s \<and> \<not> b s))) \<and> (\<not> b x \<longrightarrow> (I x \<longrightarrow> return x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)) \<and> (\<not> I x \<longrightarrow> top \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)))
 2. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (intro impI conjI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); I x; fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); b x; I x\<rbrakk> \<Longrightarrow> bind (f x) fa \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 2. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); I x; fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); b x; \<not> I x\<rbrakk> \<Longrightarrow> top \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 3. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); I x; fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 4. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); I x; fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); \<not> b x; \<not> I x\<rbrakk> \<Longrightarrow> top \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 5. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); b x; I x\<rbrakk> \<Longrightarrow> bind (f x) fa \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 2. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 3. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule ibind_rule)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); b x; I x\<rbrakk> \<Longrightarrow> f x \<le> SPEC (\<lambda>x. fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s))
 2. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 3. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (erule (1) order_trans[OF ISTEP])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); b x\<rbrakk> \<Longrightarrow> SPEC I \<le> SPEC (\<lambda>x. fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s))
 2. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 3. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule iSPEC_rule, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s)
 2. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule ireturn_rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x. I x \<Longrightarrow> fa x \<le> SPEC (\<lambda>s. I s \<and> \<not> b s); fa \<le> REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top); \<not> b x; I x\<rbrakk> \<Longrightarrow> I x \<and> \<not> b x
 2. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>s. I s \<and> \<not> b s) \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule iSPEC_rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. I x \<and> \<not> b x \<Longrightarrow> \<Phi> x
[PROOF STEP]
apply (simp add: CONS)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WHILEIT_rule:
  assumes WF: "wf R"
  assumes I0: "I s"
  assumes IS: "\<And>s. \<lbrakk> I s; b s \<rbrakk> \<Longrightarrow> f s \<le> SPEC (\<lambda>s'. I s' \<and> (s',s)\<in>R)"
  assumes PHI: "\<And>s. \<lbrakk> I s; \<not> b s \<rbrakk> \<Longrightarrow> \<Phi> s"
  shows "WHILEIT I b f s \<le> SPEC \<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEIT I b f s \<le> SPEC \<Phi>
[PROOF STEP]
unfolding WHILEIT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC\<^sub>T (WHILEI_body bind return I b f) s \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule RECT_rule[OF WHILEI_body_trimono WF, where pre=I,OF I0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; I x; REC\<^sub>T (WHILEI_body bind return I b f) = fa\<rbrakk> \<Longrightarrow> WHILEI_body bind return I b f fa x \<le> SPEC \<Phi>
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; I x; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa\<rbrakk> \<Longrightarrow> (if I x then if b x then bind (f x) fa else return x else top) \<le> SPEC \<Phi>
[PROOF STEP]
apply (split if_split)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; I x; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa\<rbrakk> \<Longrightarrow> (b x \<longrightarrow> (I x \<longrightarrow> bind (f x) fa \<le> SPEC \<Phi>) \<and> (\<not> I x \<longrightarrow> top \<le> SPEC \<Phi>)) \<and> (\<not> b x \<longrightarrow> (I x \<longrightarrow> return x \<le> SPEC \<Phi>) \<and> (\<not> I x \<longrightarrow> top \<le> SPEC \<Phi>))
[PROOF STEP]
apply (intro impI conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; I x; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; b x; I x\<rbrakk> \<Longrightarrow> bind (f x) fa \<le> SPEC \<Phi>
 2. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; I x; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; b x; \<not> I x\<rbrakk> \<Longrightarrow> top \<le> SPEC \<Phi>
 3. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; I x; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC \<Phi>
 4. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; I x; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; \<not> I x\<rbrakk> \<Longrightarrow> top \<le> SPEC \<Phi>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; b x; I x\<rbrakk> \<Longrightarrow> bind (f x) fa \<le> SPEC \<Phi>
 2. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule ibind_rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; b x; I x\<rbrakk> \<Longrightarrow> f x \<le> SPEC (\<lambda>x. fa x \<le> SPEC \<Phi>)
 2. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule order_trans[OF IS], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; b x; I x\<rbrakk> \<Longrightarrow> SPEC (\<lambda>s'. I s' \<and> (s', x) \<in> R) \<le> SPEC (\<lambda>x. fa x \<le> SPEC \<Phi>)
 2. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule iSPEC_rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa x xa. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; b x; I x; I xa \<and> (xa, x) \<in> R\<rbrakk> \<Longrightarrow> fa xa \<le> SPEC \<Phi>
 2. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC \<Phi>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; I x\<rbrakk> \<Longrightarrow> return x \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule ireturn_rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa x. \<lbrakk>\<And>x'. \<lbrakk>I x'; (x', x) \<in> R\<rbrakk> \<Longrightarrow> fa x' \<le> SPEC \<Phi>; REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top) = fa; \<not> b x; I x\<rbrakk> \<Longrightarrow> \<Phi> x
[PROOF STEP]
apply (simp add: PHI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WHILE_rule:
  assumes I0: "I s"
  assumes ISTEP: "\<And>s. \<lbrakk>I s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC I"
  assumes CONS: "\<And>s. \<lbrakk> I s; \<not> b s \<rbrakk> \<Longrightarrow> \<Phi> s"
  shows "WHILE b f s \<le> SPEC \<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILE b f s \<le> SPEC \<Phi>
[PROOF STEP]
unfolding WHILE_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI (\<lambda>_. True) b f s \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule order_trans[OF WHILEI_weaken WHILEI_rule])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. ?I2 x \<Longrightarrow> True
 2. ?I2 s
 3. \<And>s. \<lbrakk>?I2 s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC ?I2
 4. \<And>s. \<lbrakk>?I2 s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
apply (rule TrueI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?I2 s
 2. \<And>s. \<lbrakk>?I2 s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC ?I2
 3. \<And>s. \<lbrakk>?I2 s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
apply (rule I0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>I s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC I
 2. \<And>s. \<lbrakk>I s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
I s
\<lbrakk>I ?s; b ?s\<rbrakk> \<Longrightarrow> f ?s \<le> SPEC I
\<lbrakk>I ?s; \<not> b ?s\<rbrakk> \<Longrightarrow> \<Phi> ?s

goal (2 subgoals):
 1. \<And>s. \<lbrakk>I s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC I
 2. \<And>s. \<lbrakk>I s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
by auto


[STATEMENT]
lemma WHILET_rule:
  assumes WF: "wf R"
  assumes I0: "I s"
  assumes IS: "\<And>s. \<lbrakk> I s; b s \<rbrakk> \<Longrightarrow> f s \<le> SPEC (\<lambda>s'. I s' \<and> (s',s)\<in>R)"
  assumes PHI: "\<And>s. \<lbrakk> I s; \<not> b s \<rbrakk> \<Longrightarrow> \<Phi> s"
  shows "WHILET b f s \<le> SPEC \<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILET b f s \<le> SPEC \<Phi>
[PROOF STEP]
unfolding WHILET_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEIT (\<lambda>_. True) b f s \<le> SPEC \<Phi>
[PROOF STEP]
apply (rule order_trans[OF WHILEIT_weaken WHILEIT_rule])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. ?I2 x \<Longrightarrow> True
 2. wf ?R2
 3. ?I2 s
 4. \<And>s. \<lbrakk>?I2 s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC (\<lambda>s'. ?I2 s' \<and> (s', s) \<in> ?R2)
 5. \<And>s. \<lbrakk>?I2 s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
apply (rule TrueI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wf ?R2
 2. ?I2 s
 3. \<And>s. \<lbrakk>?I2 s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC (\<lambda>s'. ?I2 s' \<and> (s', s) \<in> ?R2)
 4. \<And>s. \<lbrakk>?I2 s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
apply (rule WF)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?I2 s
 2. \<And>s. \<lbrakk>?I2 s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC (\<lambda>s'. ?I2 s' \<and> (s', s) \<in> R)
 3. \<And>s. \<lbrakk>?I2 s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
apply (rule I0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>I s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC (\<lambda>s'. I s' \<and> (s', s) \<in> R)
 2. \<And>s. \<lbrakk>I s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf R
I s
\<lbrakk>I ?s; b ?s\<rbrakk> \<Longrightarrow> f ?s \<le> SPEC (\<lambda>s'. I s' \<and> (s', ?s) \<in> R)
\<lbrakk>I ?s; \<not> b ?s\<rbrakk> \<Longrightarrow> \<Phi> ?s

goal (2 subgoals):
 1. \<And>s. \<lbrakk>I s; b s\<rbrakk> \<Longrightarrow> f s \<le> SPEC (\<lambda>s'. I s' \<and> (s', s) \<in> R)
 2. \<And>s. \<lbrakk>I s; \<not> b s\<rbrakk> \<Longrightarrow> \<Phi> s
[PROOF STEP]
by auto


[STATEMENT]
lemma (in monoid_homomorphism) monoid_preimage: "Group_Theory.monoid (\<eta> \<^sup>\<inverse> M M') (\<cdot>) \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<eta> \<^sup>\<inverse> M M') (\<cdot>) \<one>
[PROOF STEP]
by (simp add: Int_absorb1 source.monoid_axioms subsetI)


[STATEMENT]
lemma (in group_homomorphism) group_preimage: "Group_Theory.group (\<eta> \<^sup>\<inverse> G G') (\<cdot>) \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group (\<eta> \<^sup>\<inverse> G G') (\<cdot>) \<one>
[PROOF STEP]
by (simp add: Int_absorb1 source.group_axioms subsetI)


[STATEMENT]
lemma (in ring_homomorphism) ring_preimage: "ring (\<eta> \<^sup>\<inverse> R R') (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (\<eta> \<^sup>\<inverse> R R') (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (simp add: Int_absorb2 Int_commute source.ring_axioms subset_iff)


[STATEMENT]
lemma invertible_0: "monoid.invertible {0} (\<lambda>n m. 0) 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid.invertible {0::'a} (\<lambda>n m. 0::'a) (0::'a) (0::'a)
[PROOF STEP]
using Group_Theory.monoid.intro monoid.unit_invertible
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>a b. \<lbrakk>a \<in> ?M; b \<in> ?M\<rbrakk> \<Longrightarrow> ?composition a b \<in> ?M; ?unit \<in> ?M; \<And>a b c. \<lbrakk>a \<in> ?M; b \<in> ?M; c \<in> ?M\<rbrakk> \<Longrightarrow> ?composition (?composition a b) c = ?composition a (?composition b c); \<And>a. a \<in> ?M \<Longrightarrow> ?composition ?unit a = a; \<And>a. a \<in> ?M \<Longrightarrow> ?composition a ?unit = a\<rbrakk> \<Longrightarrow> Group_Theory.monoid ?M ?composition ?unit
Group_Theory.monoid ?M ?composition ?unit \<Longrightarrow> monoid.invertible ?M ?composition ?unit ?unit

goal (1 subgoal):
 1. monoid.invertible {0::'a} (\<lambda>n m. 0::'a) (0::'a) (0::'a)
[PROOF STEP]
by force


[STATEMENT]
lemma mult_left_assoc: "\<lbrakk> a \<in> R; b \<in> R; c \<in> R \<rbrakk> \<Longrightarrow> b \<cdot> (a \<cdot> c) = a \<cdot> (b \<cdot> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> R; b \<in> R; c \<in> R\<rbrakk> \<Longrightarrow> b \<cdot> (a \<cdot> c) = a \<cdot> (b \<cdot> c)
[PROOF STEP]
using comm_mult multiplicative.associative
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. \<lbrakk>a \<in> R; b \<in> R; c \<in> R\<rbrakk> \<Longrightarrow> b \<cdot> (a \<cdot> c) = a \<cdot> (b \<cdot> c)
[PROOF STEP]
by auto


[STATEMENT]
lemma ideal_R_R: "ideal R R (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. R \<subseteq> R
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> R\<rbrakk> \<Longrightarrow> a + b \<in> R
 3. \<zero> \<in> R
 4. \<And>a b. \<lbrakk>a \<in> R; b \<in> R\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> R
 5. \<And>a b. \<lbrakk>a \<in> R; b \<in> R\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> R
[PROOF STEP]
qed auto


[STATEMENT]
lemma ideal_0_R: "ideal {\<zero>} R (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal {\<zero>} R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. {\<zero>} \<subseteq> R
 2. \<And>a b. \<lbrakk>a \<in> {\<zero>}; b \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a + b \<in> {\<zero>}
 3. \<zero> \<in> {\<zero>}
 4. \<And>a b c. \<lbrakk>a \<in> {\<zero>}; b \<in> {\<zero>}; c \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 5. \<And>a. a \<in> {\<zero>} \<Longrightarrow> \<zero> + a = a
 6. \<And>a. a \<in> {\<zero>} \<Longrightarrow> a + \<zero> = a
 7. \<And>u. u \<in> {\<zero>} \<Longrightarrow> monoid.invertible {\<zero>} (+) \<zero> u
 8. \<And>a b. \<lbrakk>a \<in> R; b \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> {\<zero>}
 9. \<And>a b. \<lbrakk>a \<in> R; b \<in> {\<zero>}\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> {\<zero>}
[PROOF STEP]
show "monoid.invertible {\<zero>} (+) \<zero> u"
    if "u \<in> {\<zero>}"
    for u :: 'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid.invertible {\<zero>} (+) \<zero> u
[PROOF STEP]
proof (rule monoid.invertibleI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. Group_Theory.monoid {\<zero>} (+) \<zero>
 2. u + ?v = \<zero>
 3. ?v + u = \<zero>
 4. u \<in> {\<zero>}
 5. ?v \<in> {\<zero>}
[PROOF STEP]
show "Group_Theory.monoid {\<zero>} (+) \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid {\<zero>} (+) \<zero>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> {\<zero>}; b \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a + b \<in> {\<zero>}
 2. \<zero> \<in> {\<zero>}
 3. \<And>a b c. \<lbrakk>a \<in> {\<zero>}; b \<in> {\<zero>}; c \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 4. \<And>a. a \<in> {\<zero>} \<Longrightarrow> \<zero> + a = a
 5. \<And>a. a \<in> {\<zero>} \<Longrightarrow> a + \<zero> = a
[PROOF STEP]
qed (use that in auto)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid {\<zero>} (+) \<zero>

goal (4 subgoals):
 1. u + ?v = \<zero>
 2. ?v + u = \<zero>
 3. u \<in> {\<zero>}
 4. ?v \<in> {\<zero>}
[PROOF STEP]
qed (use that in auto)
[PROOF STATE]
proof (state)
this:
?u2 \<in> {\<zero>} \<Longrightarrow> monoid.invertible {\<zero>} (+) \<zero> ?u2

goal (8 subgoals):
 1. {\<zero>} \<subseteq> R
 2. \<And>a b. \<lbrakk>a \<in> {\<zero>}; b \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a + b \<in> {\<zero>}
 3. \<zero> \<in> {\<zero>}
 4. \<And>a b c. \<lbrakk>a \<in> {\<zero>}; b \<in> {\<zero>}; c \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 5. \<And>a. a \<in> {\<zero>} \<Longrightarrow> \<zero> + a = a
 6. \<And>a. a \<in> {\<zero>} \<Longrightarrow> a + \<zero> = a
 7. \<And>a b. \<lbrakk>a \<in> R; b \<in> {\<zero>}\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> {\<zero>}
 8. \<And>a b. \<lbrakk>a \<in> R; b \<in> {\<zero>}\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> {\<zero>}
[PROOF STEP]
qed auto


[STATEMENT]
lemma ideal_zero: "ideal A R add mult zero unit \<Longrightarrow> zero \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal A R add mult \<zero> \<one> \<Longrightarrow> \<zero> \<in> A
[PROOF STEP]
by (simp add: ideal_def subgroup_of_additive_group_of_ring_def subgroup_def submonoid_def submonoid_axioms_def)


[STATEMENT]
lemma ideal_implies_subset:
  assumes "ideal A R add mult zero unit"
  shows "A \<subseteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> R
[PROOF STEP]
by (meson assms ideal_def subgroup_def subgroup_of_additive_group_of_ring_def submonoid_axioms_def submonoid_def)


[STATEMENT]
lemma ideal_inverse:
  assumes "a \<in> A" "ideal A R (+) mult zero unit"
  shows "additive.inverse a \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - a \<in> A
[PROOF STEP]
by (meson additive.invertible assms comm_ring.ideal_implies_subset comm_ring_axioms ideal_def subgroup.subgroup_inverse_iff subgroup_of_additive_group_of_ring_def subsetD)


[STATEMENT]
lemma ideal_add:
  assumes "a \<in> A"  "b \<in> A" "ideal A R add mult zero unit"
  shows "add a b \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add a b \<in> A
[PROOF STEP]
by (meson Group_Theory.group_def assms ideal_def monoid.composition_closed subgroup_def subgroup_of_additive_group_of_ring_def)


[STATEMENT]
lemma ideal_mult_in_subgroup_generated:
  assumes \<aa>: "ideal \<aa> R (+) (\<cdot>) \<zero> \<one>" and \<bb>: "ideal \<bb> R (+) (\<cdot>) \<zero> \<one>" and "a \<in> \<aa>" "b \<in> \<bb>"
  shows "a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
have "\<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>
[PROOF STEP]
using assms ideal_implies_subset
[PROOF STATE]
proof (prove)
using this:
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
a \<in> \<aa>
b \<in> \<bb>
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R

goal (1 subgoal):
 1. \<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>

goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
with ideal_implies_subset
[PROOF STATE]
proof (chain)
picking this:
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R
\<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R
\<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>

goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
unfolding additive.subgroup_generated_def ideal_gen_by_prod_def
[PROOF STATE]
proof (prove)
using this:
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R
\<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>

goal (1 subgoal):
 1. a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
using assms ideal_implies_subset
[PROOF STATE]
proof (prove)
using this:
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R
\<exists>x y. a \<cdot> b = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
a \<in> \<aa>
b \<in> \<bb>
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R

goal (1 subgoal):
 1. a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
by (blast intro: additive.generate.incl)
[PROOF STATE]
proof (state)
this:
a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_in_gen_ideal:
  assumes "x \<in> R"
  shows "\<zero> \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> \<langle>x\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<zero> \<in> \<langle>x\<rangle>
[PROOF STEP]
have "\<exists>a. a \<in> R \<and> \<zero> = a \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. a \<in> R \<and> \<zero> = a \<cdot> x
[PROOF STEP]
by (metis (lifting) additive.unit_closed assms left_zero)
[PROOF STATE]
proof (state)
this:
\<exists>a. a \<in> R \<and> \<zero> = a \<cdot> x

goal (1 subgoal):
 1. \<zero> \<in> \<langle>x\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. a \<in> R \<and> \<zero> = a \<cdot> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>a. a \<in> R \<and> \<zero> = a \<cdot> x

goal (1 subgoal):
 1. \<zero> \<in> \<langle>x\<rangle>
[PROOF STEP]
using gen_ideal_def
[PROOF STATE]
proof (prove)
using this:
\<exists>a. a \<in> R \<and> \<zero> = a \<cdot> x
\<langle>?x\<rangle> \<equiv> {y. \<exists>r\<in>R. y = r \<cdot> ?x}

goal (1 subgoal):
 1. \<zero> \<in> \<langle>x\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<zero> \<in> \<langle>x\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_in_gen_ideal:
  "\<lbrakk>x \<in> R; a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> R; a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
[PROOF STEP]
apply (clarsimp simp : gen_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>x \<in> R; r \<in> R; a = r \<cdot> x; ra \<in> R; b = ra \<cdot> x\<rbrakk> \<Longrightarrow> \<exists>rb\<in>R. r \<cdot> x + ra \<cdot> x = rb \<cdot> x
[PROOF STEP]
by (metis (no_types) additive.composition_closed distributive(2))


[STATEMENT]
lemma gen_ideal_subset:
  assumes "x \<in> R"
  shows "\<langle>x\<rangle> \<subseteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x\<rangle> \<subseteq> R
[PROOF STEP]
using assms comm_ring.gen_ideal_def local.comm_ring_axioms
[PROOF STATE]
proof (prove)
using this:
x \<in> R
comm_ring ?R ?addition ?multiplication ?zero ?unit \<Longrightarrow> comm_ring.gen_ideal ?R ?multiplication ?x \<equiv> {y. \<exists>r\<in>?R. y = ?multiplication r ?x}
comm_ring R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. \<langle>x\<rangle> \<subseteq> R
[PROOF STEP]
by fastforce


[STATEMENT]
lemma gen_ideal_monoid:
  assumes "x \<in> R"
  shows "Group_Theory.monoid \<langle>x\<rangle> (+) \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid \<langle>x\<rangle> (+) \<zero>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a b c. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>; c \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 5. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
[PROOF STEP]
show "a + b \<in> \<langle>x\<rangle>" if "a \<in> \<langle>x\<rangle>" "b \<in> \<langle>x\<rangle>" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b \<in> \<langle>x\<rangle>
[PROOF STEP]
by (simp add: add_in_gen_ideal assms that)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<in> \<langle>x\<rangle>; ?b2 \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> ?a2 + ?b2 \<in> \<langle>x\<rangle>

goal (4 subgoals):
 1. \<zero> \<in> \<langle>x\<rangle>
 2. \<And>a b c. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>; c \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 3. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
[PROOF STEP]
qed (use assms zero_in_gen_ideal gen_ideal_def in auto)


[STATEMENT]
lemma gen_ideal_group:
  assumes "x \<in> R"
  shows "Group_Theory.group \<langle>x\<rangle> (+) \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group \<langle>x\<rangle> (+) \<zero>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a b c. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>; c \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 5. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 6. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a b c. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>; c \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 5. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 6. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
assume "a \<in> \<langle>x\<rangle>" "b \<in> \<langle>x\<rangle>" "c \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (state)
this:
a \<in> \<langle>x\<rangle>
b \<in> \<langle>x\<rangle>
c \<in> \<langle>x\<rangle>

goal (6 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a b c. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>; c \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 5. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 6. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<langle>x\<rangle>
b \<in> \<langle>x\<rangle>
c \<in> \<langle>x\<rangle>
[PROOF STEP]
show "a + b + c = a + (b + c)"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<langle>x\<rangle>
b \<in> \<langle>x\<rangle>
c \<in> \<langle>x\<rangle>

goal (1 subgoal):
 1. a + b + c = a + (b + c)
[PROOF STEP]
by (meson assms gen_ideal_monoid monoid.associative)
[PROOF STATE]
proof (state)
this:
a + b + c = a + (b + c)

goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 5. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 5. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 5. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
assume a: "a \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (state)
this:
a \<in> \<langle>x\<rangle>

goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> \<zero> + a = a
 4. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 5. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
show "\<zero> + a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> + a = a
[PROOF STEP]
by (meson a assms gen_ideal_monoid monoid.left_unit)
[PROOF STATE]
proof (state)
this:
\<zero> + a = a

goal (4 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>a. a \<in> \<langle>x\<rangle> \<Longrightarrow> a + \<zero> = a
 4. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
show "a + \<zero> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + \<zero> = a
[PROOF STEP]
by (meson a assms gen_ideal_monoid monoid.right_unit)
[PROOF STATE]
proof (state)
this:
a + \<zero> = a

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> monoid.invertible \<langle>x\<rangle> (+) \<zero> u
[PROOF STEP]
interpret M: monoid "\<langle>x\<rangle>" "(+)" \<zero>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid \<langle>x\<rangle> (+) \<zero>
[PROOF STEP]
by (simp add: assms gen_ideal_monoid)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> M.invertible u
[PROOF STEP]
obtain r where r: "r\<in>R" "a = r \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> R; a = r \<cdot> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a gen_ideal_def
[PROOF STATE]
proof (prove)
using this:
a \<in> \<langle>x\<rangle>
\<langle>?x\<rangle> \<equiv> {y. \<exists>r\<in>R. y = r \<cdot> ?x}

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> R; a = r \<cdot> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> R
a = r \<cdot> x

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
 3. \<And>u. u \<in> \<langle>x\<rangle> \<Longrightarrow> M.invertible u
[PROOF STEP]
show "monoid.invertible \<langle>x\<rangle> (+) \<zero> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.invertible a
[PROOF STEP]
proof (rule M.invertibleI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. a + ?v = \<zero>
 2. ?v + a = \<zero>
 3. a \<in> \<langle>x\<rangle>
 4. ?v \<in> \<langle>x\<rangle>
[PROOF STEP]
have "\<exists>r\<in>R. - a = r \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>R. - a = r \<cdot> x
[PROOF STEP]
by (metis assms ideal_R_R ideal_inverse local.left_minus r)
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>R. - a = r \<cdot> x

goal (4 subgoals):
 1. a + ?v = \<zero>
 2. ?v + a = \<zero>
 3. a \<in> \<langle>x\<rangle>
 4. ?v \<in> \<langle>x\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r\<in>R. - a = r \<cdot> x
[PROOF STEP]
show "-a \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>R. - a = r \<cdot> x

goal (1 subgoal):
 1. - a \<in> \<langle>x\<rangle>
[PROOF STEP]
by (simp add: gen_ideal_def)
[PROOF STATE]
proof (state)
this:
- a \<in> \<langle>x\<rangle>

goal (3 subgoals):
 1. a - a = \<zero>
 2. - a + a = \<zero>
 3. a \<in> \<langle>x\<rangle>
[PROOF STEP]
qed (use a r assms in auto)
[PROOF STATE]
proof (state)
this:
M.invertible a

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<langle>x\<rangle>; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a + b \<in> \<langle>x\<rangle>
 2. \<zero> \<in> \<langle>x\<rangle>
[PROOF STEP]
qed (auto simp: zero_in_gen_ideal add_in_gen_ideal assms)


[STATEMENT]
lemma gen_ideal_ideal:
  assumes "x \<in> R"
  shows "ideal \<langle>x\<rangle> R (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal \<langle>x\<rangle> R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms \<langle>x\<rangle> R (+) \<zero>
 2. Group_Theory.monoid \<langle>x\<rangle> (+) \<zero>
 3. Group_Theory.group_axioms \<langle>x\<rangle> (+) \<zero>
 4. ideal_axioms \<langle>x\<rangle> R (\<cdot>)
[PROOF STEP]
show "submonoid_axioms \<langle>x\<rangle> R (+) \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms \<langle>x\<rangle> R (+) \<zero>
[PROOF STEP]
by (simp add: add_in_gen_ideal assms gen_ideal_subset submonoid_axioms.intro zero_in_gen_ideal)
[PROOF STATE]
proof (state)
this:
submonoid_axioms \<langle>x\<rangle> R (+) \<zero>

goal (3 subgoals):
 1. Group_Theory.monoid \<langle>x\<rangle> (+) \<zero>
 2. Group_Theory.group_axioms \<langle>x\<rangle> (+) \<zero>
 3. ideal_axioms \<langle>x\<rangle> R (\<cdot>)
[PROOF STEP]
show "Group_Theory.group_axioms \<langle>x\<rangle> (+) \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms \<langle>x\<rangle> (+) \<zero>
[PROOF STEP]
by (meson Group_Theory.group_def assms gen_ideal_group)
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms \<langle>x\<rangle> (+) \<zero>

goal (2 subgoals):
 1. Group_Theory.monoid \<langle>x\<rangle> (+) \<zero>
 2. ideal_axioms \<langle>x\<rangle> R (\<cdot>)
[PROOF STEP]
show "ideal_axioms \<langle>x\<rangle> R (\<cdot>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_axioms \<langle>x\<rangle> R (\<cdot>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> \<langle>x\<rangle>
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> \<langle>x\<rangle>
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> \<langle>x\<rangle>
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> \<langle>x\<rangle>
[PROOF STEP]
assume "a \<in> R" "b \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (state)
this:
a \<in> R
b \<in> \<langle>x\<rangle>

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> \<langle>x\<rangle>
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> \<langle>x\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> R
b \<in> \<langle>x\<rangle>
[PROOF STEP]
obtain r where r: "r\<in>R" "b = r \<cdot> x"
[PROOF STATE]
proof (prove)
using this:
a \<in> R
b \<in> \<langle>x\<rangle>

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> R; b = r \<cdot> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: gen_ideal_def)
[PROOF STATE]
proof (state)
this:
r \<in> R
b = r \<cdot> x

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> \<langle>x\<rangle>
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> \<langle>x\<rangle>
[PROOF STEP]
have "a \<cdot> (r \<cdot> x) = (a \<cdot> r) \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> (r \<cdot> x) = a \<cdot> r \<cdot> x
[PROOF STEP]
using \<open>a \<in> R\<close> \<open>r \<in> R\<close> assms multiplicative.associative
[PROOF STATE]
proof (prove)
using this:
a \<in> R
r \<in> R
x \<in> R
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. a \<cdot> (r \<cdot> x) = a \<cdot> r \<cdot> x
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
a \<cdot> (r \<cdot> x) = a \<cdot> r \<cdot> x

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> \<langle>x\<rangle>
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> \<langle>x\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<cdot> (r \<cdot> x) = a \<cdot> r \<cdot> x
[PROOF STEP]
show "a \<cdot> b \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
using this:
a \<cdot> (r \<cdot> x) = a \<cdot> r \<cdot> x

goal (1 subgoal):
 1. a \<cdot> b \<in> \<langle>x\<rangle>
[PROOF STEP]
using \<open>a \<in> R\<close> r gen_ideal_def
[PROOF STATE]
proof (prove)
using this:
a \<cdot> (r \<cdot> x) = a \<cdot> r \<cdot> x
a \<in> R
r \<in> R
b = r \<cdot> x
\<langle>?x\<rangle> \<equiv> {y. \<exists>r\<in>R. y = r \<cdot> ?x}

goal (1 subgoal):
 1. a \<cdot> b \<in> \<langle>x\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<cdot> b \<in> \<langle>x\<rangle>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> \<langle>x\<rangle>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> \<langle>x\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<cdot> b \<in> \<langle>x\<rangle>
[PROOF STEP]
show "b \<cdot> a \<in> \<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
using this:
a \<cdot> b \<in> \<langle>x\<rangle>

goal (1 subgoal):
 1. b \<cdot> a \<in> \<langle>x\<rangle>
[PROOF STEP]
by (simp add: \<open>a \<in> R\<close> assms comm_mult r)
[PROOF STATE]
proof (state)
this:
b \<cdot> a \<in> \<langle>x\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_axioms \<langle>x\<rangle> R (\<cdot>)

goal (1 subgoal):
 1. Group_Theory.monoid \<langle>x\<rangle> (+) \<zero>
[PROOF STEP]
qed (auto simp add: assms gen_ideal_monoid)


[STATEMENT]
lemma in_ideal_gen_by_prod:
  assumes \<aa>: "ideal \<aa> R (+) (\<cdot>) \<zero> \<one>" and \<bb>: "ideal \<bb> R (+) (\<cdot>) \<zero> \<one>"
    and "a \<in> R" and b: "b \<in> ideal_gen_by_prod \<aa> \<bb>"
  shows "a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
using b \<open>a \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
b \<in> ideal_gen_by_prod \<aa> \<bb>
a \<in> R

goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
unfolding additive.subgroup_generated_def ideal_gen_by_prod_def
[PROOF STATE]
proof (prove)
using this:
b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> R

goal (1 subgoal):
 1. a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
proof (induction arbitrary: a)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a. a \<in> R \<Longrightarrow> a \<cdot> \<zero> \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 3. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 4. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
case unit
[PROOF STATE]
proof (state)
this:
a \<in> R

goal (4 subgoals):
 1. \<And>a. a \<in> R \<Longrightarrow> a \<cdot> \<zero> \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 3. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 4. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> R

goal (1 subgoal):
 1. a \<cdot> \<zero> \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
by (simp add: additive.generate.unit)
[PROOF STATE]
proof (state)
this:
a \<cdot> \<zero> \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal (3 subgoals):
 1. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 3. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 3. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
case (incl x u)
[PROOF STATE]
proof (state)
this:
x \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
u \<in> R

goal (3 subgoals):
 1. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 3. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
with \<aa> \<bb>
[PROOF STATE]
proof (chain)
picking this:
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
x \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
u \<in> R
[PROOF STEP]
have "\<And>a b. \<lbrakk>a \<cdot> b \<in> R; a \<in> \<aa>; b \<in> \<bb>\<rbrakk> \<Longrightarrow> \<exists>x y. u \<cdot> (a \<cdot> b) = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>"
[PROOF STATE]
proof (prove)
using this:
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
x \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
u \<in> R

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<cdot> b \<in> R; a \<in> \<aa>; b \<in> \<bb>\<rbrakk> \<Longrightarrow> \<exists>x y. u \<cdot> (a \<cdot> b) = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>
[PROOF STEP]
by simp (metis ideal.ideal(1) ideal_implies_subset multiplicative.associative subset_iff)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<cdot> ?b2 \<in> R; ?a2 \<in> \<aa>; ?b2 \<in> \<bb>\<rbrakk> \<Longrightarrow> \<exists>x y. u \<cdot> (?a2 \<cdot> ?b2) = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>

goal (3 subgoals):
 1. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 3. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a2 \<cdot> ?b2 \<in> R; ?a2 \<in> \<aa>; ?b2 \<in> \<bb>\<rbrakk> \<Longrightarrow> \<exists>x y. u \<cdot> (?a2 \<cdot> ?b2) = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a2 \<cdot> ?b2 \<in> R; ?a2 \<in> \<aa>; ?b2 \<in> \<bb>\<rbrakk> \<Longrightarrow> \<exists>x y. u \<cdot> (?a2 \<cdot> ?b2) = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>

goal (1 subgoal):
 1. u \<cdot> x \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
using additive.generate.incl incl.hyps incl.prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a2 \<cdot> ?b2 \<in> R; ?a2 \<in> \<aa>; ?b2 \<in> \<bb>\<rbrakk> \<Longrightarrow> \<exists>x y. u \<cdot> (?a2 \<cdot> ?b2) = x \<cdot> y \<and> x \<in> \<aa> \<and> y \<in> \<bb>
?a \<in> ?H \<Longrightarrow> ?a \<in> additive.generate ?H
x \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
u \<in> R

goal (1 subgoal):
 1. u \<cdot> x \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
u \<cdot> x \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
case (inv u v)
[PROOF STATE]
proof (state)
this:
u \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
v \<in> R

goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}; aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (- a) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
 2. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
v \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
u \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
v \<in> R

goal (1 subgoal):
 1. v \<cdot> (- u) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>v \<in> R; a \<cdot> b \<in> R; u = a \<cdot> b; a \<in> \<aa>; b \<in> \<bb>\<rbrakk> \<Longrightarrow> v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>v \<in> R; a \<cdot> b \<in> R; u = a \<cdot> b; a \<in> \<aa>; b \<in> \<bb>\<rbrakk> \<Longrightarrow> v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
assume "v \<in> R" "a \<cdot> b \<in> R" "a \<in> \<aa>" "b \<in> \<bb>"
[PROOF STATE]
proof (state)
this:
v \<in> R
a \<cdot> b \<in> R
a \<in> \<aa>
b \<in> \<bb>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>v \<in> R; a \<cdot> b \<in> R; u = a \<cdot> b; a \<in> \<aa>; b \<in> \<bb>\<rbrakk> \<Longrightarrow> v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> R
a \<cdot> b \<in> R
a \<in> \<aa>
b \<in> \<bb>
[PROOF STEP]
have "v \<cdot> (- a \<cdot> b) = v \<cdot> a \<cdot> (- b) \<and> v \<cdot> a \<in> \<aa> \<and> - b \<in> \<bb>"
[PROOF STATE]
proof (prove)
using this:
v \<in> R
a \<cdot> b \<in> R
a \<in> \<aa>
b \<in> \<bb>

goal (1 subgoal):
 1. v \<cdot> (- a \<cdot> b) = v \<cdot> a \<cdot> (- b) \<and> v \<cdot> a \<in> \<aa> \<and> - b \<in> \<bb>
[PROOF STEP]
by (metis \<aa> \<bb> ideal.ideal(1) ideal_implies_subset ideal_inverse in_mono local.right_minus multiplicative.associative)
[PROOF STATE]
proof (state)
this:
v \<cdot> (- a \<cdot> b) = v \<cdot> a \<cdot> (- b) \<and> v \<cdot> a \<in> \<aa> \<and> - b \<in> \<bb>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>v \<in> R; a \<cdot> b \<in> R; u = a \<cdot> b; a \<in> \<aa>; b \<in> \<bb>\<rbrakk> \<Longrightarrow> v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<cdot> (- a \<cdot> b) = v \<cdot> a \<cdot> (- b) \<and> v \<cdot> a \<in> \<aa> \<and> - b \<in> \<bb>
[PROOF STEP]
show "v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})"
[PROOF STATE]
proof (prove)
using this:
v \<cdot> (- a \<cdot> b) = v \<cdot> a \<cdot> (- b) \<and> v \<cdot> a \<in> \<aa> \<and> - b \<in> \<bb>

goal (1 subgoal):
 1. v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
using \<aa> \<bb> additive.subgroup_generated_def ideal_mult_in_subgroup_generated
[PROOF STATE]
proof (prove)
using this:
v \<cdot> (- a \<cdot> b) = v \<cdot> a \<cdot> (- b) \<and> v \<cdot> a \<in> \<aa> \<and> - b \<in> \<bb>
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
additive.subgroup_generated ?S = additive.generate (R \<inter> ?S)
\<lbrakk>ideal ?\<aa> R (+) (\<cdot>) \<zero> \<one>; ideal ?\<bb> R (+) (\<cdot>) \<zero> \<one>; ?a \<in> ?\<aa>; ?b \<in> ?\<bb>\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> ideal_gen_by_prod ?\<aa> ?\<bb>

goal (1 subgoal):
 1. v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
unfolding ideal_gen_by_prod_def
[PROOF STATE]
proof (prove)
using this:
v \<cdot> (- a \<cdot> b) = v \<cdot> a \<cdot> (- b) \<and> v \<cdot> a \<in> \<aa> \<and> - b \<in> \<bb>
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
additive.subgroup_generated ?S = additive.generate (R \<inter> ?S)
\<lbrakk>ideal ?\<aa> R (+) (\<cdot>) \<zero> \<one>; ideal ?\<bb> R (+) (\<cdot>) \<zero> \<one>; ?a \<in> ?\<aa>; ?b \<in> ?\<bb>\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> additive.subgroup_generated {a \<cdot> b |a b. a \<in> ?\<aa> \<and> b \<in> ?\<bb>}

goal (1 subgoal):
 1. v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
v \<cdot> (- a \<cdot> b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<cdot> (- u) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
case (mult u v)
[PROOF STATE]
proof (state)
this:
u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> R

goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>aa. aa \<in> R \<Longrightarrow> aa \<cdot> a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); \<And>a. a \<in> R \<Longrightarrow> a \<cdot> b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); aa \<in> R\<rbrakk> \<Longrightarrow> aa \<cdot> (a + b) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> R

goal (1 subgoal):
 1. a \<cdot> (u + v) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
using additive.generate.mult additive.generate_into_G distributive(1)
[PROOF STATE]
proof (prove)
using this:
u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
?a2 \<in> R \<Longrightarrow> ?a2 \<cdot> v \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> R
\<lbrakk>?a \<in> additive.generate ?H; ?b \<in> additive.generate ?H\<rbrakk> \<Longrightarrow> ?a + ?b \<in> additive.generate ?H
?a \<in> additive.generate (R \<inter> ?H) \<Longrightarrow> ?a \<in> R
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c

goal (1 subgoal):
 1. a \<cdot> (u + v) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a \<cdot> (u + v) \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal:
No subgoals!
[PROOF STEP]
qed