equal
deleted
inserted
replaced
374 |
374 |
375 text \<open>\bigskip Theorems for transforming predicates on nat to predicates on \<open>int\<close>\<close> |
375 text \<open>\bigskip Theorems for transforming predicates on nat to predicates on \<open>int\<close>\<close> |
376 |
376 |
377 lemma zdiff_int_split: "P (int (x - y)) = |
377 lemma zdiff_int_split: "P (int (x - y)) = |
378 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
378 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
379 by (cases "y \<le> x") (simp_all add: zdiff_int) |
379 by (cases "y \<le> x") (simp_all add: of_nat_diff) |
380 |
380 |
381 text \<open> |
381 text \<open> |
382 \medskip Specific instances of congruence rules, to prevent |
382 \medskip Specific instances of congruence rules, to prevent |
383 simplifier from looping.\<close> |
383 simplifier from looping.\<close> |
384 |
384 |