[STATEMENT]
lemma a_distrib1: "ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have f1: "\<And>a. ad (ad (ad (a::'a)) \<cdot> ad (ad a)) = ad a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad (ad (ad a) \<cdot> ad (ad a)) = ad a
[PROOF STEP]
using a_add_idem am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. \<And>a. ad (ad (ad a) \<cdot> ad (ad a)) = ad a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a) \<cdot> ad (ad ?a)) = ad ?a

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have f2: "\<And>a aa. ad ((a::'a) \<cdot> aa) \<cdot> (a \<cdot> ad aa) = ad (a \<cdot> aa) \<cdot> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. ad (a \<cdot> aa) \<cdot> (a \<cdot> ad aa) = ad (a \<cdot> aa) \<cdot> a
[PROOF STEP]
using local.am5 mult_assoc
[PROOF STATE]
proof (prove)
using this:
ad (?x \<cdot> ?y) \<cdot> ?x \<cdot> ad ?y = ad (?x \<cdot> ?y) \<cdot> ?x
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. \<And>a aa. ad (a \<cdot> aa) \<cdot> (a \<cdot> ad aa) = ad (a \<cdot> aa) \<cdot> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (?a \<cdot> ?aa) \<cdot> (?a \<cdot> ad ?aa) = ad (?a \<cdot> ?aa) \<cdot> ?a

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have f3: "\<And>a. ad (ad (ad (a::'a))) = ad a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a) \<cdot> ad (ad ?a)) = ad ?a

goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a)) = ad ?a

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have "\<And>a. ad (a::'a) \<cdot> ad a = ad a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad a \<cdot> ad a = ad a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad ?a \<cdot> ad ?a = ad ?a

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad ?a \<cdot> ad ?a = ad ?a
[PROOF STEP]
have "\<And>a aa. ad (ad (ad (a::'a) \<cdot> ad aa)) = ad aa \<cdot> ad a"
[PROOF STATE]
proof (prove)
using this:
ad ?a \<cdot> ad ?a = ad ?a

goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a \<cdot> ad aa)) = ad aa \<cdot> ad a
[PROOF STEP]
using f3 f2
[PROOF STATE]
proof (prove)
using this:
ad ?a \<cdot> ad ?a = ad ?a
ad (ad (ad ?a)) = ad ?a
ad (?a \<cdot> ?aa) \<cdot> (?a \<cdot> ad ?aa) = ad (?a \<cdot> ?aa) \<cdot> ?a

goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a \<cdot> ad aa)) = ad aa \<cdot> ad a
[PROOF STEP]
by (metis (no_types) local.am2 local.am4 mult_assoc)
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?aa \<cdot> ad ?a

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?aa \<cdot> ad ?a
[PROOF STEP]
have  "ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y"
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?aa \<cdot> ad ?a

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y
[PROOF STEP]
using am_add_op_def am_d_def local.am2 local.am4
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?aa \<cdot> ad ?a
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)
d ?x = ad (ad ?x)
ad ?x \<cdot> ad ?y = ad ?y \<cdot> ad ?x
ad (?x \<cdot> ?y) \<cdot> ad (?x \<cdot> ad ?y) = ad ?x

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have "... = ad x \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y
[PROOF STEP]
by (simp add: mult_assoc)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> (ad y \<oplus> ad z) \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have "... = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y
[PROOF STEP]
by (simp add: mult_assoc)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y \<oplus> ad x \<cdot> (ad y \<oplus> ad z) \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have "... = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad y \<cdot> ad z \<oplus> ad x \<cdot> ad z \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad y \<cdot> ad z \<oplus> ad x \<cdot> ad z \<cdot> d y
[PROOF STEP]
by (metis a_add_idem a_mult_idem local.am4 mult_assoc am_add_op_def)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad y \<cdot> ad z \<oplus> ad x \<cdot> ad z \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad y \<cdot> ad z \<oplus> ad x \<cdot> ad z \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
have "... = ad x \<cdot> ad y \<oplus> (ad x \<cdot> ad z \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<oplus> ad x \<cdot> ad y \<cdot> ad z \<oplus> ad x \<cdot> ad z \<cdot> d y = ad x \<cdot> ad y \<oplus> (ad x \<cdot> ad z \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y)
[PROOF STEP]
by (metis am2 mult_assoc a_add_assoc)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y \<oplus> ad x \<cdot> ad y \<cdot> ad z \<oplus> ad x \<cdot> ad z \<cdot> d y = ad x \<cdot> ad y \<oplus> (ad x \<cdot> ad z \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y)

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> (ad x \<cdot> ad z \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> (ad x \<cdot> ad z \<cdot> ad y \<oplus> ad x \<cdot> ad z \<cdot> d y)

goal (1 subgoal):
 1. ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z
[PROOF STEP]
by (metis a_add_idem a_mult_idem am4 am_d_def am_add_op_def)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> (ad y \<oplus> ad z) = ad x \<cdot> ad y \<oplus> ad x \<cdot> ad z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_distrib2: "ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)
[PROOF STEP]
have f1: "\<And>a aa ab. ad (ad (ad (a::'a) \<cdot> ad aa) \<cdot> ad (ad a \<cdot> ad ab)) = ad a \<cdot> ad (ad (ad aa) \<cdot> ad (ad ab))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab. ad (ad (ad a \<cdot> ad aa) \<cdot> ad (ad a \<cdot> ad ab)) = ad a \<cdot> ad (ad (ad aa) \<cdot> ad (ad ab))
[PROOF STEP]
using a_distrib1 am_add_op_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<cdot> (ad ?y \<oplus> ad ?z) = ad ?x \<cdot> ad ?y \<oplus> ad ?x \<cdot> ad ?z
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. \<And>a aa ab. ad (ad (ad a \<cdot> ad aa) \<cdot> ad (ad a \<cdot> ad ab)) = ad a \<cdot> ad (ad (ad aa) \<cdot> ad (ad ab))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a \<cdot> ad ?aa) \<cdot> ad (ad ?a \<cdot> ad ?ab)) = ad ?a \<cdot> ad (ad (ad ?aa) \<cdot> ad (ad ?ab))

goal (1 subgoal):
 1. ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)
[PROOF STEP]
have "\<And>a. ad (ad (ad (a::'a))) = ad a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
by (metis a_absorb2 a_mult_idem am_add_op_def)
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a)) = ad ?a

goal (1 subgoal):
 1. ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad (ad ?a)) = ad ?a
[PROOF STEP]
have "ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad (ad x) \<cdot> ad (ad z)) = ad (ad (ad x) \<cdot> ad (ad y \<cdot> ad z))"
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a)) = ad ?a

goal (1 subgoal):
 1. ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad (ad x) \<cdot> ad (ad z)) = ad (ad (ad x) \<cdot> ad (ad y \<cdot> ad z))
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a)) = ad ?a
ad (ad (ad ?a \<cdot> ad ?aa) \<cdot> ad (ad ?a \<cdot> ad ?ab)) = ad ?a \<cdot> ad (ad (ad ?aa) \<cdot> ad (ad ?ab))

goal (1 subgoal):
 1. ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad (ad x) \<cdot> ad (ad z)) = ad (ad (ad x) \<cdot> ad (ad y \<cdot> ad z))
[PROOF STEP]
by (metis (full_types))
[PROOF STATE]
proof (state)
this:
ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad (ad x) \<cdot> ad (ad z)) = ad (ad (ad x) \<cdot> ad (ad y \<cdot> ad z))

goal (1 subgoal):
 1. ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad (ad x) \<cdot> ad (ad z)) = ad (ad (ad x) \<cdot> ad (ad y \<cdot> ad z))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad x) \<cdot> ad (ad y)) \<cdot> ad (ad (ad x) \<cdot> ad (ad z)) = ad (ad (ad x) \<cdot> ad (ad y \<cdot> ad z))

goal (1 subgoal):
 1. ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)
[PROOF STEP]
by (simp add: am_add_op_def)
[PROOF STATE]
proof (state)
this:
ad x \<oplus> ad y \<cdot> ad z = (ad x \<oplus> ad y) \<cdot> (ad x \<oplus> ad z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aa_loc [simp]: "d (x \<cdot> d y) = d (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (x \<cdot> d y) = d (x \<cdot> y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (x \<cdot> d y) = d (x \<cdot> y)
[PROOF STEP]
have f1: "x \<cdot> d y \<cdot> y = x \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> d y \<cdot> y = x \<cdot> y
[PROOF STEP]
by (metis am3 mult_assoc am_d_def)
[PROOF STATE]
proof (state)
this:
x \<cdot> d y \<cdot> y = x \<cdot> y

goal (1 subgoal):
 1. d (x \<cdot> d y) = d (x \<cdot> y)
[PROOF STEP]
have f2: "\<And>w z. ad (w \<cdot> z) \<cdot> (w \<cdot> ad z) = ad (w \<cdot> z) \<cdot> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w z. ad (w \<cdot> z) \<cdot> (w \<cdot> ad z) = ad (w \<cdot> z) \<cdot> w
[PROOF STEP]
by (metis am5 mult_assoc)
[PROOF STATE]
proof (state)
this:
ad (?w \<cdot> ?z) \<cdot> (?w \<cdot> ad ?z) = ad (?w \<cdot> ?z) \<cdot> ?w

goal (1 subgoal):
 1. d (x \<cdot> d y) = d (x \<cdot> y)
[PROOF STEP]
hence f3: "\<And>z. ad (x \<cdot> y) \<cdot> (x \<cdot> z) = ad (x \<cdot> y) \<cdot> (x \<cdot> (ad (ad (ad y) \<cdot> y) \<cdot> z))"
[PROOF STATE]
proof (prove)
using this:
ad (?w \<cdot> ?z) \<cdot> (?w \<cdot> ad ?z) = ad (?w \<cdot> ?z) \<cdot> ?w

goal (1 subgoal):
 1. \<And>z. ad (x \<cdot> y) \<cdot> (x \<cdot> z) = ad (x \<cdot> y) \<cdot> (x \<cdot> (ad (ad (ad y) \<cdot> y) \<cdot> z))
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
ad (?w \<cdot> ?z) \<cdot> (?w \<cdot> ad ?z) = ad (?w \<cdot> ?z) \<cdot> ?w
x \<cdot> d y \<cdot> y = x \<cdot> y

goal (1 subgoal):
 1. \<And>z. ad (x \<cdot> y) \<cdot> (x \<cdot> z) = ad (x \<cdot> y) \<cdot> (x \<cdot> (ad (ad (ad y) \<cdot> y) \<cdot> z))
[PROOF STEP]
by (metis (no_types) mult_assoc am_d_def)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> (x \<cdot> ?z) = ad (x \<cdot> y) \<cdot> (x \<cdot> (ad (ad (ad y) \<cdot> y) \<cdot> ?z))

goal (1 subgoal):
 1. d (x \<cdot> d y) = d (x \<cdot> y)
[PROOF STEP]
have "ad (x \<cdot> ad (ad y)) \<cdot> (x \<cdot> y) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> ad (ad y)) \<cdot> (x \<cdot> y) = 0
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
x \<cdot> d y \<cdot> y = x \<cdot> y

goal (1 subgoal):
 1. ad (x \<cdot> ad (ad y)) \<cdot> (x \<cdot> y) = 0
[PROOF STEP]
by (metis am1 mult_assoc n_annil a_zero_def am_d_def)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> ad (ad y)) \<cdot> (x \<cdot> y) = 0

