src/HOL/Enum.thy
 changeset 67091 1393c2340eec parent 66838 17989f6bc7b2 child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/Enum.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/Enum.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -88,7 +88,7 @@
1.4    [code del]: "enum_the = The"
1.5
1.6  lemma [code]:
1.7 -  "The P = (case filter P enum of [x] => x | _ => enum_the P)"
1.8 +  "The P = (case filter P enum of [x] \<Rightarrow> x | _ \<Rightarrow> enum_the P)"
1.9  proof -
1.10    {
1.11      fix a
1.12 @@ -212,16 +212,16 @@
1.13    then have "\<exists> n. x : bacc r n"
1.14    proof (induct x arbitrary: rule: acc.induct)
1.15      case (accI x)
1.16 -    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
1.17 +    then have "\<forall>y. \<exists> n. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n" by simp
1.18      from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
1.19 -    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
1.20 +    obtain n where "\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> bacc r n"
1.21      proof
1.22 -      fix y assume y: "(y, x) : r"
1.23 +      fix y assume y: "(y, x) \<in> r"
1.24        with n have "y : bacc r (n y)" by auto
1.25 -      moreover have "n y <= Max ((%(y, x). n y) ` r)"
1.26 +      moreover have "n y <= Max ((\<lambda>(y, x). n y) ` r)"
1.27          using y \<open>finite r\<close> by (auto intro!: Max_ge)
1.28        note bacc_mono[OF this, of r]
1.29 -      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
1.30 +      ultimately show "y : bacc r (Max ((\<lambda>(y, x). n y) ` r))" by auto
1.31      qed
1.32      then show ?case
1.33        by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
1.34 @@ -297,13 +297,13 @@
1.35  begin
1.36
1.37  definition
1.38 -  "enum = map (\<lambda>ys. the o map_of (zip (enum::'a list) ys)) (List.n_lists (length (enum::'a::enum list)) enum)"
1.39 +  "enum = map (\<lambda>ys. the \<circ> map_of (zip (enum::'a list) ys)) (List.n_lists (length (enum::'a::enum list)) enum)"
1.40
1.41  definition
1.42 -  "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
1.43 +  "enum_all P = all_n_lists (\<lambda>bs. P (the \<circ> map_of (zip enum bs))) (length (enum :: 'a list))"
1.44
1.45  definition
1.46 -  "enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
1.47 +  "enum_ex P = ex_n_lists (\<lambda>bs. P (the \<circ> map_of (zip enum bs))) (length (enum :: 'a list))"
1.48
1.49  instance proof
1.50    show "UNIV = set (enum :: ('a \<Rightarrow> 'b) list)"
1.51 @@ -368,17 +368,17 @@
1.52  end
1.53
1.54  lemma enum_fun_code [code]: "enum = (let enum_a = (enum :: 'a::{enum, equal} list)
1.55 -  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
1.56 +  in map (\<lambda>ys. the \<circ> map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
1.57    by (simp add: enum_fun_def Let_def)
1.58
1.59  lemma enum_all_fun_code [code]:
1.60    "enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list)
1.61 -   in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
1.62 +   in all_n_lists (\<lambda>bs. P (the \<circ> map_of (zip enum_a bs))) (length enum_a))"
1.63    by (simp only: enum_all_fun_def Let_def)
1.64
1.65  lemma enum_ex_fun_code [code]:
1.66    "enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list)
1.67 -   in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
1.68 +   in ex_n_lists (\<lambda>bs. P (the \<circ> map_of (zip enum_a bs))) (length enum_a))"
1.69    by (simp only: enum_ex_fun_def Let_def)
1.70
1.71  instantiation set :: (enum) enum
```