adding test case for interpretation of arguments that are predicates simply as input
authorbulwahn
Tue Sep 28 11:59:53 2010 +0200 (2010-09-28)
changeset 3976519cb8d558166
parent 39764 1cf2088cf035
child 39766 66c1e526fd44
adding test case for interpretation of arguments that are predicates simply as input
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:52 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:53 2010 +0200
     1.3 @@ -1496,8 +1496,21 @@
     1.4  
     1.5  code_pred test_relation_in_output_terms .
     1.6  
     1.7 -
     1.8  thm test_relation_in_output_terms.equation
     1.9  
    1.10  
    1.11 +text {*
    1.12 +  We want that the argument r is not treated as a higher-order relation, but simply as input.
    1.13 +*}
    1.14 +
    1.15 +inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
    1.16 +where
    1.17 +  "list_all r xs ==> test_uninterpreted_relation r xs"
    1.18 +
    1.19 +code_pred (modes: i => i => bool) test_uninterpreted_relation .
    1.20 +
    1.21 +thm test_uninterpreted_relation.equation
    1.22 +
    1.23 +
    1.24 +
    1.25  end