goal (1 subgoal):
 1. d (x \<cdot> d y) = d (x \<cdot> y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (x \<cdot> ad (ad y)) \<cdot> (x \<cdot> y) = 0

goal (1 subgoal):
 1. d (x \<cdot> d y) = d (x \<cdot> y)
[PROOF STEP]
by (metis a_d_zero am_d_def f3 local.am1 local.am2 local.am3 local.am4)
[PROOF STATE]
proof (state)
this:
d (x \<cdot> d y) = d (x \<cdot> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_loc [simp]: "ad (x \<cdot> d y) = ad (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> d y) = ad (x \<cdot> y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad (x \<cdot> d y) = ad (x \<cdot> y)
[PROOF STEP]
have "\<And>a. ad (ad (ad (a::'a))) = ad a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
using am_add_op_def am_d_def prod_split
[PROOF STATE]
proof (prove)
using this:
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)
d ?x = ad (ad ?x)
ad ?x \<cdot> ad ?y \<oplus> ad ?x \<cdot> d ?y = ad ?x

goal (1 subgoal):
 1. \<And>a. ad (ad (ad a)) = ad a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a)) = ad ?a

goal (1 subgoal):
 1. ad (x \<cdot> d y) = ad (x \<cdot> y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad (ad ?a)) = ad ?a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a)) = ad ?a

goal (1 subgoal):
 1. ad (x \<cdot> d y) = ad (x \<cdot> y)
