[STATEMENT]
lemma is_pure_iff_pure_assn: "is_pure P = (\<forall>x x'. is_pure_assn (P x x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure P = (\<forall>x x'. is_pure_assn (P x x'))
[PROOF STEP]
unfolding is_pure_def is_pure_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>P'. \<forall>x x'. P x x' = \<up> (P' x x')) = (\<forall>x x'. \<exists>Pa. P x x' = \<up> Pa)
[PROOF STEP]
by metis