[STATEMENT]
lemma atom_map_compl_pres: "atom_map (-x) = Collect atom - atom_map x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
have "(y \<in> atom_map (-x)) = (atom y \<and> y \<le> -x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> atom_map (- x)) = (atom y \<and> y \<le> - x)
[PROOF STEP]
by (simp add: atom_map_def)
[PROOF STATE]
proof (state)
this:
(y \<in> atom_map (- x)) = (atom y \<and> y \<le> - x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y \<in> atom_map (- x)) = (atom y \<and> y \<le> - x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
have "... = (atom y \<and> \<not>(y \<le> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom y \<and> y \<le> - x) = (atom y \<and> \<not> y \<le> x)
[PROOF STEP]
by (metis atom_sup_iff inf.orderE inf_shunt sup_compl_top top.ordering_top_axioms ordering_top.extremum)
[PROOF STATE]
proof (state)
this:
(atom y \<and> y \<le> - x) = (atom y \<and> \<not> y \<le> x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(atom y \<and> y \<le> - x) = (atom y \<and> \<not> y \<le> x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
have "... = (y \<in> Collect atom - atom_map x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom y \<and> \<not> y \<le> x) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
using atom_map_def
[PROOF STATE]
proof (prove)
using this:
atom_map ?x = {y. atom y \<and> y \<le> ?x}

goal (1 subgoal):
 1. (atom y \<and> \<not> y \<le> x) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(atom y \<and> \<not> y \<le> x) = (y \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
have "(y \<in> atom_map (-x)) = (y \<in> Collect atom - atom_map x)"
[PROOF STATE]
proof (prove)
using this:
(y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. (y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?y2 \<in> atom_map (- x)) = (?y2 \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?y2 \<in> atom_map (- x)) = (?y2 \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
atom_map (- x) = Collect atom - atom_map x

goal:
No subgoals!
[PROOF STEP]
qed