[STATEMENT]
lemma b_def_equiv: "d_aux a b c \<le> e_aux a b c \<Longrightarrow> b_aux a b c = (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> b_aux a b c = (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
apply (cut_tac a = b and b = c and c = a in a_def_equiv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> d_aux b c a \<le> e_aux b c a
 2. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux b c a = (b \<squnion> d_aux b c a) \<sqinter> e_aux b c a\<rbrakk> \<Longrightarrow> b_aux a b c = (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
by (simp_all add: d_b_c_a e_b_c_a b_a)


[STATEMENT]
lemma c_def_equiv: "d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = (c \<squnion> d_aux a b c) \<sqinter> e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = (c \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
apply (cut_tac a = c and b = a and c = b in a_def_equiv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> d_aux c a b \<le> e_aux c a b
 2. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux c a b = (c \<squnion> d_aux c a b) \<sqinter> e_aux c a b\<rbrakk> \<Longrightarrow> c_aux a b c = (c \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
by (simp_all add: d_c_a_b e_c_a_b c_a)


[STATEMENT]
lemma a_join_b_eq_e: "d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
assume d_less_e: " d_aux a b c \<le> e_aux a b c"
[PROOF STATE]
proof (state)
this:
d_aux a b c \<le> e_aux a b c

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "((a \<squnion> d_aux a b c) \<sqinter> e_aux a b c) \<squnion> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c) = ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c) \<squnion> (e_aux a b c \<sqinter> (a \<squnion> d_aux a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c = (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> e_aux a b c \<sqinter> (a \<squnion> d_aux a b c)
[PROOF STEP]
by (simp add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
(a \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c = (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> e_aux a b c \<sqinter> (a \<squnion> d_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c = (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> e_aux a b c \<sqinter> (a \<squnion> d_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c) \<squnion> (a \<squnion> d_aux a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> e_aux a b c \<sqinter> (a \<squnion> d_aux a b c) = e_aux a b c \<sqinter> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (a \<squnion> d_aux a b c))
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
(b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> e_aux a b c \<sqinter> (a \<squnion> d_aux a b c) = e_aux a b c \<sqinter> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (a \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> e_aux a b c \<sqinter> (a \<squnion> d_aux a b c) = e_aux a b c \<sqinter> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (a \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> ((e_aux a b c \<sqinter> (d_aux a b c \<squnion> b)) \<squnion> (a \<squnion> d_aux a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<squnion> (a \<squnion> d_aux a b c))
[PROOF STEP]
by (simp add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<squnion> (a \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<squnion> (a \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> ((d_aux a b c \<squnion> (e_aux a b c \<sqinter> b)) \<squnion> (a \<squnion> d_aux a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b \<squnion> (a \<squnion> d_aux a b c))
[PROOF STEP]
by (cut_tac d_less_e, simp add: modular)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b \<squnion> (a \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b \<squnion> (a \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> ((a \<squnion> d_aux a b c) \<squnion> (d_aux a b c \<squnion> (b \<sqinter> e_aux a b c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (d_aux a b c \<squnion> b \<sqinter> e_aux a b c))
[PROOF STEP]
by (simp add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (d_aux a b c \<squnion> b \<sqinter> e_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b \<squnion> (a \<squnion> d_aux a b c)) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (d_aux a b c \<squnion> b \<sqinter> e_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (b \<sqinter> e_aux a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (d_aux a b c \<squnion> b \<sqinter> e_aux a b c)) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> e_aux a b c)
[PROOF STEP]
by (simp add: sup_assoc)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (d_aux a b c \<squnion> b \<sqinter> e_aux a b c)) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (d_aux a b c \<squnion> b \<sqinter> e_aux a b c)) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (b \<sqinter> (c \<squnion> a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> e_aux a b c) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> (c \<squnion> a))
[PROOF STEP]
by (simp add: b_meet_e)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> e_aux a b c) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> (c \<squnion> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> e_aux a b c) = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> (c \<squnion> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c) \<squnion> (b \<sqinter> (c \<squnion> a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a))
[PROOF STEP]
by (simp add: a_join_d)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (a \<squnion> ((b \<sqinter> c) \<squnion> (b \<sqinter> (c \<squnion> a))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a)))
[PROOF STEP]
by (simp add: sup_assoc)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a)))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a)))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> ((b \<sqinter> c) \<squnion> (c \<squnion> a))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a))) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (b \<sqinter> c \<squnion> (c \<squnion> a)))
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a))) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (b \<sqinter> c \<squnion> (c \<squnion> a)))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c \<squnion> b \<sqinter> (c \<squnion> a))) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (b \<sqinter> c \<squnion> (c \<squnion> a)))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> (c \<squnion> a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (b \<sqinter> c \<squnion> (c \<squnion> a))) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (c \<squnion> a))
[PROOF STEP]
by (simp add: sup_absorb2)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (b \<sqinter> c \<squnion> (c \<squnion> a))) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (c \<squnion> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (b \<sqinter> c \<squnion> (c \<squnion> a))) = e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (c \<squnion> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> (a \<squnion> ((c \<squnion> a) \<sqinter> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> (c \<squnion> a) \<sqinter> b)
[PROOF STEP]
by (simp add: sup_commute inf_commute)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> (c \<squnion> a) \<sqinter> b)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> b \<sqinter> (c \<squnion> a)) = e_aux a b c \<sqinter> (a \<squnion> (c \<squnion> a) \<sqinter> b)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c \<sqinter> ((c \<squnion> a) \<sqinter> (a \<squnion> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> (a \<squnion> (c \<squnion> a) \<sqinter> b) = e_aux a b c \<sqinter> ((c \<squnion> a) \<sqinter> (a \<squnion> b))
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> (c \<squnion> a) \<sqinter> b) = e_aux a b c \<sqinter> ((c \<squnion> a) \<sqinter> (a \<squnion> b))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> (a \<squnion> (c \<squnion> a) \<sqinter> b) = e_aux a b c \<sqinter> ((c \<squnion> a) \<sqinter> (a \<squnion> b))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
have "\<dots> = e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux a b c \<sqinter> ((c \<squnion> a) \<sqinter> (a \<squnion> b)) = e_aux a b c
[PROOF STEP]
by (rule order.antisym, simp_all, simp_all add: e_aux_def)
[PROOF STATE]
proof (state)
this:
e_aux a b c \<sqinter> ((c \<squnion> a) \<sqinter> (a \<squnion> b)) = e_aux a b c

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(a \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c = e_aux a b c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(a \<squnion> d_aux a b c) \<sqinter> e_aux a b c \<squnion> (b \<squnion> d_aux a b c) \<sqinter> e_aux a b c = e_aux a b c

goal (1 subgoal):
 1. a_aux a b c \<squnion> b_aux a b c = e_aux a b c
[PROOF STEP]
by (cut_tac d_less_e, simp add: a_def_equiv b_def_equiv)
[PROOF STATE]
proof (state)
this:
a_aux a b c \<squnion> b_aux a b c = e_aux a b c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma b_join_c_eq_e: " d_aux a b c <= e_aux a b c \<Longrightarrow> b_aux a b c \<squnion> c_aux a b c = e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> b_aux a b c \<squnion> c_aux a b c = e_aux a b c
[PROOF STEP]
apply (subst b_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux b c a \<squnion> c_aux a b c = e_aux a b c
[PROOF STEP]
apply (subgoal_tac "c_aux a b c = b_aux b c a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> a_aux b c a \<squnion> c_aux a b c = e_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = b_aux b c a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> a_aux b c a \<squnion> b_aux b c a = e_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = b_aux b c a
[PROOF STEP]
apply (subst a_join_b_eq_e)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> d_aux b c a \<le> e_aux b c a
 2. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> e_aux b c a = e_aux a b c
 3. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = b_aux b c a
[PROOF STEP]
by (simp_all add: c_aux_def b_aux_def d_b_c_a e_b_c_a)


[STATEMENT]
lemma c_join_a_eq_e: "d_aux a b c <= e_aux a b c \<Longrightarrow> c_aux a b c \<squnion> a_aux a b c = e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c \<squnion> a_aux a b c = e_aux a b c
[PROOF STEP]
apply (subst c_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux c a b \<squnion> a_aux a b c = e_aux a b c
[PROOF STEP]
apply (subgoal_tac "a_aux a b c = b_aux c a b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> a_aux c a b \<squnion> a_aux a b c = e_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = b_aux c a b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> a_aux c a b \<squnion> b_aux c a b = e_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = b_aux c a b
[PROOF STEP]
apply (subst a_join_b_eq_e)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> d_aux c a b \<le> e_aux c a b
 2. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> e_aux c a b = e_aux a b c
 3. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = b_aux c a b
[PROOF STEP]
by (simp_all add: a_aux_def b_aux_def d_b_c_a e_b_c_a)


[STATEMENT]
lemma "no_distrib a b c \<Longrightarrow> incomp a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_distrib a b c \<Longrightarrow> incomp a b
[PROOF STEP]
apply (simp add: no_distrib_def incomp_def ac_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> \<not> a \<le> b \<and> \<not> b \<le> a
[PROOF STEP]
using order.strict_iff_not inf.absorb_iff2 inf.commute modular
[PROOF STATE]
proof (prove)
using this:
(?a < ?b) = (?a \<le> ?b \<and> \<not> ?b \<le> ?a)
(?b \<le> ?a) = (?a \<sqinter> ?b = ?b)
?a \<sqinter> ?b = ?b \<sqinter> ?a
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?y \<sqinter> ?z = ?y \<sqinter> (?x \<squnion> ?z)

goal (1 subgoal):
 1. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> \<not> a \<le> b \<and> \<not> b \<le> a
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma M5_modular: "no_distrib a b c \<Longrightarrow> M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_distrib a b c \<Longrightarrow> M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)
[PROOF STEP]
apply (frule d_less_e)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_distrib a b c; d_aux a b c < e_aux a b c\<rbrakk> \<Longrightarrow> M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)
[PROOF STEP]
by (simp add: M5_lattice_def a_meet_b_eq_d b_meet_c_eq_d c_meet_a_eq_d a_join_b_eq_e b_join_c_eq_e c_join_a_eq_e)


[STATEMENT]
lemma M5_modular_def: "M5_lattice a b c = (a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M5_lattice a b c = (a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b)
[PROOF STEP]
by (simp add: M5_lattice_def)


[STATEMENT]
lemma not_modular_N5: "(\<not> class.modular_lattice inf ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) sup) =
   (\<exists> a b c::'a . N5_lattice a b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)) = (\<exists>a b c. N5_lattice a b c)
[PROOF STEP]
apply (subgoal_tac "class.lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) sup")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> (\<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)) = (\<exists>a b c. N5_lattice a b c)
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (unfold N5_lattice_def class.modular_lattice_def class.modular_lattice_axioms_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> (\<not> (class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<and> (\<forall>x y z. x \<le> y \<longrightarrow> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)))) = (\<exists>a b c. a \<sqinter> c = b \<sqinter> c \<and> a < b \<and> a \<squnion> c = b \<squnion> c)
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> (\<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))) = (\<exists>a b c. a \<sqinter> c = b \<sqinter> c \<and> a < b \<and> a \<squnion> c = b \<squnion> c)
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> \<exists>a b c. a \<sqinter> c = b \<sqinter> c \<and> a < b \<and> a \<squnion> c = b \<squnion> c
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 3. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (subgoal_tac "x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> \<exists>a b c. a \<sqinter> c = b \<sqinter> c \<and> a < b \<and> a \<squnion> c = b \<squnion> c
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 3. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 4. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac x = "x \<squnion> y \<sqinter> z" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> \<exists>b c. (x \<squnion> y \<sqinter> z) \<sqinter> c = b \<sqinter> c \<and> x \<squnion> y \<sqinter> z < b \<and> x \<squnion> y \<sqinter> z \<squnion> c = b \<squnion> c
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 3. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 4. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac x = "y \<sqinter> (x \<squnion> z)" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> \<exists>c. (x \<squnion> y \<sqinter> z) \<sqinter> c = y \<sqinter> (x \<squnion> z) \<sqinter> c \<and> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z) \<and> x \<squnion> y \<sqinter> z \<squnion> c = y \<sqinter> (x \<squnion> z) \<squnion> c
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 3. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 4. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac x = z in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> (x \<squnion> y \<sqinter> z) \<sqinter> z = y \<sqinter> (x \<squnion> z) \<sqinter> z \<and> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z) \<and> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 3. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 4. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> (x \<squnion> y \<sqinter> z) \<sqinter> z = y \<sqinter> (x \<squnion> z) \<sqinter> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 4. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 5. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> (x \<squnion> y \<sqinter> z) \<sqinter> z \<le> y \<sqinter> (x \<squnion> z) \<sqinter> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<sqinter> z \<le> (x \<squnion> y \<sqinter> z) \<sqinter> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 4. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 5. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 6. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> (x \<squnion> y \<sqinter> z) \<sqinter> z \<le> y
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<sqinter> z \<le> (x \<squnion> y \<sqinter> z) \<sqinter> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 4. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 5. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 6. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac y = "x \<squnion> y \<sqinter> z" in order_trans)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> (x \<squnion> y \<sqinter> z) \<sqinter> z \<le> x \<squnion> y \<sqinter> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<le> y
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<sqinter> z \<le> (x \<squnion> y \<sqinter> z) \<sqinter> z
 4. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 5. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 6. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 7. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<sqinter> z \<le> x \<squnion> y \<sqinter> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 4. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 5. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac y = "y \<sqinter> z" in order_trans)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<sqinter> z \<le> y \<sqinter> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> z \<le> x \<squnion> y \<sqinter> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 4. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 5. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 6. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z = y \<sqinter> (x \<squnion> z) \<squnion> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 3. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 4. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<squnion> z \<le> y \<sqinter> (x \<squnion> z) \<squnion> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<squnion> z \<le> x \<squnion> y \<sqinter> z \<squnion> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 4. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 5. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<le> y \<sqinter> (x \<squnion> z) \<squnion> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<le> x \<squnion> y \<sqinter> z \<squnion> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 4. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 5. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac y = "y \<sqinter> (x \<squnion> z)" in order_trans)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<le> y \<sqinter> (x \<squnion> z)
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<le> y \<sqinter> (x \<squnion> z) \<squnion> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<le> x \<squnion> y \<sqinter> z \<squnion> z
 4. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 5. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 6. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<le> x \<squnion> y \<sqinter> z \<squnion> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 3. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 4. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac y = "x \<squnion> z" in order_trans)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> y \<sqinter> (x \<squnion> z) \<le> x \<squnion> z
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z); x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> z \<le> x \<squnion> y \<sqinter> z \<squnion> z
 3. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 4. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 5. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 3. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule neq_le_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)
 2. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<le> y \<sqinter> (x \<squnion> z)
 3. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 4. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y; x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z \<le> y \<sqinter> (x \<squnion> z)
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 3. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>x y. x \<le> y \<and> (\<exists>z. x \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (x \<squnion> z))
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac x = a in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>y\<ge>a. \<exists>z. a \<squnion> y \<sqinter> z \<noteq> y \<sqinter> (a \<squnion> z)
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac x = b in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> a \<le> b \<and> (\<exists>z. a \<squnion> b \<sqinter> z \<noteq> b \<sqinter> (a \<squnion> z))
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> a \<le> b
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>z. a \<squnion> b \<sqinter> z \<noteq> b \<sqinter> (a \<squnion> z)
 3. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (simp add: less_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> \<exists>z. a \<squnion> b \<sqinter> z \<noteq> b \<sqinter> (a \<squnion> z)
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (rule_tac x = c in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> a \<squnion> b \<sqinter> c \<noteq> b \<sqinter> (a \<squnion> c)
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a < b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> a \<squnion> b \<sqinter> c \<noteq> b
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (simp add: less_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a \<le> b \<and> a \<noteq> b; a \<squnion> c = b \<squnion> c\<rbrakk> \<Longrightarrow> a \<squnion> b \<sqinter> c \<noteq> b
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a \<squnion> c = b \<squnion> c; a \<le> b; a \<noteq> b; a \<squnion> b \<sqinter> c = b\<rbrakk> \<Longrightarrow> False
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (subgoal_tac "a \<squnion> a \<sqinter> c = b")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a \<squnion> c = b \<squnion> c; a \<le> b; a \<noteq> b; a \<squnion> b \<sqinter> c = b; a \<squnion> a \<sqinter> c = b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a \<squnion> c = b \<squnion> c; a \<le> b; a \<noteq> b; a \<squnion> b \<sqinter> c = b\<rbrakk> \<Longrightarrow> a \<squnion> a \<sqinter> c = b
 3. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (unfold sup_inf_absorb) [1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a \<squnion> c = b \<squnion> c; a \<le> b; a \<noteq> b; a \<squnion> b \<sqinter> c = b; a = b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a \<squnion> c = b \<squnion> c; a \<le> b; a \<noteq> b; a \<squnion> b \<sqinter> c = b\<rbrakk> \<Longrightarrow> a \<squnion> a \<sqinter> c = b
 3. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); a \<sqinter> c = b \<sqinter> c; a \<squnion> c = b \<squnion> c; a \<le> b; a \<noteq> b; a \<squnion> b \<sqinter> c = b\<rbrakk> \<Longrightarrow> a \<squnion> a \<sqinter> c = b
 2. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_distrib_N5_M5: "(\<not> class.distrib_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)) =
   ((\<exists> a b c::'a . N5_lattice a b c) \<or> (\<exists> a b c::'a . M5_lattice a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)) = ((\<exists>a b c. N5_lattice a b c) \<or> (\<exists>a b c. M5_lattice a b c))
[PROOF STEP]
apply (unfold not_modular_N5 [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)) = (\<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c)
 2. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c) \<Longrightarrow> \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
assume A: "\<not> class.distrib_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)"
[PROOF STATE]
proof (state)
this:
\<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)

goal (2 subgoals):
 1. \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c)
 2. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c) \<Longrightarrow> \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have B: "\<exists> a b c:: 'a . (a \<sqinter> b) \<squnion> (a \<sqinter> c) < a \<sqinter> (b \<squnion> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)
