actually check list comprehension examples;
authorwenzelm
Wed Mar 30 20:19:21 2011 +0200 (2011-03-30)
changeset 421677d8cb105373c
parent 42166 efd229daeb2c
child 42168 3164e7263b53
actually check list comprehension examples;
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Mar 30 17:54:10 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Mar 30 20:19:21 2011 +0200
     1.3 @@ -426,26 +426,45 @@
     1.4  in [(@{syntax_const "_listcompr"}, lc_tr)] end
     1.5  *}
     1.6  
     1.7 -term "[(x,y,z). b]"
     1.8 -term "[(x,y,z). x\<leftarrow>xs]"
     1.9 -term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
    1.10 -term "[(x,y,z). x<a, x>b]"
    1.11 -term "[(x,y,z). x\<leftarrow>xs, x>b]"
    1.12 -term "[(x,y,z). x<a, x\<leftarrow>xs]"
    1.13 -term "[(x,y). Cons True x \<leftarrow> xs]"
    1.14 -term "[(x,y,z). Cons x [] \<leftarrow> xs]"
    1.15 -term "[(x,y,z). x<a, x>b, x=d]"
    1.16 -term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
    1.17 -term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
    1.18 -term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
    1.19 -term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
    1.20 -term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
    1.21 -term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
    1.22 -term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
    1.23 +ML {*
    1.24 +  let
    1.25 +    val read = Syntax.read_term @{context};
    1.26 +    fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1);
    1.27 +  in
    1.28 +    check "[(x,y,z). b]" "if b then [(x, y, z)] else []";
    1.29 +    check "[(x,y,z). x\<leftarrow>xs]" "map (\<lambda>x. (x, y, z)) xs";
    1.30 +    check "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]" "concat (map (\<lambda>x. map (\<lambda>y. e x y) ys) xs)";
    1.31 +    check "[(x,y,z). x<a, x>b]" "if x < a then if b < x then [(x, y, z)] else [] else []";
    1.32 +    check "[(x,y,z). x\<leftarrow>xs, x>b]" "concat (map (\<lambda>x. if b < x then [(x, y, z)] else []) xs)";
    1.33 +    check "[(x,y,z). x<a, x\<leftarrow>xs]" "if x < a then map (\<lambda>x. (x, y, z)) xs else []";
    1.34 +    check "[(x,y). Cons True x \<leftarrow> xs]"
    1.35 +      "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | True # x \<Rightarrow> [(x, y)] | False # x \<Rightarrow> []) xs)";
    1.36 +    check "[(x,y,z). Cons x [] \<leftarrow> xs]"
    1.37 +      "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | [x] \<Rightarrow> [(x, y, z)] | x # aa # lista \<Rightarrow> []) xs)";
    1.38 +    check "[(x,y,z). x<a, x>b, x=d]"
    1.39 +      "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []";
    1.40 +    check "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
    1.41 +      "if x < a then if b < x then map (\<lambda>y. (x, y, z)) ys else [] else []";
    1.42 +    check "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
    1.43 +      "if x < a then concat (map (\<lambda>x. if b < y then [(x, y, z)] else []) xs) else []";
    1.44 +    check "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
    1.45 +      "if x < a then concat (map (\<lambda>x. map (\<lambda>y. (x, y, z)) ys) xs) else []";
    1.46 +    check "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
    1.47 +      "concat (map (\<lambda>x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)";
    1.48 +    check "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
    1.49 +      "concat (map (\<lambda>x. if b < x then map (\<lambda>y. (x, y, z)) ys else []) xs)";
    1.50 +    check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
    1.51 +      "concat (map (\<lambda>x. concat (map (\<lambda>y. if x < y then [(x, y, z)] else []) ys)) xs)";
    1.52 +    check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
    1.53 +      "concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)"
    1.54 +  end;
    1.55 +*}
    1.56 +
    1.57  (*
    1.58  term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
    1.59  *)
    1.60  
    1.61 +
    1.62  use "Tools/list_to_set_comprehension.ML"
    1.63  
    1.64  simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}