src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 47108 2a1953f0d20d
parent 46752 e9e7209eb375
child 47433 07f4bf913230
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Mar 25 20:15:39 2012 +0200
     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 "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
     1.8 +values [expected "{1::nat, 2::nat}"] "{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 @@ -442,7 +442,7 @@
    1.13  values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
    1.14  
    1.15  values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.16 -values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.17 +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.18  values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.19  values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.20  values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    1.21 @@ -1241,8 +1241,8 @@
    1.22  values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
    1.23  values [expected "{}"] "{x. plus_nat_test x 9 7}"
    1.24  values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
    1.25 -values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
    1.26 -values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"]
    1.27 +values [expected "{(0::nat, 1::nat), (1, 0)}"] "{(x, y). plus_nat_test x y 1}"
    1.28 +values [expected "{(0::nat, 5::nat), (4, 1), (3, 2), (2, 3), (1, 4), (5, 0)}"]
    1.29    "{(x, y). plus_nat_test x y 5}"
    1.30  
    1.31  inductive minus_nat_test :: "nat => nat => nat => bool"
    1.32 @@ -1259,7 +1259,7 @@
    1.33  values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
    1.34  values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
    1.35  values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
    1.36 -values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}"
    1.37 +values [expected "{0::nat, 1, 2, 3}"] "{x. minus_nat_test x 3 0}"
    1.38  values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
    1.39  
    1.40  subsection {* Examples on int *}