27 |
27 |
28 lemma Rep_inject: |
28 lemma Rep_inject: |
29 "(Rep x = Rep y) = (x = y)" |
29 "(Rep x = Rep y) = (x = y)" |
30 proof |
30 proof |
31 assume "Rep x = Rep y" |
31 assume "Rep x = Rep y" |
32 hence "Abs (Rep x) = Abs (Rep y)" by (simp only:) |
32 then have "Abs (Rep x) = Abs (Rep y)" by (simp only:) |
33 also have "Abs (Rep x) = x" by (rule Rep_inverse) |
33 moreover have "Abs (Rep x) = x" by (rule Rep_inverse) |
34 also have "Abs (Rep y) = y" by (rule Rep_inverse) |
34 moreover have "Abs (Rep y) = y" by (rule Rep_inverse) |
35 finally show "x = y" . |
35 ultimately show "x = y" by simp |
36 next |
36 next |
37 assume "x = y" |
37 assume "x = y" |
38 thus "Rep x = Rep y" by (simp only:) |
38 thus "Rep x = Rep y" by (simp only:) |
39 qed |
39 qed |
40 |
40 |
41 lemma Abs_inject: |
41 lemma Abs_inject: |
42 assumes x: "x \<in> A" and y: "y \<in> A" |
42 assumes x: "x \<in> A" and y: "y \<in> A" |
43 shows "(Abs x = Abs y) = (x = y)" |
43 shows "(Abs x = Abs y) = (x = y)" |
44 proof |
44 proof |
45 assume "Abs x = Abs y" |
45 assume "Abs x = Abs y" |
46 hence "Rep (Abs x) = Rep (Abs y)" by (simp only:) |
46 then have "Rep (Abs x) = Rep (Abs y)" by (simp only:) |
47 also from x have "Rep (Abs x) = x" by (rule Abs_inverse) |
47 moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse) |
48 also from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
48 moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
49 finally show "x = y" . |
49 ultimately show "x = y" by simp |
50 next |
50 next |
51 assume "x = y" |
51 assume "x = y" |
52 thus "Abs x = Abs y" by (simp only:) |
52 thus "Abs x = Abs y" by (simp only:) |
53 qed |
53 qed |
54 |
54 |
74 assumes y: "y \<in> A" |
74 assumes y: "y \<in> A" |
75 and hyp: "!!x. P (Rep x)" |
75 and hyp: "!!x. P (Rep x)" |
76 shows "P y" |
76 shows "P y" |
77 proof - |
77 proof - |
78 have "P (Rep (Abs y))" by (rule hyp) |
78 have "P (Rep (Abs y))" by (rule hyp) |
79 also from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
79 moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
80 finally show "P y" . |
80 ultimately show "P y" by simp |
81 qed |
81 qed |
82 |
82 |
83 lemma Abs_induct [induct type]: |
83 lemma Abs_induct [induct type]: |
84 assumes r: "!!y. y \<in> A ==> P (Abs y)" |
84 assumes r: "!!y. y \<in> A ==> P (Abs y)" |
85 shows "P x" |
85 shows "P x" |
86 proof - |
86 proof - |
87 have "Rep x \<in> A" by (rule Rep) |
87 have "Rep x \<in> A" by (rule Rep) |
88 hence "P (Abs (Rep x))" by (rule r) |
88 then have "P (Abs (Rep x))" by (rule r) |
89 also have "Abs (Rep x) = x" by (rule Rep_inverse) |
89 moreover have "Abs (Rep x) = x" by (rule Rep_inverse) |
90 finally show "P x" . |
90 ultimately show "P x" by simp |
91 qed |
91 qed |
92 |
92 |
93 lemma Rep_range: |
93 lemma Rep_range: |
94 assumes "type_definition Rep Abs A" |
94 assumes "type_definition Rep Abs A" |
95 shows "range Rep = A" |
95 shows "range Rep = A" |