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