equal
deleted
inserted
replaced
10 |
10 |
11 section {* Alternative list definitions *} |
11 section {* Alternative list definitions *} |
12 |
12 |
13 subsection {* Alternative rules for set *} |
13 subsection {* Alternative rules for set *} |
14 |
14 |
15 lemma set_ConsI1 [code_pred_intros]: |
15 lemma set_ConsI1 [code_pred_intro]: |
16 "set (x # xs) x" |
16 "set (x # xs) x" |
17 unfolding mem_def[symmetric, of _ x] |
17 unfolding mem_def[symmetric, of _ x] |
18 by auto |
18 by auto |
19 |
19 |
20 lemma set_ConsI2 [code_pred_intros]: |
20 lemma set_ConsI2 [code_pred_intro]: |
21 "set xs x ==> set (x' # xs) x" |
21 "set xs x ==> set (x' # xs) x" |
22 unfolding mem_def[symmetric, of _ x] |
22 unfolding mem_def[symmetric, of _ x] |
23 by auto |
23 by auto |
24 |
24 |
25 code_pred set |
25 code_pred set |
35 done |
35 done |
36 qed |
36 qed |
37 |
37 |
38 subsection {* Alternative rules for list_all2 *} |
38 subsection {* Alternative rules for list_all2 *} |
39 |
39 |
40 lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []" |
40 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []" |
41 by auto |
41 by auto |
42 |
42 |
43 lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" |
43 lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" |
44 by auto |
44 by auto |
45 |
45 |
46 code_pred list_all2 |
46 code_pred list_all2 |
47 proof - |
47 proof - |
48 case list_all2 |
48 case list_all2 |