[STATEMENT]
lemma inf_bool_def: "(a :: bool) \<sqinter> b = (a l\<rightarrow> b) * a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> b = (a l\<rightarrow> b) * a
[PROOF STEP]
by (auto simp add: times_bool_def impl_bool_def)


[STATEMENT]
lemma "\<not> class.cancel_pseudo_hoop_algebra (*) (\<sqinter>)  (l\<rightarrow>) (\<le>) (<) (1:: bool) (r\<rightarrow>) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> class.cancel_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>)
[PROOF STEP]
apply (unfold  class.cancel_pseudo_hoop_algebra_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>) \<and> class.cancel_pseudo_hoop_algebra_axioms (*))
[PROOF STEP]
apply (unfold  class.cancel_pseudo_hoop_algebra_axioms_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>) \<and> (\<forall>a b c. a * b = a * c \<longrightarrow> b = c) \<and> (\<forall>b a c. b * a = c * a \<longrightarrow> b = c))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. a * b = a * c \<longrightarrow> b = c; \<forall>b a c. b * a = c * a \<longrightarrow> b = c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b c. a * b = a * c \<longrightarrow> b = c; \<forall>b a c. b * a = c * a \<longrightarrow> b = c; True\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac x = "False" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>b a c. b * a = c * a \<longrightarrow> b = c; True; \<forall>b c. False * b = False * c \<longrightarrow> b = c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True; \<forall>b c. False * b = False * c \<longrightarrow> b = c; True\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac x = "True" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True; True; \<forall>c. False * True = False * c \<longrightarrow> True = c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac x = "False" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True; True; False * True = False * False \<longrightarrow> True = False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: times_bool_def)


[STATEMENT]
lemma classorder: "class.order (\<le>) (<)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.order (\<le>) (<)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma impl_OrdSum_first: "Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1) = Abs_OrdSum (x l\<rightarrow> y, 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_OrdSum (x, 1::'b) l\<rightarrow> Abs_OrdSum (y, 1::'b) = Abs_OrdSum (x l\<rightarrow> y, 1::'b)
[PROOF STEP]
by (simp add: impl_OrdSum_def first_def second_def  Abs_OrdSum_inverse Rep_OrdSum_inverse)


[STATEMENT]
lemma impl_OrdSum_second: "Abs_OrdSum (1, x) l\<rightarrow> Abs_OrdSum (1, y) = Abs_OrdSum (1, x l\<rightarrow> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_OrdSum (1::'a, x) l\<rightarrow> Abs_OrdSum (1::'a, y) = Abs_OrdSum (1::'a, x l\<rightarrow> y)
[PROOF STEP]
by (simp add: impl_OrdSum_def first_def second_def  Abs_OrdSum_inverse Rep_OrdSum_inverse)


[STATEMENT]
lemma impl_OrdSum_first_second: "x \<noteq> 1 \<Longrightarrow> Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (1, y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> (1::'a) \<Longrightarrow> Abs_OrdSum (x, 1::'b) l\<rightarrow> Abs_OrdSum (1::'a, y) = 1
[PROOF STEP]
by (simp add: one_OrdSum_def impl_OrdSum_def first_def second_def  Abs_OrdSum_inverse Rep_OrdSum_inverse)


[STATEMENT]
lemma Abs_OrdSum_bijective: "x \<in> OrdSum \<Longrightarrow> y \<in> OrdSum \<Longrightarrow> (Abs_OrdSum x = Abs_OrdSum y) = (x = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum\<rbrakk> \<Longrightarrow> (Abs_OrdSum x = Abs_OrdSum y) = (x = y)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (subgoal_tac  "Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y; Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)
[PROOF STEP]
apply (unfold Abs_OrdSum_inverse) [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y; x = y\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma "class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a::pseudo_hoop_algebra) (r\<rightarrow>)
          \<Longrightarrow> \<not> (class.linear_pseudo_hoop_algebra (\<le>) (<)  (*) (\<sqinter>) (l\<rightarrow>) (1::'a) (r\<rightarrow>))
          \<Longrightarrow> \<not> class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::('a, bool) OrdSum) (r\<rightarrow>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> class.linear_pseudo_hoop_algebra (\<le>) (<) (*) (\<sqinter>) (l\<rightarrow>) (1::'a) (r\<rightarrow>)\<rbrakk> \<Longrightarrow> \<not> class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>)
[PROOF STEP]
apply (unfold class.linear_pseudo_hoop_algebra_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> (class.linorder (\<le>) (<) \<and> class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>))\<rbrakk> \<Longrightarrow> \<not> class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>)
[PROOF STEP]
apply (unfold class.linorder_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> ((class.order (\<le>) (<) \<and> class.linorder_axioms (\<le>)) \<and> class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>))\<rbrakk> \<Longrightarrow> \<not> class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>)
[PROOF STEP]
apply (unfold class.linorder_axioms_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> ((class.order (\<le>) (<) \<and> (\<forall>x y. x \<le> y \<or> y \<le> x)) \<and> class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>))\<rbrakk> \<Longrightarrow> \<not> class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<not> False\<rbrakk> \<Longrightarrow> class.order (\<le>) (<)
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<not> False; \<not> y \<le> x\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (rule classorder)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); class.basic_pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<not> False; \<not> y \<le> x\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (unfold class.basic_pseudo_hoop_algebra_def) [1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>) \<and> class.basic_pseudo_hoop_algebra_axioms (l\<rightarrow>) (\<le>) (r\<rightarrow>); \<not> False; \<not> y \<le> x\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>) \<and> class.basic_pseudo_hoop_algebra_axioms (l\<rightarrow>) (\<le>) (r\<rightarrow>); \<not> y \<le> x\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (unfold class.basic_pseudo_hoop_algebra_axioms_def) [1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>) \<and> (\<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c) \<and> (\<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c); \<not> y \<le> x\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (subgoal_tac "(Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1, False) \<le>
         ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1, False)) l\<rightarrow> Abs_OrdSum (1, False)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)
[PROOF STEP]
apply (unfold impl_OrdSum_first) [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)
[PROOF STEP]
apply (case_tac "x l\<rightarrow> y \<noteq> 1 \<and> y l\<rightarrow> x \<noteq> 1")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False); \<not> (x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a))\<rbrakk> \<Longrightarrow> x \<le> y
 3. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)
[PROOF STEP]
apply (simp add: impl_OrdSum_first_second)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; 1 \<le> Abs_OrdSum (1::'a, False); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False); \<not> (x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a))\<rbrakk> \<Longrightarrow> x \<le> y
 3. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)
[PROOF STEP]
apply (unfold order_OrdSum_def one_OrdSum_def one_bool_def impl_OrdSum_second impl_bool_def ) [1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = Abs_OrdSum (1::'a, True)) (<) (Abs_OrdSum (1::'a, True)) (r\<rightarrow>); \<forall>a b c. ((a l\<rightarrow> b) l\<rightarrow> c) l\<rightarrow> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c = Abs_OrdSum (1::'a, True); \<forall>a b c. ((a r\<rightarrow> b) r\<rightarrow> c) l\<rightarrow> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c = Abs_OrdSum (1::'a, True); Abs_OrdSum (1::'a, True \<longrightarrow> False) = Abs_OrdSum (1::'a, True); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False); \<not> (x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a))\<rbrakk> \<Longrightarrow> x \<le> y
 3. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = Abs_OrdSum (1::'a, True)) (<) (Abs_OrdSum (1::'a, True)) (r\<rightarrow>); \<forall>a b c. ((a l\<rightarrow> b) l\<rightarrow> c) l\<rightarrow> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c = Abs_OrdSum (1::'a, True); \<forall>a b c. ((a r\<rightarrow> b) r\<rightarrow> c) l\<rightarrow> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c = Abs_OrdSum (1::'a, True); Abs_OrdSum (1::'a, False) = Abs_OrdSum (1::'a, True); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False); \<not> (x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a))\<rbrakk> \<Longrightarrow> x \<le> y
 3. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)
