[STATEMENT]
lemma WHILEI_weaken:
  assumes IW: "\<And>x. I x \<Longrightarrow> I' x"
  shows "WHILEI I' b f x \<le> WHILEI I b f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI I' b f x \<le> WHILEI I b f x
[PROOF STEP]
unfolding WHILEI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC (WHILEI_body bind return I' b f) x \<le> REC (WHILEI_body bind return I b f) x
[PROOF STEP]
apply (rule REC_mono_ref[OF WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D x. WHILEI_body bind return I' b f D x \<le> WHILEI_body bind return I b f D x
[PROOF STEP]
apply (auto simp add: WHILEI_body_def dest: IW)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done