[PROOF STEP]
apply (cut_tac A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> \<exists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)
[PROOF STEP]
apply (unfold  class.distrib_lattice_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<and> class.distrib_lattice_axioms (\<sqinter>) (\<squnion>)) \<Longrightarrow> \<exists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<nexists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
 2. \<nexists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> class.distrib_lattice_axioms (\<sqinter>) (\<squnion>)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
 2. \<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> class.distrib_lattice_axioms (\<sqinter>) (\<squnion>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)
[PROOF STEP]
fix x y z::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)
[PROOF STEP]
assume A: "\<forall>(a::'a) (b::'a) c::'a. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)"
[PROOF STATE]
proof (state)
this:
\<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)

goal (1 subgoal):
 1. \<And>x y z. \<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)
[PROOF STEP]
show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)
[PROOF STEP]
apply (cut_tac A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)
[PROOF STEP]
apply (rule distrib_imp1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<forall>a b c. \<not> a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c) \<Longrightarrow> x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z
[PROOF STEP]
by (simp add: less_le)
[PROOF STATE]
proof (state)
this:
x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)

goal (2 subgoals):
 1. \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c)
 2. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c) \<Longrightarrow> \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
from B
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)
[PROOF STEP]
show "\<not> class.modular_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>) \<or> (\<exists>a b c::'a. M5_lattice a b c)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b c. a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)

