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