farewell to theory More_List
authorhaftmann
Fri Jan 06 20:39:50 2012 +0100 (2012-01-06)
changeset 46143c932c80d3eae
parent 46142 94479a979129
child 46144 cc374091999b
farewell to theory More_List
src/HOL/IsaMakefile
src/HOL/Library/Monad_Syntax.thy
src/HOL/List.thy
src/HOL/More_List.thy
src/HOL/More_Set.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 06 11:15:02 2012 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 06 20:39:50 2012 +0100
     1.3 @@ -286,7 +286,6 @@
     1.4    List.thy \
     1.5    Main.thy \
     1.6    Map.thy \
     1.7 -  More_List.thy \
     1.8    More_Set.thy \
     1.9    Nat_Numeral.thy \
    1.10    Nat_Transfer.thy \
     2.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Jan 06 11:15:02 2012 +0100
     2.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Fri Jan 06 20:39:50 2012 +0100
     2.3 @@ -74,7 +74,7 @@
     2.4    #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
     2.5    #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
     2.6    #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
     2.7 -  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
     2.8 +  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
     2.9  *}
    2.10  
    2.11  end
     3.1 --- a/src/HOL/List.thy	Fri Jan 06 11:15:02 2012 +0100
     3.2 +++ b/src/HOL/List.thy	Fri Jan 06 20:39:50 2012 +0100
     3.3 @@ -5109,6 +5109,19 @@
     3.4  by (induct xs) force+
     3.5  
     3.6  
     3.7 +subsection {* Monad operation *}
     3.8 +
     3.9 +definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
    3.10 +  "bind xs f = concat (map f xs)"
    3.11 +
    3.12 +hide_const (open) bind
    3.13 +
    3.14 +lemma bind_simps [simp]:
    3.15 +  "List.bind [] f = []"
    3.16 +  "List.bind (x # xs) f = f x @ List.bind xs f"
    3.17 +  by (simp_all add: bind_def)
    3.18 +
    3.19 +
    3.20  subsection {* Transfer *}
    3.21  
    3.22  definition
     4.1 --- a/src/HOL/More_List.thy	Fri Jan 06 11:15:02 2012 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,19 +0,0 @@
     4.4 -(* Author:  Florian Haftmann, TU Muenchen *)
     4.5 -
     4.6 -header {* Operations on lists beyond the standard List theory *}
     4.7 -
     4.8 -theory More_List
     4.9 -imports List
    4.10 -begin
    4.11 -
    4.12 -text {* monad operation *}
    4.13 -
    4.14 -definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
    4.15 -  "bind xs f = concat (map f xs)"
    4.16 -
    4.17 -lemma bind_simps [simp]:
    4.18 -  "bind [] f = []"
    4.19 -  "bind (x # xs) f = f x @ bind xs f"
    4.20 -  by (simp_all add: bind_def)
    4.21 -
    4.22 -end
     5.1 --- a/src/HOL/More_Set.thy	Fri Jan 06 11:15:02 2012 +0100
     5.2 +++ b/src/HOL/More_Set.thy	Fri Jan 06 20:39:50 2012 +0100
     5.3 @@ -4,7 +4,7 @@
     5.4  header {* Relating (finite) sets and lists *}
     5.5  
     5.6  theory More_Set
     5.7 -imports More_List
     5.8 +imports List
     5.9  begin
    5.10  
    5.11  lemma comp_fun_idem_remove: