[STATEMENT]
lemma (in Yoneda) unsandwich_right_inverse:
  assumes 1: "A \<in> Ob"
  and 2: "u : Hom(A,_) \<Rightarrow> F in Func(AA,Set)"
  shows "\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) = u
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) \<in> extensional ?A
 2. u \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
show "\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) \<in> extensional (Ob)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) \<in> extensional (Ob)
[PROOF STEP]
by (unfold sandwich_def, rule restrict_extensional)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) \<in> extensional (Ob)

goal (2 subgoals):
 1. u \<in> extensional (Ob)
 2. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
[PROOF STEP]
show "u \<in>  extensional (Ob)"
[PROOF STATE]
proof (prove)
using this:
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )

goal (1 subgoal):
 1. u \<in> extensional (Ob)
[PROOF STEP]
by (simp add: natural_transformation_def natural_transformation_axioms_def)
[PROOF STATE]
proof (state)
this:
u \<in> extensional (Ob)

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
assume 3: "B \<in> Ob"
[PROOF STATE]
proof (state)
this:
B \<in> Ob

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
B \<in> Ob
[PROOF STEP]
have one: "\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = \<lparr>
    set_dom = Hom A B,
    set_func = (\<lambda>f\<in>Hom A B. (set_func (F\<^bsub>\<a>\<^esub> f)) (set_func (u A) (Id A))),
    set_cod = F\<^bsub>\<o>\<^esub> B \<rparr>"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
B \<in> Ob

goal (1 subgoal):
 1. \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A)), set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>
[PROOF STEP]
by (simp add: sandwich_def unsandwich_def)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A)), set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
[PROOF STEP]
have "Hom(A,_)\<^bsub>\<o>\<^esub> A = Hom A A"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob

goal (1 subgoal):
 1. Hom(A,_) \<^bsub>\<o>\<^esub> A = Hom A A
[PROOF STEP]
by (simp add: homf_def)
[PROOF STATE]
proof (state)
this:
Hom(A,_) \<^bsub>\<o>\<^esub> A = Hom A A

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
with 1 and 2
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
Hom(A,_) \<^bsub>\<o>\<^esub> A = Hom A A
[PROOF STEP]
have "(u A) \<in> hom Set (Hom A A) (F\<^bsub>\<o>\<^esub> A)"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
Hom(A,_) \<^bsub>\<o>\<^esub> A = Hom A A

goal (1 subgoal):
 1. u A \<in> Hom\<^bsub>Set\<^esub> (Hom A A) F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp add: natural_transformation_def natural_transformation_axioms_def,
      auto)
[PROOF STATE]
proof (state)
this:
u A \<in> Hom\<^bsub>Set\<^esub> (Hom A A) F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
hence "set_dom (u A) = Hom A A"
[PROOF STATE]
proof (prove)
using this:
u A \<in> Hom\<^bsub>Set\<^esub> (Hom A A) F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. set_dom (u A) = Hom A A
[PROOF STEP]
by (simp add: hom_def Set_def)
[PROOF STATE]
proof (state)
this:
set_dom (u A) = Hom A A

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
set_dom (u A) = Hom A A
[PROOF STEP]
have applicable: "Id A \<in> set_dom (u A)"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
set_dom (u A) = Hom A A

goal (1 subgoal):
 1. Id A \<in> set_dom (u A)
[PROOF STEP]
by (simp)(rule)
[PROOF STATE]
proof (state)
this:
Id A \<in> set_dom (u A)

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have two: "(\<lambda>f\<in>Hom A B. (set_func (F\<^bsub>\<a>\<^esub> f)) (set_func (u A) (Id A)))
    = (\<lambda>f\<in>Hom A B. (set_func ((F\<^bsub>\<a>\<^esub> f) \<odot> (u A)) (Id A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A))) = (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A))
[PROOF STEP]
by (rule extensionalityI,
      rule restrict_extensional, rule restrict_extensional,
      simp add: set_comp_def compose_def applicable)
[PROOF STATE]
proof (state)
this:
(\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A))) = (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A))

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
[PROOF STEP]
have "(\<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. (F\<^bsub>\<a>\<^esub> f) \<bullet>\<^bsub>BB\<^esub> (u X) = (u Y) \<bullet>\<^bsub>BB\<^esub> (Hom(A,_)\<^bsub>\<a>\<^esub> f))"
[PROOF STATE]
proof (prove)
using this:
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )

goal (1 subgoal):
 1. \<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>BB\<^esub> u X = u Y \<bullet>\<^bsub>BB\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
