15 "datatype_new" :: thy_decl and |
15 "datatype_new" :: thy_decl and |
16 "datatype_compat" :: thy_decl |
16 "datatype_compat" :: thy_decl |
17 begin |
17 begin |
18 |
18 |
19 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
19 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
20 by blast |
20 by blast |
21 |
21 |
22 lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |
22 lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |
23 by blast |
23 by blast |
24 |
24 |
25 lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X" |
25 lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X" |
26 by auto |
26 by auto |
27 |
27 |
28 lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x" |
28 lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x" |
29 by auto |
29 by auto |
30 |
30 |
31 lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j" |
31 lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j" |
32 unfolding underS_def by simp |
32 unfolding underS_def by simp |
33 |
33 |
34 lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R" |
34 lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R" |
35 unfolding underS_def by simp |
35 unfolding underS_def by simp |
36 |
36 |
37 lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R" |
37 lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R" |
38 unfolding underS_def Field_def by auto |
38 unfolding underS_def Field_def by auto |
39 |
39 |
40 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" |
40 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" |
41 unfolding Field_def by auto |
41 unfolding Field_def by auto |
42 |
42 |
43 lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x" |
43 lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x" |
44 using fst_convol unfolding convol_def by simp |
44 using fst_convol unfolding convol_def by simp |
45 |
45 |
46 lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x" |
46 lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x" |
47 using snd_convol unfolding convol_def by simp |
47 using snd_convol unfolding convol_def by simp |
48 |
48 |
49 lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f" |
49 lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f" |
50 unfolding convol_def by auto |
50 unfolding convol_def by auto |
51 |
51 |
52 lemma convol_expand_snd': |
52 lemma convol_expand_snd': |
53 assumes "(fst o f = g)" |
53 assumes "(fst o f = g)" |
54 shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f" |
54 shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f" |
55 proof - |
55 proof - |
57 then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp |
57 then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp |
58 moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol) |
58 moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol) |
59 moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff) |
59 moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff) |
60 ultimately show ?thesis by simp |
60 ultimately show ?thesis by simp |
61 qed |
61 qed |
|
62 |
62 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B" |
63 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B" |
63 unfolding bij_betw_def by auto |
64 unfolding bij_betw_def by auto |
64 |
65 |
65 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B" |
66 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B" |
66 unfolding bij_betw_def by auto |
67 unfolding bij_betw_def by auto |
67 |
68 |
68 lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow> |
69 lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow> |
69 (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x" |
70 (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x" |
70 unfolding bij_betw_def by (blast intro: f_the_inv_into_f) |
71 unfolding bij_betw_def by (blast intro: f_the_inv_into_f) |
71 |
72 |
75 |
76 |
76 lemma bij_betwI': |
77 lemma bij_betwI': |
77 "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y); |
78 "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y); |
78 \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y; |
79 \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y; |
79 \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y" |
80 \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y" |
80 unfolding bij_betw_def inj_on_def by blast |
81 unfolding bij_betw_def inj_on_def by blast |
81 |
82 |
82 lemma surj_fun_eq: |
83 lemma surj_fun_eq: |
83 assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x" |
84 assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x" |
84 shows "g1 = g2" |
85 shows "g1 = g2" |
85 proof (rule ext) |
86 proof (rule ext) |