goal (1 subgoal):
 1. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c)
[PROOF STEP]
proof (unfold disj_not1, safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ba c ca. \<lbrakk>a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c); aa \<sqinter> ba \<squnion> aa \<sqinter> ca < aa \<sqinter> (ba \<squnion> ca); class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)\<rbrakk> \<Longrightarrow> \<exists>a b. Ex (M5_lattice a b)
[PROOF STEP]
fix a b c::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ba c ca. \<lbrakk>a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c); aa \<sqinter> ba \<squnion> aa \<sqinter> ca < aa \<sqinter> (ba \<squnion> ca); class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)\<rbrakk> \<Longrightarrow> \<exists>a b. Ex (M5_lattice a b)
[PROOF STEP]
assume A: "a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)"
[PROOF STATE]
proof (state)
this:
a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)

goal (1 subgoal):
 1. \<And>a aa b ba c ca. \<lbrakk>a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c); aa \<sqinter> ba \<squnion> aa \<sqinter> ca < aa \<sqinter> (ba \<squnion> ca); class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)\<rbrakk> \<Longrightarrow> \<exists>a b. Ex (M5_lattice a b)
[PROOF STEP]
assume B: "class.modular_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)"
[PROOF STATE]
proof (state)
this:
class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)

goal (1 subgoal):
 1. \<And>a aa b ba c ca. \<lbrakk>a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c); aa \<sqinter> ba \<squnion> aa \<sqinter> ca < aa \<sqinter> (ba \<squnion> ca); class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)\<rbrakk> \<Longrightarrow> \<exists>a b. Ex (M5_lattice a b)