by (simp add: natural_transformation_def natural_transformation_axioms_def BB_Set)
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>BB\<^esub> u X = u Y \<bullet>\<^bsub>BB\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
with 1 and 3
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
B \<in> Ob
\<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>BB\<^esub> u X = u Y \<bullet>\<^bsub>BB\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
have three: "(\<lambda>f\<in>Hom A B. (set_func ((F\<^bsub>\<a>\<^esub> f) \<odot> (u A)) (Id A)))
    = (\<lambda>f\<in>Hom A B. (set_func ((u B) \<odot> (Hom(A,_))\<^bsub>\<a>\<^esub> f)) (Id A))"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
B \<in> Ob
\<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>BB\<^esub> u X = u Y \<bullet>\<^bsub>BB\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f

goal (1 subgoal):
 1. (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) = (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A))
[PROOF STEP]
apply (simp add: BB_Set Set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> Ob; B \<in> Ob; \<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<odot> u X = u Y \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) = (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A))
[PROOF STEP]
apply (rule extensionalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>A \<in> Ob; B \<in> Ob; \<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<odot> u X = u Y \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) \<in> extensional ?A16
 2. \<lbrakk>A \<in> Ob; B \<in> Ob; \<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<odot> u X = u Y \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) \<in> extensional ?A16
 3. \<And>x. \<lbrakk>A \<in> Ob; B \<in> Ob; \<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<odot> u X = u Y \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f; x \<in> ?A16\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) x = (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) x
[PROOF STEP]
apply (rule restrict_extensional, rule restrict_extensional)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>A \<in> Ob; B \<in> Ob; \<forall>X\<in>Ob. \<forall>Y\<in>Ob. \<forall>f\<in>Hom X Y. F \<^bsub>\<a>\<^esub> f \<odot> u X = u Y \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f; x \<in> Hom A B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) x = (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) = (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A))

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have "\<forall>f \<in> Hom A B. set_dom (Hom(A,_)\<^bsub>\<a>\<^esub> f) = Hom A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>Hom A B. set_dom (Hom(A,_) \<^bsub>\<a>\<^esub> f) = Hom A A
[PROOF STEP]
by (intro ballI, simp add: homf_def hom_def)
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>Hom A B. set_dom (Hom(A,_) \<^bsub>\<a>\<^esub> f) = Hom A A

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have roolz: "\<And>f. f \<in> Hom A B \<Longrightarrow> set_dom (Hom(A,_)\<^bsub>\<a>\<^esub> f) = Hom A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> set_dom (Hom(A,_) \<^bsub>\<a>\<^esub> f) = Hom A A
[PROOF STEP]
by (simp add: homf_def hom_def)
[PROOF STATE]
proof (state)
this:
?f \<in> Hom A B \<Longrightarrow> set_dom (Hom(A,_) \<^bsub>\<a>\<^esub> ?f) = Hom A A

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
[PROOF STEP]
have rooly: "Id A \<in> Hom A A"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob

goal (1 subgoal):
 1. Id A \<in> Hom A A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Id A \<in> Hom A A

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have roolx: "\<And>f. f \<in> Hom A B \<Longrightarrow> f \<in> Ar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> f \<in> Ar
[PROOF STEP]
by (simp add: hom_def)
[PROOF STATE]
proof (state)
this:
?f \<in> Hom A B \<Longrightarrow> ?f \<in> Ar

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have roolw: "\<And>f. f \<in> Hom A B \<Longrightarrow> Id A \<in> Hom A (Dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> Id A \<in> Hom A (Dom f)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> Id A \<in> Hom A (Dom f)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> Id A \<in> Hom A (Dom f)
[PROOF STEP]
assume "f \<in> Hom A B"
[PROOF STATE]
proof (state)
this:
f \<in> Hom A B

goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> Id A \<in> Hom A (Dom f)
[PROOF STEP]
hence "Dom f = A"
[PROOF STATE]
proof (prove)
using this:
f \<in> Hom A B

goal (1 subgoal):
 1. Dom f = A
[PROOF STEP]
by (simp add: hom_def)
[PROOF STATE]
proof (state)
this:
Dom f = A

goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> Id A \<in> Hom A (Dom f)
[PROOF STEP]
thus "Id A \<in> Hom A (Dom f)"
[PROOF STATE]
proof (prove)
using this:
Dom f = A

goal (1 subgoal):
 1. Id A \<in> Hom A (Dom f)
[PROOF STEP]
by (simp add: rooly)
[PROOF STATE]
proof (state)
this:
Id A \<in> Hom A (Dom f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f \<in> Hom A B \<Longrightarrow> Id A \<in> Hom A (Dom ?f)

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have annoying: "\<And>f. f \<in> Hom A B \<Longrightarrow> Id A = Id (Dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. f \<in> Hom A B \<Longrightarrow> Id A = Id (Dom f)
[PROOF STEP]
by (simp add: hom_def)
[PROOF STATE]
proof (state)
this:
?f \<in> Hom A B \<Longrightarrow> Id A = Id (Dom ?f)

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have "(\<lambda>f\<in>Hom A B. (set_func ((u B) \<odot> (Hom(A,_))\<^bsub>\<a>\<^esub> f)) (Id A))
    = (\<lambda>f\<in>Hom A B. (compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_)\<^bsub>\<a>\<^esub> f))) (Id A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A))
