equal
deleted
inserted
replaced
12 begin |
12 begin |
13 |
13 |
14 setup {* Predicate_Compile.setup *} |
14 setup {* Predicate_Compile.setup *} |
15 setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *} |
15 setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *} |
16 |
16 |
|
17 section {* Alternative rules for set *} |
|
18 |
|
19 lemma set_ConsI1 [code_pred_intros]: |
|
20 "set (x # xs) x" |
|
21 unfolding mem_def[symmetric, of _ x] |
|
22 by auto |
|
23 |
|
24 lemma set_ConsI2 [code_pred_intros]: |
|
25 "set xs x ==> set (x' # xs) x" |
|
26 unfolding mem_def[symmetric, of _ x] |
|
27 by auto |
|
28 |
|
29 code_pred set |
|
30 proof - |
|
31 case set |
|
32 from this show thesis |
|
33 apply (case_tac a1) |
|
34 apply auto |
|
35 unfolding mem_def[symmetric, of _ a2] |
|
36 apply auto |
|
37 unfolding mem_def |
|
38 apply auto |
|
39 done |
|
40 qed |
|
41 |
|
42 section {* Alternative rules for list_all2 *} |
|
43 |
|
44 lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []" |
|
45 by auto |
|
46 |
|
47 lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" |
|
48 by auto |
|
49 |
|
50 code_pred list_all2 |
|
51 proof - |
|
52 case list_all2 |
|
53 from this show thesis |
|
54 apply - |
|
55 apply (case_tac a1) |
|
56 apply (case_tac a2) |
|
57 apply auto |
|
58 apply (case_tac a2) |
|
59 apply auto |
|
60 done |
|
61 qed |
|
62 |
17 end |
63 end |