equal
deleted
inserted
replaced
1509 |
1509 |
1510 code_pred (modes: i => i => bool) test_uninterpreted_relation . |
1510 code_pred (modes: i => i => bool) test_uninterpreted_relation . |
1511 |
1511 |
1512 thm test_uninterpreted_relation.equation |
1512 thm test_uninterpreted_relation.equation |
1513 |
1513 |
|
1514 inductive list_ex' |
|
1515 where |
|
1516 "P x ==> list_ex' P (x#xs)" |
|
1517 | "list_ex' P xs ==> list_ex' P (x#xs)" |
|
1518 |
|
1519 code_pred list_ex' . |
|
1520 |
|
1521 inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool" |
|
1522 where |
|
1523 "list_ex r xs ==> test_uninterpreted_relation2 r xs" |
|
1524 | "list_ex' r xs ==> test_uninterpreted_relation2 r xs" |
|
1525 |
|
1526 text {* Proof procedure cannot handle this situation yet. *} |
|
1527 |
|
1528 code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 . |
|
1529 |
|
1530 thm test_uninterpreted_relation2.equation |
|
1531 |
|
1532 |
1514 text {* Trivial predicate *} |
1533 text {* Trivial predicate *} |
1515 |
1534 |
1516 inductive implies_itself :: "'a => bool" |
1535 inductive implies_itself :: "'a => bool" |
1517 where |
1536 where |
1518 "implies_itself x ==> implies_itself x" |
1537 "implies_itself x ==> implies_itself x" |