[PROOF STEP]
interpret modular: modular_lattice "(\<sqinter>)" "((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool)" "(<)" "(\<squnion>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
by (fact B)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ba c ca. \<lbrakk>a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c); aa \<sqinter> ba \<squnion> aa \<sqinter> ca < aa \<sqinter> (ba \<squnion> ca); class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)\<rbrakk> \<Longrightarrow> \<exists>a b. Ex (M5_lattice a b)
[PROOF STEP]
have H: "M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)
[PROOF STEP]
apply (cut_tac a = a and b = b and c = c in  modular.M5_modular)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. no_distrib a b c
 2. M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c) \<Longrightarrow> M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)
[PROOF STEP]
apply (unfold no_distrib_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<sqinter> b \<squnion> c \<sqinter> a < a \<sqinter> (b \<squnion> c)
 2. M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c) \<Longrightarrow> M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)
[PROOF STEP]
by (simp_all add: A inf_commute)
[PROOF STATE]
proof (state)
this:
M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)

goal (1 subgoal):
 1. \<And>a aa b ba c ca. \<lbrakk>a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c); aa \<sqinter> ba \<squnion> aa \<sqinter> ca < aa \<sqinter> (ba \<squnion> ca); class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)\<rbrakk> \<Longrightarrow> \<exists>a b. Ex (M5_lattice a b)
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)
[PROOF STEP]
show "\<exists>a b c::'a. M5_lattice a b c"
[PROOF STATE]
proof (prove)
using this:
M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)

