11608
|
1 |
(* Title: HOL/Typedef.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Munich
|
11743
|
4 |
*)
|
11608
|
5 |
|
11743
|
6 |
header {* Set-theory lemmas and HOL type definitions *}
|
11608
|
7 |
|
|
8 |
theory Typedef = Set
|
11659
|
9 |
files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
|
11608
|
10 |
|
11770
|
11 |
(*belongs to theory Set*)
|
|
12 |
declare atomize_ball [symmetric, rulify]
|
|
13 |
|
11608
|
14 |
(* Courtesy of Stephan Merz *)
|
|
15 |
lemma Least_mono:
|
|
16 |
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
|
|
17 |
==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
|
|
18 |
apply clarify
|
|
19 |
apply (erule_tac P = "%x. x : S" in LeastI2)
|
|
20 |
apply fast
|
|
21 |
apply (rule LeastI2)
|
|
22 |
apply (auto elim: monoD intro!: order_antisym)
|
|
23 |
done
|
|
24 |
|
|
25 |
|
11743
|
26 |
subsection {* HOL type definitions *}
|
11608
|
27 |
|
|
28 |
constdefs
|
|
29 |
type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
|
|
30 |
"type_definition Rep Abs A ==
|
|
31 |
(\<forall>x. Rep x \<in> A) \<and>
|
|
32 |
(\<forall>x. Abs (Rep x) = x) \<and>
|
|
33 |
(\<forall>y \<in> A. Rep (Abs y) = y)"
|
|
34 |
-- {* This will be stated as an axiom for each typedef! *}
|
|
35 |
|
|
36 |
lemma type_definitionI [intro]:
|
|
37 |
"(!!x. Rep x \<in> A) ==>
|
|
38 |
(!!x. Abs (Rep x) = x) ==>
|
|
39 |
(!!y. y \<in> A ==> Rep (Abs y) = y) ==>
|
|
40 |
type_definition Rep Abs A"
|
|
41 |
by (unfold type_definition_def) blast
|
|
42 |
|
|
43 |
theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
|
|
44 |
by (unfold type_definition_def) blast
|
|
45 |
|
|
46 |
theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
|
|
47 |
by (unfold type_definition_def) blast
|
|
48 |
|
|
49 |
theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
|
|
50 |
by (unfold type_definition_def) blast
|
|
51 |
|
|
52 |
theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
|
|
53 |
proof -
|
|
54 |
assume tydef: "type_definition Rep Abs A"
|
|
55 |
show ?thesis
|
|
56 |
proof
|
|
57 |
assume "Rep x = Rep y"
|
|
58 |
hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
|
|
59 |
thus "x = y" by (simp only: Rep_inverse [OF tydef])
|
|
60 |
next
|
|
61 |
assume "x = y"
|
|
62 |
thus "Rep x = Rep y" by simp
|
|
63 |
qed
|
|
64 |
qed
|
|
65 |
|
|
66 |
theorem Abs_inject:
|
|
67 |
"type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
|
|
68 |
proof -
|
|
69 |
assume tydef: "type_definition Rep Abs A"
|
|
70 |
assume x: "x \<in> A" and y: "y \<in> A"
|
|
71 |
show ?thesis
|
|
72 |
proof
|
|
73 |
assume "Abs x = Abs y"
|
|
74 |
hence "Rep (Abs x) = Rep (Abs y)" by simp
|
|
75 |
moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
|
|
76 |
moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
|
|
77 |
ultimately show "x = y" by (simp only:)
|
|
78 |
next
|
|
79 |
assume "x = y"
|
|
80 |
thus "Abs x = Abs y" by simp
|
|
81 |
qed
|
|
82 |
qed
|
|
83 |
|
|
84 |
theorem Rep_cases:
|
|
85 |
"type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
|
|
86 |
proof -
|
|
87 |
assume tydef: "type_definition Rep Abs A"
|
|
88 |
assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
|
|
89 |
show P
|
|
90 |
proof (rule r)
|
|
91 |
from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
|
|
92 |
thus "y = Rep (Abs y)" ..
|
|
93 |
qed
|
|
94 |
qed
|
|
95 |
|
|
96 |
theorem Abs_cases:
|
|
97 |
"type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
|
|
98 |
proof -
|
|
99 |
assume tydef: "type_definition Rep Abs A"
|
|
100 |
assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
|
|
101 |
show P
|
|
102 |
proof (rule r)
|
|
103 |
have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
|
|
104 |
thus "x = Abs (Rep x)" ..
|
|
105 |
show "Rep x \<in> A" by (rule Rep [OF tydef])
|
|
106 |
qed
|
|
107 |
qed
|
|
108 |
|
|
109 |
theorem Rep_induct:
|
|
110 |
"type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
|
|
111 |
proof -
|
|
112 |
assume tydef: "type_definition Rep Abs A"
|
|
113 |
assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
|
|
114 |
moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
|
|
115 |
ultimately show "P y" by (simp only:)
|
|
116 |
qed
|
|
117 |
|
|
118 |
theorem Abs_induct:
|
|
119 |
"type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
|
|
120 |
proof -
|
|
121 |
assume tydef: "type_definition Rep Abs A"
|
|
122 |
assume r: "!!y. y \<in> A ==> P (Abs y)"
|
|
123 |
have "Rep x \<in> A" by (rule Rep [OF tydef])
|
|
124 |
hence "P (Abs (Rep x))" by (rule r)
|
|
125 |
moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
|
|
126 |
ultimately show "P x" by (simp only:)
|
|
127 |
qed
|
|
128 |
|
|
129 |
use "Tools/typedef_package.ML"
|
|
130 |
|
|
131 |
end
|