[PROOF STEP]
apply (rule extensionalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) \<in> extensional ?A
 2. (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) x = (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) x
[PROOF STEP]
apply (rule restrict_extensional, rule restrict_extensional)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) x = (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) x
[PROOF STEP]
by (simp add: compose_def set_comp_def roolz rooly)
[PROOF STATE]
proof (state)
this:
(\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A))

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A))

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have "\<dots> = (\<lambda>f\<in>Hom A B. (set_func (u B) f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) = restrict (set_func (u B)) (Hom A B)
[PROOF STEP]
apply (rule extensionalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) \<in> extensional ?A
 2. restrict (set_func (u B)) (Hom A B) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) x = restrict (set_func (u B)) (Hom A B) x
[PROOF STEP]
apply (rule restrict_extensional, rule restrict_extensional)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> (\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) x = restrict (set_func (u B)) (Hom A B) x
[PROOF STEP]
apply (simp add: compose_def homf_def rooly roolx roolw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (u B) (x \<bullet> Id A) = set_func (u B) x
[PROOF STEP]
apply (simp only: annoying)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (u B) (x \<bullet> Id (Dom x)) = set_func (u B) x
[PROOF STEP]
apply (simp add: roolx id_right)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>f\<in>Hom A B. compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_) \<^bsub>\<a>\<^esub> f)) (Id A)) = restrict (set_func (u B)) (Hom A B)

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = restrict (set_func (u B)) (Hom A B)
[PROOF STEP]
have four:
    "(\<lambda>f\<in>Hom A B. (set_func ((u B) \<odot> (Hom(A,_))\<^bsub>\<a>\<^esub> f)) (Id A))
    = (\<lambda>f\<in>Hom A B. (set_func (u B) f))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = restrict (set_func (u B)) (Hom A B)

goal (1 subgoal):
 1. (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = restrict (set_func (u B)) (Hom A B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = restrict (set_func (u B)) (Hom A B)

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
from 2 and  3
[PROOF STATE]
proof (chain)
picking this:
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
B \<in> Ob
[PROOF STEP]
have uBhom: "u B \<in> hom Set (Hom(A,_)\<^bsub>\<o>\<^esub> B) (F\<^bsub>\<o>\<^esub> B)"
[PROOF STATE]
proof (prove)
using this:
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
B \<in> Ob

goal (1 subgoal):
 1. u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (simp add: natural_transformation_def natural_transformation_axioms_def)
[PROOF STATE]
proof (state)
this:
u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
B \<in> Ob
u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
have five: "set_dom (u B) = Hom A B"
[PROOF STATE]
proof (prove)
using this:
B \<in> Ob
u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. set_dom (u B) = Hom A B
[PROOF STEP]
by (simp add: hom_def homf_def Set_def set_cat_def)
[PROOF STATE]
proof (state)
this:
set_dom (u B) = Hom A B

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
from uBhom
[PROOF STATE]
proof (chain)
picking this:
u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
have six: "set_cod (u B) = F\<^bsub>\<o>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. set_cod (u B) = F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (simp add: hom_def homf_def Set_def set_cat_def)
[PROOF STATE]
proof (state)
this:
set_cod (u B) = F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
have seven: "restrict (set_func (u B)) (Hom A B) = set_func (u B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (set_func (u B)) (Hom A B) = set_func (u B)
[PROOF STEP]
apply (rule extensionalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. restrict (set_func (u B)) (Hom A B) \<in> extensional ?A
 2. set_func (u B) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
apply (rule restrict_extensional)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set_func (u B) \<in> extensional (Hom A B)
 2. \<And>x. x \<in> Hom A B \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set_func (u B) \<in> extensional (Hom A B)
 2. \<And>x. x \<in> Hom A B \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
from uBhom
[PROOF STATE]
proof (chain)
picking this:
u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
have "u B \<in> ar Set"
[PROOF STATE]
proof (prove)
using this:
u B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. u B \<in> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
by (simp add: hom_def)
[PROOF STATE]
proof (state)
this:
u B \<in> Ar\<^bsub>Set\<^esub>

goal (2 subgoals):
 1. set_func (u B) \<in> extensional (Hom A B)
 2. \<And>x. x \<in> Hom A B \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
hence almost: "set_func (u B) \<in> extensional (set_dom (u B))"
[PROOF STATE]
proof (prove)
using this:
u B \<in> Ar\<^bsub>Set\<^esub>

goal (1 subgoal):
 1. set_func (u B) \<in> extensional (set_dom (u B))
[PROOF STEP]
by (simp add: Set_def set_cat_def set_arrow_def)
[PROOF STATE]
proof (state)
this:
set_func (u B) \<in> extensional (set_dom (u B))

goal (2 subgoals):
 1. set_func (u B) \<in> extensional (Hom A B)
 2. \<And>x. x \<in> Hom A B \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
from almost and five
[PROOF STATE]
proof (chain)
picking this:
set_func (u B) \<in> extensional (set_dom (u B))
set_dom (u B) = Hom A B
[PROOF STEP]
show "set_func (u B) \<in> extensional (Hom A B)"
[PROOF STATE]
proof (prove)
using this:
set_func (u B) \<in> extensional (set_dom (u B))
set_dom (u B) = Hom A B

goal (1 subgoal):
 1. set_func (u B) \<in> extensional (Hom A B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_func (u B) \<in> extensional (Hom A B)

goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
assume "f \<in> Hom A B"
[PROOF STATE]
proof (state)
this:
f \<in> Hom A B

goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> restrict (set_func (u B)) (Hom A B) x = set_func (u B) x
[PROOF STEP]
thus "restrict (set_func (u B)) (Hom A B) f = set_func (u B) f"
[PROOF STATE]
proof (prove)
using this:
f \<in> Hom A B

goal (1 subgoal):
 1. restrict (set_func (u B)) (Hom A B) f = set_func (u B) f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
restrict (set_func (u B)) (Hom A B) f = set_func (u B) f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
restrict (set_func (u B)) (Hom A B) = set_func (u B)

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) x = u x
[PROOF STEP]
from one and two and three and four and five and six and seven
[PROOF STATE]
proof (chain)
picking this:
\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A)), set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>
(\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A))) = (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A))
(\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) = (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A))
(\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = restrict (set_func (u B)) (Hom A B)
set_dom (u B) = Hom A B
set_cod (u B) = F \<^bsub>\<o>\<^esub> B
restrict (set_func (u B)) (Hom A B) = set_func (u B)
[PROOF STEP]
show "\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = u B"
[PROOF STATE]
proof (prove)
using this:
\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A)), set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>
(\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (set_func (u A) (Id A))) = (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A))
(\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f \<odot> u A) (Id A)) = (\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A))
(\<lambda>f\<in>Hom A B. set_func (u B \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) (Id A)) = restrict (set_func (u B)) (Hom A B)
set_dom (u B) = Hom A B
set_cod (u B) = F \<^bsub>\<o>\<^esub> B
restrict (set_func (u B)) (Hom A B) = set_func (u B)

