author | paulson <lp15@cam.ac.uk> |
Thu, 12 Jan 2023 17:12:36 +0000 | |
changeset 76946 | 5df58a471d9e |
parent 75624 | 22d1c5f2b9f4 |
permissions | -rw-r--r-- |
49310 | 1 |
(* Title: HOL/Cardinals/Fun_More.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
More on injections, bijections and inverses. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
63167 | 8 |
section \<open>More on Injections, Bijections and Inverses\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
theory Fun_More |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
11 |
imports Main |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
63167 | 14 |
subsection \<open>Purely functional properties\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
(* unused *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
(*1*)lemma bij_betw_diff_singl: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
18 |
assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
19 |
shows "bij_betw f (A - {a}) (A' - {f a})" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
let ?B = "A - {a}" let ?B' = "A' - {f a}" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
have "f a \<in> A'" using IN BIJ unfolding bij_betw_def by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
hence "a \<notin> ?B \<and> f a \<notin> ?B' \<and> A = ?B \<union> {a} \<and> A' = ?B' \<union> {f a}" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
24 |
using IN by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
|
63167 | 29 |
subsection \<open>Properties involving finite and infinite sets\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
(* unused *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
(*1*)lemma bij_betw_inv_into_RIGHT: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
33 |
assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
34 |
shows "f `((inv_into A f)`B') = B'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
35 |
by (metis BIJ SUB bij_betw_imp_surj_on image_inv_into_cancel) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
36 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
(* unused *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
(*1*)lemma bij_betw_inv_into_RIGHT_LEFT: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
40 |
assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
41 |
IM: "(inv_into A f) ` B' = B" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
42 |
shows "f ` B = B'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
43 |
by (metis BIJ IM SUB bij_betw_inv_into_RIGHT) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
(* unused *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
(*2*)lemma bij_betw_inv_into_twice: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
47 |
assumes "bij_betw f A A'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
48 |
shows "\<forall>a \<in> A. inv_into A' (inv_into A f) a = f a" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
49 |
by (simp add: assms inv_into_inv_into_eq) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
|
63167 | 52 |
subsection \<open>Properties involving Hilbert choice\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
|
54478 | 54 |
(*1*)lemma bij_betw_inv_into_LEFT: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
55 |
assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
56 |
shows "(inv_into A f)`(f ` B) = B" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
57 |
using assms unfolding bij_betw_def using inv_into_image_cancel by force |
54478 | 58 |
|
59 |
(*1*)lemma bij_betw_inv_into_LEFT_RIGHT: |
|
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
60 |
assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
61 |
IM: "f ` B = B'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
62 |
shows "(inv_into A f) ` B' = B" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
63 |
using assms bij_betw_inv_into_LEFT[of f A A' B] by fast |
54478 | 64 |
|
65 |
||
63167 | 66 |
subsection \<open>Other facts\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
(*3*)lemma atLeastLessThan_injective: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
69 |
assumes "{0 ..< m::nat} = {0 ..< n}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
70 |
shows "m = n" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
71 |
using assms atLeast0LessThan by force |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
(*2*)lemma atLeastLessThan_injective2: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
74 |
"bij_betw f {0 ..< m::nat} {0 ..< n} \<Longrightarrow> m = n" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
75 |
using bij_betw_same_card by fastforce |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
|
54581
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54481
diff
changeset
|
77 |
(*2*)lemma atLeastLessThan_less_eq: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
78 |
"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
79 |
by auto |
54581
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54481
diff
changeset
|
80 |
|
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54481
diff
changeset
|
81 |
(*2*)lemma atLeastLessThan_less_eq2: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
82 |
assumes "inj_on f {0..<(m::nat)}" "f ` {0..<m} \<le> {0..<n}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
83 |
shows "m \<le> n" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
84 |
by (metis assms card_inj_on_le card_lessThan finite_lessThan lessThan_atLeast0) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
(* unused *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
(*3*)lemma atLeastLessThan_less: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
88 |
"({0..<m} < {0..<n}) = ((m::nat) < n)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
89 |
by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
end |