goal (1 subgoal):
 1. \<exists>a b c. M5_lattice a b c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a b c. M5_lattice a b c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c)

goal (1 subgoal):
 1. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c) \<Longrightarrow> \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c) \<Longrightarrow> \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
assume A: "\<not> class.modular_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>) \<or> (\<exists>(a::'a) (b::'a) c::'a. M5_lattice a b c)"
[PROOF STATE]
proof (state)
this:
\<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c)

goal (1 subgoal):
 1. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c) \<Longrightarrow> \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
show "\<not> class.distrib_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (cut_tac A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<or> (\<exists>a b c. M5_lattice a b c) \<Longrightarrow> \<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); \<not> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b c. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); M5_lattice a b c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<Longrightarrow> class.modular_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
 2. \<And>a b c. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); M5_lattice a b c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<le> y\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)
 2. \<And>a b c. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); M5_lattice a b c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold class.distrib_lattice_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<and> class.distrib_lattice_axioms (\<sqinter>) (\<squnion>); x \<le> y\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<and> class.distrib_lattice_axioms (\<sqinter>) (\<squnion>); M5_lattice a b c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold class.distrib_lattice_axioms_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<and> (\<forall>x y z. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)); x \<le> y\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)
 2. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>) \<and> (\<forall>x y z. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)); M5_lattice a b c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>x \<le> y; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); \<forall>x y z. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)
 2. \<And>a b c. \<lbrakk>M5_lattice a b c; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); \<forall>x y z. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: sup_absorb2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>M5_lattice a b c; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); \<forall>x y z. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule M5_lattice_incomp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>M5_lattice a b c; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); \<forall>x y z. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z); incomp a b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold M5_lattice_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); \<forall>x y z. x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z); incomp a b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac x = a in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; \<forall>y z. a \<squnion> y \<sqinter> z = (a \<squnion> y) \<sqinter> (a \<squnion> z)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac x = b in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; \<forall>z. a \<squnion> b \<sqinter> z = (a \<squnion> b) \<sqinter> (a \<squnion> z)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac x = c in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b; class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a b c:: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume A:"a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)"
