# HG changeset patch # User bulwahn # Date 1285749195 -7200 # Node ID 30c077288dfe841183309520e85c355c3e1f08e1 # Parent 05c4e9ecf5f6a1ee3227e378653bc51cb3ae5757 added test case for predicate arguments in higher-order argument position diff -r 05c4e9ecf5f6 -r 30c077288dfe src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 29 10:33:15 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 29 10:33:15 2010 +0200 @@ -1511,6 +1511,25 @@ thm test_uninterpreted_relation.equation +inductive list_ex' +where + "P x ==> list_ex' P (x#xs)" +| "list_ex' P xs ==> list_ex' P (x#xs)" + +code_pred list_ex' . + +inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool" +where + "list_ex r xs ==> test_uninterpreted_relation2 r xs" +| "list_ex' r xs ==> test_uninterpreted_relation2 r xs" + +text {* Proof procedure cannot handle this situation yet. *} + +code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 . + +thm test_uninterpreted_relation2.equation + + text {* Trivial predicate *} inductive implies_itself :: "'a => bool"