[PROOF STEP]
by (metis (full_types) aa_loc am_d_def)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> d y) = ad (x \<cdot> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d_a_export [simp]: "d (ad x \<cdot> y) = ad x \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x \<cdot> y) = ad x \<cdot> d y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (ad x \<cdot> y) = ad x \<cdot> d y
[PROOF STEP]
have f1: "\<And>a aa. ad ((a::'a) \<cdot> ad (ad aa)) = ad (a \<cdot> aa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. ad (a \<cdot> ad (ad aa)) = ad (a \<cdot> aa)
[PROOF STEP]
using a_loc am_d_def
[PROOF STATE]
proof (prove)
using this:
ad (?x \<cdot> d ?y) = ad (?x \<cdot> ?y)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. \<And>a aa. ad (a \<cdot> ad (ad aa)) = ad (a \<cdot> aa)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (?a \<cdot> ad (ad ?aa)) = ad (?a \<cdot> ?aa)

goal (1 subgoal):
 1. d (ad x \<cdot> y) = ad x \<cdot> d y
[PROOF STEP]
have "\<And>a. ad (ad (a::'a) \<cdot> a) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ad (ad a \<cdot> a) = (1::'a)
[PROOF STEP]
using a_d_one am_add_op_def am_d_def
[PROOF STATE]
proof (prove)
using this:
d ?x \<oplus> ad ?x = (1::'a)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. \<And>a. ad (ad a \<cdot> a) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (ad ?a \<cdot> ?a) = (1::'a)

goal (1 subgoal):
 1. d (ad x \<cdot> y) = ad x \<cdot> d y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad ?a \<cdot> ?a) = (1::'a)
[PROOF STEP]
have "\<And>a aa. ad (ad (ad (a::'a) \<cdot> ad aa)) = ad a \<cdot> ad aa"
[PROOF STATE]
proof (prove)
using this:
ad (ad ?a \<cdot> ?a) = (1::'a)

goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a \<cdot> ad aa)) = ad a \<cdot> ad aa
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
ad (ad ?a \<cdot> ?a) = (1::'a)
ad (?a \<cdot> ad (ad ?aa)) = ad (?a \<cdot> ?aa)

goal (1 subgoal):
 1. \<And>a aa. ad (ad (ad a \<cdot> ad aa)) = ad a \<cdot> ad aa
[PROOF STEP]
by (metis a_distrib2 am_add_op_def local.mult_1_left)
[PROOF STATE]
proof (state)
this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?a \<cdot> ad ?aa

goal (1 subgoal):
 1. d (ad x \<cdot> y) = ad x \<cdot> d y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?a \<cdot> ad ?aa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?a \<cdot> ad ?aa

goal (1 subgoal):
 1. d (ad x \<cdot> y) = ad x \<cdot> d y
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
ad (ad (ad ?a \<cdot> ad ?aa)) = ad ?a \<cdot> ad ?aa
ad (?a \<cdot> ad (ad ?aa)) = ad (?a \<cdot> ?aa)

goal (1 subgoal):
 1. d (ad x \<cdot> y) = ad x \<cdot> d y
[PROOF STEP]
by (metis (no_types) am_d_def)
[PROOF STATE]
proof (state)
this:
d (ad x \<cdot> y) = ad x \<cdot> d y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ds_ord_iso1: "x \<sqsubseteq> y \<Longrightarrow> z \<cdot> x \<sqsubseteq> z \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> y \<Longrightarrow> z \<cdot> x \<sqsubseteq> z \<cdot> y
[PROOF STEP]
(*nitpick [expect=genuine]*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> y \<Longrightarrow> z \<cdot> x \<sqsubseteq> z \<cdot> y
[PROOF STEP]
oops


[STATEMENT]
lemma a_very_costrict: "ad x = 1 \<longleftrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x = (1::'a)) = (x = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ad x = (1::'a) \<Longrightarrow> x = 0
 2. x = 0 \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
assume a: "ad x = 1"
[PROOF STATE]
proof (state)
this:
ad x = (1::'a)

goal (2 subgoals):
 1. ad x = (1::'a) \<Longrightarrow> x = 0
 2. x = 0 \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
hence "0 = ad x \<cdot> x"
[PROOF STATE]
proof (prove)
using this:
ad x = (1::'a)

goal (1 subgoal):
 1. 0 = ad x \<cdot> x
[PROOF STEP]
using a_zero_def
[PROOF STATE]
proof (prove)
using this:
ad x = (1::'a)
0 = ad (1::'a)

goal (1 subgoal):
 1. 0 = ad x \<cdot> x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 = ad x \<cdot> x

goal (2 subgoals):
 1. ad x = (1::'a) \<Longrightarrow> x = 0
 2. x = 0 \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
thus "x = 0"
[PROOF STATE]
proof (prove)
using this:
0 = ad x \<cdot> x

goal (1 subgoal):
 1. x = 0
[PROOF STEP]
by (simp add: a)
[PROOF STATE]
proof (state)
this:
x = 0

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = 0 \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
assume "x = 0"
[PROOF STATE]
proof (state)
this:
x = 0

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
thus "ad x = 1"
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. ad x = (1::'a)
[PROOF STEP]
using a_zero_def am_d_def dm.dom_one
[PROOF STATE]
proof (prove)
using this:
x = 0
0 = ad (1::'a)
d ?x = ad (ad ?x)
d (1::'a) = (1::'a)

goal (1 subgoal):
 1. ad x = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad x = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_weak_loc: "x \<cdot> y = 0 \<longleftrightarrow> x \<cdot> d y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> y = 0) = (x \<cdot> d y = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<cdot> y = 0) = (x \<cdot> d y = 0)
[PROOF STEP]
have "x \<cdot> y = 0 \<longleftrightarrow> ad (x \<cdot> y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> y = 0) = (ad (x \<cdot> y) = (1::'a))
[PROOF STEP]
by (simp add: a_very_costrict)
[PROOF STATE]
proof (state)
this:
(x \<cdot> y = 0) = (ad (x \<cdot> y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = 0) = (x \<cdot> d y = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<cdot> y = 0) = (ad (x \<cdot> y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = 0) = (x \<cdot> d y = 0)
[PROOF STEP]
have "... \<longleftrightarrow> ad (x \<cdot> d y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad (x \<cdot> y) = (1::'a)) = (ad (x \<cdot> d y) = (1::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ad (x \<cdot> y) = (1::'a)) = (ad (x \<cdot> d y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = 0) = (x \<cdot> d y = 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x \<cdot> y = 0) = (ad (x \<cdot> d y) = (1::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x \<cdot> y = 0) = (ad (x \<cdot> d y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = 0) = (x \<cdot> d y = 0)
[PROOF STEP]
using a_very_costrict
[PROOF STATE]
proof (prove)
using this:
(x \<cdot> y = 0) = (ad (x \<cdot> d y) = (1::'a))
(ad ?x = (1::'a)) = (?x = 0)

goal (1 subgoal):
 1. (x \<cdot> y = 0) = (x \<cdot> d y = 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x \<cdot> y = 0) = (x \<cdot> d y = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_closure [simp]: "d (ad x) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
using a_add_idem am_add_op_def am_d_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<oplus> ad ?x = ad ?x
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
by auto


[STATEMENT]
lemma a_d_mult_closure [simp]: "d (ad x \<cdot> ad y) = ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x \<cdot> ad y) = ad x \<cdot> ad y
[PROOF STEP]
by simp


[STATEMENT]
lemma kat_3': "d x \<cdot> y \<cdot> ad z = 0 \<Longrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> y \<cdot> ad z = 0 \<Longrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z
[PROOF STEP]
by (metis dm.dom_one local.am5 local.mult_1_left a_zero_def am_d_def)


[STATEMENT]
lemma s4 [simp]: "ad x \<cdot> ad (ad x \<cdot> y) = ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad (ad x \<cdot> y) = ad x \<cdot> ad y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> ad (ad x \<cdot> y) = ad x \<cdot> ad y
[PROOF STEP]
have "\<And>a aa. ad (a::'a) \<cdot> ad (ad aa) = ad (ad (ad a \<cdot> aa))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. ad a \<cdot> ad (ad aa) = ad (ad (ad a \<cdot> aa))
[PROOF STEP]
using am_d_def d_a_export
[PROOF STATE]
proof (prove)
using this:
d ?x = ad (ad ?x)
d (ad ?x \<cdot> ?y) = ad ?x \<cdot> d ?y

goal (1 subgoal):
 1. \<And>a aa. ad a \<cdot> ad (ad aa) = ad (ad (ad a \<cdot> aa))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad ?a \<cdot> ad (ad ?aa) = ad (ad (ad ?a \<cdot> ?aa))

goal (1 subgoal):
 1. ad x \<cdot> ad (ad x \<cdot> y) = ad x \<cdot> ad y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad ?a \<cdot> ad (ad ?aa) = ad (ad (ad ?a \<cdot> ?aa))
[PROOF STEP]
have "\<And>a aa. ad (ad (a::'a)) \<cdot> ad aa = ad (ad (ad aa \<cdot> a))"
[PROOF STATE]
proof (prove)
using this:
ad ?a \<cdot> ad (ad ?aa) = ad (ad (ad ?a \<cdot> ?aa))

goal (1 subgoal):
 1. \<And>a aa. ad (ad a) \<cdot> ad aa = ad (ad (ad aa \<cdot> a))
[PROOF STEP]
using local.am2
[PROOF STATE]
proof (prove)
using this:
ad ?a \<cdot> ad (ad ?aa) = ad (ad (ad ?a \<cdot> ?aa))
ad ?x \<cdot> ad ?y = ad ?y \<cdot> ad ?x

goal (1 subgoal):
 1. \<And>a aa. ad (ad a) \<cdot> ad aa = ad (ad (ad aa \<cdot> a))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad (ad ?a) \<cdot> ad ?aa = ad (ad (ad ?aa \<cdot> ?a))

goal (1 subgoal):
 1. ad x \<cdot> ad (ad x \<cdot> y) = ad x \<cdot> ad y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad ?a) \<cdot> ad ?aa = ad (ad (ad ?aa \<cdot> ?a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad ?a) \<cdot> ad ?aa = ad (ad (ad ?aa \<cdot> ?a))

goal (1 subgoal):
 1. ad x \<cdot> ad (ad x \<cdot> y) = ad x \<cdot> ad y
[PROOF STEP]
by (metis a_comp_simp a_d_mult_closure am_add_op_def am_d_def local.am2)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad (ad x \<cdot> y) = ad x \<cdot> ad y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kat_3_equiv: "d x \<cdot> y \<cdot> ad z = 0 \<longleftrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<cdot> y \<cdot> ad z = 0) = (d x \<cdot> y = d x \<cdot> y \<cdot> d z)
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d x \<cdot> y \<cdot> ad z = 0 \<Longrightarrow> d x \<cdot> y = d x \<cdot> y \<cdot> d z
 2. d x \<cdot> y = d x \<cdot> y \<cdot> d z \<Longrightarrow> d x \<cdot> y \<cdot> ad z = 0
[PROOF STEP]
apply (metis kat_3')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> y = d x \<cdot> y \<cdot> d z \<Longrightarrow> d x \<cdot> y \<cdot> ad z = 0
[PROOF STEP]
by (simp add: mult_assoc a_zero_def am_d_def)


[STATEMENT]
lemma a_a_one [simp]: "d 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (1::'a) = (1::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (1::'a) = (1::'a)
[PROOF STEP]
have "d 1 = d 1 + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (1::'a) = d (1::'a) + (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d (1::'a) = d (1::'a) + (0::'a)

goal (1 subgoal):
 1. d (1::'a) = (1::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (1::'a) = d (1::'a) + (0::'a)

goal (1 subgoal):
 1. d (1::'a) = (1::'a)
[PROOF STEP]
have "... = d 1 + ad 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (1::'a) + (0::'a) = d (1::'a) + ad (1::'a)
[PROOF STEP]
by (metis ans1 mult_1_right)
[PROOF STATE]
proof (state)
this:
d (1::'a) + (0::'a) = d (1::'a) + ad (1::'a)

goal (1 subgoal):
 1. d (1::'a) = (1::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d (1::'a) = d (1::'a) + ad (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d (1::'a) = d (1::'a) + ad (1::'a)

goal (1 subgoal):
 1. d (1::'a) = (1::'a)
[PROOF STEP]
by (simp add: ans_d_def)
[PROOF STATE]
proof (state)
this:
d (1::'a) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_very_costrict': "ad x = 1 \<longleftrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x = (1::'a)) = (x = (0::'a))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ad x = (1::'a) \<Longrightarrow> x = (0::'a)
 2. x = (0::'a) \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
assume "ad x = 1"
[PROOF STATE]
proof (state)
this:
ad x = (1::'a)

goal (2 subgoals):
 1. ad x = (1::'a) \<Longrightarrow> x = (0::'a)
 2. x = (0::'a) \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
hence "x = ad x \<cdot> x"
[PROOF STATE]
proof (prove)
using this:
ad x = (1::'a)

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

goal (2 subgoals):
 1. ad x = (1::'a) \<Longrightarrow> x = (0::'a)
 2. x = (0::'a) \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
thus "x = 0"
[PROOF STATE]
proof (prove)
using this:
x = ad x \<cdot> x

goal (1 subgoal):
 1. x = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (0::'a)

goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
assume "x = 0"
[PROOF STATE]
proof (state)
this:
x = (0::'a)

goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
hence "ad x = ad 0"
[PROOF STATE]
proof (prove)
using this:
x = (0::'a)

goal (1 subgoal):
 1. ad x = ad (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ad x = ad (0::'a)

goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> ad x = (1::'a)
[PROOF STEP]
thus "ad x = 1"
[PROOF STATE]
proof (prove)
using this:
ad x = ad (0::'a)

goal (1 subgoal):
 1. ad x = (1::'a)
[PROOF STEP]
by (metis a_a_one ans_d_def local.ans1 local.mult_1_right)
[PROOF STATE]
proof (state)
this:
ad x = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_idem [simp]: "1 + 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
have "1 + 1 = d 1 + d 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) + (1::'a) = d (1::'a) + d (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1::'a) + (1::'a) = d (1::'a) + d (1::'a)

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::'a) + (1::'a) = d (1::'a) + d (1::'a)

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
have "... = ad (ad 1 \<cdot> 1) + ad (ad 1 \<cdot> d 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (1::'a) + d (1::'a) = ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a))
[PROOF STEP]
using a_a_one ans_d_def
[PROOF STATE]
proof (prove)
using this:
d (1::'a) = (1::'a)
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. d (1::'a) + d (1::'a) = ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d (1::'a) + d (1::'a) = ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a))

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (1::'a) + d (1::'a) = ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a))

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
have "... = ad (ad 1 \<cdot> d 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a)) = ad (ad (1::'a) \<cdot> d (1::'a))
[PROOF STEP]
using ans_d_def local.ans2
[PROOF STATE]
proof (prove)
using this:
d ?x = ad (ad ?x)
ad (?x \<cdot> ?y) + ad (?x \<cdot> ad (ad ?y)) = ad (?x \<cdot> ad (ad ?y))

goal (1 subgoal):
 1. ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a)) = ad (ad (1::'a) \<cdot> d (1::'a))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a)) = ad (ad (1::'a) \<cdot> d (1::'a))

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad (ad (1::'a) \<cdot> (1::'a)) + ad (ad (1::'a) \<cdot> d (1::'a)) = ad (ad (1::'a) \<cdot> d (1::'a))

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
have "... = ad (ad 1 \<cdot> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad (1::'a) \<cdot> d (1::'a)) = ad (ad (1::'a) \<cdot> (1::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad (ad (1::'a) \<cdot> d (1::'a)) = ad (ad (1::'a) \<cdot> (1::'a))

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad (ad (1::'a) \<cdot> d (1::'a)) = ad (ad (1::'a) \<cdot> (1::'a))

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
have "... = d 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad (1::'a) \<cdot> (1::'a)) = d (1::'a)
[PROOF STEP]
by (simp add: ans_d_def)
[PROOF STATE]
proof (state)
this:
ad (ad (1::'a) \<cdot> (1::'a)) = d (1::'a)

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1::'a) + (1::'a) = d (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(1::'a) + (1::'a) = d (1::'a)

goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1::'a) + (1::'a) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d1_a [simp]: "d x \<cdot> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
have "x = (d x + ad x) \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (d x + ad x) \<cdot> x
[PROOF STEP]
by (simp add: ans_d_def)
[PROOF STATE]
proof (state)
this:
x = (d x + ad x) \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = (d x + ad x) \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
have "... = d x \<cdot> x + ad x \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x
[PROOF STEP]
using distrib_right'
[PROOF STATE]
proof (prove)
using this:
(?x + ?y) \<cdot> ?z = ?x \<cdot> ?z + ?y \<cdot> ?z

goal (1 subgoal):
 1. (d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
have "... = d x \<cdot> x + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> x + ad x \<cdot> x = d x \<cdot> x + (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d x \<cdot> x + ad x \<cdot> x = d x \<cdot> x + (0::'a)

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x = d x \<cdot> x + (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = d x \<cdot> x + (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_comm: "ad x \<cdot> ad y = ad y \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y = ad y \<cdot> ad x
[PROOF STEP]
using add_commute ans4
[PROOF STATE]
proof (prove)
using this:
?a + ?b = ?b + ?a
ad (?x + ?y) = ad ?x \<cdot> ad ?y

goal (1 subgoal):
 1. ad x \<cdot> ad y = ad y \<cdot> ad x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a_subid: "ad x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<le> (1::'a)
[PROOF STEP]
using local.ans3 local.join.sup_ge2
[PROOF STATE]
proof (prove)
using this:
ad (ad ?x) + ad ?x = (1::'a)
?y \<le> ?x + ?y

goal (1 subgoal):
 1. ad x \<le> (1::'a)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a_subid_aux1: "ad x \<cdot> y \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> y \<le> y
[PROOF STEP]
using a_subid mult_isor
[PROOF STATE]
proof (prove)
using this:
ad ?x \<le> (1::'a)
?x \<le> ?y \<Longrightarrow> ?x \<cdot> ?z \<le> ?y \<cdot> ?z

goal (1 subgoal):
 1. ad x \<cdot> y \<le> y
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a_subdist: "ad (x + y) \<le> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x + y) \<le> ad x
[PROOF STEP]
by (metis a_subid_aux1 ans4 add_comm)


[STATEMENT]
lemma a_antitone: "x \<le> y \<Longrightarrow> ad y \<le> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ad y \<le> ad x
[PROOF STEP]
using a_subdist local.order_prop
[PROOF STATE]
proof (prove)
using this:
ad (?x + ?y) \<le> ad ?x
(?x \<le> ?y) = (\<exists>z. ?x + z = ?y)

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ad y \<le> ad x
[PROOF STEP]
by auto


[STATEMENT]
lemma a_gla1: "ad x \<cdot> y = 0 \<Longrightarrow> ad x \<le> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
assume "ad x \<cdot> y = 0"
[PROOF STATE]
proof (state)
this:
ad x \<cdot> y = (0::'a)

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
hence a: "ad x \<cdot> d y = 0"
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> y = (0::'a)

goal (1 subgoal):
 1. ad x \<cdot> d y = (0::'a)
[PROOF STEP]
by (metis a_subid a_very_costrict' ans_d_def local.ans2 local.join.sup.order_iff)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> d y = (0::'a)

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
have "ad x = (d y + ad y ) \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x = (d y + ad y) \<cdot> ad x
[PROOF STEP]
by (simp add: ans_d_def)
[PROOF STATE]
proof (state)
this:
ad x = (d y + ad y) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x = (d y + ad y) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
have "... = d y \<cdot> ad x + ad y \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d y + ad y) \<cdot> ad x = d y \<cdot> ad x + ad y \<cdot> ad x
[PROOF STEP]
using distrib_right'
[PROOF STATE]
proof (prove)
using this:
(?x + ?y) \<cdot> ?z = ?x \<cdot> ?z + ?y \<cdot> ?z

goal (1 subgoal):
 1. (d y + ad y) \<cdot> ad x = d y \<cdot> ad x + ad y \<cdot> ad x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(d y + ad y) \<cdot> ad x = d y \<cdot> ad x + ad y \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(d y + ad y) \<cdot> ad x = d y \<cdot> ad x + ad y \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
have "... = ad x \<cdot> d y + ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d y \<cdot> ad x + ad y \<cdot> ad x = ad x \<cdot> d y + ad x \<cdot> ad y
[PROOF STEP]
using a_comm ans_d_def
[PROOF STATE]
proof (prove)
using this:
ad ?x \<cdot> ad ?y = ad ?y \<cdot> ad ?x
d ?x = ad (ad ?x)

goal (1 subgoal):
 1. d y \<cdot> ad x + ad y \<cdot> ad x = ad x \<cdot> d y + ad x \<cdot> ad y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d y \<cdot> ad x + ad y \<cdot> ad x = ad x \<cdot> d y + ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d y \<cdot> ad x + ad y \<cdot> ad x = ad x \<cdot> d y + ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
have "... = ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> d y + ad x \<cdot> ad y = ad x \<cdot> ad y
[PROOF STEP]
by (simp add: a)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> d y + ad x \<cdot> ad y = ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad x = ad x \<cdot> ad y
[PROOF STEP]
show "ad x \<le> ad y"
[PROOF STATE]
proof (prove)
using this:
ad x = ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<le> ad y
[PROOF STEP]
by (metis a_subid_aux1)
[PROOF STATE]
proof (state)
this:
ad x \<le> ad y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_gla2: "ad x \<le> ad y \<Longrightarrow> ad x \<cdot> y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<le> ad y \<Longrightarrow> ad x \<cdot> y = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<le> ad y \<Longrightarrow> ad x \<cdot> y = (0::'a)
[PROOF STEP]
assume "ad x \<le> ad y"
[PROOF STATE]
proof (state)
this:
ad x \<le> ad y

goal (1 subgoal):
 1. ad x \<le> ad y \<Longrightarrow> ad x \<cdot> y = (0::'a)
[PROOF STEP]
hence "ad x \<cdot> y \<le> ad y \<cdot> y"
[PROOF STATE]
proof (prove)
using this:
ad x \<le> ad y

goal (1 subgoal):
 1. ad x \<cdot> y \<le> ad y \<cdot> y
[PROOF STEP]
using mult_isor
[PROOF STATE]
proof (prove)
using this:
ad x \<le> ad y
?x \<le> ?y \<Longrightarrow> ?x \<cdot> ?z \<le> ?y \<cdot> ?z

goal (1 subgoal):
 1. ad x \<cdot> y \<le> ad y \<cdot> y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ad x \<cdot> y \<le> ad y \<cdot> y

goal (1 subgoal):
 1. ad x \<le> ad y \<Longrightarrow> ad x \<cdot> y = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> y \<le> ad y \<cdot> y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a)
[PROOF STEP]
by (simp add: join.le_bot)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> y = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a2_eq [simp]: "ad (x \<cdot> d y) = ad (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> d y) = ad (x \<cdot> y)
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
 2. ad (x \<cdot> y) \<le> ad (x \<cdot> d y)
[PROOF STEP]
show "ad (x \<cdot> y) \<le> ad (x \<cdot> d y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<le> ad (x \<cdot> d y)
[PROOF STEP]
by (simp add: ans_d_def local.less_eq_def)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<le> ad (x \<cdot> d y)

goal (1 subgoal):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
[PROOF STEP]
show "ad (x \<cdot> d y) \<le> ad (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
[PROOF STEP]
by (metis a_gla1 a_mul_d ans1 d1_a mult_assoc)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> d y) \<le> ad (x \<cdot> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_export' [simp]: "ad (ad x \<cdot> y) = d x + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> y) = d x + ad y
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
have "ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = (0::'a)
[PROOF STEP]
by (simp add: a_gla2 local.mult.semigroup_axioms semigroup.assoc)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = (0::'a)

goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
hence a: "ad (ad x \<cdot> y) \<cdot> d y \<le> ad (ad x)"
[PROOF STATE]
proof (prove)
using this:
ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = (0::'a)

goal (1 subgoal):
 1. ad (ad x \<cdot> y) \<cdot> d y \<le> ad (ad x)
[PROOF STEP]
by (metis a_comm a_gla1 ans4 mult_assoc ans_d_def)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) \<cdot> d y \<le> ad (ad x)

goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
have "ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y
[PROOF STEP]
by (metis (no_types) add_commute ans3 ans4 distrib_right' mult_onel ans_d_def)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y

goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
thus "ad (ad x \<cdot> y) \<le> d x + ad y"
[PROOF STATE]
proof (prove)
using this:
ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y

goal (1 subgoal):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
[PROOF STEP]
by (metis a_subid_aux1 a join.sup_mono ans_d_def)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) \<le> d x + ad y

goal (1 subgoal):
 1. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
show "d x + ad y \<le> ad (ad x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
by (metis a2_eq a_antitone a_comm a_subid_aux1 join.sup_least ans_d_def)
[PROOF STATE]
proof (state)
this:
d x + ad y \<le> ad (ad x \<cdot> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_idem [simp]: "ad x \<cdot> ad x = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
have "ad x = (d x + ad x ) \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x = (d x + ad x) \<cdot> ad x
[PROOF STEP]
by (simp add: ans_d_def)
[PROOF STATE]
proof (state)
this:
ad x = (d x + ad x) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x = (d x + ad x) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
have "... = d x \<cdot> ad x + ad x \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x + ad x) \<cdot> ad x = d x \<cdot> ad x + ad x \<cdot> ad x
[PROOF STEP]
using distrib_right'
[PROOF STATE]
proof (prove)
using this:
(?x + ?y) \<cdot> ?z = ?x \<cdot> ?z + ?y \<cdot> ?z

goal (1 subgoal):
 1. (d x + ad x) \<cdot> ad x = d x \<cdot> ad x + ad x \<cdot> ad x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> ad x = d x \<cdot> ad x + ad x \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad x = d x \<cdot> ad x + ad x \<cdot> ad x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad x = d x \<cdot> ad x + ad x \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad x = ad x
[PROOF STEP]
by (simp add: ans_d_def)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad x = ad x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_3_var [simp]: "ad x \<cdot> ad y \<cdot> (x + y) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<cdot> (x + y) = (0::'a)
[PROOF STEP]
by (metis ans1 ans4)


[STATEMENT]
lemma a_3 [simp]: "ad x \<cdot> ad y \<cdot> d (x + y) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<cdot> d (x + y) = (0::'a)
[PROOF STEP]
by (metis a_mul_d ans4)


[STATEMENT]
lemma a_closure' [simp]: "d (ad x) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
have "d (ad x) = ad (1 \<cdot> d x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x) = ad ((1::'a) \<cdot> d x)
[PROOF STEP]
by (simp add: ans_d_def)
[PROOF STATE]
proof (state)
this:
d (ad x) = ad ((1::'a) \<cdot> d x)

goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (ad x) = ad ((1::'a) \<cdot> d x)

goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
have "... = ad (1 \<cdot> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad ((1::'a) \<cdot> d x) = ad ((1::'a) \<cdot> x)
[PROOF STEP]
using a2_eq
[PROOF STATE]
proof (prove)
using this:
ad (?x \<cdot> d ?y) = ad (?x \<cdot> ?y)

goal (1 subgoal):
 1. ad ((1::'a) \<cdot> d x) = ad ((1::'a) \<cdot> x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ad ((1::'a) \<cdot> d x) = ad ((1::'a) \<cdot> x)

goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d (ad x) = ad ((1::'a) \<cdot> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d (ad x) = ad ((1::'a) \<cdot> x)

goal (1 subgoal):
 1. d (ad x) = ad x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d (ad x) = ad x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "x \<cdot> ad 1 = ad 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> ad (1::'a) = ad (1::'a)
[PROOF STEP]
(*nitpick [expect=genuine]*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> ad (1::'a) = ad (1::'a)
[PROOF STEP]
oops


[STATEMENT]
lemma "ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
(*nitpick [expect=genuine]*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
oops


[STATEMENT]
lemma phl_seq_inv: "d v \<cdot> x \<cdot> y \<cdot> ad w = 0 \<Longrightarrow> \<exists>z. d v \<cdot> x \<cdot> d z = 0 \<and> ad z \<cdot> y \<cdot> ad w = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d v \<cdot> x \<cdot> y \<cdot> ad w = (0::'a) \<Longrightarrow> \<exists>z. d v \<cdot> x \<cdot> d z = (0::'a) \<and> ad z \<cdot> y \<cdot> ad w = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d v \<cdot> x \<cdot> y \<cdot> ad w = (0::'a) \<Longrightarrow> \<exists>z. d v \<cdot> x \<cdot> d z = (0::'a) \<and> ad z \<cdot> y \<cdot> ad w = (0::'a)
[PROOF STEP]
assume "d v \<cdot> x \<cdot> y \<cdot> ad w = 0"
[PROOF STATE]
proof (state)
this:
d v \<cdot> x \<cdot> y \<cdot> ad w = (0::'a)

goal (1 subgoal):
 1. d v \<cdot> x \<cdot> y \<cdot> ad w = (0::'a) \<Longrightarrow> \<exists>z. d v \<cdot> x \<cdot> d z = (0::'a) \<and> ad z \<cdot> y \<cdot> ad w = (0::'a)
[PROOF STEP]
hence "d v \<cdot> x \<cdot> d (y \<cdot> ad w) = 0 \<and> ad (y \<cdot> ad w) \<cdot> y \<cdot> ad w = 0"
[PROOF STATE]
proof (prove)
using this:
d v \<cdot> x \<cdot> y \<cdot> ad w = (0::'a)

goal (1 subgoal):
 1. d v \<cdot> x \<cdot> d (y \<cdot> ad w) = (0::'a) \<and> ad (y \<cdot> ad w) \<cdot> y \<cdot> ad w = (0::'a)
[PROOF STEP]
by (metis dnsz.dom_weakly_local local.ans1 mult_assoc)
[PROOF STATE]
proof (state)
this:
d v \<cdot> x \<cdot> d (y \<cdot> ad w) = (0::'a) \<and> ad (y \<cdot> ad w) \<cdot> y \<cdot> ad w = (0::'a)

goal (1 subgoal):
 1. d v \<cdot> x \<cdot> y \<cdot> ad w = (0::'a) \<Longrightarrow> \<exists>z. d v \<cdot> x \<cdot> d z = (0::'a) \<and> ad z \<cdot> y \<cdot> ad w = (0::'a)
[PROOF STEP]
thus "\<exists>z. d v \<cdot> x \<cdot> d z = 0 \<and> ad z \<cdot> y \<cdot> ad w = 0"
[PROOF STATE]
proof (prove)
using this:
d v \<cdot> x \<cdot> d (y \<cdot> ad w) = (0::'a) \<and> ad (y \<cdot> ad w) \<cdot> y \<cdot> ad w = (0::'a)

goal (1 subgoal):
 1. \<exists>z. d v \<cdot> x \<cdot> d z = (0::'a) \<and> ad z \<cdot> y \<cdot> ad w = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>z. d v \<cdot> x \<cdot> d z = (0::'a) \<and> ad z \<cdot> y \<cdot> ad w = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_fixpoint: "ad x = x \<Longrightarrow> (\<forall>y. y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x = x \<Longrightarrow> \<forall>y. y = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x = x \<Longrightarrow> \<forall>y. y = (0::'a)
[PROOF STEP]
assume a1: "ad x = x"
[PROOF STATE]
proof (state)
this:
ad x = x

goal (1 subgoal):
 1. ad x = x \<Longrightarrow> \<forall>y. y = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ad x = x

goal (1 subgoal):
 1. ad x = x \<Longrightarrow> \<forall>y. y = (0::'a)
[PROOF STEP]
fix aa :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x = x \<Longrightarrow> \<forall>y. y = (0::'a)
[PROOF STEP]
have "aa = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aa = (0::'a)
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
ad x = x

goal (1 subgoal):
 1. aa = (0::'a)
[PROOF STEP]
by (metis (no_types) a_mul_d ans_d_def local.annil local.ans3 local.join.sup.idem local.mult_1_left)
[PROOF STATE]
proof (state)
this:
aa = (0::'a)

goal (1 subgoal):
 1. ad x = x \<Longrightarrow> \<forall>y. y = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?aa3 = (0::'a)

goal (1 subgoal):
 1. ad x = x \<Longrightarrow> \<forall>y. y = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?aa3 = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?aa3 = (0::'a)

goal (1 subgoal):
 1. \<forall>y. y = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>y. y = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_very_costrict'': "ad x = 1 \<longleftrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x = (1::'a)) = (x = (0::'a))
[PROOF STEP]
by (metis add_commute local.add_zerol order.antisym local.apd1 local.apd3 local.join.bot_least local.mult_1_right local.phl_skip)


[STATEMENT]
lemma a_subid': "ad x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<le> (1::'a)
[PROOF STEP]
using local.apd3 local.join.sup_ge2
[PROOF STATE]
proof (prove)
using this:
ad (ad ?x) + ad ?x = (1::'a)
?y \<le> ?x + ?y

goal (1 subgoal):
 1. ad x \<le> (1::'a)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma d1_a' [simp]: "d x \<cdot> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
have "x = (d x + ad x) \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (d x + ad x) \<cdot> x
[PROOF STEP]
by (simp add: apd_d_def)
[PROOF STATE]
proof (state)
this:
x = (d x + ad x) \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = (d x + ad x) \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
have "... = d x \<cdot> x + ad x \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x
[PROOF STEP]
using distrib_right'
[PROOF STATE]
proof (prove)
using this:
(?x + ?y) \<cdot> ?z = ?x \<cdot> ?z + ?y \<cdot> ?z

goal (1 subgoal):
 1. (d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> x = d x \<cdot> x + ad x \<cdot> x

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
have "... = d x \<cdot> x + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> x + ad x \<cdot> x = d x \<cdot> x + (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d x \<cdot> x + ad x \<cdot> x = d x \<cdot> x + (0::'a)

goal (1 subgoal):
 1. d x \<cdot> x = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x = d x \<cdot> x + (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = d x \<cdot> x + (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_subid_aux1': "ad x \<cdot> y \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> y \<le> y
[PROOF STEP]
using a_subid' mult_isor
[PROOF STATE]
proof (prove)
using this:
ad ?x \<le> (1::'a)
?x \<le> ?y \<Longrightarrow> ?x \<cdot> ?z \<le> ?y \<cdot> ?z

goal (1 subgoal):
 1. ad x \<cdot> y \<le> y
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a_mul_d' [simp]: "ad x \<cdot> d x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> d x = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> d x = (0::'a)
[PROOF STEP]
have "1 = ad (ad x \<cdot> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) = ad (ad x \<cdot> x)
[PROOF STEP]
using a_very_costrict''
[PROOF STATE]
proof (prove)
using this:
(ad ?x = (1::'a)) = (?x = (0::'a))

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

goal (1 subgoal):
 1. ad x \<cdot> d x = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(1::'a) = ad (ad x \<cdot> x)

goal (1 subgoal):
 1. ad x \<cdot> d x = (0::'a)
[PROOF STEP]
by (metis a_subid' a_very_costrict'' apd_d_def order.antisym local.apd2)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> d x = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma meet_ord_def: "ad x \<le> ad y \<longleftrightarrow> ad x \<cdot> ad y = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<le> ad y) = (ad x \<cdot> ad y = ad x)
[PROOF STEP]
by (metis a_d_closed a_subid_aux1' d1_a' order.eq_iff mult_1_right mult_isol)


[STATEMENT]
lemma d_weak_loc: "x \<cdot> y = 0 \<longleftrightarrow> x \<cdot> d y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> y = (0::'a)) = (x \<cdot> d y = (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<cdot> y = (0::'a)) = (x \<cdot> d y = (0::'a))
[PROOF STEP]
have "x \<cdot> y = 0 \<longleftrightarrow> ad (x \<cdot> y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> y = (0::'a)) = (ad (x \<cdot> y) = (1::'a))
[PROOF STEP]
by (simp add: a_very_costrict'')
[PROOF STATE]
proof (state)
this:
(x \<cdot> y = (0::'a)) = (ad (x \<cdot> y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = (0::'a)) = (x \<cdot> d y = (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<cdot> y = (0::'a)) = (ad (x \<cdot> y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = (0::'a)) = (x \<cdot> d y = (0::'a))
[PROOF STEP]
have "... \<longleftrightarrow> ad (x \<cdot> d y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad (x \<cdot> y) = (1::'a)) = (ad (x \<cdot> d y) = (1::'a))
[PROOF STEP]
by (metis apd1 apd2 a_subid' apd_d_def d1_a' order.eq_iff mult_1_left mult_assoc)
[PROOF STATE]
proof (state)
this:
(ad (x \<cdot> y) = (1::'a)) = (ad (x \<cdot> d y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = (0::'a)) = (x \<cdot> d y = (0::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x \<cdot> y = (0::'a)) = (ad (x \<cdot> d y) = (1::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x \<cdot> y = (0::'a)) = (ad (x \<cdot> d y) = (1::'a))

goal (1 subgoal):
 1. (x \<cdot> y = (0::'a)) = (x \<cdot> d y = (0::'a))
[PROOF STEP]
by (simp add: a_very_costrict'')
[PROOF STATE]
proof (state)
this:
(x \<cdot> y = (0::'a)) = (x \<cdot> d y = (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gla_1: "ad x \<cdot> y = 0 \<Longrightarrow> ad x \<le> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
assume "ad x \<cdot> y = 0"
[PROOF STATE]
proof (state)
this:
ad x \<cdot> y = (0::'a)

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
hence a: "ad x \<cdot> d y = 0"
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> y = (0::'a)

goal (1 subgoal):
 1. ad x \<cdot> d y = (0::'a)
[PROOF STEP]
using d_weak_loc
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> y = (0::'a)
(?x \<cdot> ?y = (0::'a)) = (?x \<cdot> d ?y = (0::'a))

goal (1 subgoal):
 1. ad x \<cdot> d y = (0::'a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ad x \<cdot> d y = (0::'a)

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
hence "d y = ad x \<cdot> d y + d y"
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> d y = (0::'a)

goal (1 subgoal):
 1. d y = ad x \<cdot> d y + d y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d y = ad x \<cdot> d y + d y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d y = ad x \<cdot> d y + d y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
have "... = (1 + ad x) \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> d y + d y = ((1::'a) + ad x) \<cdot> d y
[PROOF STEP]
using join.sup_commute
[PROOF STATE]
proof (prove)
using this:
?x + ?y = ?y + ?x

goal (1 subgoal):
 1. ad x \<cdot> d y + d y = ((1::'a) + ad x) \<cdot> d y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad x \<cdot> d y + d y = ((1::'a) + ad x) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> d y + d y = ((1::'a) + ad x) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
have "... = (d x + ad x) \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) + ad x) \<cdot> d y = (d x + ad x) \<cdot> d y
[PROOF STEP]
using apd_d_def calculation
[PROOF STATE]
proof (prove)
using this:
d ?x = ad (ad ?x)
d y = ((1::'a) + ad x) \<cdot> d y

goal (1 subgoal):
 1. ((1::'a) + ad x) \<cdot> d y = (d x + ad x) \<cdot> d y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((1::'a) + ad x) \<cdot> d y = (d x + ad x) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((1::'a) + ad x) \<cdot> d y = (d x + ad x) \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
have "... = d x \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x + ad x) \<cdot> d y = d x \<cdot> d y
[PROOF STEP]
by (simp add: a join.sup_commute)
[PROOF STATE]
proof (state)
this:
(d x + ad x) \<cdot> d y = d x \<cdot> d y

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d y = d x \<cdot> d y
[PROOF STEP]
have "d y \<le> d x"
[PROOF STATE]
proof (prove)
using this:
d y = d x \<cdot> d y

goal (1 subgoal):
 1. d y \<le> d x
[PROOF STEP]
by (metis apd_d_def a_subid' mult_1_right mult_isol)
[PROOF STATE]
proof (state)
this:
d y \<le> d x

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
hence "d y \<cdot> ad x = 0"
[PROOF STATE]
proof (prove)
using this:
d y \<le> d x

goal (1 subgoal):
 1. d y \<cdot> ad x = (0::'a)
[PROOF STEP]
by (metis apd_d_def a_d_closed a_mul_d' distrib_right' less_eq_def no_trivial_inverse)
[PROOF STATE]
proof (state)
this:
d y \<cdot> ad x = (0::'a)

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
hence "ad x = ad y \<cdot> ad x"
[PROOF STATE]
proof (prove)
using this:
d y \<cdot> ad x = (0::'a)

goal (1 subgoal):
 1. ad x = ad y \<cdot> ad x
[PROOF STEP]
by (metis apd_d_def apd3 add_0_left distrib_right' mult_1_left)
[PROOF STATE]
proof (state)
this:
ad x = ad y \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> y = (0::'a) \<Longrightarrow> ad x \<le> ad y
[PROOF STEP]
thus "ad x \<le> ad y"
[PROOF STATE]
proof (prove)
using this:
ad x = ad y \<cdot> ad x

goal (1 subgoal):
 1. ad x \<le> ad y
[PROOF STEP]
by (metis add_commute apd3 mult_oner subdistl)
[PROOF STATE]
proof (state)
this:
ad x \<le> ad y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a2_eq' [simp]: "ad (x \<cdot> d y) = ad (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> d y) = ad (x \<cdot> y)
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
 2. ad (x \<cdot> y) \<le> ad (x \<cdot> d y)
[PROOF STEP]
show "ad (x \<cdot> y) \<le> ad (x \<cdot> d y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<le> ad (x \<cdot> d y)
[PROOF STEP]
by (simp add: apd_d_def)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<le> ad (x \<cdot> d y)

goal (1 subgoal):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
[PROOF STEP]
show "ad (x \<cdot> d y) \<le> ad (x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> d y) \<le> ad (x \<cdot> y)
[PROOF STEP]
by (metis gla_1 apd1 a_mul_d' d1_a' mult_assoc)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> d y) \<le> ad (x \<cdot> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_supdist_var: "ad (x + y) \<le> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x + y) \<le> ad x
[PROOF STEP]
by (metis gla_1 apd1 join.le_bot subdistl)


[STATEMENT]
lemma a_antitone': "x \<le> y \<Longrightarrow> ad y \<le> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ad y \<le> ad x
[PROOF STEP]
using a_supdist_var local.order_prop
[PROOF STATE]
proof (prove)
using this:
ad (?x + ?y) \<le> ad ?x
(?x \<le> ?y) = (\<exists>z. ?x + z = ?y)

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ad y \<le> ad x
[PROOF STEP]
by auto


[STATEMENT]
lemma a_comm_var: "ad x \<cdot> ad y \<le> ad y \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
have "ad x \<cdot> ad y = d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y = d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y
[PROOF STEP]
by (simp add: mult_assoc)
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y = d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y = d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
have "... \<le> d (ad x \<cdot> ad y) \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y \<le> d (ad x \<cdot> ad y) \<cdot> ad x
[PROOF STEP]
using a_subid' mult_isol
[PROOF STATE]
proof (prove)
using this:
ad ?x \<le> (1::'a)
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y

goal (1 subgoal):
 1. d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y \<le> d (ad x \<cdot> ad y) \<cdot> ad x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y \<le> d (ad x \<cdot> ad y) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (ad x \<cdot> ad y) \<cdot> ad x \<cdot> ad y \<le> d (ad x \<cdot> ad y) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
have "... \<le> d (ad y) \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x \<cdot> ad y) \<cdot> ad x \<le> d (ad y) \<cdot> ad x
[PROOF STEP]
by (simp add: a_antitone' a_subid_aux1' apd_d_def local.mult_isor)
[PROOF STATE]
proof (state)
this:
d (ad x \<cdot> ad y) \<cdot> ad x \<le> d (ad y) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad x \<cdot> ad y \<le> d (ad y) \<cdot> ad x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> ad y \<le> d (ad y) \<cdot> ad x

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad y \<cdot> ad x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y \<le> ad y \<cdot> ad x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_comm': "ad x \<cdot> ad y = ad y \<cdot> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y = ad y \<cdot> ad x
[PROOF STEP]
by (simp add: a_comm_var order.eq_iff)


[STATEMENT]
lemma a_closed [simp]: "d (ad x \<cdot> ad y) = ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (ad x \<cdot> ad y) = ad x \<cdot> ad y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (ad x \<cdot> ad y) = ad x \<cdot> ad y
[PROOF STEP]
have f1: "\<And>x y. ad x \<le> ad (ad y \<cdot> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. ad x \<le> ad (ad y \<cdot> x)
[PROOF STEP]
by (simp add: a_antitone' a_subid_aux1')
[PROOF STATE]
proof (state)
this:
ad ?x1 \<le> ad (ad ?y1 \<cdot> ?x1)

goal (1 subgoal):
 1. d (ad x \<cdot> ad y) = ad x \<cdot> ad y
[PROOF STEP]
have "\<And>x y. d (ad x \<cdot> y) \<le> ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. d (ad x \<cdot> y) \<le> ad x
[PROOF STEP]
by (metis a2_eq' a_antitone' a_comm' a_d_closed apd_d_def f1)
[PROOF STATE]
proof (state)
this:
d (ad ?x1 \<cdot> ?y1) \<le> ad ?x1

goal (1 subgoal):
 1. d (ad x \<cdot> ad y) = ad x \<cdot> ad y
[PROOF STEP]
hence "\<And>x y. d (ad x \<cdot> y) \<cdot> y = ad x \<cdot> y"
[PROOF STATE]
proof (prove)
using this:
d (ad ?x1 \<cdot> ?y1) \<le> ad ?x1

goal (1 subgoal):
 1. \<And>x y. d (ad x \<cdot> y) \<cdot> y = ad x \<cdot> y
[PROOF STEP]
by (metis d1_a' meet_ord_def mult_assoc apd_d_def)
[PROOF STATE]
proof (state)
this:
d (ad ?x1 \<cdot> ?y1) \<cdot> ?y1 = ad ?x1 \<cdot> ?y1

goal (1 subgoal):
 1. d (ad x \<cdot> ad y) = ad x \<cdot> ad y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d (ad ?x1 \<cdot> ?y1) \<cdot> ?y1 = ad ?x1 \<cdot> ?y1

goal (1 subgoal):
 1. d (ad x \<cdot> ad y) = ad x \<cdot> ad y
[PROOF STEP]
by (metis f1 a_comm' apd_d_def meet_ord_def)
[PROOF STATE]
proof (state)
this:
d (ad x \<cdot> ad y) = ad x \<cdot> ad y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_export'' [simp]: "ad (ad x \<cdot> y) = d x + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> y) = d x + ad y
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
have "ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = (0::'a)
[PROOF STEP]
using d_weak_loc mult_assoc
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> ?y = (0::'a)) = (?x \<cdot> d ?y = (0::'a))
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = (0::'a)

goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
hence a: "ad (ad x \<cdot> y) \<cdot> d y \<le> d x"
[PROOF STATE]
proof (prove)
using this:
ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = (0::'a)

goal (1 subgoal):
 1. ad (ad x \<cdot> y) \<cdot> d y \<le> d x
[PROOF STEP]
by (metis a_closed a_comm' apd_d_def gla_1 mult_assoc)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) \<cdot> d y \<le> d x

goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
have "ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y
[PROOF STEP]
by (metis apd3 a_comm' d1_a' distrib_right' mult_1_right apd_d_def)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y

goal (2 subgoals):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
 2. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
thus "ad (ad x \<cdot> y) \<le> d x + ad y"
[PROOF STATE]
proof (prove)
using this:
ad (ad x \<cdot> y) = ad (ad x \<cdot> y) \<cdot> d y + ad (ad x \<cdot> y) \<cdot> ad y

goal (1 subgoal):
 1. ad (ad x \<cdot> y) \<le> d x + ad y
[PROOF STEP]
by (metis a_subid_aux1' a join.sup_mono)
[PROOF STATE]
proof (state)
this:
ad (ad x \<cdot> y) \<le> d x + ad y

goal (1 subgoal):
 1. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
have "ad y \<le> ad (ad x \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
by (simp add: a_antitone' a_subid_aux1')
[PROOF STATE]
proof (state)
this:
ad y \<le> ad (ad x \<cdot> y)

goal (1 subgoal):
 1. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
thus "d x + ad y \<le> ad (ad x \<cdot> y)"
[PROOF STATE]
proof (prove)
using this:
ad y \<le> ad (ad x \<cdot> y)

goal (1 subgoal):
 1. d x + ad y \<le> ad (ad x \<cdot> y)
[PROOF STEP]
by (metis apd_d_def a_mul_d' d1_a' gla_1 apd1 join.sup_least mult_assoc)
[PROOF STATE]
proof (state)
this:
d x + ad y \<le> ad (ad x \<cdot> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d1_sum_var: "x + y \<le> (d x + d y) \<cdot> (x + y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + y \<le> (d x + d y) \<cdot> (x + y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x + y \<le> (d x + d y) \<cdot> (x + y)
[PROOF STEP]
have "x + y = d x \<cdot> x + d y \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + y = d x \<cdot> x + d y \<cdot> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x + y = d x \<cdot> x + d y \<cdot> y

goal (1 subgoal):
 1. x + y \<le> (d x + d y) \<cdot> (x + y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x + y = d x \<cdot> x + d y \<cdot> y

goal (1 subgoal):
 1. x + y \<le> (d x + d y) \<cdot> (x + y)
[PROOF STEP]
have "... \<le> (d x + d y) \<cdot> x + (d x + d y) \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> x + d y \<cdot> y \<le> (d x + d y) \<cdot> x + (d x + d y) \<cdot> y
[PROOF STEP]
using local.distrib_right' local.join.sup_ge1 local.join.sup_ge2 local.join.sup_mono
[PROOF STATE]
proof (prove)
using this:
(?x + ?y) \<cdot> ?z = ?x \<cdot> ?z + ?y \<cdot> ?z
?x \<le> ?x + ?y
?y \<le> ?x + ?y
\<lbrakk>?a \<le> ?c; ?b \<le> ?d\<rbrakk> \<Longrightarrow> ?a + ?b \<le> ?c + ?d

goal (1 subgoal):
 1. d x \<cdot> x + d y \<cdot> y \<le> (d x + d y) \<cdot> x + (d x + d y) \<cdot> y
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
d x \<cdot> x + d y \<cdot> y \<le> (d x + d y) \<cdot> x + (d x + d y) \<cdot> y

goal (1 subgoal):
 1. x + y \<le> (d x + d y) \<cdot> (x + y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x + y \<le> (d x + d y) \<cdot> x + (d x + d y) \<cdot> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x + y \<le> (d x + d y) \<cdot> x + (d x + d y) \<cdot> y

goal (1 subgoal):
 1. x + y \<le> (d x + d y) \<cdot> (x + y)
[PROOF STEP]
using order_trans subdistl_var
[PROOF STATE]
proof (prove)
using this:
x + y \<le> (d x + d y) \<cdot> x + (d x + d y) \<cdot> y
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?z \<cdot> ?x + ?z \<cdot> ?y \<le> ?z \<cdot> (?x + ?y)

goal (1 subgoal):
 1. x + y \<le> (d x + d y) \<cdot> (x + y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x + y \<le> (d x + d y) \<cdot> (x + y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a4': "ad (x + y) = ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x + y) = ad x \<cdot> ad y
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ad (x + y) \<le> ad x \<cdot> ad y
 2. ad x \<cdot> ad y \<le> ad (x + y)
[PROOF STEP]
show "ad (x + y) \<le> ad x \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x + y) \<le> ad x \<cdot> ad y
[PROOF STEP]
by (metis a_d_closed a_supdist_var add_commute d1_a' local.mult_isol_var)
[PROOF STATE]
proof (state)
this:
ad (x + y) \<le> ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad (x + y)
[PROOF STEP]
hence "ad x \<cdot> ad y = ad x \<cdot> ad y + ad (x + y)"
[PROOF STATE]
proof (prove)
using this:
ad (x + y) \<le> ad x \<cdot> ad y

goal (1 subgoal):
 1. ad x \<cdot> ad y = ad x \<cdot> ad y + ad (x + y)
[PROOF STEP]
using less_eq_def add_commute
[PROOF STATE]
proof (prove)
using this:
ad (x + y) \<le> ad x \<cdot> ad y
(?x \<le> ?y) = (?x + ?y = ?y)
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. ad x \<cdot> ad y = ad x \<cdot> ad y + ad (x + y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y = ad x \<cdot> ad y + ad (x + y)

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad (x + y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y = ad x \<cdot> ad y + ad (x + y)

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad (x + y)
[PROOF STEP]
have "... = ad (ad (ad x \<cdot> ad y) \<cdot> (x + y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> ad y + ad (x + y) = ad (ad (ad x \<cdot> ad y) \<cdot> (x + y))
[PROOF STEP]
by (metis a_closed a_export'')
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y + ad (x + y) = ad (ad (ad x \<cdot> ad y) \<cdot> (x + y))

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad (x + y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad x \<cdot> ad y = ad (ad (ad x \<cdot> ad y) \<cdot> (x + y))
[PROOF STEP]
show "ad x \<cdot> ad y \<le> ad (x + y)"
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> ad y = ad (ad (ad x \<cdot> ad y) \<cdot> (x + y))

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad (x + y)
[PROOF STEP]
using a_antitone' apd_d_def d1_sum_var
[PROOF STATE]
proof (prove)
using this:
ad x \<cdot> ad y = ad (ad (ad x \<cdot> ad y) \<cdot> (x + y))
?x \<le> ?y \<Longrightarrow> ad ?y \<le> ad ?x
d ?x = ad (ad ?x)
?x + ?y \<le> (d ?x + d ?y) \<cdot> (?x + ?y)

goal (1 subgoal):
 1. ad x \<cdot> ad y \<le> ad (x + y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad x \<cdot> ad y \<le> ad (x + y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_supdist: "ad (x + y) \<le> ad x + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x + y) \<le> ad x + ad y
[PROOF STEP]
using a_supdist_var local.join.le_supI1
[PROOF STATE]
proof (prove)
using this:
ad (?x + ?y) \<le> ad ?x
?x \<le> ?a \<Longrightarrow> ?x \<le> ?a + ?b

goal (1 subgoal):
 1. ad (x + y) \<le> ad x + ad y
[PROOF STEP]
by auto


[STATEMENT]
lemma a_gla: "ad x \<cdot> y = 0 \<longleftrightarrow> ad x \<le> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<cdot> y = (0::'a)) = (ad x \<le> ad y)
[PROOF STEP]
using gla_1 a_gla2
[PROOF STATE]
proof (prove)
using this:
ad ?x \<cdot> ?y = (0::'a) \<Longrightarrow> ad ?x \<le> ad ?y
ad ?x \<le> ad ?y \<Longrightarrow> ad ?x \<cdot> ?y = (0::'a)

goal (1 subgoal):
 1. (ad x \<cdot> y = (0::'a)) = (ad x \<le> ad y)
[PROOF STEP]
by blast


[STATEMENT]
lemma a_subid_aux2: "x \<cdot> ad y \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> ad y \<le> x
[PROOF STEP]
using a_subid' mult_isol
[PROOF STATE]
proof (prove)
using this:
ad ?x \<le> (1::'a)
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y

goal (1 subgoal):
 1. x \<cdot> ad y \<le> x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma a42_var: "d x \<cdot> d y \<le> ad (ad x + ad y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> d y \<le> ad (ad x + ad y)
[PROOF STEP]
by (simp add: apd_d_def)


[STATEMENT]
lemma d1_weak [simp]: "(d x + d y) \<cdot> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x + d y) \<cdot> x = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (d x + d y) \<cdot> x = x
[PROOF STEP]
have "(d x + d y) \<cdot> x = (1 + d y) \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x + d y) \<cdot> x = ((1::'a) + d y) \<cdot> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(d x + d y) \<cdot> x = ((1::'a) + d y) \<cdot> x

goal (1 subgoal):
 1. (d x + d y) \<cdot> x = x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(d x + d y) \<cdot> x = ((1::'a) + d y) \<cdot> x

goal (1 subgoal):
 1. (d x + d y) \<cdot> x = x
[PROOF STEP]
by (metis add_commute apd_d_def dpdz.dnso3 local.mult_1_left)
[PROOF STATE]
proof (state)
this:
(d x + d y) \<cdot> x = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "x \<cdot> ad 1 = ad 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> ad (1::'a) = ad (1::'a)
[PROOF STEP]
(*nitpick [expect=genuine]*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> ad (1::'a) = ad (1::'a)
[PROOF STEP]
oops


[STATEMENT]
lemma "ad x \<cdot> (y + z) = ad x \<cdot> y + ad x \<cdot> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> (y + z) = ad x \<cdot> y + ad x \<cdot> z
[PROOF STEP]
(*nitpick [expect=genuine]*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad x \<cdot> (y + z) = ad x \<cdot> y + ad x \<cdot> z
[PROOF STEP]
oops


[STATEMENT]
lemma "ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
(*nitpick [expect=genuine]*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
oops


[STATEMENT]
lemma one_idem': "1 + 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) + (1::'a) = (1::'a)
[PROOF STEP]
by (metis as1 as2 as3 add_zeror mult.right_neutral)


[STATEMENT]
lemma am5_lem [simp]: "ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
have "ad (x \<cdot> y ) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y)
[PROOF STEP]
using ads_d_def local.a2_eq' local.apd_d_def
[PROOF STATE]
proof (prove)
using this:
d ?x = ad (ad ?x)
ad (?x \<cdot> apd_d ?y) = ad (?x \<cdot> ?y)
apd_d ?x = ad (ad ?x)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
have "... = ad (x \<cdot> d y + x \<cdot> ad y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y + x \<cdot> ad y)
[PROOF STEP]
using ans4
[PROOF STATE]
proof (prove)
using this:
ad (?x + ?y) = ad ?x \<cdot> ad ?y

goal (1 subgoal):
 1. ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y + x \<cdot> ad y)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y + x \<cdot> ad y)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> d y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> d y + x \<cdot> ad y)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
have "... = ad (x \<cdot> (d y + ad y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> d y + x \<cdot> ad y) = ad (x \<cdot> (d y + ad y))
[PROOF STEP]
using distrib_left
[PROOF STATE]
proof (prove)
using this:
?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c

goal (1 subgoal):
 1. ad (x \<cdot> d y + x \<cdot> ad y) = ad (x \<cdot> (d y + ad y))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> d y + x \<cdot> ad y) = ad (x \<cdot> (d y + ad y))

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> (d y + ad y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad (x \<cdot> (d y + ad y))

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x
[PROOF STEP]
by (simp add: ads_d_def)
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> ad (x \<cdot> ad y) = ad x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma am6_lem [simp]: "ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
have "ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + (0::'a)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + (0::'a)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
have "... = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y + (0::'a) = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y
[PROOF STEP]
using ans1 mult_assoc
[PROOF STATE]
proof (prove)
using this:
ad ?x \<cdot> ?x = (0::'a)
?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y + (0::'a) = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y + (0::'a) = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y + (0::'a) = ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
have "... = ad (x \<cdot> y) \<cdot> x \<cdot> (ad y + d y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y = ad (x \<cdot> y) \<cdot> x \<cdot> (ad y + d y)
[PROOF STEP]
using ads_d_def local.a2_eq' local.apd_d_def local.distrib_left
[PROOF STATE]
proof (prove)
using this:
d ?x = ad (ad ?x)
ad (?x \<cdot> apd_d ?y) = ad (?x \<cdot> ?y)
apd_d ?x = ad (ad ?x)
?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y = ad (x \<cdot> y) \<cdot> x \<cdot> (ad y + d y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y + ad (x \<cdot> d y) \<cdot> x \<cdot> d y = ad (x \<cdot> y) \<cdot> x \<cdot> (ad y + d y)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x \<cdot> (ad y + d y)
[PROOF STEP]
show "ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x"
[PROOF STATE]
proof (prove)
using this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x \<cdot> (ad y + d y)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
using add_commute ads_d_def local.as3
[PROOF STATE]
proof (prove)
using this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x \<cdot> (ad y + d y)
?a + ?b = ?b + ?a
d ?x = ad (ad ?x)
ad (ad ?x) + ad ?x = (1::'a)

goal (1 subgoal):
 1. ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ad (x \<cdot> y) \<cdot> x \<cdot> ad y = ad (x \<cdot> y) \<cdot> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_zero [simp]: "ad 0 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (0::'a) = (1::'a)
[PROOF STEP]
by (simp add: local.a_very_costrict'')


[STATEMENT]
lemma a_one [simp]: "ad 1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ad (1::'a) = (0::'a)
[PROOF STEP]
using a_zero local.dpdz.dpd5
[PROOF STATE]
proof (prove)
using this:
ad (0::'a) = (1::'a)
ad (ad (0::'a)) = (0::'a)

goal (1 subgoal):
 1. ad (1::'a) = (0::'a)
[PROOF STEP]
by blast


[STATEMENT]
lemma fd_eq_fdia [simp]: "domain_semiringl.fd (\<cdot>) d x y \<equiv> fdia x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y
[PROOF STEP]
have "class.domain_semiringl (+) (\<cdot>) 1 0 d (\<le>) (<)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.domain_semiringl (+) (\<cdot>) (1::'a) (zero_class.zero::'a) d (\<le>) (<)
[PROOF STEP]
by (unfold_locales, auto simp: ads_d_def local.ans_d_def)
[PROOF STATE]
proof (state)
this:
class.domain_semiringl (+) (\<cdot>) (1::'a) (zero_class.zero::'a) d (\<le>) (<)

goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y
[PROOF STEP]
hence "domain_semiringl.fd (\<cdot>) d x y = d ((\<cdot>) x y)"
[PROOF STATE]
proof (prove)
using this:
class.domain_semiringl (+) (\<cdot>) (1::'a) (zero_class.zero::'a) d (\<le>) (<)

goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y = d (x \<cdot> y)
[PROOF STEP]
by (rule domain_semiringl.fd_def)
[PROOF STATE]
proof (state)
this:
domain_semiringl.fd (\<cdot>) d x y = d (x \<cdot> y)

goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
domain_semiringl.fd (\<cdot>) d x y = d (x \<cdot> y)

goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y
[PROOF STEP]
have "... = ds.fd x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (x \<cdot> y) =  |x\<rangle> y
[PROOF STEP]
by (simp add: ds.fd_def ads_d_def)
[PROOF STATE]
proof (state)
this:
d (x \<cdot> y) =  |x\<rangle> y

goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
domain_semiringl.fd (\<cdot>) d x y =  |x\<rangle> y
[PROOF STEP]
show "domain_semiringl.fd (\<cdot>) d x y \<equiv> |x\<rangle> y"
[PROOF STATE]
proof (prove)
using this:
domain_semiringl.fd (\<cdot>) d x y =  |x\<rangle> y

goal (1 subgoal):
 1. domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_semiringl.fd (\<cdot>) d x y \<equiv>  |x\<rangle> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "a_zero = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_zero = (zero_class.zero::'a)
[PROOF STEP]
by (simp add: local.a_zero_def)


[STATEMENT]
lemma a_2_var: "ad x \<cdot> d y = 0 \<longleftrightarrow> ad x \<le> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<cdot> d y = (zero_class.zero::'a)) = (ad x \<le> ad y)
[PROOF STEP]
using local.a_gla local.ads_d_def local.dpdz.dom_weakly_local
[PROOF STATE]
proof (prove)
using this:
(ad ?x \<cdot> ?y = (zero_class.zero::'a)) = (ad ?x \<le> ad ?y)
d ?x = ad (ad ?x)
(?x \<cdot> ?y = (zero_class.zero::'a)) = (?x \<cdot> ad (ad ?y) = (zero_class.zero::'a))

goal (1 subgoal):
 1. (ad x \<cdot> d y = (zero_class.zero::'a)) = (ad x \<le> ad y)
[PROOF STEP]
by auto


[STATEMENT]
lemma da_shunt1: "x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
assume "x \<le> d y + z"
[PROOF STATE]
proof (state)
this:
x \<le> d y + z

goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
hence "x \<cdot> ad y \<le> (d y + z) \<cdot> ad y"
[PROOF STATE]
proof (prove)
using this:
x \<le> d y + z

goal (1 subgoal):
 1. x \<cdot> ad y \<le> (d y + z) \<cdot> ad y
[PROOF STEP]
using mult_isor
[PROOF STATE]
proof (prove)
using this:
x \<le> d y + z
?x \<le> ?y \<Longrightarrow> ?x \<cdot> ?z \<le> ?y \<cdot> ?z

goal (1 subgoal):
 1. x \<cdot> ad y \<le> (d y + z) \<cdot> ad y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<cdot> ad y \<le> (d y + z) \<cdot> ad y

goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<cdot> ad y \<le> (d y + z) \<cdot> ad y

goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
have "... = d y \<cdot> ad y + z \<cdot> ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d y + z) \<cdot> ad y = d y \<cdot> ad y + z \<cdot> ad y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(d y + z) \<cdot> ad y = d y \<cdot> ad y + z \<cdot> ad y

goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(d y + z) \<cdot> ad y = d y \<cdot> ad y + z \<cdot> ad y

goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
have "... \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d y \<cdot> ad y + z \<cdot> ad y \<le> z
[PROOF STEP]
by (simp add: a_subid_aux2 ads_d_def)
[PROOF STATE]
proof (state)
this:
d y \<cdot> ad y + z \<cdot> ad y \<le> z

goal (1 subgoal):
 1. x \<le> d y + z \<Longrightarrow> x \<cdot> ad y \<le> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<cdot> ad y \<le> z
[PROOF STEP]
show "x \<cdot> ad y \<le> z"
[PROOF STATE]
proof (prove)
using this:
x \<cdot> ad y \<le> z

goal (1 subgoal):
 1. x \<cdot> ad y \<le> z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<cdot> ad y \<le> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma da_shunt2: "x \<le> ad y + z \<Longrightarrow> x \<cdot> d y \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> ad y + z \<Longrightarrow> x \<cdot> d y \<le> z
[PROOF STEP]
using da_shunt1 local.a_add_idem local.ads_d_def am_add_op_def
[PROOF STATE]
proof (prove)
using this:
?x \<le> d ?y + ?z \<Longrightarrow> ?x \<cdot> ad ?y \<le> ?z
ad ?x \<oplus> ad ?x = ad ?x
d ?x = ad (ad ?x)
?x \<oplus> ?y \<equiv> ad (ad ?x \<cdot> ad ?y)

goal (1 subgoal):
 1. x \<le> ad y + z \<Longrightarrow> x \<cdot> d y \<le> z
[PROOF STEP]
by auto


[STATEMENT]
lemma d_a_galois1: "d x \<cdot> ad y \<le> d z \<longleftrightarrow> d x \<le> d z + d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<cdot> ad y \<le> d z) = (d x \<le> d z + d y)
[PROOF STEP]
by (metis add_assoc local.a_gla local.ads_d_def local.am2 local.ans4 local.ans_d_def local.dnsz.dnso4)


[STATEMENT]
lemma d_a_galois2: "d x \<cdot> d y \<le> d z \<longleftrightarrow> d x \<le> d z + ad y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<cdot> d y \<le> d z) = (d x \<le> d z + ad y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (d x \<cdot> d y \<le> d z) = (d x \<le> d z + ad y)
[PROOF STEP]
have "\<And>a aa. ad ((a::'a) \<cdot> ad (ad aa)) = ad (a \<cdot> aa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. ad (a \<cdot> ad (ad aa)) = ad (a \<cdot> aa)
[PROOF STEP]
using local.a2_eq' local.apd_d_def
[PROOF STATE]
proof (prove)
using this:
ad (?x \<cdot> apd_d ?y) = ad (?x \<cdot> ?y)
apd_d ?x = ad (ad ?x)

goal (1 subgoal):
 1. \<And>a aa. ad (a \<cdot> ad (ad aa)) = ad (a \<cdot> aa)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ad (?a1 \<cdot> ad (ad ?aa1)) = ad (?a1 \<cdot> ?aa1)

goal (1 subgoal):
 1. (d x \<cdot> d y \<le> d z) = (d x \<le> d z + ad y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (?a1 \<cdot> ad (ad ?aa1)) = ad (?a1 \<cdot> ?aa1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (?a1 \<cdot> ad (ad ?aa1)) = ad (?a1 \<cdot> ?aa1)

goal (1 subgoal):
 1. (d x \<cdot> d y \<le> d z) = (d x \<le> d z + ad y)
[PROOF STEP]
by (metis d_a_galois1 local.a_export' local.ads_d_def local.ans_d_def)
[PROOF STATE]
proof (state)
this:
(d x \<cdot> d y \<le> d z) = (d x \<le> d z + ad y)

goal:
No subgoals!
[PROOF STEP]
qed