equal
deleted
inserted
replaced
1396 using assms by simp |
1396 using assms by simp |
1397 |
1397 |
1398 lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)" |
1398 lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)" |
1399 by simp |
1399 by simp |
1400 |
1400 |
|
1401 lemma if_distribR: "(if b then f else g) x = (if b then f x else g x)" |
|
1402 by simp |
|
1403 |
1401 lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)" |
1404 lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)" |
1402 by auto |
1405 by auto |
1403 |
1406 |
1404 lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)" |
1407 lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)" |
1405 by auto |
1408 by auto |