goal (1 subgoal):
 1. \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = u B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) B = u B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_eq:
  "bij_betw f A B \<longleftrightarrow>
    inj_on f A \<and> (\<forall>y\<in>B. \<exists>x\<in>A. f(x)=y) \<and> (\<forall>x\<in>A. f x \<in> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B = (inj_on f A \<and> (\<forall>y\<in>B. \<exists>x\<in>A. f x = y) \<and> (\<forall>x\<in>A. f x \<in> B))
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inj_on f A \<and> f ` A = B) = (inj_on f A \<and> (\<forall>y\<in>B. \<exists>x\<in>A. f x = y) \<and> (\<forall>x\<in>A. f x \<in> B))
[PROOF STEP]
by auto


[STATEMENT]
theorem (in Yoneda) Yoneda:
  assumes 1: "A \<in> Ob"
  shows "F\<^bsub>\<o>\<^esub> A \<cong> {u. u : Hom(A,_) \<Rightarrow> F in Func(AA,Set)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<^bsub>\<o>\<^esub> A \<cong> {u. u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )}
[PROOF STEP]
unfolding equinumerous_def bij_betw_eq inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. (\<forall>x\<in>F \<^bsub>\<o>\<^esub> A. \<forall>y\<in>F \<^bsub>\<o>\<^esub> A. f x = f y \<longrightarrow> x = y) \<and> (\<forall>y\<in>Collect (natural_transformation AA Set Hom(A,_) F). \<exists>x\<in>F \<^bsub>\<o>\<^esub> A. f x = y) \<and> (\<forall>x\<in>F \<^bsub>\<o>\<^esub> A. f x \<in> Collect (natural_transformation AA Set Hom(A,_) F))
[PROOF STEP]
proof (intro exI conjI bexI ballI impI)
  \<comment> \<open>Sandwich is injective\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F \<^bsub>\<o>\<^esub> A; y \<in> F \<^bsub>\<o>\<^esub> A; ?f x = ?f y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?f (?x5 y) = y
 3. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 4. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> ?f x \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
fix x and y
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F \<^bsub>\<o>\<^esub> A; y \<in> F \<^bsub>\<o>\<^esub> A; ?f x = ?f y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?f (?x5 y) = y
 3. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 4. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> ?f x \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
assume 2: "x \<in> F\<^bsub>\<o>\<^esub> A" and 3: "y \<in> F\<^bsub>\<o>\<^esub> A"
  and 4: "\<sigma>(A,x) = \<sigma>(A,y)"
[PROOF STATE]
proof (state)
this:
x \<in> F \<^bsub>\<o>\<^esub> A
y \<in> F \<^bsub>\<o>\<^esub> A
\<sigma>(A,x) = \<sigma>(A,y)

goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F \<^bsub>\<o>\<^esub> A; y \<in> F \<^bsub>\<o>\<^esub> A; ?f x = ?f y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?f (?x5 y) = y
 3. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 4. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> ?f x \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
hence "\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,x)) = \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,y))"
[PROOF STATE]
proof (prove)
using this:
x \<in> F \<^bsub>\<o>\<^esub> A
y \<in> F \<^bsub>\<o>\<^esub> A
\<sigma>(A,x) = \<sigma>(A,y)

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,x)) = \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,x)) = \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,y))

goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F \<^bsub>\<o>\<^esub> A; y \<in> F \<^bsub>\<o>\<^esub> A; ?f x = ?f y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?f (?x5 y) = y
 3. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 4. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> ?f x \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
with unsandwich_left_inverse
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?A \<in> Ob; ?a \<in> F \<^bsub>\<o>\<^esub> ?A\<rbrakk> \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(?A,\<sigma>(?A,?a)) = ?a
\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,x)) = \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,y))
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> Ob; ?a \<in> F \<^bsub>\<o>\<^esub> ?A\<rbrakk> \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(?A,\<sigma>(?A,?a)) = ?a
\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,x)) = \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,y))

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

goal (3 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>(A,?x5 y) = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 3. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
next
  \<comment> \<open>Sandwich covers F A\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>(A,?x5 y) = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 3. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>(A,?x5 y) = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 3. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
assume "u \<in> {y. y : Hom(A,_) \<Rightarrow> F in Func (AA,Set)}"
[PROOF STATE]
proof (state)
this:
u \<in> {y. y : Hom(A,_) \<Rightarrow> F in Func (AA , Set )}

goal (3 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>(A,?x5 y) = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 3. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
hence 2: "u : Hom(A,_) \<Rightarrow> F in Func (AA,Set)"
[PROOF STATE]
proof (prove)
using this:
u \<in> {y. y : Hom(A,_) \<Rightarrow> F in Func (AA , Set )}

goal (1 subgoal):
 1. u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )

goal (3 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>(A,?x5 y) = y
 2. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> ?x5 y \<in> F \<^bsub>\<o>\<^esub> A
 3. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
[PROOF STEP]
show "\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) = u"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )

goal (1 subgoal):
 1. \<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) = u
[PROOF STEP]
by (rule unsandwich_right_inverse)
  \<comment> \<open>Sandwich is into F A\<close>
[PROOF STATE]
proof (state)
this:
\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) = u

goal (2 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(A,y) \<in> F \<^bsub>\<o>\<^esub> A
 2. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
(* there is really similar reasoning elsewhere*)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,\<sigma>\<^sup>\<leftarrow>(A,u)) = u

goal (2 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(A,y) \<in> F \<^bsub>\<o>\<^esub> A
 2. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
from 1 and 2
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
[PROOF STEP]
have "u A \<in> hom Set (Hom A A) (F\<^bsub>\<o>\<^esub> A)"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
u : Hom(A,_) \<Rightarrow> F in Func (AA , Set )

goal (1 subgoal):
 1. u A \<in> Hom\<^bsub>Set\<^esub> (Hom A A) F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp add: natural_transformation_def natural_transformation_axioms_def homf_def)
[PROOF STATE]
proof (state)
this:
u A \<in> Hom\<^bsub>Set\<^esub> (Hom A A) F \<^bsub>\<o>\<^esub> A

goal (2 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(A,y) \<in> F \<^bsub>\<o>\<^esub> A
 2. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
hence "u A \<in> ar Set" and "dom Set (u A) = Hom A A" and "cod Set (u A) = F\<^bsub>\<o>\<^esub> A"
[PROOF STATE]
proof (prove)
using this:
u A \<in> Hom\<^bsub>Set\<^esub> (Hom A A) F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. u A \<in> Ar\<^bsub>Set\<^esub> &&& Dom\<^bsub>Set\<^esub> u A = Hom A A &&& Cod\<^bsub>Set\<^esub> u A = F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp_all add: hom_def)
[PROOF STATE]
proof (state)
this:
u A \<in> Ar\<^bsub>Set\<^esub>
Dom\<^bsub>Set\<^esub> u A = Hom A A
Cod\<^bsub>Set\<^esub> u A = F \<^bsub>\<o>\<^esub> A

goal (2 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(A,y) \<in> F \<^bsub>\<o>\<^esub> A
 2. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
hence uAfuncset: "set_func (u A) : (Hom A A) \<rightarrow> (F\<^bsub>\<o>\<^esub> A)"
[PROOF STATE]
proof (prove)
using this:
u A \<in> Ar\<^bsub>Set\<^esub>
Dom\<^bsub>Set\<^esub> u A = Hom A A
Cod\<^bsub>Set\<^esub> u A = F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. set_func (u A) \<in> Hom A A \<rightarrow> F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp add: Set_def set_cat_def set_arrow_def)
[PROOF STATE]
proof (state)
this:
set_func (u A) \<in> Hom A A \<rightarrow> F \<^bsub>\<o>\<^esub> A

goal (2 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(A,y) \<in> F \<^bsub>\<o>\<^esub> A
 2. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
[PROOF STEP]
have "Id A \<in> Hom A A"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob

goal (1 subgoal):
 1. Id A \<in> Hom A A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Id A \<in> Hom A A

goal (2 subgoals):
 1. \<And>y. y \<in> Collect (natural_transformation AA Set Hom(A,_) F) \<Longrightarrow> \<sigma>\<^sup>\<leftarrow>(A,y) \<in> F \<^bsub>\<o>\<^esub> A
 2. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
with uAfuncset
[PROOF STATE]
proof (chain)
picking this:
set_func (u A) \<in> Hom A A \<rightarrow> F \<^bsub>\<o>\<^esub> A
Id A \<in> Hom A A
[PROOF STEP]
show "\<sigma>\<^sup>\<leftarrow>(A,u) \<in> F\<^bsub>\<o>\<^esub> A"
[PROOF STATE]
proof (prove)
using this:
set_func (u A) \<in> Hom A A \<rightarrow> F \<^bsub>\<o>\<^esub> A
Id A \<in> Hom A A

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,u) \<in> F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp add: unsandwich_def, rule funcset_mem)
[PROOF STATE]
proof (state)
this:
\<sigma>\<^sup>\<leftarrow>(A,u) \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
assume "x \<in> F\<^bsub>\<o>\<^esub> A"
[PROOF STATE]
proof (state)
this:
x \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
x \<in> F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
have "\<sigma>(A,x) : Hom(A,_) \<Rightarrow> F in Func (AA,Set)"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
x \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<sigma>(A,x) : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
[PROOF STEP]
by (rule sandwich_natural)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,x) : Hom(A,_) \<Rightarrow> F in Func (AA , Set )

goal (1 subgoal):
 1. \<And>x. x \<in> F \<^bsub>\<o>\<^esub> A \<Longrightarrow> \<sigma>(A,x) \<in> Collect (natural_transformation AA Set Hom(A,_) F)
[PROOF STEP]
thus "\<sigma>(A,x) \<in> {y. y : Hom(A,_) \<Rightarrow> F in Func (AA,Set)}"
[PROOF STATE]
proof (prove)
using this:
\<sigma>(A,x) : Hom(A,_) \<Rightarrow> F in Func (AA , Set )

goal (1 subgoal):
 1. \<sigma>(A,x) \<in> {y. y : Hom(A,_) \<Rightarrow> F in Func (AA , Set )}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma>(A,x) \<in> {y. y : Hom(A,_) \<Rightarrow> F in Func (AA , Set )}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma att_and_one: assumes "\<turnstile> a" and  "attack a = s"
  shows  "\<turnstile>([a] \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[a] \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile>[a] \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>
[PROOF STEP]
show " \<turnstile>([a] \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[a] \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile>a
attack a = s

goal (1 subgoal):
 1. \<turnstile>[a] \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>
[PROOF STEP]
by (subst att_and, simp del: att_and att_or)
[PROOF STATE]
proof (state)
this:
\<turnstile>[a] \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma att_and_empty[rule_format] : " \<turnstile>([] \<oplus>\<^sub>\<and>\<^bsup>(s', s'')\<^esup>) \<longrightarrow> s' \<subseteq> s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>(s', s'')\<^esup> \<longrightarrow> s' \<subseteq> s''
[PROOF STEP]
by (simp add: is_attack_tree.simps(2))


[STATEMENT]
lemma att_and_empty2: " \<turnstile>([] \<oplus>\<^sub>\<and>\<^bsup>(s, s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[] \<oplus>\<^sub>\<and>\<^bsup>(s, s)\<^esup>
[PROOF STEP]
by (simp add: is_attack_tree.simps(2))


[STATEMENT]
lemma att_or_empty[rule_format] : " \<turnstile>([] \<oplus>\<^sub>\<or>\<^bsup>(s', s'')\<^esup>) \<longrightarrow> s' \<subseteq> s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>(s', s'')\<^esup> \<longrightarrow> s' \<subseteq> s''
[PROOF STEP]
by (simp add: is_attack_tree.simps(3))


[STATEMENT]
lemma att_or_empty_back[rule_format]: " s' \<subseteq> s'' \<longrightarrow>  \<turnstile>([] \<oplus>\<^sub>\<or>\<^bsup>(s', s'')\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<subseteq> s'' \<longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>(s', s'')\<^esup>
[PROOF STEP]
by (simp add: is_attack_tree.simps(3))


[STATEMENT]
lemma att_or_empty_rev: assumes "\<turnstile>(l \<oplus>\<^sub>\<or>\<^bsup>(s, s')\<^esup>)" and "\<not>(s \<subseteq> s')" shows "l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> []
[PROOF STEP]
using assms att_or_empty
[PROOF STATE]
proof (prove)
using this:
\<turnstile>l \<oplus>\<^sub>\<or>\<^bsup>(s, s')\<^esup>
\<not> s \<subseteq> s'
\<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>(?s', ?s'')\<^esup> \<Longrightarrow> ?s' \<subseteq> ?s''

goal (1 subgoal):
 1. l \<noteq> []
[PROOF STEP]
by blast


[STATEMENT]
lemma att_andD1: " \<turnstile>(x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>) \<Longrightarrow> \<turnstile> x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>s\<^esup> \<Longrightarrow> \<turnstile>x1
[PROOF STEP]
by (metis (no_types, lifting) is_attack_tree.simps(2) list.exhaust list.simps(4) list.simps(5))


[STATEMENT]
lemma att_and_nonemptyD2[rule_format]:
       "(x2 \<noteq> [] \<longrightarrow> \<turnstile>(x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>) \<longrightarrow> \<turnstile> (x2 \<oplus>\<^sub>\<and>\<^bsup>(snd(attack x1),snd s)\<^esup>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2 \<noteq> [] \<longrightarrow> \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>s\<^esup> \<longrightarrow> \<turnstile>x2 \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd s)\<^esup>
[PROOF STEP]
by (metis (no_types, lifting) is_attack_tree.simps(2) list.exhaust list.simps(5))


[STATEMENT]
lemma att_andD2 : " \<turnstile>(x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>s\<^esup>) \<Longrightarrow> \<turnstile> (x2 \<oplus>\<^sub>\<and>\<^bsup>(snd(attack x1),snd s)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 # x2 \<oplus>\<^sub>\<and>\<^bsup>s\<^esup> \<Longrightarrow> \<turnstile>x2 \<oplus>\<^sub>\<and>\<^bsup>(snd (attack x1), snd s)\<^esup>
[PROOF STEP]
by (metis (mono_tags, lifting) att_and_empty2 att_and_nonemptyD2 is_attack_tree.simps(2) list.simps(4) list.simps(5))


[STATEMENT]
lemma att_and_fst_lem[rule_format]:
   "\<turnstile>(x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>) \<longrightarrow> xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>))
                     \<longrightarrow> xa \<in> fst (attack x1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup> \<longrightarrow> xa \<in> fst (attack (x1 # x2a \<oplus>\<^sub>\<and>\<^bsup>x\<^esup>)) \<longrightarrow> xa \<in> fst (attack x1)
[PROOF STEP]
by (induction x2a, (subst att_and, simp)+)


[STATEMENT]
lemma att_orD1: " \<turnstile>(x1 # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup>) \<Longrightarrow> \<turnstile> x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<Longrightarrow> \<turnstile>x1
[PROOF STEP]
by (case_tac x2, (subst (asm) att_or, simp)+)


[STATEMENT]
lemma att_or_snd_hd: " \<turnstile>(a # list \<oplus>\<^sub>\<or>\<^bsup>(aa, b)\<^esup>) \<Longrightarrow> snd(attack a) \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>a # list \<oplus>\<^sub>\<or>\<^bsup>(aa, b)\<^esup> \<Longrightarrow> snd (attack a) \<subseteq> b
[PROOF STEP]
by (case_tac list,  (subst (asm) att_or, simp)+)


[STATEMENT]
lemma att_or_singleton[rule_format]:
   " \<turnstile>([x1] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup>) \<longrightarrow> \<turnstile>([] \<oplus>\<^sub>\<or>\<^bsup>(fst x - fst (attack x1), snd x)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[x1] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>(fst x - fst (attack x1), snd x)\<^esup>
[PROOF STEP]
by (subst att_or, simp, rule impI, rule att_or_empty_back, blast)


[STATEMENT]
lemma att_orD2[rule_format]:
     " \<turnstile>(x1 # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup>) \<longrightarrow>  \<turnstile> (x2 \<oplus>\<^sub>\<or>\<^bsup>(fst x - fst(attack x1), snd x)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>x1 # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>(fst x - fst (attack x1), snd x)\<^esup>
[PROOF STEP]
by (case_tac x2, simp add: att_or_singleton, simp, subst att_or, simp)


[STATEMENT]
lemma att_or_snd_att[rule_format]: "\<forall> x. \<turnstile> (x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup>) \<longrightarrow> (\<forall> a \<in> (set x2). snd(attack a) \<subseteq> snd x )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x)
[PROOF STEP]
proof (induction x2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set []. snd (attack a) \<subseteq> snd x)
 2. \<And>a x2. \<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x) \<Longrightarrow> \<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set []. snd (attack a) \<subseteq> snd x)
 2. \<And>a x2. \<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x) \<Longrightarrow> \<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set []. snd (attack a) \<subseteq> snd x)
[PROOF STEP]
by (simp add: att_or)
[PROOF STATE]
proof (state)
this:
\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set []. snd (attack a) \<subseteq> snd x)

goal (1 subgoal):
 1. \<And>a x2. \<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x) \<Longrightarrow> \<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x2. \<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x) \<Longrightarrow> \<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)
[PROOF STEP]
case (Cons a x2)
[PROOF STATE]
proof (state)
this:
\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x)

goal (1 subgoal):
 1. \<And>a x2. \<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x) \<Longrightarrow> \<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x)

goal (1 subgoal):
 1. \<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)
[PROOF STEP]
using att_orD2 att_or_snd_hd
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set x2. snd (attack a) \<subseteq> snd x)
\<turnstile>?x1.0 # ?x2.0 \<oplus>\<^sub>\<or>\<^bsup>?x\<^esup> \<Longrightarrow> \<turnstile>?x2.0 \<oplus>\<^sub>\<or>\<^bsup>(fst ?x - fst (attack ?x1.0), snd ?x)\<^esup>
\<turnstile>?a # ?list \<oplus>\<^sub>\<or>\<^bsup>(?aa, ?b)\<^esup> \<Longrightarrow> snd (attack ?a) \<subseteq> ?b

goal (1 subgoal):
 1. \<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> (\<forall>a\<in>set (a # x2). snd (attack a) \<subseteq> snd x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_or_lem: " \<turnstile>([x1] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup>)  \<Longrightarrow> fst x \<subseteq> fst(attack x1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>[x1] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<Longrightarrow> fst x \<subseteq> fst (attack x1)
[PROOF STEP]
by (subst (asm) att_or, simp)+


[STATEMENT]
lemma or_att_fst_sup0[rule_format]: "x2 \<noteq> [] \<longrightarrow> (\<forall> x. (\<turnstile> ((x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup>):: ('s :: state) attree)) \<longrightarrow>
                      ((\<Union> y::'s attree\<in> set x2. fst (attack y)) \<supseteq> fst(x))) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y)))
[PROOF STEP]
proof (induction x2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set []. fst (attack y)))
 2. \<And>a x2. x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y))) \<Longrightarrow> a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [] \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set []. fst (attack y)))
 2. \<And>a x2. x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y))) \<Longrightarrow> a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set []. fst (attack y)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>[] \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set []. fst (attack y)))

goal (1 subgoal):
 1. \<And>a x2. x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y))) \<Longrightarrow> a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x2. x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y))) \<Longrightarrow> a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))
[PROOF STEP]
case (Cons a x2)
[PROOF STATE]
proof (state)
this:
x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y)))

goal (1 subgoal):
 1. \<And>a x2. x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y))) \<Longrightarrow> a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y)))

goal (1 subgoal):
 1. a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))
[PROOF STEP]
using att_orD2 singleton_or_lem
[PROOF STATE]
proof (prove)
using this:
x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set x2. fst (attack y)))
\<turnstile>?x1.0 # ?x2.0 \<oplus>\<^sub>\<or>\<^bsup>?x\<^esup> \<Longrightarrow> \<turnstile>?x2.0 \<oplus>\<^sub>\<or>\<^bsup>(fst ?x - fst (attack ?x1.0), snd ?x)\<^esup>
\<turnstile>[?x1.0] \<oplus>\<^sub>\<or>\<^bsup>?x\<^esup> \<Longrightarrow> fst ?x \<subseteq> fst (attack ?x1.0)

goal (1 subgoal):
 1. a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a # x2 \<noteq> [] \<longrightarrow> (\<forall>x. \<turnstile>a # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup> \<longrightarrow> fst x \<subseteq> (\<Union>y\<in>set (a # x2). fst (attack y)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma or_att_fst_sup:
    assumes "(\<turnstile> ((x1 # x2 \<oplus>\<^sub>\<or>\<^bsup>x\<^esup>):: ('s :: state) attree))"
    shows   "((\<Union> y::'s attree\<in> set (x1 # x2). fst (attack y)) \<supseteq> fst(x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst x \<subseteq> (\<Union>y\<in>set (x1 # x2). fst (attack y))
[PROOF STEP]
by (rule or_att_fst_sup0, simp, rule assms)