equal
deleted
inserted
replaced
464 |
464 |
465 lemma subsetCE [elim]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P" |
465 lemma subsetCE [elim]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P" |
466 \<comment> \<open>Classical elimination rule.\<close> |
466 \<comment> \<open>Classical elimination rule.\<close> |
467 by (auto simp add: less_eq_set_def le_fun_def) |
467 by (auto simp add: less_eq_set_def le_fun_def) |
468 |
468 |
469 lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" |
469 lemma subset_eq: "A \<subseteq> B = (\<forall>x\<in>A. x \<in> B)" |
470 by blast |
470 by blast |
471 |
471 |
472 lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A" |
472 lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A" |
473 by blast |
473 by blast |
474 |
474 |
940 by blast |
940 by blast |
941 |
941 |
942 lemma image_diff_subset: "f ` A - f ` B \<subseteq> f ` (A - B)" |
942 lemma image_diff_subset: "f ` A - f ` B \<subseteq> f ` (A - B)" |
943 by blast |
943 by blast |
944 |
944 |
945 lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A" |
945 lemma Setcompr_eq_image: "{f x |x. x \<in> A} = f ` A" |
946 by blast |
946 by blast |
947 |
947 |
948 lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}" |
948 lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}" |
949 by auto |
949 by auto |
950 |
950 |
976 by auto |
976 by auto |
977 |
977 |
978 lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g" |
978 lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g" |
979 by auto |
979 by auto |
980 |
980 |
981 lemma range_eq_singletonD: |
981 lemma range_eq_singletonD: "range f = {a} \<Longrightarrow> f x = a" |
982 assumes "range f = {a}" |
982 by auto |
983 shows "f x = a" |
|
984 using assms by auto |
|
985 |
983 |
986 |
984 |
987 subsubsection \<open>Some rules with \<open>if\<close>\<close> |
985 subsubsection \<open>Some rules with \<open>if\<close>\<close> |
988 |
986 |
989 text \<open>Elimination of \<open>{x. \<dots> \<and> x = t \<and> \<dots>}\<close>.\<close> |
987 text \<open>Elimination of \<open>{x. \<dots> \<and> x = t \<and> \<dots>}\<close>.\<close> |