494 code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 . |
494 code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 . |
495 |
495 |
496 code_pred [dseq] filter3 . |
496 code_pred [dseq] filter3 . |
497 thm filter3.dseq_equation |
497 thm filter3.dseq_equation |
498 *) |
498 *) |
|
499 (* |
499 inductive filter4 |
500 inductive filter4 |
500 where |
501 where |
501 "List.filter P xs = ys ==> filter4 P xs ys" |
502 "List.filter P xs = ys ==> filter4 P xs ys" |
502 |
503 |
503 (*code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .*) |
504 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 . |
504 (*code_pred [depth_limited] filter4 .*) |
505 (*code_pred [depth_limited] filter4 .*) |
505 (*code_pred [random] filter4 .*) |
506 (*code_pred [random] filter4 .*) |
506 |
507 *) |
507 subsection {* reverse predicate *} |
508 subsection {* reverse predicate *} |
508 |
509 |
509 inductive rev where |
510 inductive rev where |
510 "rev [] []" |
511 "rev [] []" |
511 | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" |
512 | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" |
887 by auto |
888 by auto |
888 qed |
889 qed |
889 |
890 |
890 code_pred [random_dseq inductify] lexn |
891 code_pred [random_dseq inductify] lexn |
891 proof - |
892 proof - |
892 fix n xs ys |
893 fix r n xs ys |
893 assume 1: "lexn r n (xs, ys)" |
894 assume 1: "lexn r n (xs, ys)" |
894 assume 2: "\<And>i x xs' y ys'. r = r ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r (x, y) ==> thesis" |
895 assume 2: "\<And>r' i x xs' y ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r' (x, y) ==> thesis" |
895 assume 3: "\<And>i x xs' ys'. r = r ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r i (xs', ys') ==> thesis" |
896 assume 3: "\<And>r' i x xs' ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r' i (xs', ys') ==> thesis" |
896 from 1 2 3 show thesis |
897 from 1 2 3 show thesis |
897 unfolding lexn_conv Collect_def mem_def |
898 unfolding lexn_conv Collect_def mem_def |
898 apply (auto simp add: has_length) |
899 apply (auto simp add: has_length) |
899 apply (case_tac xys) |
900 apply (case_tac xys) |
900 apply auto |
901 apply auto |
901 apply fastsimp |
902 apply fastsimp |
911 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *} |
912 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *} |
912 code_pred [inductify] lex . |
913 code_pred [inductify] lex . |
913 thm lex.equation |
914 thm lex.equation |
914 thm lex_def |
915 thm lex_def |
915 declare lenlex_conv[code_pred_def] |
916 declare lenlex_conv[code_pred_def] |
916 code_pred [inductify, show_steps, show_intermediate_results] lenlex . |
917 code_pred [inductify] lenlex . |
917 thm lenlex.equation |
918 thm lenlex.equation |
918 |
919 |
919 code_pred [random_dseq inductify] lenlex . |
920 code_pred [random_dseq inductify] lenlex . |
920 thm lenlex.random_dseq_equation |
921 thm lenlex.random_dseq_equation |
921 |
922 |
922 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}" |
923 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}" |
923 thm lists.intros |
924 thm lists.intros |
924 |
925 |
925 code_pred [inductify] lists . |
926 code_pred [inductify] lists . |
926 |
|
927 thm lists.equation |
927 thm lists.equation |
928 |
928 |
929 subsection {* AVL Tree *} |
929 subsection {* AVL Tree *} |
930 |
930 |
931 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat |
931 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat |
1000 code_pred (modes: |
1000 code_pred (modes: |
1001 (o * o => bool) => o => bool, |
1001 (o * o => bool) => o => bool, |
1002 (o * o => bool) => i => bool, |
1002 (o * o => bool) => i => bool, |
1003 (i * o => bool) => i => bool) [inductify] Domain . |
1003 (i * o => bool) => i => bool) [inductify] Domain . |
1004 thm Domain.equation |
1004 thm Domain.equation |
|
1005 |
1005 thm Range_def |
1006 thm Range_def |
1006 |
|
1007 code_pred (modes: |
1007 code_pred (modes: |
1008 (o * o => bool) => o => bool, |
1008 (o * o => bool) => o => bool, |
1009 (o * o => bool) => i => bool, |
1009 (o * o => bool) => i => bool, |
1010 (o * i => bool) => i => bool) [inductify] Range . |
1010 (o * i => bool) => i => bool) [inductify] Range . |
1011 thm Range.equation |
1011 thm Range.equation |
1012 |
1012 |
1013 code_pred [inductify] Field . |
1013 code_pred [inductify] Field . |
1014 thm Field.equation |
1014 thm Field.equation |
1015 |
1015 |
1016 (*thm refl_on_def |
1016 thm refl_on_def |
1017 code_pred [inductify] refl_on . |
1017 code_pred [inductify] refl_on . |
1018 thm refl_on.equation*) |
1018 thm refl_on.equation |
1019 code_pred [inductify] total_on . |
1019 code_pred [inductify] total_on . |
1020 thm total_on.equation |
1020 thm total_on.equation |
1021 code_pred [inductify] antisym . |
1021 code_pred [inductify] antisym . |
1022 thm antisym.equation |
1022 thm antisym.equation |
1023 code_pred [inductify] trans . |
1023 code_pred [inductify] trans . |
1024 thm trans.equation |
1024 thm trans.equation |
1025 code_pred [inductify] single_valued . |
1025 code_pred [inductify] single_valued . |
1026 thm single_valued.equation |
1026 thm single_valued.equation |
1027 thm inv_image_def |
1027 thm inv_image_def |
1028 (*code_pred [inductify] inv_image . |
1028 code_pred [inductify] inv_image . |
1029 thm inv_image.equation |
1029 thm inv_image.equation |
1030 *) |
1030 |
1031 subsection {* Inverting list functions *} |
1031 subsection {* Inverting list functions *} |
1032 |
1032 |
1033 (*code_pred [inductify] length . |
1033 (*code_pred [inductify] length . |
1034 code_pred [random inductify] length . |
1034 code_pred [random inductify] length . |
1035 thm size_listP.equation |
1035 thm size_listP.equation |