src/ZF/List.thy

 section\<open>Lists in Zermelo-Fraenkel Set Theory\<close>
 
 theory List imports Datatype ArithSimp begin
 
 consts
-  list       :: "i=>i"
+  list       :: "i\<Rightarrow>i"
 
 datatype
   "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)")
 
 
 syntax
  "_Nil" :: i  (\<open>[]\<close>)
- "_List" :: "is => i"  (\<open>[(_)]\<close>)
+ "_List" :: "is \<Rightarrow> i"  (\<open>[(_)]\<close>)
 
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
   "[]"          == "CONST Nil"
 
 
 consts
-  length :: "i=>i"
-  hd     :: "i=>i"
-  tl     :: "i=>i"
+  length :: "i\<Rightarrow>i"
+  hd     :: "i\<Rightarrow>i"
+  tl     :: "i\<Rightarrow>i"
 
 primrec
   "length([]) = 0"
   "length(Cons(a,l)) = succ(length(l))"
 

   "tl([]) = []"
   "tl(Cons(a,l)) = l"
 
 
 consts
-  map         :: "[i=>i, i] => i"
-  set_of_list :: "i=>i"
-  app         :: "[i,i]=>i"                        (infixr \<open>@\<close> 60)
+  map         :: "[i\<Rightarrow>i, i] \<Rightarrow> i"
+  set_of_list :: "i\<Rightarrow>i"
+  app         :: "[i,i]\<Rightarrow>i"                        (infixr \<open>@\<close> 60)
 
 (*map is a binding operator -- it applies to meta-level functions, not
 object-level functions.  This simplifies the final form of term_rec_conv,
 although complicating its derivation.*)
 primrec

   app_Nil:  "[] @ ys = ys"
   app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
 
 
 consts
-  rev :: "i=>i"
-  flat       :: "i=>i"
-  list_add   :: "i=>i"
+  rev :: "i\<Rightarrow>i"
+  flat       :: "i\<Rightarrow>i"
+  list_add   :: "i\<Rightarrow>i"
 
 primrec
   "rev([]) = []"
   "rev(Cons(a,l)) = rev(l) @ [a]"
 

 primrec
   "list_add([]) = 0"
   "list_add(Cons(a,l)) = a #+ list_add(l)"
 
 consts
-  drop       :: "[i,i]=>i"
+  drop       :: "[i,i]\<Rightarrow>i"
 
 primrec
   drop_0:    "drop(0,l) = l"
   drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
 
 
 (*** Thanks to Sidi Ehmety for the following ***)
 
 definition
 (* Function `take' returns the first n elements of a list *)
-  take     :: "[i,i]=>i"  where
+  take     :: "[i,i]\<Rightarrow>i"  where
   "take(n, as) \<equiv> list_rec(\<lambda>n\<in>nat. [],
-                %a l r. \<lambda>n\<in>nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
+                \<lambda>a l r. \<lambda>n\<in>nat. nat_case([], \<lambda>m. Cons(a, r`m), n), as)`n"
 
 definition
-  nth :: "[i, i]=>i"  where
+  nth :: "[i, i]\<Rightarrow>i"  where
   \<comment> \<open>returns the (n+1)th element of a list, or 0 if the
    list is too short.\<close>
   "nth(n, as) \<equiv> list_rec(\<lambda>n\<in>nat. 0,
-                          %a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n"
+                          \<lambda>a l r. \<lambda>n\<in>nat. nat_case(a, \<lambda>m. r`m, n), as) ` n"
 
 definition
-  list_update :: "[i, i, i]=>i"  where
+  list_update :: "[i, i, i]\<Rightarrow>i"  where
   "list_update(xs, i, v) \<equiv> list_rec(\<lambda>n\<in>nat. Nil,
-      %u us vs. \<lambda>n\<in>nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"
+      \<lambda>u us vs. \<lambda>n\<in>nat. nat_case(Cons(v, us), \<lambda>m. Cons(u, vs`m), n), xs)`i"
 
 consts
-  filter :: "[i=>o, i] => i"
-  upt :: "[i, i] =>i"
+  filter :: "[i\<Rightarrow>o, i] \<Rightarrow> i"
+  upt :: "[i, i] \<Rightarrow>i"
 
 primrec
   "filter(P, Nil) = Nil"
   "filter(P, Cons(x, xs)) =
      (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"

 primrec
   "upt(i, 0) = Nil"
   "upt(i, succ(j)) = (if i \<le> j then upt(i, j)@[j] else Nil)"
 
 definition
-  min :: "[i,i] =>i"  where
+  min :: "[i,i] \<Rightarrow>i"  where
     "min(x, y) \<equiv> (if x \<le> y then x else y)"
 
 definition
-  max :: "[i, i] =>i"  where
+  max :: "[i, i] \<Rightarrow>i"  where
     "max(x, y) \<equiv> (if x \<le> y then y else x)"
 
 (*** Aspects of the datatype definition ***)
 
 declare list.intros [simp,TC]

 by (simp add: list_add_list_def)
 
 
 (*** theorems about map ***)
 
-lemma map_ident [simp]: "l \<in> list(A) \<Longrightarrow> map(%u. u, l) = l"
+lemma map_ident [simp]: "l \<in> list(A) \<Longrightarrow> map(\<lambda>u. u, l) = l"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp))
 done
 
-lemma map_compose: "l \<in> list(A) \<Longrightarrow> map(h, map(j,l)) = map(%u. h(j(u)), l)"
+lemma map_compose: "l \<in> list(A) \<Longrightarrow> map(h, map(j,l)) = map(\<lambda>u. h(j(u)), l)"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp))
 done
 
 lemma map_app_distrib: "xs: list(A) \<Longrightarrow> map(h, xs@ys) = map(h,xs) @ map(h,ys)"

 done
 
 lemma list_rec_map:
      "l \<in> list(A) \<Longrightarrow>
       list_rec(c, d, map(h,l)) =
-      list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
+      list_rec(c, \<lambda>x xs r. d(h(x), map(h,xs), r), l)"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp))
 done
 
 (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)

 done
 
 lemma filter_is_subset: "xs:list(A) \<Longrightarrow> set_of_list(filter(P,xs)) \<subseteq> set_of_list(xs)"
 by (induct_tac "xs", auto)
 
-lemma filter_False [simp]: "xs:list(A) \<Longrightarrow> filter(%p. False, xs) = Nil"
+lemma filter_False [simp]: "xs:list(A) \<Longrightarrow> filter(\<lambda>p. False, xs) = Nil"
 by (induct_tac "xs", auto)
 
-lemma filter_True [simp]: "xs:list(A) \<Longrightarrow> filter(%p. True, xs) = xs"
+lemma filter_True [simp]: "xs:list(A) \<Longrightarrow> filter(\<lambda>p. True, xs) = xs"
 by (induct_tac "xs", auto)
 
 (** length **)
 
 lemma length_is_0_iff [simp]: "xs:list(A) \<Longrightarrow> length(xs)=0 \<longleftrightarrow> xs=Nil"

 subsection\<open>The function zip\<close>
 
 text\<open>Crafty definition to eliminate a type argument\<close>
 
 consts
-  zip_aux        :: "[i,i]=>i"
+  zip_aux        :: "[i,i]\<Rightarrow>i"
 
 primrec (*explicit lambda is required because both arguments of "un" vary*)
   "zip_aux(B,[]) =
-     (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
+     (\<lambda>ys \<in> list(B). list_case([], \<lambda>y l. [], ys))"
 
   "zip_aux(B,Cons(x,l)) =
      (\<lambda>ys \<in> list(B).
-        list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
+        list_case(Nil, \<lambda>y zs. Cons(\<langle>x,y\<rangle>, zip_aux(B,l)`zs), ys))"
 
 definition
-  zip :: "[i, i]=>i"  where
+  zip :: "[i, i]\<Rightarrow>i"  where
    "zip(xs, ys) \<equiv> zip_aux(set_of_list(ys),xs)`ys"
 
 
 (* zip equations *)
 

 apply (blast intro: list_mono [THEN subsetD])
 done
 
 lemma zip_Cons_Cons [simp]:
      "\<lbrakk>xs:list(A); ys:list(B); x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow>
-      zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
+      zip(Cons(x,xs), Cons(y, ys)) = Cons(\<langle>x,y\<rangle>, zip(xs, ys))"
 apply (simp add: zip_def, auto)
 apply (rule zip_aux_unique, auto)
 apply (simp add: list_on_set_of_list [of _ B])
 apply (blast intro: list_on_set_of_list list_mono [THEN subsetD])
 done

 declare nth_zip [simp]
 
 lemma set_of_list_zip [rule_format]:
      "\<lbrakk>xs:list(A); ys:list(B); i \<in> nat\<rbrakk>
       \<Longrightarrow> set_of_list(zip(xs, ys)) =
-          {<x, y>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys))
+          {\<langle>x, y\<rangle>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys))
           \<and> x = nth(i, xs) \<and> y = nth(i, ys)}"
 by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
 
 (** list_update **)
 

 done
 
 (** sublist (a generalization of nth to sets) **)
 
 definition
-  sublist :: "[i, i] => i"  where
+  sublist :: "[i, i] \<Rightarrow> i"  where
     "sublist(xs, A)\<equiv>
-     map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
+     map(fst, (filter(\<lambda>p. snd(p): A, zip(xs, upt(0,length(xs))))))"
 
 lemma sublist_0 [simp]: "xs:list(A) \<Longrightarrow>sublist(xs, 0) =Nil"
 by (unfold sublist_def, auto)
 
 lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
 by (unfold sublist_def, auto)
 
 lemma sublist_shift_lemma:
  "\<lbrakk>xs:list(B); i \<in> nat\<rbrakk> \<Longrightarrow>
-  map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
-  map(fst, filter(%p. snd(p):nat \<and> snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))"
+  map(fst, filter(\<lambda>p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
+  map(fst, filter(\<lambda>p. snd(p):nat \<and> snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))"
 apply (erule list_append_induct)
 apply (simp (no_asm_simp))
 apply (auto simp add: add_commute length_app filter_append map_app_distrib)
 done
 

 apply (simp_all add: sublist_Cons)
 done
 
 text\<open>Repetition of a List Element\<close>
 
-consts   repeat :: "[i,i]=>i"
+consts   repeat :: "[i,i]\<Rightarrow>i"
 primrec
   "repeat(a,0) = []"
 
   "repeat(a,succ(n)) = Cons(a,repeat(a,n))"