diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/Enum.thy --- a/src/HOL/Enum.thy Tue Sep 01 17:25:36 2015 +0200 +++ b/src/HOL/Enum.thy Tue Sep 01 22:32:58 2015 +0200 @@ -144,7 +144,7 @@ by (fact equal_refl) lemma order_fun [code]: - fixes f g :: "'a\enum \ 'b\order" + fixes f g :: "'a::enum \ 'b::order" shows "f \ g \ enum_all (\x. f x \ g x)" and "f < g \ f \ g \ enum_ex (\x. f x \ g x)" by (simp_all add: fun_eq_iff le_fun_def order_less_le) @@ -244,32 +244,32 @@ subsection \Default instances for @{class enum}\ lemma map_of_zip_enum_is_Some: - assumes "length ys = length (enum \ 'a\enum list)" - shows "\y. map_of (zip (enum \ 'a\enum list) ys) x = Some y" + assumes "length ys = length (enum :: 'a::enum list)" + shows "\y. map_of (zip (enum :: 'a::enum list) ys) x = Some y" proof - - from assms have "x \ set (enum \ 'a\enum list) \ - (\y. map_of (zip (enum \ 'a\enum list) ys) x = Some y)" + from assms have "x \ set (enum :: 'a::enum list) \ + (\y. map_of (zip (enum :: 'a::enum list) ys) x = Some y)" by (auto intro!: map_of_zip_is_Some) then show ?thesis using enum_UNIV by auto qed lemma map_of_zip_enum_inject: - fixes xs ys :: "'b\enum list" - assumes length: "length xs = length (enum \ 'a\enum list)" - "length ys = length (enum \ 'a\enum list)" - and map_of: "the \ map_of (zip (enum \ 'a\enum list) xs) = the \ map_of (zip (enum \ 'a\enum list) ys)" + fixes xs ys :: "'b::enum list" + assumes length: "length xs = length (enum :: 'a::enum list)" + "length ys = length (enum :: 'a::enum list)" + and map_of: "the \ map_of (zip (enum :: 'a::enum list) xs) = the \ map_of (zip (enum :: 'a::enum list) ys)" shows "xs = ys" proof - - have "map_of (zip (enum \ 'a list) xs) = map_of (zip (enum \ 'a list) ys)" + have "map_of (zip (enum :: 'a list) xs) = map_of (zip (enum :: 'a list) ys)" proof fix x :: 'a from length map_of_zip_enum_is_Some obtain y1 y2 - where "map_of (zip (enum \ 'a list) xs) x = Some y1" - and "map_of (zip (enum \ 'a list) ys) x = Some y2" by blast + where "map_of (zip (enum :: 'a list) xs) x = Some y1" + and "map_of (zip (enum :: 'a list) ys) x = Some y2" by blast moreover from map_of - have "the (map_of (zip (enum \ 'a\enum list) xs) x) = the (map_of (zip (enum \ 'a\enum list) ys) x)" + have "the (map_of (zip (enum :: 'a::enum list) xs) x) = the (map_of (zip (enum :: 'a::enum list) ys) x)" by (auto dest: fun_cong) - ultimately show "map_of (zip (enum \ 'a\enum list) xs) x = map_of (zip (enum \ 'a\enum list) ys) x" + ultimately show "map_of (zip (enum :: 'a::enum list) xs) x = map_of (zip (enum :: 'a::enum list) ys) x" by simp qed with length enum_distinct show "xs = ys" by (rule map_of_zip_inject) @@ -297,7 +297,7 @@ begin definition - "enum = map (\ys. the o map_of (zip (enum\'a list) ys)) (List.n_lists (length (enum\'a\enum list)) enum)" + "enum = map (\ys. the o map_of (zip (enum::'a list) ys)) (List.n_lists (length (enum::'a::enum list)) enum)" definition "enum_all P = all_n_lists (\bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" @@ -306,17 +306,17 @@ "enum_ex P = ex_n_lists (\bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" instance proof - show "UNIV = set (enum \ ('a \ 'b) list)" + show "UNIV = set (enum :: ('a \ 'b) list)" proof (rule UNIV_eq_I) fix f :: "'a \ 'b" - have "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" + have "f = the \ map_of (zip (enum :: 'a::enum list) (map f enum))" by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) then show "f \ set enum" by (auto simp add: enum_fun_def set_n_lists intro: in_enum) qed next from map_of_zip_enum_inject - show "distinct (enum \ ('a \ 'b) list)" + show "distinct (enum :: ('a \ 'b) list)" by (auto intro!: inj_onI simp add: enum_fun_def distinct_map distinct_n_lists enum_distinct set_n_lists) next @@ -327,7 +327,7 @@ show "Ball UNIV P" proof fix f :: "'a \ 'b" - have f: "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" + have f: "f = the \ map_of (zip (enum :: 'a::enum list) (map f enum))" by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) from \enum_all P\ have "P (the \ map_of (zip enum (map f enum)))" unfolding enum_all_fun_def all_n_lists_def @@ -352,9 +352,9 @@ next assume "Bex UNIV P" from this obtain f where "P f" .. - have f: "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" + have f: "f = the \ map_of (zip (enum :: 'a::enum list) (map f enum))" by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) - from \P f\ this have "P (the \ map_of (zip (enum \ 'a\enum list) (map f enum)))" + from \P f\ this have "P (the \ map_of (zip (enum :: 'a::enum list) (map f enum)))" by auto from this show "enum_ex P" unfolding enum_ex_fun_def ex_n_lists_def @@ -367,7 +367,7 @@ end -lemma enum_fun_code [code]: "enum = (let enum_a = (enum \ 'a\{enum, equal} list) +lemma enum_fun_code [code]: "enum = (let enum_a = (enum :: 'a::{enum, equal} list) in map (\ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))" by (simp add: enum_fun_def Let_def)