equal
deleted
inserted
replaced
4 |
4 |
5 Misc set-theory lemmas and HOL type definitions. |
5 Misc set-theory lemmas and HOL type definitions. |
6 *) |
6 *) |
7 |
7 |
8 theory Typedef = Set |
8 theory Typedef = Set |
9 files "subset.ML" "equalities.ML" "mono.ML" |
9 files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"): |
10 "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"): |
|
11 |
10 |
12 (* Courtesy of Stephan Merz *) |
11 (* Courtesy of Stephan Merz *) |
13 lemma Least_mono: |
12 lemma Least_mono: |
14 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y |
13 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y |
15 ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" |
14 ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" |
126 hence "P (Abs (Rep x))" by (rule r) |
125 hence "P (Abs (Rep x))" by (rule r) |
127 moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef]) |
126 moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef]) |
128 ultimately show "P x" by (simp only:) |
127 ultimately show "P x" by (simp only:) |
129 qed |
128 qed |
130 |
129 |
131 setup InductAttrib.setup |
|
132 use "Tools/typedef_package.ML" |
130 use "Tools/typedef_package.ML" |
133 |
131 |
134 end |
132 end |