src/HOL/Enum.thy
changeset 61076 bdc1e2f0a86a
parent 60758 d8d85a8172b5
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Enum.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Enum.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4    by (fact equal_refl)
     1.5  
     1.6  lemma order_fun [code]:
     1.7 -  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
     1.8 +  fixes f g :: "'a::enum \<Rightarrow> 'b::order"
     1.9    shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)"
    1.10      and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)"
    1.11    by (simp_all add: fun_eq_iff le_fun_def order_less_le)
    1.12 @@ -244,32 +244,32 @@
    1.13  subsection \<open>Default instances for @{class enum}\<close>
    1.14  
    1.15  lemma map_of_zip_enum_is_Some:
    1.16 -  assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
    1.17 -  shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
    1.18 +  assumes "length ys = length (enum :: 'a::enum list)"
    1.19 +  shows "\<exists>y. map_of (zip (enum :: 'a::enum list) ys) x = Some y"
    1.20  proof -
    1.21 -  from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
    1.22 -    (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
    1.23 +  from assms have "x \<in> set (enum :: 'a::enum list) \<longleftrightarrow>
    1.24 +    (\<exists>y. map_of (zip (enum :: 'a::enum list) ys) x = Some y)"
    1.25      by (auto intro!: map_of_zip_is_Some)
    1.26    then show ?thesis using enum_UNIV by auto
    1.27  qed
    1.28  
    1.29  lemma map_of_zip_enum_inject:
    1.30 -  fixes xs ys :: "'b\<Colon>enum list"
    1.31 -  assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
    1.32 -      "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
    1.33 -    and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)"
    1.34 +  fixes xs ys :: "'b::enum list"
    1.35 +  assumes length: "length xs = length (enum :: 'a::enum list)"
    1.36 +      "length ys = length (enum :: 'a::enum list)"
    1.37 +    and map_of: "the \<circ> map_of (zip (enum :: 'a::enum list) xs) = the \<circ> map_of (zip (enum :: 'a::enum list) ys)"
    1.38    shows "xs = ys"
    1.39  proof -
    1.40 -  have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
    1.41 +  have "map_of (zip (enum :: 'a list) xs) = map_of (zip (enum :: 'a list) ys)"
    1.42    proof
    1.43      fix x :: 'a
    1.44      from length map_of_zip_enum_is_Some obtain y1 y2
    1.45 -      where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
    1.46 -        and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
    1.47 +      where "map_of (zip (enum :: 'a list) xs) x = Some y1"
    1.48 +        and "map_of (zip (enum :: 'a list) ys) x = Some y2" by blast
    1.49      moreover from map_of
    1.50 -      have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
    1.51 +      have "the (map_of (zip (enum :: 'a::enum list) xs) x) = the (map_of (zip (enum :: 'a::enum list) ys) x)"
    1.52        by (auto dest: fun_cong)
    1.53 -    ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
    1.54 +    ultimately show "map_of (zip (enum :: 'a::enum list) xs) x = map_of (zip (enum :: 'a::enum list) ys) x"
    1.55        by simp
    1.56    qed
    1.57    with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
    1.58 @@ -297,7 +297,7 @@
    1.59  begin
    1.60  
    1.61  definition
    1.62 -  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (List.n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
    1.63 +  "enum = map (\<lambda>ys. the o map_of (zip (enum::'a list) ys)) (List.n_lists (length (enum::'a::enum list)) enum)"
    1.64  
    1.65  definition
    1.66    "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
    1.67 @@ -306,17 +306,17 @@
    1.68    "enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
    1.69  
    1.70  instance proof
    1.71 -  show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
    1.72 +  show "UNIV = set (enum :: ('a \<Rightarrow> 'b) list)"
    1.73    proof (rule UNIV_eq_I)
    1.74      fix f :: "'a \<Rightarrow> 'b"
    1.75 -    have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
    1.76 +    have "f = the \<circ> map_of (zip (enum :: 'a::enum list) (map f enum))"
    1.77        by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
    1.78      then show "f \<in> set enum"
    1.79        by (auto simp add: enum_fun_def set_n_lists intro: in_enum)
    1.80    qed
    1.81  next
    1.82    from map_of_zip_enum_inject
    1.83 -  show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
    1.84 +  show "distinct (enum :: ('a \<Rightarrow> 'b) list)"
    1.85      by (auto intro!: inj_onI simp add: enum_fun_def
    1.86        distinct_map distinct_n_lists enum_distinct set_n_lists)
    1.87  next
    1.88 @@ -327,7 +327,7 @@
    1.89      show "Ball UNIV P"
    1.90      proof
    1.91        fix f :: "'a \<Rightarrow> 'b"
    1.92 -      have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
    1.93 +      have f: "f = the \<circ> map_of (zip (enum :: 'a::enum list) (map f enum))"
    1.94          by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
    1.95        from \<open>enum_all P\<close> have "P (the \<circ> map_of (zip enum (map f enum)))"
    1.96          unfolding enum_all_fun_def all_n_lists_def
    1.97 @@ -352,9 +352,9 @@
    1.98    next
    1.99      assume "Bex UNIV P"
   1.100      from this obtain f where "P f" ..
   1.101 -    have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   1.102 +    have f: "f = the \<circ> map_of (zip (enum :: 'a::enum list) (map f enum))"
   1.103        by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) 
   1.104 -    from \<open>P f\<close> this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))"
   1.105 +    from \<open>P f\<close> this have "P (the \<circ> map_of (zip (enum :: 'a::enum list) (map f enum)))"
   1.106        by auto
   1.107      from  this show "enum_ex P"
   1.108        unfolding enum_ex_fun_def ex_n_lists_def
   1.109 @@ -367,7 +367,7 @@
   1.110  
   1.111  end
   1.112  
   1.113 -lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
   1.114 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum :: 'a::{enum, equal} list)
   1.115    in map (\<lambda>ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
   1.116    by (simp add: enum_fun_def Let_def)
   1.117