src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 51143 0a2371e7ced3
parent 47433 07f4bf913230
child 51144 0ede9e2266a8
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  thm True'.equation
     1.5  thm True'.dseq_equation
     1.6  thm True'.random_dseq_equation
     1.7 -values [expected "{()}" ]"{x. True'}"
     1.8 +values [expected "{()}"] "{x. True'}"
     1.9  values [expected "{}" dseq 0] "{x. True'}"
    1.10  values [expected "{()}" dseq 1] "{x. True'}"
    1.11  values [expected "{()}" dseq 2] "{x. True'}"
    1.12 @@ -119,22 +119,22 @@
    1.13  
    1.14  code_pred nested_tuples .
    1.15  
    1.16 -inductive JamesBond :: "nat => int => code_numeral => bool"
    1.17 +inductive JamesBond :: "nat => int => natural => bool"
    1.18  where
    1.19    "JamesBond 0 0 7"
    1.20  
    1.21  code_pred JamesBond .
    1.22  
    1.23 -values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
    1.24 -values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
    1.25 -values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
    1.26 -values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
    1.27 -values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
    1.28 -values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
    1.29 +values [expected "{(0::nat, 0::int , 7::natural)}"] "{(a, b, c). JamesBond a b c}"
    1.30 +values [expected "{(0::nat, 7::natural, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
    1.31 +values [expected "{(0::int, 0::nat, 7::natural)}"] "{(b, a, c). JamesBond a b c}"
    1.32 +values [expected "{(0::int, 7::natural, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
    1.33 +values [expected "{(7::natural, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
    1.34 +values [expected "{(7::natural, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
    1.35  
    1.36 -values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
    1.37 -values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
    1.38 -values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
    1.39 +values [expected "{(7::natural, 0::int)}"] "{(a, b). JamesBond 0 b a}"
    1.40 +values [expected "{(7::natural, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
    1.41 +values [expected "{(0::nat, 7::natural)}"] "{(a, c). JamesBond a 0 c}"
    1.42  
    1.43  
    1.44  subsection {* Alternative Rules *}