src/HOL/Mutabelle/MutabelleExtra.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 43018 121aa59b4d17 child 46453 9e83b7c24b05 permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
```     1 theory MutabelleExtra
```
```     2 imports Complex_Main
```
```     3 (*  "~/repos/afp/thys/AVL-Trees/AVL"
```
```     4   "~/repos/afp/thys/BinarySearchTree/BinaryTree"
```
```     5   "~/repos/afp/thys/Huffman/Huffman"
```
```     6   "~/repos/afp/thys/List-Index/List_Index"
```
```     7   "~/repos/afp/thys/Matrix/Matrix"
```
```     8   "~/repos/afp/thys/NormByEval/NBE"
```
```     9   "~/repos/afp/thys/Polynomials/Polynomial"
```
```    10   "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
```
```    11   "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
```
```    12 uses
```
```    13      "mutabelle.ML"
```
```    14      "mutabelle_extra.ML"
```
```    15 begin
```
```    16
```
```    17
```
```    18 section {* configuration *}
```
```    19
```
```    20 ML {* val log_directory = "" *}
```
```    21
```
```    22
```
```    23 quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
```
```    24
```
```    25 (*
```
```    26 nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
```
```    27 refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
```
```    28 *)
```
```    29 ML {* Try.auto_time_limit := 10.0 *}
```
```    30
```
```    31 ML {* val mtds = [
```
```    32   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
```
```    33   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
```
```    34   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
```
```    35   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
```
```    36 ]
```
```    37 *}
```
```    38
```
```    39 ML {*
```
```    40 fun mutation_testing_of (name, thy) =
```
```    41   (MutabelleExtra.random_seed := 1.0;
```
```    42   MutabelleExtra.thms_of false thy
```
```    43   |> MutabelleExtra.take_random 200
```
```    44   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
```
```    45          @{theory} mtds thms (log_directory ^ "/" ^ name)))
```
```    46 *}
```
```    47
```
```    48
```
```    49 text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
```
```    50
```
```    51 (*
```
```    52 ML {*
```
```    53
```
```    54       MutabelleExtra.random_seed := 1.0;
```
```    55       MutabelleExtra.thms_of true @{theory Complex_Main}
```
```    56       |> MutabelleExtra.take_random 1000000
```
```    57       |> (fn thms => List.drop (thms, 1000))
```
```    58       |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
```
```    59              @{theory} [
```
```    60                         MutabelleExtra.quickcheck_mtd "code",
```
```    61                         MutabelleExtra.smallcheck_mtd
```
```    62                         (*MutabelleExtra.refute_mtd,
```
```    63                         MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
```
```    64
```
```    65  *}
```
```    66 *)
```
```    67
```
```    68 section {* Mutation testing Isabelle theories *}
```
```    69
```
```    70 subsection {* List theory *}
```
```    71
```
```    72 (*
```
```    73 ML {*
```
```    74 mutation_testing_of ("List", @{theory List})
```
```    75  *}
```
```    76 *)
```
```    77
```
```    78 section {* Mutation testing AFP theories *}
```
```    79
```
```    80 subsection {* AVL-Trees *}
```
```    81
```
```    82 (*
```
```    83 ML {*
```
```    84 mutation_testing_of ("AVL-Trees", @{theory AVL})
```
```    85  *}
```
```    86 *)
```
```    87
```
```    88 subsection {* BinaryTree *}
```
```    89
```
```    90 (*
```
```    91 ML {*
```
```    92 mutation_testing_of ("BinaryTree", @{theory BinaryTree})
```
```    93  *}
```
```    94 *)
```
```    95
```
```    96 subsection {* Huffman *}
```
```    97
```
```    98 (*
```
```    99 ML {*
```
```   100 mutation_testing_of ("Huffman", @{theory Huffman})
```
```   101  *}
```
```   102 *)
```
```   103
```
```   104 subsection {* List_Index *}
```
```   105
```
```   106 (*
```
```   107 ML {*
```
```   108 mutation_testing_of ("List_Index", @{theory List_Index})
```
```   109  *}
```
```   110 *)
```
```   111
```
```   112 subsection {* Matrix *}
```
```   113
```
```   114 (*
```
```   115 ML {*
```
```   116 mutation_testing_of ("Matrix", @{theory Matrix})
```
```   117  *}
```
```   118 *)
```
```   119
```
```   120 subsection {* NBE *}
```
```   121
```
```   122 (*
```
```   123 ML {*
```
```   124 mutation_testing_of ("NBE", @{theory NBE})
```
```   125  *}
```
```   126 *)
```
```   127
```
```   128 subsection {* Polynomial *}
```
```   129
```
```   130 (*
```
```   131 ML {*
```
```   132 mutation_testing_of ("Polynomial", @{theory Polynomial})
```
```   133  *}
```
```   134 *)
```
```   135
```
```   136 subsection {* Presburger Automata *}
```
```   137
```
```   138 (*
```
```   139 ML {*
```
```   140 mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
```
```   141  *}
```
```   142 *)
```
```   143
```
```   144 end
```