[PROOF STEP]
apply (cut_tac x = "(1::'a, False)" and y = "(1::'a, True)" in  Abs_OrdSum_eq)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = Abs_OrdSum (1::'a, True)) (<) (Abs_OrdSum (1::'a, True)) (r\<rightarrow>); \<forall>a b c. ((a l\<rightarrow> b) l\<rightarrow> c) l\<rightarrow> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c = Abs_OrdSum (1::'a, True); \<forall>a b c. ((a r\<rightarrow> b) r\<rightarrow> c) l\<rightarrow> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c = Abs_OrdSum (1::'a, True); Abs_OrdSum (1::'a, False) = Abs_OrdSum (1::'a, True); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> (1::'a, False) \<in> OrdSum
 2. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = Abs_OrdSum (1::'a, True)) (<) (Abs_OrdSum (1::'a, True)) (r\<rightarrow>); \<forall>a b c. ((a l\<rightarrow> b) l\<rightarrow> c) l\<rightarrow> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c = Abs_OrdSum (1::'a, True); \<forall>a b c. ((a r\<rightarrow> b) r\<rightarrow> c) l\<rightarrow> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c = Abs_OrdSum (1::'a, True); Abs_OrdSum (1::'a, False) = Abs_OrdSum (1::'a, True); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> (1::'a, True) \<in> OrdSum
 3. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = Abs_OrdSum (1::'a, True)) (<) (Abs_OrdSum (1::'a, True)) (r\<rightarrow>); \<forall>a b c. ((a l\<rightarrow> b) l\<rightarrow> c) l\<rightarrow> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c = Abs_OrdSum (1::'a, True); \<forall>a b c. ((a r\<rightarrow> b) r\<rightarrow> c) l\<rightarrow> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c = Abs_OrdSum (1::'a, True); Abs_OrdSum (1::'a, False) = Abs_OrdSum (1::'a, True); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, False) = Abs_OrdSum (1::'a, True)
 4. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = Abs_OrdSum (1::'a, True)) (<) (Abs_OrdSum (1::'a, True)) (r\<rightarrow>); \<forall>a b c. ((a l\<rightarrow> b) l\<rightarrow> c) l\<rightarrow> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c = Abs_OrdSum (1::'a, True); \<forall>a b c. ((a r\<rightarrow> b) r\<rightarrow> c) l\<rightarrow> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c = Abs_OrdSum (1::'a, True); Abs_OrdSum (1::'a, False) = Abs_OrdSum (1::'a, True); x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a); (1::'a, False) = (1::'a, True)\<rbrakk> \<Longrightarrow> x \<le> y
 5. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False); \<not> (x l\<rightarrow> y \<noteq> (1::'a) \<and> y l\<rightarrow> x \<noteq> (1::'a))\<rbrakk> \<Longrightarrow> x \<le> y
 6. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c\<rbrakk> \<Longrightarrow> (Abs_OrdSum (x, 1) l\<rightarrow> Abs_OrdSum (y, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> ((Abs_OrdSum (y, 1) l\<rightarrow> Abs_OrdSum (x, 1)) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>); \<not> y \<le> x; class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>); \<forall>a b c. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c; \<forall>a b c. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c; Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False) \<le> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False); x l\<rightarrow> y = (1::'a) \<or> y l\<rightarrow> x = (1::'a)\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (unfold left_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = (1::'a)) (<) (1::'a) (r\<rightarrow>); y l\<rightarrow> x \<noteq> (1::'a); class.pseudo_hoop_algebra (*) (\<sqinter>) (l\<rightarrow>) (\<lambda>a b. a l\<rightarrow> b = 1) (<) 1 (r\<rightarrow>); \<forall>a b c. ((a l\<rightarrow> b) l\<rightarrow> c) l\<rightarrow> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c = 1; \<forall>a b c. ((a r\<rightarrow> b) r\<rightarrow> c) l\<rightarrow> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c = 1; (Abs_OrdSum (x l\<rightarrow> y, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> (Abs_OrdSum (y l\<rightarrow> x, 1) l\<rightarrow> Abs_OrdSum (1::'a, False)) l\<rightarrow> Abs_OrdSum (1::'a, False) = 1; x l\<rightarrow> y = (1::'a) \<or> y l\<rightarrow> x = (1::'a)\<rbrakk> \<Longrightarrow> x l\<rightarrow> y = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma null_char [simp]:
    shows "null = C.null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null = C.null
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. null = C.null
[PROOF STEP]
have "\<forall>f. C.null \<cdot> f = C.null \<and> f \<cdot> C.null = C.null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. C.null \<cdot> f = C.null \<and> f \<cdot> C.null = C.null
[PROOF STEP]
by (metis C.comp_null(1) C.ex_un_null comp_def)
[PROOF STATE]
proof (state)
this:
\<forall>f. C.null \<cdot> f = C.null \<and> f \<cdot> C.null = C.null

goal (1 subgoal):
 1. null = C.null
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>f. C.null \<cdot> f = C.null \<and> f \<cdot> C.null = C.null

goal (1 subgoal):
 1. null = C.null
[PROOF STEP]
using ex_un_null
[PROOF STATE]
proof (prove)
using this:
\<forall>f. C.null \<cdot> f = C.null \<and> f \<cdot> C.null = C.null
\<exists>!n. \<forall>f. n \<cdot> f = n \<and> f \<cdot> n = n

goal (1 subgoal):
 1. null = C.null
[PROOF STEP]
by (metis comp_null(2))
[PROOF STATE]
proof (state)
this:
null = C.null

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideI\<^sub>S\<^sub>b\<^sub>C:
    assumes "Arr a" and "C.ide a"
    shows "ide a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide a
[PROOF STEP]
unfolding ide_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> a \<noteq> null \<and> (\<forall>f. (f \<cdot> a \<noteq> null \<longrightarrow> f \<cdot> a = f) \<and> (a \<cdot> f \<noteq> null \<longrightarrow> a \<cdot> f = f))
[PROOF STEP]
using assms null_char C.ide_def comp_def
[PROOF STATE]
proof (prove)
using this:
Arr a
C.ide a
null = C.null
C.ide ?a \<equiv> ?a \<cdot>\<^sub>C ?a \<noteq> C.null \<and> (\<forall>f. (f \<cdot>\<^sub>C ?a \<noteq> C.null \<longrightarrow> f \<cdot>\<^sub>C ?a = f) \<and> (?a \<cdot>\<^sub>C f \<noteq> C.null \<longrightarrow> ?a \<cdot>\<^sub>C f = f))
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)

goal (1 subgoal):
 1. a \<cdot> a \<noteq> null \<and> (\<forall>f. (f \<cdot> a \<noteq> null \<longrightarrow> f \<cdot> a = f) \<and> (a \<cdot> f \<noteq> null \<longrightarrow> a \<cdot> f = f))
[PROOF STEP]
by auto


[STATEMENT]
lemma Arr_iff_dom_in_domain:
    shows "Arr f \<longleftrightarrow> C.dom f \<in> domains f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arr f = (C.dom f \<in> domains f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
 2. C.dom f \<in> domains f \<Longrightarrow> Arr f
[PROOF STEP]
show "C.dom f \<in> domains f \<Longrightarrow> Arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.dom f \<in> domains f \<Longrightarrow> Arr f
[PROOF STEP]
using domains_def comp_def ide_def
[PROOF STATE]
proof (prove)
using this:
domains ?f \<equiv> {a. ide a \<and> ?f \<cdot> a \<noteq> null}
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
ide ?a \<equiv> ?a \<cdot> ?a \<noteq> null \<and> (\<forall>f. (f \<cdot> ?a \<noteq> null \<longrightarrow> f \<cdot> ?a = f) \<and> (?a \<cdot> f \<noteq> null \<longrightarrow> ?a \<cdot> f = f))

goal (1 subgoal):
 1. C.dom f \<in> domains f \<Longrightarrow> Arr f
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
C.dom f \<in> domains f \<Longrightarrow> Arr f

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
[PROOF STEP]
show "Arr f \<Longrightarrow> C.dom f \<in> domains f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
[PROOF STEP]
assume f: "Arr f"
[PROOF STATE]
proof (state)
this:
Arr f

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
[PROOF STEP]
have "ide (C.dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (C.dom f)
[PROOF STEP]
using f inclusion C.dom_in_domains C.has_domain_iff_arr C.domains_def
                dom_closed ideI\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
Arr f
Arr ?f \<Longrightarrow> C.arr ?f
C.domains ?f \<noteq> {} \<Longrightarrow> C.dom ?f \<in> C.domains ?f
(C.domains ?f \<noteq> {}) = C.arr ?f
C.domains ?f \<equiv> {a. C.ide a \<and> ?f \<cdot>\<^sub>C a \<noteq> C.null}
Arr ?f \<Longrightarrow> Arr (C.dom ?f)
\<lbrakk>Arr ?a; C.ide ?a\<rbrakk> \<Longrightarrow> ide ?a

