src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 51144 0ede9e2266a8
parent 51143 0a2371e7ced3
child 55932 68c5104d2204
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:31 2013 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -334,7 +334,7 @@
     1.4  code_pred [dseq] one_or_two .
     1.5  code_pred [random_dseq] one_or_two .
     1.6  thm one_or_two.dseq_equation
     1.7 -values [expected "{1::nat, 2::nat}"] "{x. one_or_two x}"
     1.8 +values [expected "{Suc 0, Suc (Suc 0)}"] "{x. one_or_two x}"
     1.9  values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
    1.10  
    1.11  inductive one_or_two' :: "nat => bool"
    1.12 @@ -387,9 +387,9 @@
    1.13  
    1.14  values [expected "{}" dseq 0] 8 "{x. even x}"
    1.15  values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
    1.16 -values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
    1.17 -values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
    1.18 -values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
    1.19 +values [expected "{0, Suc (Suc 0)}" dseq 3] 8 "{x. even x}"
    1.20 +values [expected "{0, Suc (Suc 0)}" dseq 4] 8 "{x. even x}"
    1.21 +values [expected "{0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))}" dseq 6] 8 "{x. even x}"
    1.22  
    1.23  values [random_dseq 1, 1, 0] 8 "{x. even x}"
    1.24  values [random_dseq 1, 1, 1] 8 "{x. even x}"
    1.25 @@ -442,7 +442,7 @@
    1.26  values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
    1.27  
    1.28  values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.29 -values [expected "{(([]::nat list), [1, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.30 +values [expected "{(([]::nat list), [Suc 0, Suc (Suc 0), Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc 0))), Suc (Suc (Suc (Suc (Suc 0))))])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.31  values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.32  values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.33  values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.34 @@ -553,9 +553,9 @@
    1.35  
    1.36  thm filter1.equation
    1.37  
    1.38 -values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    1.39 +values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    1.40  values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    1.41 -values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    1.42 +values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    1.43  
    1.44  inductive filter2
    1.45  where
    1.46 @@ -1233,16 +1233,21 @@
    1.47  thm plus_nat_test.equation
    1.48  thm plus_nat_test.new_random_dseq_equation
    1.49  
    1.50 -values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
    1.51 -values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
    1.52 -values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
    1.53 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 4 5 z}"
    1.54 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 7 2 z}"
    1.55 +values [expected "{Suc (Suc (Suc (Suc 0)))}"] "{y. plus_nat_test 5 y 9}"
    1.56  values [expected "{}"] "{y. plus_nat_test 9 y 8}"
    1.57 -values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
    1.58 -values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
    1.59 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc 0)))))}"] "{y. plus_nat_test 1 y 7}"
    1.60 +values [expected "{Suc (Suc 0)}"] "{x. plus_nat_test x 7 9}"
    1.61  values [expected "{}"] "{x. plus_nat_test x 9 7}"
    1.62 -values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
    1.63 -values [expected "{(0::nat, 1::nat), (1, 0)}"] "{(x, y). plus_nat_test x y 1}"
    1.64 -values [expected "{(0::nat, 5::nat), (4, 1), (3, 2), (2, 3), (1, 4), (5, 0)}"]
    1.65 +values [expected "{(0::nat, 0::nat)}"] "{(x, y). plus_nat_test x y 0}"
    1.66 +values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
    1.67 +values [expected "{(0, Suc (Suc (Suc (Suc (Suc 0))))),
    1.68 +                  (Suc 0, Suc (Suc (Suc (Suc 0)))),
    1.69 +                  (Suc (Suc 0), Suc (Suc (Suc 0))),
    1.70 +                  (Suc (Suc (Suc 0)), Suc (Suc 0)),
    1.71 +                  (Suc (Suc (Suc (Suc 0))), Suc 0),
    1.72 +                  (Suc (Suc (Suc (Suc (Suc 0)))), 0)}"]
    1.73    "{(x, y). plus_nat_test x y 5}"
    1.74  
    1.75  inductive minus_nat_test :: "nat => nat => nat => bool"
    1.76 @@ -1256,10 +1261,10 @@
    1.77  thm minus_nat_test.new_random_dseq_equation
    1.78  
    1.79  values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
    1.80 -values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
    1.81 -values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
    1.82 -values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
    1.83 -values [expected "{0::nat, 1, 2, 3}"] "{x. minus_nat_test x 3 0}"
    1.84 +values [expected "{Suc (Suc (Suc (Suc (Suc 0))))}"] "{z. minus_nat_test 7 2 z}"
    1.85 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 7 9}"
    1.86 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 9 7}"
    1.87 +values [expected "{0, Suc 0, Suc (Suc 0), Suc (Suc (Suc 0))}"] "{x. minus_nat_test x 3 0}"
    1.88  values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
    1.89  
    1.90  subsection {* Examples on int *}