1 theory Examples |
1 theory Examples |
2 imports Spec_Check |
2 imports Spec_Check |
3 begin |
3 begin |
4 |
4 |
5 section {* List examples *} |
5 section \<open>List examples\<close> |
6 |
6 |
7 ML_command {* |
7 ML_command \<open> |
8 check_property "ALL xs. rev xs = xs"; |
8 check_property "ALL xs. rev xs = xs"; |
9 *} |
9 \<close> |
10 |
10 |
11 ML_command {* |
11 ML_command \<open> |
12 check_property "ALL xs. rev (rev xs) = xs"; |
12 check_property "ALL xs. rev (rev xs) = xs"; |
13 *} |
13 \<close> |
14 |
14 |
15 |
15 |
16 section {* AList Specification *} |
16 section \<open>AList Specification\<close> |
17 |
17 |
18 ML_command {* |
18 ML_command \<open> |
19 (* map_entry applies the function to the element *) |
19 (* map_entry applies the function to the element *) |
20 check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)"; |
20 check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)"; |
21 *} |
21 \<close> |
22 |
22 |
23 ML_command {* |
23 ML_command \<open> |
24 (* update always results in an entry *) |
24 (* update always results in an entry *) |
25 check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k"; |
25 check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k"; |
26 *} |
26 \<close> |
27 |
27 |
28 ML_command {* |
28 ML_command \<open> |
29 (* update always writes the value *) |
29 (* update always writes the value *) |
30 check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v"; |
30 check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v"; |
31 *} |
31 \<close> |
32 |
32 |
33 ML_command {* |
33 ML_command \<open> |
34 (* default always results in an entry *) |
34 (* default always results in an entry *) |
35 check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k"; |
35 check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k"; |
36 *} |
36 \<close> |
37 |
37 |
38 ML_command {* |
38 ML_command \<open> |
39 (* delete always removes the entry *) |
39 (* delete always removes the entry *) |
40 check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)"; |
40 check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)"; |
41 *} |
41 \<close> |
42 |
42 |
43 ML_command {* |
43 ML_command \<open> |
44 (* default writes the entry iff it didn't exist *) |
44 (* default writes the entry iff it didn't exist *) |
45 check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))"; |
45 check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))"; |
46 *} |
46 \<close> |
47 |
47 |
48 section {* Examples on Types and Terms *} |
48 section \<open>Examples on Types and Terms\<close> |
49 |
49 |
50 ML_command {* |
50 ML_command \<open> |
51 check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t"; |
51 check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t"; |
52 *} |
52 \<close> |
53 |
53 |
54 ML_command {* |
54 ML_command \<open> |
55 check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t"; |
55 check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t"; |
56 *} |
56 \<close> |
57 |
57 |
58 |
58 |
59 text {* One would think this holds: *} |
59 text \<open>One would think this holds:\<close> |
60 |
60 |
61 ML_command {* |
61 ML_command \<open> |
62 check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)" |
62 check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)" |
63 *} |
63 \<close> |
64 |
64 |
65 text {* But it only holds with this precondition: *} |
65 text \<open>But it only holds with this precondition:\<close> |
66 |
66 |
67 ML_command {* |
67 ML_command \<open> |
68 check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)" |
68 check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)" |
69 *} |
69 \<close> |
70 |
70 |
71 section {* Some surprises *} |
71 section \<open>Some surprises\<close> |
72 |
72 |
73 ML_command {* |
73 ML_command \<open> |
74 check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)" |
74 check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)" |
75 *} |
75 \<close> |
76 |
76 |
77 |
77 |
78 ML_command {* |
78 ML_command \<open> |
79 val thy = @{theory}; |
79 val thy = @{theory}; |
80 check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true" |
80 check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true" |
81 *} |
81 \<close> |
82 |
82 |
83 end |
83 end |