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