equal
deleted
inserted
replaced
294 lemma invariant_to_eq: |
294 lemma invariant_to_eq: |
295 assumes "invariant P x y" |
295 assumes "invariant P x y" |
296 shows "x = y" |
296 shows "x = y" |
297 using assms by (simp add: invariant_def) |
297 using assms by (simp add: invariant_def) |
298 |
298 |
299 lemma fun_rel_eq_invariant: |
299 lemma fun_rel_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))" |
|
300 unfolding invariant_def fun_rel_def by auto |
|
301 |
|
302 lemma fun_rel_invariant_rel: |
300 shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))" |
303 shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))" |
301 by (auto simp add: invariant_def fun_rel_def) |
304 by (auto simp add: invariant_def fun_rel_def) |
302 |
305 |
303 lemma invariant_same_args: |
306 lemma invariant_same_args: |
304 shows "invariant P x x \<equiv> P x" |
307 shows "invariant P x x \<equiv> P x" |