[PROOF STATE]
proof (state)
this:
a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume B: "a \<sqinter> b = b \<sqinter> c"
[PROOF STATE]
proof (state)
this:
a \<sqinter> b = b \<sqinter> c

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume D: "a \<squnion> b = b \<squnion> c"
[PROOF STATE]
proof (state)
this:
a \<squnion> b = b \<squnion> c

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume E: "c \<squnion> a = b \<squnion> c"
[PROOF STATE]
proof (state)
this:
c \<squnion> a = b \<squnion> c

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume G: "incomp a b"
[PROOF STATE]
proof (state)
this:
incomp a b

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have H: "a \<squnion> b \<sqinter> c = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion> b \<sqinter> c = a
[PROOF STEP]
by (simp add: B [THEN sym] sup_absorb1)
[PROOF STATE]
proof (state)
this:
a \<squnion> b \<sqinter> c = a

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have I: "(a \<squnion> b) \<sqinter> (a \<squnion> c) = a \<squnion> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<squnion> b) \<sqinter> (a \<squnion> c) = a \<squnion> b
[PROOF STEP]
by (cut_tac E, simp add: sup_commute D)
[PROOF STATE]
proof (state)
this:
(a \<squnion> b) \<sqinter> (a \<squnion> c) = a \<squnion> b

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have J: "a = a \<squnion> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = a \<squnion> b
[PROOF STEP]
by (cut_tac A, simp add: H I)
[PROOF STATE]
proof (state)
this:
a = a \<squnion> b

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>class.lattice (\<sqinter>) (\<le>) (<) (\<squnion>); incomp a b; a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c); a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
apply (cut_tac G J)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>incomp a b; a = a \<squnion> b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "b \<le> a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>incomp a b; a = a \<squnion> b; b \<le> a\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>incomp a b; a = a \<squnion> b\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
apply (simp add: incomp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>incomp a b; a = a \<squnion> b\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
apply (rule_tac y = "a \<squnion> b" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>incomp a b; a = a \<squnion> b\<rbrakk> \<Longrightarrow> b \<le> a \<squnion> b
 2. \<lbrakk>incomp a b; a = a \<squnion> b\<rbrakk> \<Longrightarrow> a \<squnion> b \<le> a
[PROOF STEP]
apply (rule sup_ge2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>incomp a b; a = a \<squnion> b\<rbrakk> \<Longrightarrow> a \<squnion> b \<le> a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distrib_not_N5_M5: "(class.distrib_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)) =
   ((\<forall> a b c::'a . \<not> N5_lattice a b c) \<and> (\<forall> a b c::'a . \<not> M5_lattice a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) = ((\<forall>a b c. \<not> N5_lattice a b c) \<and> (\<forall>a b c. \<not> M5_lattice a b c))
[PROOF STEP]
apply (cut_tac not_distrib_N5_M5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)) = ((\<exists>a b c. N5_lattice a b c) \<or> (\<exists>a b c. M5_lattice a b c)) \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) = ((\<forall>a b c. \<not> N5_lattice a b c) \<and> (\<forall>a b c. \<not> M5_lattice a b c))
[PROOF STEP]
by auto


[STATEMENT]
lemma distrib_inf_sup_eq:
  "(class.distrib_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)) =
    (\<forall> x y z::'a . x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>) = (\<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
fix x y z:: 'a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
assume A: "class.distrib_lattice (\<sqinter>) ((\<le>) ::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)"
[PROOF STATE]
proof (state)
this:
class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
interpret distrib: distrib_lattice "(\<sqinter>)" "(\<le>) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "(<)" "(\<squnion>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
by (fact A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
assume B: "x \<sqinter> z = y \<sqinter> z"
[PROOF STATE]
proof (state)
this:
x \<sqinter> z = y \<sqinter> z

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
assume C: "x \<squnion> z = y \<squnion> z"
[PROOF STATE]
proof (state)
this:
x \<squnion> z = y \<squnion> z

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have "x = x \<sqinter> (x \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x \<sqinter> (x \<squnion> z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = x \<sqinter> (x \<squnion> z)

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = x \<sqinter> (x \<squnion> z)

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have "\<dots> = x \<sqinter> (y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> (x \<squnion> z) = x \<sqinter> (y \<squnion> z)
[PROOF STEP]
by (simp add: C)
[PROOF STATE]
proof (state)
this:
x \<sqinter> (x \<squnion> z) = x \<sqinter> (y \<squnion> z)

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> (x \<squnion> z) = x \<sqinter> (y \<squnion> z)

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z
[PROOF STEP]
by (simp add: distrib.inf_sup_distrib)
[PROOF STATE]
proof (state)
this:
x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have "\<dots> = (y \<sqinter> x) \<squnion> (y \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> y \<squnion> x \<sqinter> z = y \<sqinter> x \<squnion> y \<sqinter> z
[PROOF STEP]
by (simp add: B inf_commute)
[PROOF STATE]
proof (state)
this:
x \<sqinter> y \<squnion> x \<sqinter> z = y \<sqinter> x \<squnion> y \<sqinter> z

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> y \<squnion> x \<sqinter> z = y \<sqinter> x \<squnion> y \<sqinter> z

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have "\<dots> = y \<sqinter> (x \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqinter> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)
[PROOF STEP]
by (simp add: distrib.inf_sup_distrib)
[PROOF STATE]
proof (state)
this:
y \<sqinter> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<sqinter> x \<squnion> y \<sqinter> z = y \<sqinter> (x \<squnion> z)

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have "\<dots> = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqinter> (x \<squnion> z) = y
[PROOF STEP]
by (simp add: C)
[PROOF STATE]
proof (state)
this:
y \<sqinter> (x \<squnion> z) = y

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>); x \<sqinter> z = y \<sqinter> z; x \<squnion> z = y \<squnion> z\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
assume A: "(\<forall>x y z:: 'a. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y)"
[PROOF STATE]
proof (state)
this:
\<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y

goal (1 subgoal):
 1. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
have B: "!! x y z :: 'a. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<Longrightarrow> x = y
[PROOF STEP]
by (cut_tac A, blast)
[PROOF STATE]
proof (state)
this:
?x \<sqinter> ?z = ?y \<sqinter> ?z \<and> ?x \<squnion> ?z = ?y \<squnion> ?z \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<forall>x y z. x \<sqinter> z = y \<sqinter> z \<and> x \<squnion> z = y \<squnion> z \<longrightarrow> x = y \<Longrightarrow> class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
show "class.distrib_lattice (\<sqinter>) ((\<le>)::'a \<Rightarrow> 'a \<Rightarrow> bool) (<) (\<squnion>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)
[PROOF STEP]
apply (unfold distrib_not_N5_M5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a b c. \<not> N5_lattice a b c) \<and> (\<forall>a b c. \<not> M5_lattice a b c)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. N5_lattice a b c \<Longrightarrow> False
 2. \<And>a b c. M5_lattice a b c \<Longrightarrow> False
[PROOF STEP]
apply (unfold N5_lattice_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. a \<sqinter> c = b \<sqinter> c \<and> a < b \<and> a \<squnion> c = b \<squnion> c \<Longrightarrow> False
 2. \<And>a b c. M5_lattice a b c \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac x = a and y = b and z = c in B)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c. a \<sqinter> c = b \<sqinter> c \<and> a < b \<and> a \<squnion> c = b \<squnion> c \<Longrightarrow> a \<sqinter> c = b \<sqinter> c \<and> a \<squnion> c = b \<squnion> c
 2. \<And>a b c. \<lbrakk>a \<sqinter> c = b \<sqinter> c \<and> a < b \<and> a \<squnion> c = b \<squnion> c; a = b\<rbrakk> \<Longrightarrow> False
 3. \<And>a b c. M5_lattice a b c \<Longrightarrow> False
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. M5_lattice a b c \<Longrightarrow> False
[PROOF STEP]
apply (unfold M5_lattice_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac x = a and y = b and z = c in B)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b \<Longrightarrow> a \<sqinter> c = b \<sqinter> c \<and> a \<squnion> c = b \<squnion> c
 2. \<And>a b c. \<lbrakk>a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b; a = b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp_all add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
class.distrib_lattice (\<sqinter>) (\<le>) (<) (\<squnion>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in category) homI:
  assumes "f \<in> Ar" and "Dom f = A" and "Cod f = B"
  shows "f \<in> Hom A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> Hom A B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> Ar
Dom f = A
Cod f = B

goal (1 subgoal):
 1. f \<in> Hom A B
[PROOF STEP]
by (auto simp add: hom_def)


[STATEMENT]
lemma (in category) homE:
  assumes "A \<in> Ob" and "B \<in> Ob" and "f \<in> Hom A B"
  shows "Dom f = A" and "Cod f = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom f = A &&& Cod f = B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Dom f = A
 2. Cod f = B
[PROOF STEP]
show "Dom f = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom f = A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
B \<in> Ob
f \<in> Hom A B

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

goal (1 subgoal):
 1. Cod f = B
[PROOF STEP]
show "Cod f = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cod f = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
B \<in> Ob
f \<in> Hom A B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in category) id_arrow [intro]:
  assumes "A \<in> Ob"
  shows "Id A \<in> Ar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Id A \<in> Ar
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Id A \<in> Ar
[PROOF STEP]
from \<open>A \<in> Ob\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
[PROOF STEP]
have "Id A \<in> Hom A A"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob

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

goal (1 subgoal):
 1. Id A \<in> Ar
[PROOF STEP]
thus "Id A \<in> Ar"
[PROOF STATE]
proof (prove)
using this:
Id A \<in> Hom A A

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

goal:
No subgoals!
[PROOF STEP]
qed