[STATEMENT]
lemma inj_signed_lconjaction: "inj (signed_lconjaction s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (signed_lconjaction s)
[PROOF STEP]
proof (rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
assume 1: "signed_lconjaction s x = signed_lconjaction s y"
[PROOF STATE]
proof (state)
this:
signed_lconjaction s x = signed_lconjaction s y

goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
signed_lconjaction s x = signed_lconjaction s y

goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
obtain a1 a2 :: 'a and b1 b2 :: bool
    where xy: "x = (a1,b1)" "y = (a2,b2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a1 b1 a2 b2. \<lbrakk>x = (a1, b1); y = (a2, b2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
x = (a1, b1)
y = (a2, b2)

goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
signed_lconjaction s x = signed_lconjaction s y
x = (a1, b1)
y = (a2, b2)
[PROOF STEP]
show "x=y"
[PROOF STATE]
proof (prove)
using this:
signed_lconjaction s x = signed_lconjaction s y
x = (a1, b1)
y = (a2, b2)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using injD[OF lconjby_inj, of s a1 a2] signed_lconjactionD
[PROOF STATE]
proof (prove)
using this:
signed_lconjaction s x = signed_lconjaction s y
x = (a1, b1)
y = (a2, b2)
lconjby s a1 = lconjby s a2 \<Longrightarrow> a1 = a2
signed_lconjaction ?s ?x \<equiv> map_prod (lconjby ?s) (\<lambda>b. b \<noteq> (fst ?x = ?s)) ?x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by    (cases "a1=s" "a2=s" rule: two_cases) auto
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed