# HG changeset patch # User nipkow # Date 1181149927 -7200 # Node ID e39dd93161d90fc92cdcbf5860b22f52f9020683 # Parent 375335bf619f8d90bbacd1b6f799e4caf17ee701 tuned list comprehension, changed filter syntax from : to <- diff -r 375335bf619f -r e39dd93161d9 src/HOL/List.thy --- a/src/HOL/List.thy Wed Jun 06 18:32:05 2007 +0200 +++ b/src/HOL/List.thy Wed Jun 06 19:12:07 2007 +0200 @@ -42,8 +42,8 @@ "distinct":: "'a list => bool" replicate :: "nat => 'a => 'a list" splice :: "'a list \ 'a list \ 'a list" + partition :: "('a \ bool) \'a list \ (('a list) \ ('a list))" allpairs :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ 'c list" - partition :: "('a \ bool) \'a list \ (('a list) \ ('a list))" abbreviation upto:: "nat => nat => nat list" ("(1[_../_])") where @@ -57,7 +57,7 @@ "@list" :: "args => 'a list" ("[(_)]") -- {* Special syntax for filter *} - "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_:_./ _])") + "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])") -- {* list update *} "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") @@ -68,16 +68,16 @@ translations "[x, xs]" == "x#[xs]" "[x]" == "x#[]" - "[x:xs . P]"== "filter (%x. P) xs" + "[x<-xs . P]"== "filter (%x. P) xs" "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs" "xs[i:=x]" == "list_update xs i x" syntax (xsymbols) - "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") + "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") syntax (HTML output) - "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") + "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") text {* @@ -253,20 +253,25 @@ syntax "_listcompr" :: "'a \ lc_qual \ lc_quals \ 'a list" ("[_ . __") -"_lc_gen" :: "pttrn \ 'a list \ lc_qual" ("_ \ _") "_lc_gen" :: "pttrn \ 'a list \ lc_qual" ("_ <- _") "_lc_test" :: "bool \ lc_qual" ("_") "_lc_end" :: "lc_quals" ("]") "_lc_quals" :: "lc_qual \ lc_quals \ lc_quals" (", __") translations -"[e. p\xs]" => "map (%p. e) xs" +"[e. p<-xs]" => "map (%p. e) xs" "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" => "concat (map (%p. _listcompr e Q Qs) xs)" "[e. P]" => "if P then [e] else []" "_listcompr e (_lc_test P) (_lc_quals Q Qs)" => "if P then (_listcompr e Q Qs) else []" +syntax (xsymbols) +"_lc_gen" :: "pttrn \ 'a list \ lc_qual" ("_ \ _") +syntax (HTML output) +"_lc_gen" :: "pttrn \ 'a list \ lc_qual" ("_ \ _") + + (* term "[(x,y,z). b]" term "[(x,y,z). x \ xs]" @@ -2270,8 +2275,8 @@ done lemma sublist_shift_lemma: - "map fst [p:zip xs [i..