goal (1 subgoal):
 1. ide (C.dom f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ide (C.dom f)

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (C.dom f)

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
[PROOF STEP]
have "f \<cdot> C.dom f \<noteq> null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<cdot> C.dom f \<noteq> null
[PROOF STEP]
using f comp_def dom_closed null_char inclusion C.comp_arr_dom
[PROOF STATE]
proof (prove)
using this:
Arr f
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
Arr ?f \<Longrightarrow> Arr (C.dom ?f)
null = C.null
Arr ?f \<Longrightarrow> C.arr ?f
\<lbrakk>C.arr ?f; C.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot>\<^sub>C ?a = ?f

goal (1 subgoal):
 1. f \<cdot> C.dom f \<noteq> null
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f \<cdot> C.dom f \<noteq> null

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.dom f \<in> domains f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (C.dom f)
f \<cdot> C.dom f \<noteq> null
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (C.dom f)
f \<cdot> C.dom f \<noteq> null

goal (1 subgoal):
 1. C.dom f \<in> domains f
[PROOF STEP]
using domains_def
[PROOF STATE]
proof (prove)
using this:
ide (C.dom f)
f \<cdot> C.dom f \<noteq> null
domains ?f \<equiv> {a. ide a \<and> ?f \<cdot> a \<noteq> null}

goal (1 subgoal):
 1. C.dom f \<in> domains f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.dom f \<in> domains f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Arr f \<Longrightarrow> C.dom f \<in> domains f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Arr_iff_cod_in_codomain:
    shows "Arr f \<longleftrightarrow> C.cod f \<in> codomains f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arr f = (C.cod f \<in> codomains f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
 2. C.cod f \<in> codomains f \<Longrightarrow> Arr f
[PROOF STEP]
show "C.cod f \<in> codomains f \<Longrightarrow> Arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.cod f \<in> codomains f \<Longrightarrow> Arr f
[PROOF STEP]
using codomains_def comp_def ide_def
[PROOF STATE]
proof (prove)
using this:
codomains ?f \<equiv> {b. ide b \<and> b \<cdot> ?f \<noteq> null}
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
ide ?a \<equiv> ?a \<cdot> ?a \<noteq> null \<and> (\<forall>f. (f \<cdot> ?a \<noteq> null \<longrightarrow> f \<cdot> ?a = f) \<and> (?a \<cdot> f \<noteq> null \<longrightarrow> ?a \<cdot> f = f))

goal (1 subgoal):
 1. C.cod f \<in> codomains f \<Longrightarrow> Arr f
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
C.cod f \<in> codomains f \<Longrightarrow> Arr f

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
[PROOF STEP]
show "Arr f \<Longrightarrow> C.cod f \<in> codomains f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
[PROOF STEP]
assume f: "Arr f"
[PROOF STATE]
proof (state)
this:
Arr f

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
[PROOF STEP]
have "ide (C.cod f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (C.cod f)
[PROOF STEP]
using f inclusion C.cod_in_codomains C.has_codomain_iff_arr C.codomains_def
                cod_closed ideI\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
Arr f
Arr ?f \<Longrightarrow> C.arr ?f
C.codomains ?f \<noteq> {} \<Longrightarrow> C.cod ?f \<in> C.codomains ?f
(C.codomains ?f \<noteq> {}) = C.arr ?f
C.codomains ?f \<equiv> {b. C.ide b \<and> b \<cdot>\<^sub>C ?f \<noteq> C.null}
Arr ?f \<Longrightarrow> Arr (C.cod ?f)
\<lbrakk>Arr ?a; C.ide ?a\<rbrakk> \<Longrightarrow> ide ?a

goal (1 subgoal):
 1. ide (C.cod f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ide (C.cod f)

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (C.cod f)

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
[PROOF STEP]
have "C.cod f \<cdot> f \<noteq> null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.cod f \<cdot> f \<noteq> null
[PROOF STEP]
using f comp_def cod_closed null_char inclusion C.comp_cod_arr
[PROOF STATE]
proof (prove)
using this:
Arr f
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
Arr ?f \<Longrightarrow> Arr (C.cod ?f)
null = C.null
Arr ?f \<Longrightarrow> C.arr ?f
\<lbrakk>C.arr ?f; C.cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot>\<^sub>C ?f = ?f

goal (1 subgoal):
 1. C.cod f \<cdot> f \<noteq> null
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
C.cod f \<cdot> f \<noteq> null

goal (1 subgoal):
 1. Arr f \<Longrightarrow> C.cod f \<in> codomains f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (C.cod f)
C.cod f \<cdot> f \<noteq> null
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (C.cod f)
C.cod f \<cdot> f \<noteq> null

goal (1 subgoal):
 1. C.cod f \<in> codomains f
[PROOF STEP]
using codomains_def
[PROOF STATE]
proof (prove)
using this:
ide (C.cod f)
C.cod f \<cdot> f \<noteq> null
codomains ?f \<equiv> {b. ide b \<and> b \<cdot> ?f \<noteq> null}

goal (1 subgoal):
 1. C.cod f \<in> codomains f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.cod f \<in> codomains f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Arr f \<Longrightarrow> C.cod f \<in> codomains f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arr_char\<^sub>S\<^sub>b\<^sub>C:
    shows "arr f \<longleftrightarrow> Arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr f = Arr f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. arr f \<Longrightarrow> Arr f
 2. Arr f \<Longrightarrow> arr f
[PROOF STEP]
show "Arr f \<Longrightarrow> arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arr f \<Longrightarrow> arr f
[PROOF STEP]
using arr_def comp_def Arr_iff_dom_in_domain Arr_iff_cod_in_codomain
[PROOF STATE]
proof (prove)
using this:
arr ?f \<equiv> domains ?f \<noteq> {} \<or> codomains ?f \<noteq> {}
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
Arr ?f = (C.dom ?f \<in> domains ?f)
Arr ?f = (C.cod ?f \<in> codomains ?f)

goal (1 subgoal):
 1. Arr f \<Longrightarrow> arr f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arr f \<Longrightarrow> arr f

goal (1 subgoal):
 1. arr f \<Longrightarrow> Arr f
[PROOF STEP]
show "arr f \<Longrightarrow> Arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr f \<Longrightarrow> Arr f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arr f \<Longrightarrow> Arr f
[PROOF STEP]
assume f: "arr f"
[PROOF STATE]
proof (state)
this:
arr f

goal (1 subgoal):
 1. arr f \<Longrightarrow> Arr f
[PROOF STEP]
obtain a where a: "a \<in> domains f \<or> a \<in> codomains f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> domains f \<or> a \<in> codomains f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f arr_def
[PROOF STATE]
proof (prove)
using this:
arr f
arr ?f \<equiv> domains ?f \<noteq> {} \<or> codomains ?f \<noteq> {}

goal (1 subgoal):
 1. (\<And>a. a \<in> domains f \<or> a \<in> codomains f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> domains f \<or> a \<in> codomains f

goal (1 subgoal):
 1. arr f \<Longrightarrow> Arr f
[PROOF STEP]
have "f \<cdot> a \<noteq> C.null \<or> a \<cdot> f \<noteq> C.null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<cdot> a \<noteq> C.null \<or> a \<cdot> f \<noteq> C.null
[PROOF STEP]
using a domains_def codomains_def null_char
[PROOF STATE]
proof (prove)
using this:
a \<in> domains f \<or> a \<in> codomains f
domains ?f \<equiv> {a. ide a \<and> ?f \<cdot> a \<noteq> null}
codomains ?f \<equiv> {b. ide b \<and> b \<cdot> ?f \<noteq> null}
null = C.null

goal (1 subgoal):
 1. f \<cdot> a \<noteq> C.null \<or> a \<cdot> f \<noteq> C.null
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<cdot> a \<noteq> C.null \<or> a \<cdot> f \<noteq> C.null

goal (1 subgoal):
 1. arr f \<Longrightarrow> Arr f
[PROOF STEP]
thus "Arr f"
[PROOF STATE]
proof (prove)
using this:
f \<cdot> a \<noteq> C.null \<or> a \<cdot> f \<noteq> C.null

goal (1 subgoal):
 1. Arr f
[PROOF STEP]
using comp_def
[PROOF STATE]
proof (prove)
using this:
f \<cdot> a \<noteq> C.null \<or> a \<cdot> f \<noteq> C.null
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)

goal (1 subgoal):
 1. Arr f
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Arr f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
arr f \<Longrightarrow> Arr f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arrI\<^sub>S\<^sub>b\<^sub>C [intro]:
    assumes "Arr f"
    shows "arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr f
[PROOF STEP]
using assms arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
Arr f
arr ?f = Arr ?f

goal (1 subgoal):
 1. arr f
[PROOF STEP]
by simp


[STATEMENT]
lemma arrE [elim]:
    assumes "arr f"
    shows "Arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arr f
[PROOF STEP]
using assms arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
arr ?f = Arr ?f

goal (1 subgoal):
 1. Arr f
[PROOF STEP]
by simp


[STATEMENT]
theorem is_category:
    shows "category comp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category (\<cdot>)
[PROOF STEP]
..


[STATEMENT]
lemma dom_simp:
    assumes "arr f"
    shows "dom f = C.dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom f = C.dom f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.dom f = C.dom f
[PROOF STEP]
have "ide (C.dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (C.dom f)
[PROOF STEP]
using assms ideI\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
\<lbrakk>Arr ?a; C.ide ?a\<rbrakk> \<Longrightarrow> ide ?a

goal (1 subgoal):
 1. ide (C.dom f)
[PROOF STEP]
by (meson C.ide_dom arr_char\<^sub>S\<^sub>b\<^sub>C dom_closed inclusion)
[PROOF STATE]
proof (state)
this:
ide (C.dom f)

goal (1 subgoal):
 1. local.dom f = C.dom f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (C.dom f)

goal (1 subgoal):
 1. local.dom f = C.dom f
[PROOF STEP]
have "f \<cdot> C.dom f \<noteq> null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<cdot> C.dom f \<noteq> null
[PROOF STEP]
using assms inclusion comp_def null_char dom_closed not_arr_null C.comp_arr_dom arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
Arr ?f \<Longrightarrow> C.arr ?f
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
null = C.null
Arr ?f \<Longrightarrow> Arr (C.dom ?f)
\<not> arr null
\<lbrakk>C.arr ?f; C.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot>\<^sub>C ?a = ?f
arr ?f = Arr ?f

goal (1 subgoal):
 1. f \<cdot> C.dom f \<noteq> null
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<cdot> C.dom f \<noteq> null

goal (1 subgoal):
 1. local.dom f = C.dom f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (C.dom f)
f \<cdot> C.dom f \<noteq> null
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (C.dom f)
f \<cdot> C.dom f \<noteq> null

goal (1 subgoal):
 1. local.dom f = C.dom f
[PROOF STEP]
using dom_eqI ext
[PROOF STATE]
proof (prove)
using this:
ide (C.dom f)
f \<cdot> C.dom f \<noteq> null
\<lbrakk>ide ?a; seq ?f ?a\<rbrakk> \<Longrightarrow> local.dom ?f = ?a
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. local.dom f = C.dom f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.dom f = C.dom f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dom_char\<^sub>S\<^sub>b\<^sub>C:
    shows "dom f = (if arr f then C.dom f else C.null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom f = (if arr f then C.dom f else C.null)
[PROOF STEP]
using dom_simp dom_def arr_def arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr ?f \<Longrightarrow> local.dom ?f = C.dom ?f
local.dom ?f = (if domains ?f \<noteq> {} then SOME a. a \<in> domains ?f else null)
arr ?f \<equiv> domains ?f \<noteq> {} \<or> codomains ?f \<noteq> {}
arr ?f = Arr ?f

goal (1 subgoal):
 1. local.dom f = (if arr f then C.dom f else C.null)
[PROOF STEP]
by auto


[STATEMENT]
lemma cod_simp:
    assumes "arr f"
    shows "cod f = C.cod f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod f = C.cod f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cod f = C.cod f
[PROOF STEP]
have "ide (C.cod f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (C.cod f)
[PROOF STEP]
using assms ideI\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
\<lbrakk>Arr ?a; C.ide ?a\<rbrakk> \<Longrightarrow> ide ?a

goal (1 subgoal):
 1. ide (C.cod f)
[PROOF STEP]
by (meson C.ide_cod arr_char\<^sub>S\<^sub>b\<^sub>C cod_closed inclusion)
[PROOF STATE]
proof (state)
this:
ide (C.cod f)

goal (1 subgoal):
 1. cod f = C.cod f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (C.cod f)

goal (1 subgoal):
 1. cod f = C.cod f
[PROOF STEP]
have "C.cod f \<cdot> f \<noteq> null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.cod f \<cdot> f \<noteq> null
[PROOF STEP]
using assms inclusion comp_def null_char cod_closed not_arr_null C.comp_cod_arr arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
Arr ?f \<Longrightarrow> C.arr ?f
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
null = C.null
Arr ?f \<Longrightarrow> Arr (C.cod ?f)
\<not> arr null
\<lbrakk>C.arr ?f; C.cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot>\<^sub>C ?f = ?f
arr ?f = Arr ?f

goal (1 subgoal):
 1. C.cod f \<cdot> f \<noteq> null
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C.cod f \<cdot> f \<noteq> null

goal (1 subgoal):
 1. cod f = C.cod f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (C.cod f)
C.cod f \<cdot> f \<noteq> null
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (C.cod f)
C.cod f \<cdot> f \<noteq> null

goal (1 subgoal):
 1. cod f = C.cod f
[PROOF STEP]
using cod_eqI ext
[PROOF STATE]
proof (prove)
using this:
ide (C.cod f)
C.cod f \<cdot> f \<noteq> null
\<lbrakk>ide ?b; seq ?b ?f\<rbrakk> \<Longrightarrow> cod ?f = ?b
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. cod f = C.cod f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cod f = C.cod f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cod_char\<^sub>S\<^sub>b\<^sub>C:
    shows "cod f = (if arr f then C.cod f else C.null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod f = (if arr f then C.cod f else C.null)
[PROOF STEP]
using cod_simp cod_def arr_def
[PROOF STATE]
proof (prove)
using this:
arr ?f \<Longrightarrow> cod ?f = C.cod ?f
cod ?f = (if codomains ?f \<noteq> {} then SOME b. b \<in> codomains ?f else null)
arr ?f \<equiv> domains ?f \<noteq> {} \<or> codomains ?f \<noteq> {}

goal (1 subgoal):
 1. cod f = (if arr f then C.cod f else C.null)
[PROOF STEP]
by auto


[STATEMENT]
lemma in_hom_char\<^sub>S\<^sub>b\<^sub>C:
    shows "\<guillemotleft>f : a \<rightarrow> b\<guillemotright> \<longleftrightarrow> arr a \<and> arr b \<and> arr f \<and> \<guillemotleft>f : a \<rightarrow>\<^sub>C b\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f : a \<rightarrow> b\<guillemotright> = (arr a \<and> arr b \<and> arr f \<and> \<guillemotleft>f : a \<rightarrow>\<^sub>C b\<guillemotright>)
[PROOF STEP]
using inclusion arr_char\<^sub>S\<^sub>b\<^sub>C cod_closed dom_closed
[PROOF STATE]
proof (prove)
using this:
Arr ?f \<Longrightarrow> C.arr ?f
arr ?f = Arr ?f
Arr ?f \<Longrightarrow> Arr (C.cod ?f)
Arr ?f \<Longrightarrow> Arr (C.dom ?f)

goal (1 subgoal):
 1. \<guillemotleft>f : a \<rightarrow> b\<guillemotright> = (arr a \<and> arr b \<and> arr f \<and> \<guillemotleft>f : a \<rightarrow>\<^sub>C b\<guillemotright>)
[PROOF STEP]
by (metis C.arr_iff_in_hom C.in_homE arr_iff_in_hom cod_simp dom_simp in_homE)


[STATEMENT]
lemma ide_char\<^sub>S\<^sub>b\<^sub>C:
    shows "ide a \<longleftrightarrow> arr a \<and> C.ide a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide a = (arr a \<and> C.ide a)
[PROOF STEP]
using ide_in_hom C.ide_in_hom in_hom_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide ?a = \<guillemotleft>?a : ?a \<rightarrow> ?a\<guillemotright>
C.ide ?a = \<guillemotleft>?a : ?a \<rightarrow>\<^sub>C ?a\<guillemotright>
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> arr ?f \<and> \<guillemotleft>?f : ?a \<rightarrow>\<^sub>C ?b\<guillemotright>)

goal (1 subgoal):
 1. ide a = (arr a \<and> C.ide a)
[PROOF STEP]
by simp


[STATEMENT]
lemma seq_char\<^sub>S\<^sub>b\<^sub>C:
    shows "seq g f \<longleftrightarrow> arr f \<and> arr g \<and> C.seq g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq g f = (arr f \<and> arr g \<and> C.seq g f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. seq g f \<Longrightarrow> arr f \<and> arr g \<and> C.seq g f
 2. arr f \<and> arr g \<and> C.seq g f \<Longrightarrow> seq g f
[PROOF STEP]
show "arr f \<and> arr g \<and> C.seq g f \<Longrightarrow> seq g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr f \<and> arr g \<and> C.seq g f \<Longrightarrow> seq g f
[PROOF STEP]
using arr_char\<^sub>S\<^sub>b\<^sub>C dom_char\<^sub>S\<^sub>b\<^sub>C cod_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr ?f = Arr ?f
local.dom ?f = (if arr ?f then C.dom ?f else C.null)
cod ?f = (if arr ?f then C.cod ?f else C.null)

goal (1 subgoal):
 1. arr f \<and> arr g \<and> C.seq g f \<Longrightarrow> seq g f
[PROOF STEP]
by (intro seqI, auto)
[PROOF STATE]
proof (state)
this:
arr f \<and> arr g \<and> C.seq g f \<Longrightarrow> seq g f

goal (1 subgoal):
 1. seq g f \<Longrightarrow> arr f \<and> arr g \<and> C.seq g f
[PROOF STEP]
show "seq g f \<Longrightarrow> arr f \<and> arr g \<and> C.seq g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq g f \<Longrightarrow> arr f \<and> arr g \<and> C.seq g f
[PROOF STEP]
apply (elim seqE, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arr f; arr g; local.dom g = cod f\<rbrakk> \<Longrightarrow> C.seq g f
[PROOF STEP]
using inclusion arr_char\<^sub>S\<^sub>b\<^sub>C dom_simp cod_simp
[PROOF STATE]
proof (prove)
using this:
Arr ?f \<Longrightarrow> C.arr ?f
arr ?f = Arr ?f
arr ?f \<Longrightarrow> local.dom ?f = C.dom ?f
arr ?f \<Longrightarrow> cod ?f = C.cod ?f

goal (1 subgoal):
 1. \<lbrakk>arr f; arr g; local.dom g = cod f\<rbrakk> \<Longrightarrow> C.seq g f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
seq g f \<Longrightarrow> arr f \<and> arr g \<and> C.seq g f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hom_char:
    shows "hom a b = C.hom a b \<inter> Collect Arr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hom a b = C.hom a b \<inter> Collect Arr
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hom a b \<subseteq> C.hom a b \<inter> Collect Arr
 2. C.hom a b \<inter> Collect Arr \<subseteq> hom a b
[PROOF STEP]
show "hom a b \<subseteq> C.hom a b \<inter> Collect Arr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hom a b \<subseteq> C.hom a b \<inter> Collect Arr
[PROOF STEP]
using in_hom_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> arr ?f \<and> \<guillemotleft>?f : ?a \<rightarrow>\<^sub>C ?b\<guillemotright>)

goal (1 subgoal):
 1. hom a b \<subseteq> C.hom a b \<inter> Collect Arr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hom a b \<subseteq> C.hom a b \<inter> Collect Arr

goal (1 subgoal):
 1. C.hom a b \<inter> Collect Arr \<subseteq> hom a b
[PROOF STEP]
show "C.hom a b \<inter> Collect Arr \<subseteq> hom a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.hom a b \<inter> Collect Arr \<subseteq> hom a b
[PROOF STEP]
using arr_char\<^sub>S\<^sub>b\<^sub>C dom_char\<^sub>S\<^sub>b\<^sub>C cod_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr ?f = Arr ?f
local.dom ?f = (if arr ?f then C.dom ?f else C.null)
cod ?f = (if arr ?f then C.cod ?f else C.null)

goal (1 subgoal):
 1. C.hom a b \<inter> Collect Arr \<subseteq> hom a b
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
C.hom a b \<inter> Collect Arr \<subseteq> hom a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_char:
    shows "g \<cdot> f = (if arr f \<and> arr g \<and> C.seq g f then g \<cdot>\<^sub>C f else C.null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<cdot> f = (if arr f \<and> arr g \<and> C.seq g f then g \<cdot>\<^sub>C f else C.null)
[PROOF STEP]
using arr_char\<^sub>S\<^sub>b\<^sub>C comp_def comp_closed C.ext
[PROOF STATE]
proof (prove)
using this:
arr ?f = Arr ?f
?g \<cdot> ?f = (if Arr ?f \<and> Arr ?g \<and> C.cod ?f = C.dom ?g then ?g \<cdot>\<^sub>C ?f else C.null)
\<lbrakk>Arr ?f; Arr ?g; C.cod ?f = C.dom ?g\<rbrakk> \<Longrightarrow> Arr (?g \<cdot>\<^sub>C ?f)
?g \<cdot>\<^sub>C ?f \<noteq> C.null \<Longrightarrow> C.seq ?g ?f

goal (1 subgoal):
 1. g \<cdot> f = (if arr f \<and> arr g \<and> C.seq g f then g \<cdot>\<^sub>C f else C.null)
[PROOF STEP]
by force


[STATEMENT]
lemma comp_simp:
    assumes "seq g f"
    shows "g \<cdot> f = g \<cdot>\<^sub>C f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<cdot> f = g \<cdot>\<^sub>C f
[PROOF STEP]
using assms comp_char seq_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
seq g f
?g \<cdot> ?f = (if arr ?f \<and> arr ?g \<and> C.seq ?g ?f then ?g \<cdot>\<^sub>C ?f else C.null)
seq ?g ?f = (arr ?f \<and> arr ?g \<and> C.seq ?g ?f)

goal (1 subgoal):
 1. g \<cdot> f = g \<cdot>\<^sub>C f
[PROOF STEP]
by metis


[STATEMENT]
lemma inclusion_preserves_inverse:
    assumes "inverse_arrows f g"
    shows "C.inverse_arrows f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.inverse_arrows f g
[PROOF STEP]
using assms ide_char\<^sub>S\<^sub>b\<^sub>C comp_simp arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
inverse_arrows f g
ide ?a = (arr ?a \<and> C.ide ?a)
seq ?g ?f \<Longrightarrow> ?g \<cdot> ?f = ?g \<cdot>\<^sub>C ?f
arr ?f = Arr ?f

goal (1 subgoal):
 1. C.inverse_arrows f g
[PROOF STEP]
by (intro C.inverse_arrowsI, auto)


[STATEMENT]
lemma iso_char\<^sub>S\<^sub>b\<^sub>C:
    shows "iso f \<longleftrightarrow> C.iso f \<and> arr f \<and> arr (C.inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.iso f = (C.iso f \<and> arr f \<and> arr (C.inv f))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. local.iso f \<Longrightarrow> C.iso f \<and> arr f \<and> arr (C.inv f)
 2. C.iso f \<and> arr f \<and> arr (C.inv f) \<Longrightarrow> local.iso f
[PROOF STEP]
assume f: "iso f"
[PROOF STATE]
proof (state)
this:
local.iso f

goal (2 subgoals):
 1. local.iso f \<Longrightarrow> C.iso f \<and> arr f \<and> arr (C.inv f)
 2. C.iso f \<and> arr f \<and> arr (C.inv f) \<Longrightarrow> local.iso f
[PROOF STEP]
show "C.iso f \<and> arr f \<and> arr (C.inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
have 1: "inverse_arrows f (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_arrows f (local.inv f)
[PROOF STEP]
using f inv_is_inverse
[PROOF STATE]
proof (prove)
using this:
local.iso f
local.iso ?f \<Longrightarrow> inverse_arrows ?f (local.inv ?f)

goal (1 subgoal):
 1. inverse_arrows f (local.inv f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inverse_arrows f (local.inv f)

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
have 2: "C.inverse_arrows f (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.inverse_arrows f (local.inv f)
[PROOF STEP]
using 1 inclusion_preserves_inverse
[PROOF STATE]
proof (prove)
using this:
inverse_arrows f (local.inv f)
inverse_arrows ?f ?g \<Longrightarrow> C.inverse_arrows ?f ?g

goal (1 subgoal):
 1. C.inverse_arrows f (local.inv f)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C.inverse_arrows f (local.inv f)

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C.inverse_arrows f (local.inv f)

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
have "arr (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr (local.inv f)
[PROOF STEP]
using 1 iso_is_arr
[PROOF STATE]
proof (prove)
using this:
inverse_arrows f (local.inv f)
local.iso ?f \<Longrightarrow> arr ?f

goal (1 subgoal):
 1. arr (local.inv f)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
arr (local.inv f)

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arr (local.inv f)

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
have "inv f = C.inv f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv f = C.inv f
[PROOF STEP]
using 1 2 C.inv_is_inverse C.inverse_arrow_unique
[PROOF STATE]
proof (prove)
using this:
inverse_arrows f (local.inv f)
C.inverse_arrows f (local.inv f)
C.iso ?f \<Longrightarrow> C.inverse_arrows ?f (C.inv ?f)
\<lbrakk>C.inverse_arrows ?f ?g; C.inverse_arrows ?f ?g'\<rbrakk> \<Longrightarrow> ?g = ?g'

goal (1 subgoal):
 1. local.inv f = C.inv f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.inv f = C.inv f

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C.inverse_arrows f (local.inv f)
arr (local.inv f)
local.inv f = C.inv f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f (local.inv f)
arr (local.inv f)
local.inv f = C.inv f

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
using f 2 iso_is_arr
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f (local.inv f)
arr (local.inv f)
local.inv f = C.inv f
local.iso f
C.inverse_arrows f (local.inv f)
local.iso ?f \<Longrightarrow> arr ?f

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C.iso f \<and> arr f \<and> arr (C.inv f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C.iso f \<and> arr f \<and> arr (C.inv f)

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f) \<Longrightarrow> local.iso f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f) \<Longrightarrow> local.iso f
[PROOF STEP]
assume f: "C.iso f \<and> arr f \<and> arr (C.inv f)"
[PROOF STATE]
proof (state)
this:
C.iso f \<and> arr f \<and> arr (C.inv f)

goal (1 subgoal):
 1. C.iso f \<and> arr f \<and> arr (C.inv f) \<Longrightarrow> local.iso f
[PROOF STEP]
show "iso f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.iso f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse_arrows f ?g
[PROOF STEP]
have 1: "C.inverse_arrows f (C.inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.inverse_arrows f (C.inv f)
[PROOF STEP]
using f C.inv_is_inverse
[PROOF STATE]
proof (prove)
using this:
C.iso f \<and> arr f \<and> arr (C.inv f)
C.iso ?f \<Longrightarrow> C.inverse_arrows ?f (C.inv ?f)

goal (1 subgoal):
 1. C.inverse_arrows f (C.inv f)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C.inverse_arrows f (C.inv f)

goal (1 subgoal):
 1. inverse_arrows f ?g
[PROOF STEP]
show "inverse_arrows f (C.inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_arrows f (C.inv f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ide (C.inv f \<cdot> f)
 2. ide (f \<cdot> C.inv f)
[PROOF STEP]
have 2: "C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f
[PROOF STEP]
using f 1 comp_char
[PROOF STATE]
proof (prove)
using this:
C.iso f \<and> arr f \<and> arr (C.inv f)
C.inverse_arrows f (C.inv f)
?g \<cdot> ?f = (if arr ?f \<and> arr ?g \<and> C.seq ?g ?f then ?g \<cdot>\<^sub>C ?f else C.null)

goal (1 subgoal):
 1. C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f

goal (2 subgoals):
 1. ide (C.inv f \<cdot> f)
 2. ide (f \<cdot> C.inv f)
[PROOF STEP]
have 3: "antipar f (C.inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antipar f (C.inv f)
[PROOF STEP]
using f C.seqE seqI dom_simp cod_simp
[PROOF STATE]
proof (prove)
using this:
C.iso f \<and> arr f \<and> arr (C.inv f)
\<lbrakk>C.seq ?g ?f; \<lbrakk>C.arr ?f; C.arr ?g; C.dom ?g = C.cod ?f\<rbrakk> \<Longrightarrow> ?T\<rbrakk> \<Longrightarrow> ?T
\<lbrakk>arr ?f; arr ?g; local.dom ?g = cod ?f\<rbrakk> \<Longrightarrow> seq ?g ?f
arr ?f \<Longrightarrow> local.dom ?f = C.dom ?f
arr ?f \<Longrightarrow> cod ?f = C.cod ?f

goal (1 subgoal):
 1. antipar f (C.inv f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
antipar f (C.inv f)

goal (2 subgoals):
 1. ide (C.inv f \<cdot> f)
 2. ide (f \<cdot> C.inv f)
[PROOF STEP]
show "ide (C.inv f \<cdot> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (C.inv f \<cdot> f)
[PROOF STEP]
using 1 2 3 ide_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f (C.inv f)
C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f
antipar f (C.inv f)
ide ?a = (arr ?a \<and> C.ide ?a)

goal (1 subgoal):
 1. ide (C.inv f \<cdot> f)
[PROOF STEP]
apply (elim C.inverse_arrowsE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f; antipar f (C.inv f); \<And>a. ide a = (arr a \<and> C.ide a); C.ide (C.inv f \<cdot>\<^sub>C f); C.ide (f \<cdot>\<^sub>C C.inv f)\<rbrakk> \<Longrightarrow> ide (C.inv f \<cdot> f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide (C.inv f \<cdot> f)

goal (1 subgoal):
 1. ide (f \<cdot> C.inv f)
[PROOF STEP]
show "ide (f \<cdot> C.inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (f \<cdot> C.inv f)
[PROOF STEP]
using 1 2 3 ide_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f (C.inv f)
C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f
antipar f (C.inv f)
ide ?a = (arr ?a \<and> C.ide ?a)

goal (1 subgoal):
 1. ide (f \<cdot> C.inv f)
[PROOF STEP]
apply (elim C.inverse_arrowsE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C.inv f \<cdot> f = C.inv f \<cdot>\<^sub>C f \<and> f \<cdot> C.inv f = f \<cdot>\<^sub>C C.inv f; antipar f (C.inv f); \<And>a. ide a = (arr a \<and> C.ide a); C.ide (C.inv f \<cdot>\<^sub>C f); C.ide (f \<cdot>\<^sub>C C.inv f)\<rbrakk> \<Longrightarrow> ide (f \<cdot> C.inv f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide (f \<cdot> C.inv f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverse_arrows f (C.inv f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.iso f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_char\<^sub>S\<^sub>b\<^sub>C:
    assumes "iso f"
    shows "inv f = C.inv f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv f = C.inv f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.inv f = C.inv f
[PROOF STEP]
have "C.inverse_arrows f (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.inverse_arrows f (local.inv f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C.ide (local.inv f \<cdot>\<^sub>C f)
 2. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
have 1: "inverse_arrows f (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_arrows f (local.inv f)
[PROOF STEP]
using assms iso_char\<^sub>S\<^sub>b\<^sub>C inv_is_inverse
[PROOF STATE]
proof (prove)
using this:
local.iso f
local.iso ?f = (C.iso ?f \<and> arr ?f \<and> arr (C.inv ?f))
local.iso ?f \<Longrightarrow> inverse_arrows ?f (local.inv ?f)

goal (1 subgoal):
 1. inverse_arrows f (local.inv f)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse_arrows f (local.inv f)

goal (2 subgoals):
 1. C.ide (local.inv f \<cdot>\<^sub>C f)
 2. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
show "C.ide (inv f \<cdot>\<^sub>C f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.ide (local.inv f \<cdot>\<^sub>C f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C.ide (local.inv f \<cdot>\<^sub>C f)
[PROOF STEP]
have "inv f \<cdot> f = inv f \<cdot>\<^sub>C f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv f \<cdot> f = local.inv f \<cdot>\<^sub>C f
[PROOF STEP]
using assms 1 inv_in_hom iso_char\<^sub>S\<^sub>b\<^sub>C [of f] comp_char [of "inv f" f] seq_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
local.iso f
inverse_arrows f (local.inv f)
\<lbrakk>local.iso ?f; \<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright>\<rbrakk> \<Longrightarrow> \<guillemotleft>local.inv ?f : ?b \<rightarrow> ?a\<guillemotright>
local.iso f = (C.iso f \<and> arr f \<and> arr (C.inv f))
local.inv f \<cdot> f = (if arr f \<and> arr (local.inv f) \<and> C.seq (local.inv f) f then local.inv f \<cdot>\<^sub>C f else C.null)
seq ?g ?f = (arr ?f \<and> arr ?g \<and> C.seq ?g ?f)

goal (1 subgoal):
 1. local.inv f \<cdot> f = local.inv f \<cdot>\<^sub>C f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.inv f \<cdot> f = local.inv f \<cdot>\<^sub>C f

goal (1 subgoal):
 1. C.ide (local.inv f \<cdot>\<^sub>C f)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
local.inv f \<cdot> f = local.inv f \<cdot>\<^sub>C f

goal (1 subgoal):
 1. C.ide (local.inv f \<cdot>\<^sub>C f)
[PROOF STEP]
using 1 ide_char\<^sub>S\<^sub>b\<^sub>C arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
local.inv f \<cdot> f = local.inv f \<cdot>\<^sub>C f
inverse_arrows f (local.inv f)
ide ?a = (arr ?a \<and> C.ide ?a)
arr ?f = Arr ?f

goal (1 subgoal):
 1. C.ide (local.inv f \<cdot>\<^sub>C f)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
C.ide (local.inv f \<cdot>\<^sub>C f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C.ide (local.inv f \<cdot>\<^sub>C f)

goal (1 subgoal):
 1. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
show "C.ide (f \<cdot>\<^sub>C inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
have "f \<cdot> inv f = f \<cdot>\<^sub>C inv f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<cdot> local.inv f = f \<cdot>\<^sub>C local.inv f
[PROOF STEP]
using assms 1 inv_in_hom iso_char\<^sub>S\<^sub>b\<^sub>C [of f] comp_char [of f "inv f"] seq_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
local.iso f
inverse_arrows f (local.inv f)
\<lbrakk>local.iso ?f; \<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright>\<rbrakk> \<Longrightarrow> \<guillemotleft>local.inv ?f : ?b \<rightarrow> ?a\<guillemotright>
local.iso f = (C.iso f \<and> arr f \<and> arr (C.inv f))
f \<cdot> local.inv f = (if arr (local.inv f) \<and> arr f \<and> C.seq f (local.inv f) then f \<cdot>\<^sub>C local.inv f else C.null)
seq ?g ?f = (arr ?f \<and> arr ?g \<and> C.seq ?g ?f)

goal (1 subgoal):
 1. f \<cdot> local.inv f = f \<cdot>\<^sub>C local.inv f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<cdot> local.inv f = f \<cdot>\<^sub>C local.inv f

goal (1 subgoal):
 1. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<cdot> local.inv f = f \<cdot>\<^sub>C local.inv f

goal (1 subgoal):
 1. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
using 1 ide_char\<^sub>S\<^sub>b\<^sub>C arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
f \<cdot> local.inv f = f \<cdot>\<^sub>C local.inv f
inverse_arrows f (local.inv f)
ide ?a = (arr ?a \<and> C.ide ?a)
arr ?f = Arr ?f

goal (1 subgoal):
 1. C.ide (f \<cdot>\<^sub>C local.inv f)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
C.ide (f \<cdot>\<^sub>C local.inv f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C.ide (f \<cdot>\<^sub>C local.inv f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C.inverse_arrows f (local.inv f)

goal (1 subgoal):
 1. local.inv f = C.inv f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f (local.inv f)

goal (1 subgoal):
 1. local.inv f = C.inv f
[PROOF STEP]
using C.inverse_arrow_unique C.inv_is_inverse
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f (local.inv f)
\<lbrakk>C.inverse_arrows ?f ?g; C.inverse_arrows ?f ?g'\<rbrakk> \<Longrightarrow> ?g = ?g'
C.iso ?f \<Longrightarrow> C.inverse_arrows ?f (C.inv ?f)

goal (1 subgoal):
 1. local.inv f = C.inv f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.inv f = C.inv f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_subcategory:
    shows "subcategory C (\<lambda>f. C.arr f \<and> Ide (C.dom f) \<and> Ide (C.cod f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcategory C (\<lambda>f. C.arr f \<and> Ide (C.dom f) \<and> Ide (C.cod f))
[PROOF STEP]
..


[STATEMENT]
lemma in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C:
    shows "\<guillemotleft>f : a \<rightarrow> b\<guillemotright> \<longleftrightarrow> arr a \<and> arr b \<and> \<guillemotleft>f : a \<rightarrow>\<^sub>C b\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f : a \<rightarrow> b\<guillemotright> = (arr a \<and> arr b \<and> \<guillemotleft>f : a \<rightarrow>\<^sub>C b\<guillemotright>)
[PROOF STEP]
using arr_char\<^sub>S\<^sub>b\<^sub>C in_hom_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr ?f = (C.arr ?f \<and> Ide (C.dom ?f) \<and> Ide (C.cod ?f))
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> arr ?f \<and> \<guillemotleft>?f : ?a \<rightarrow>\<^sub>C ?b\<guillemotright>)

goal (1 subgoal):
 1. \<guillemotleft>f : a \<rightarrow> b\<guillemotright> = (arr a \<and> arr b \<and> \<guillemotleft>f : a \<rightarrow>\<^sub>C b\<guillemotright>)
[PROOF STEP]
by auto


[STATEMENT]
lemma iso_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C:
    shows "iso f \<longleftrightarrow> arr f \<and> C.iso f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.iso f = (arr f \<and> C.iso f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. local.iso f \<Longrightarrow> arr f \<and> C.iso f
 2. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
assume f: "iso f"
[PROOF STATE]
proof (state)
this:
local.iso f

goal (2 subgoals):
 1. local.iso f \<Longrightarrow> arr f \<and> C.iso f
 2. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
obtain g where g: "inverse_arrows f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. inverse_arrows f g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
local.iso f

goal (1 subgoal):
 1. (\<And>g. inverse_arrows f g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse_arrows f g

goal (2 subgoals):
 1. local.iso f \<Longrightarrow> arr f \<and> C.iso f
 2. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
show "arr f \<and> C.iso f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr f \<and> C.iso f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arr f \<and> C.iso f
[PROOF STEP]
have "C.inverse_arrows f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.inverse_arrows f g
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
inverse_arrows f g

goal (1 subgoal):
 1. C.inverse_arrows f g
[PROOF STEP]
apply (elim inverse_arrowsE, intro C.inverse_arrowsI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ide (local.comp g f); ide (local.comp f g); inverse_arrows f g\<rbrakk> \<Longrightarrow> C.ide (C g f)
 2. \<lbrakk>ide (local.comp g f); ide (local.comp f g); inverse_arrows f g\<rbrakk> \<Longrightarrow> C.ide (C f g)
[PROOF STEP]
using comp_simp ide_char\<^sub>S\<^sub>b\<^sub>C arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
seq ?g ?f \<Longrightarrow> local.comp ?g ?f = C ?g ?f
ide ?a = (arr ?a \<and> C.ide ?a)
arr ?f = (C.arr ?f \<and> Ide (C.dom ?f) \<and> Ide (C.cod ?f))

goal (2 subgoals):
 1. \<lbrakk>ide (local.comp g f); ide (local.comp f g); inverse_arrows f g\<rbrakk> \<Longrightarrow> C.ide (C g f)
 2. \<lbrakk>ide (local.comp g f); ide (local.comp f g); inverse_arrows f g\<rbrakk> \<Longrightarrow> C.ide (C f g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C.inverse_arrows f g

goal (1 subgoal):
 1. arr f \<and> C.iso f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f g

goal (1 subgoal):
 1. arr f \<and> C.iso f
[PROOF STEP]
using f iso_is_arr
[PROOF STATE]
proof (prove)
using this:
C.inverse_arrows f g
local.iso f
local.iso ?f \<Longrightarrow> arr ?f

goal (1 subgoal):
 1. arr f \<and> C.iso f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
arr f \<and> C.iso f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
arr f \<and> C.iso f

goal (1 subgoal):
 1. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
assume f: "arr f \<and> C.iso f"
[PROOF STATE]
proof (state)
this:
arr f \<and> C.iso f

goal (1 subgoal):
 1. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
obtain g where g: "C.inverse_arrows f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. C.inverse_arrows f g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
arr f \<and> C.iso f

goal (1 subgoal):
 1. (\<And>g. C.inverse_arrows f g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C.inverse_arrows f g

goal (1 subgoal):
 1. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
have "inverse_arrows f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_arrows f g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ide (local.comp g f)
 2. ide (local.comp f g)
[PROOF STEP]
show "ide (comp g f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (local.comp g f)
[PROOF STEP]
using f g
[PROOF STATE]
proof (prove)
using this:
arr f \<and> C.iso f
C.inverse_arrows f g

goal (1 subgoal):
 1. ide (local.comp g f)
[PROOF STEP]
by (metis (no_types, lifting) C.seqE C.ide_compE C.inverse_arrowsE
              arr_char\<^sub>S\<^sub>b\<^sub>C dom_simp ide_dom comp_def)
[PROOF STATE]
proof (state)
this:
ide (local.comp g f)

goal (1 subgoal):
 1. ide (local.comp f g)
[PROOF STEP]
show "ide (comp f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (local.comp f g)
[PROOF STEP]
using f g C.inverse_arrows_sym [of f g]
[PROOF STATE]
proof (prove)
using this:
arr f \<and> C.iso f
C.inverse_arrows f g
C.inverse_arrows f g = C.inverse_arrows g f

goal (1 subgoal):
 1. ide (local.comp f g)
[PROOF STEP]
by (metis (no_types, lifting) C.seqE C.ide_compE C.inverse_arrowsE
              arr_char\<^sub>S\<^sub>b\<^sub>C dom_simp ide_dom comp_def)
[PROOF STATE]
proof (state)
this:
ide (local.comp f g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverse_arrows f g

goal (1 subgoal):
 1. arr f \<and> C.iso f \<Longrightarrow> local.iso f
[PROOF STEP]
thus "iso f"
[PROOF STATE]
proof (prove)
using this:
inverse_arrows f g

goal (1 subgoal):
 1. local.iso f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.iso f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_functor:
    shows "functor S.comp C S.map"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functor (\<cdot>) C S.map
[PROOF STEP]
..


[STATEMENT]
lemma is_faithful_functor:
    shows "faithful_functor S.comp C S.map"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. faithful_functor (\<cdot>) C S.map
[PROOF STEP]
..


[STATEMENT]
lemma is_embedding_functor:
    shows "embedding_functor S.comp C S.map"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. embedding_functor (\<cdot>) C S.map
[PROOF STEP]
..


[STATEMENT]
lemma is_inclusion_functor:
    shows "inclusion_functor C (\<lambda>f. C.arr f \<and> Ide (C.dom f) \<and> Ide (C.cod f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inclusion_functor C (\<lambda>f. C.arr f \<and> Ide (C.dom f) \<and> Ide (C.cod f))
[PROOF STEP]
..


[STATEMENT]
lemma is_full_functor:
    shows "full_functor S.comp C S.map"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. full_functor S.comp C S.map
[PROOF STEP]
..


[STATEMENT]
lemma "set (n_sequence_enum xs n) = set (List.n_lists n xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (n_sequence_enum xs n) = set (List.n_lists n xs)
[PROOF STEP]
by(induct n) auto


[STATEMENT]
theorem n_sequence_enum_correct:
  "set (n_sequence_enum xs n) = n_sequences (set xs) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (n_sequence_enum xs n) = n_sequences (set xs) n
[PROOF STEP]
proof standard
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (n_sequence_enum xs n) \<subseteq> n_sequences (set xs) n
 2. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)
[PROOF STEP]
show "set (n_sequence_enum xs n) \<subseteq> n_sequences (set xs) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (n_sequence_enum xs n) \<subseteq> n_sequences (set xs) n
[PROOF STEP]
unfolding n_sequences_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (n_sequence_enum xs n) \<subseteq> {xsa. set xsa \<subseteq> set xs \<and> length xsa = n}
[PROOF STEP]
by (induct n) auto+
[PROOF STATE]
proof (state)
this:
set (n_sequence_enum xs n) \<subseteq> n_sequences (set xs) n

goal (1 subgoal):
 1. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)
[PROOF STEP]
show "n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n_sequences (set xs) 0 \<subseteq> set (n_sequence_enum xs 0)
 2. \<And>n. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n) \<Longrightarrow> n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. n_sequences (set xs) 0 \<subseteq> set (n_sequence_enum xs 0)
 2. \<And>n. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n) \<Longrightarrow> n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_sequences (set xs) 0 \<subseteq> set (n_sequence_enum xs 0)
[PROOF STEP]
unfolding n_sequences_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {xsa. set xsa \<subseteq> set xs \<and> length xsa = 0} \<subseteq> set (n_sequence_enum xs 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n_sequences (set xs) 0 \<subseteq> set (n_sequence_enum xs 0)

goal (1 subgoal):
 1. \<And>n. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n) \<Longrightarrow> n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n) \<Longrightarrow> n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)

goal (1 subgoal):
 1. \<And>n. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n) \<Longrightarrow> n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
have "\<lbrakk>n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n); set x \<subseteq> set xs; length x = Suc n\<rbrakk>
      \<Longrightarrow> \<exists>xa\<in>set xs. x \<in> (#) xa ` set (n_sequence_enum xs n)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n); set x \<subseteq> set xs; length x = Suc n\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set xs. x \<in> (#) xa ` set (n_sequence_enum xs n)
[PROOF STEP]
unfolding n_sequences_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{xsa. set xsa \<subseteq> set xs \<and> length xsa = n} \<subseteq> set (n_sequence_enum xs n); set x \<subseteq> set xs; length x = Suc n\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set xs. x \<in> (#) xa ` set (n_sequence_enum xs n)
[PROOF STEP]
by (cases x) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n); set ?x \<subseteq> set xs; length ?x = Suc n\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set xs. ?x \<in> (#) xa ` set (n_sequence_enum xs n)

goal (1 subgoal):
 1. \<And>n. n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n) \<Longrightarrow> n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
from this Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n); set ?x \<subseteq> set xs; length ?x = Suc n\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set xs. ?x \<in> (#) xa ` set (n_sequence_enum xs n)
n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n); set ?x \<subseteq> set xs; length ?x = Suc n\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set xs. ?x \<in> (#) xa ` set (n_sequence_enum xs n)
n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)

goal (1 subgoal):
 1. n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
unfolding n_sequences_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{xsa. set xsa \<subseteq> set xs \<and> length xsa = n} \<subseteq> set (n_sequence_enum xs n); set ?x \<subseteq> set xs; length ?x = Suc n\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set xs. ?x \<in> (#) xa ` set (n_sequence_enum xs n)
{xsa. set xsa \<subseteq> set xs \<and> length xsa = n} \<subseteq> set (n_sequence_enum xs n)

goal (1 subgoal):
 1. {xsa. set xsa \<subseteq> set xs \<and> length xsa = Suc n} \<subseteq> set (n_sequence_enum xs (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n_sequences (set xs) (Suc n) \<subseteq> set (n_sequence_enum xs (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n_sequences (set xs) n \<subseteq> set (n_sequence_enum xs n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem n_sequence_enum_distinct:
  "distinct xs \<Longrightarrow> distinct (n_sequence_enum xs n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> distinct (n_sequence_enum xs n)
[PROOF STEP]
by (induct n) (auto simp: Cons_distinct_concat_map)


[STATEMENT]
lemma n_sequence_enum_length:
  "length (n_sequence_enum xs n) = (length xs) ^ n "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (n_sequence_enum xs n) = length xs ^ n
[PROOF STEP]
by(induct n arbitrary: xs) (auto simp: length_concat_map)


[STATEMENT]
theorem n_sequences_card:
  assumes "finite A"
  shows "card (n_sequences A n) = card A ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
obtain xs where set: "set xs = A" and dis: "distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs = A; distinct xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms finite_distinct_list
[PROOF STATE]
proof (prove)
using this:
finite A
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A \<and> distinct xs

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs = A; distinct xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set xs = A
distinct xs

goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
have "length (n_sequence_enum xs n) = (length xs) ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (n_sequence_enum xs n) = length xs ^ n
[PROOF STEP]
using n_sequence_enum_distinct n_sequence_enum_length
[PROOF STATE]
proof (prove)
using this:
distinct ?xs \<Longrightarrow> distinct (n_sequence_enum ?xs ?n)
length (n_sequence_enum ?xs ?n) = length ?xs ^ ?n

goal (1 subgoal):
 1. length (n_sequence_enum xs n) = length xs ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (n_sequence_enum xs n) = length xs ^ n

goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (n_sequence_enum xs n) = length xs ^ n
[PROOF STEP]
have "card (set (n_sequence_enum xs n)) = card (set xs) ^ n"
[PROOF STATE]
proof (prove)
using this:
length (n_sequence_enum xs n) = length xs ^ n

goal (1 subgoal):
 1. card (set (n_sequence_enum xs n)) = card (set xs) ^ n
[PROOF STEP]
by (simp add: dis distinct_card n_sequence_enum_distinct)
[PROOF STATE]
proof (state)
this:
card (set (n_sequence_enum xs n)) = card (set xs) ^ n

goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (set (n_sequence_enum xs n)) = card (set xs) ^ n
[PROOF STEP]
have "card (n_sequences (set xs) n) = card (set xs) ^ n"
[PROOF STATE]
proof (prove)
using this:
card (set (n_sequence_enum xs n)) = card (set xs) ^ n

goal (1 subgoal):
 1. card (n_sequences (set xs) n) = card (set xs) ^ n
[PROOF STEP]
by (simp add: n_sequence_enum_correct)
[PROOF STATE]
proof (state)
this:
card (n_sequences (set xs) n) = card (set xs) ^ n

goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (n_sequences (set xs) n) = card (set xs) ^ n
[PROOF STEP]
show "card (n_sequences A n) = card A ^ n"
[PROOF STATE]
proof (prove)
using this:
card (n_sequences (set xs) n) = card (set xs) ^ n

goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
using set
[PROOF STATE]
proof (prove)
using this:
card (n_sequences (set xs) n) = card (set xs) ^ n
set xs = A

goal (1 subgoal):
 1. card (n_sequences A n) = card A ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (n_sequences A n) = card A ^ n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enat_Suc0[simp]: "enat (Suc 0) = eSuc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (Suc 0) = eSuc 0
[PROOF STEP]
by (metis One_nat_def one_eSuc one_enat_def)


[STATEMENT]
lemma le_epred[iff]: "l < epred k \<longleftrightarrow> eSuc l < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l < epred k) = (eSuc l < k)
[PROOF STEP]
by (metis eSuc_le_iff epred_eSuc epred_le_epredI less_le_not_le not_le)


[STATEMENT]
lemma eq_infI[intro]:
    assumes "\<And> n. enat n \<le> m"
    shows "m = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = \<infinity>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
enat ?n \<le> m

goal (1 subgoal):
 1. m = \<infinity>
[PROOF STEP]
by (metis enat_less_imp_le enat_ord_simps(5) less_le_not_le)


[STATEMENT]
lemma ufun_apply_lit [simp]:
  "\<guillemotleft>f\<guillemotright>(\<guillemotleft>x\<guillemotright>)\<^sub>a = \<guillemotleft>f(x)\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f\<guillemotright>(\<guillemotleft>x\<guillemotright>)\<^sub>a = \<guillemotleft>f x\<guillemotright>
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma lit_plus_appl [lit_norm]: "\<guillemotleft>(+)\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x + y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>(+)\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x + y
[PROOF STEP]
by (simp add: uexpr_defs, transfer, simp)


[STATEMENT]
lemma lit_minus_appl [lit_norm]: "\<guillemotleft>(-)\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x - y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>(-)\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x - y
[PROOF STEP]
by (simp add: uexpr_defs, transfer, simp)


[STATEMENT]
lemma lit_mult_appl [lit_norm]: "\<guillemotleft>times\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>(*)\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x * y
[PROOF STEP]
by (simp add: uexpr_defs, transfer, simp)


[STATEMENT]
lemma lit_divide_apply [lit_norm]: "\<guillemotleft>(/)\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>(/)\<guillemotright>(x)\<^sub>a(y)\<^sub>a = x / y
[PROOF STEP]
by (simp add: uexpr_defs, transfer, simp)


[STATEMENT]
lemma pfun_entries_apply [simp]:
  "(entr\<^sub>u(d,f) :: (('k, 'v) pfun, '\<alpha>) uexpr)(i)\<^sub>a = ((\<guillemotleft>f\<guillemotright>(i)\<^sub>a) \<triangleleft> i \<in>\<^sub>u d \<triangleright> \<bottom>\<^sub>u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entr\<^sub>u(d,f)(i)\<^sub>a = \<guillemotleft>f\<guillemotright>(i)\<^sub>a \<triangleleft> i \<in>\<^sub>u d \<triangleright> \<bottom>\<^sub>u
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma udom_uupdate_pfun [simp]:
  fixes m :: "(('k, 'v) pfun, '\<alpha>) uexpr"
  shows "dom\<^sub>u(m(k \<mapsto> v)\<^sub>u) = {k}\<^sub>u \<union>\<^sub>u dom\<^sub>u(m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom\<^sub>u(m(k \<mapsto> v)\<^sub>u) = {k}\<^sub>u \<union>\<^sub>u dom\<^sub>u(m)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma uapply_uupdate_pfun [simp]:
  fixes m :: "(('k, 'v) pfun, '\<alpha>) uexpr"
  shows "(m(k \<mapsto> v)\<^sub>u)(i)\<^sub>a = v \<triangleleft> i =\<^sub>u k \<triangleright> m(i)\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m(k \<mapsto> v)\<^sub>u)(i)\<^sub>a = v \<triangleleft> i =\<^sub>u k \<triangleright> m(i)\<^sub>a
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma ft_empty_impl: "al_empty ft_\<alpha> ft_invar ft_empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_empty ft_\<alpha> (\<lambda>_. True) ft_empty
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True
 2. ft_\<alpha> (ft_empty ()) = []
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_consl_impl: "al_consl ft_\<alpha> ft_invar ft_consl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_consl ft_\<alpha> (\<lambda>_. True) ft_consl
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s e a. True \<Longrightarrow> True
 2. \<And>s e a. True \<Longrightarrow> ft_\<alpha> (ft_consl e a s) = (e, a) # ft_\<alpha> s
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.lcons_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_consr_impl: "al_consr ft_\<alpha> ft_invar ft_consr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_consr ft_\<alpha> (\<lambda>_. True) ft_consr
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s e a. True \<Longrightarrow> True
 2. \<And>s e a. True \<Longrightarrow> ft_\<alpha> (ft_consr s e a) = ft_\<alpha> s @ [(e, a)]
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.rcons_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_isEmpty_impl: "al_isEmpty ft_\<alpha> ft_invar ft_isEmpty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_isEmpty ft_\<alpha> (\<lambda>_. True) ft_isEmpty
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ft_isEmpty s = (ft_\<alpha> s = [])
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.isEmpty_correct FingerTree.empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_count_impl: "al_count ft_\<alpha> ft_invar ft_count"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_count ft_\<alpha> (\<lambda>_. True) ft_count
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ft_count s = length (ft_\<alpha> s)
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.count_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_head_impl: "al_head ft_\<alpha> ft_invar ft_head"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_head ft_\<alpha> (\<lambda>_. True) ft_head
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>True; ft_\<alpha> s \<noteq> []\<rbrakk> \<Longrightarrow> ft_head s = hd (ft_\<alpha> s)
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.head_correct FingerTree.empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_tail_impl: "al_tail ft_\<alpha> ft_invar ft_tail"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_tail ft_\<alpha> (\<lambda>_. True) ft_tail
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>True; ft_\<alpha> s \<noteq> []\<rbrakk> \<Longrightarrow> ft_\<alpha> (ft_tail s) = tl (ft_\<alpha> s)
 2. \<And>s. \<lbrakk>True; ft_\<alpha> s \<noteq> []\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.tail_correct FingerTree.empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_headR_impl: "al_headR ft_\<alpha> ft_invar ft_headR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_headR ft_\<alpha> (\<lambda>_. True) ft_headR
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>True; ft_\<alpha> s \<noteq> []\<rbrakk> \<Longrightarrow> ft_headR s = last (ft_\<alpha> s)
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.headR_correct FingerTree.empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_tailR_impl: "al_tailR ft_\<alpha> ft_invar ft_tailR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_tailR ft_\<alpha> (\<lambda>_. True) ft_tailR
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>True; ft_\<alpha> s \<noteq> []\<rbrakk> \<Longrightarrow> ft_\<alpha> (ft_tailR s) = butlast (ft_\<alpha> s)
 2. \<And>s. \<lbrakk>True; ft_\<alpha> s \<noteq> []\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.tailR_correct FingerTree.empty_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done