src/HOL/Mutabelle/Mutabelle.thy
author haftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39557 fe5722fce758
permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
bulwahn@34965
     1
theory Mutabelle
bulwahn@34965
     2
imports Main
bulwahn@34965
     3
uses "mutabelle.ML"
bulwahn@34965
     4
begin
bulwahn@34965
     5
bulwahn@34965
     6
ML {*
haftmann@38864
     7
val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
bulwahn@34965
     8
bulwahn@34965
     9
val forbidden =
haftmann@34974
    10
 [(@{const_name Power.power}, "'a"),
haftmann@34974
    11
  (@{const_name HOL.induct_equal}, "'a"),
haftmann@34974
    12
  (@{const_name HOL.induct_implies}, "'a"),
haftmann@34974
    13
  (@{const_name HOL.induct_conj}, "'a"),
haftmann@34974
    14
  (@{const_name HOL.undefined}, "'a"),
haftmann@34974
    15
  (@{const_name HOL.default}, "'a"),
haftmann@34974
    16
  (@{const_name dummy_pattern}, "'a::{}"),
haftmann@35267
    17
  (@{const_name Groups.uminus}, "'a"),
haftmann@34974
    18
  (@{const_name Nat.size}, "'a"),
haftmann@35092
    19
  (@{const_name Groups.abs}, "'a")];
bulwahn@34965
    20
bulwahn@34965
    21
val forbidden_thms =
bulwahn@34965
    22
 ["finite_intvl_succ_class",
bulwahn@34965
    23
  "nibble"];
bulwahn@34965
    24
bulwahn@34965
    25
val forbidden_consts =
bulwahn@34965
    26
 [@{const_name nibble_pair_of_char}];
bulwahn@34965
    27
bulwahn@34965
    28
fun is_forbidden s th =
bulwahn@34965
    29
 exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
bulwahn@34965
    30
 exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts;
bulwahn@34965
    31
bulwahn@34965
    32
fun test j = List.app (fn i =>
bulwahn@34965
    33
 Mutabelle.mutqc_thystat_mix is_forbidden
bulwahn@34965
    34
   @{theory List} @{theory Main} comms forbidden 1 [] i j ("list_" ^ string_of_int i ^ ".txt"))
bulwahn@34965
    35
 (1 upto 10);
bulwahn@34965
    36
bulwahn@34965
    37
fun get_numbers xs =
bulwahn@34965
    38
 let
bulwahn@34965
    39
   val (_, xs1) = take_prefix (not o equal ":") xs;
bulwahn@34965
    40
   val (_, xs2) = take_prefix (fn ":" => true | " " => true | _ => false) xs1;
bulwahn@34965
    41
   val (xs3, xs4) = take_prefix Symbol.is_digit xs2;
bulwahn@34965
    42
   val (_, xs5) = take_prefix (equal " ") xs4;
bulwahn@34965
    43
   val (xs6, xs7) = take_prefix Symbol.is_digit xs5
bulwahn@34965
    44
 in
bulwahn@34965
    45
   case (xs3, xs6) of
bulwahn@34965
    46
     ([], _) => NONE
bulwahn@34965
    47
   | (_, []) => NONE
bulwahn@34965
    48
   | (ys, zs) => SOME (fst (read_int ys), fst (read_int zs), xs7)
bulwahn@34965
    49
 end;
bulwahn@34965
    50
bulwahn@34965
    51
fun add_numbers s =
bulwahn@34965
    52
 let
bulwahn@34965
    53
   fun strip ("\n" :: "\n" :: "\n" :: xs) = xs
bulwahn@34965
    54
     | strip (_ :: xs) = strip xs;
bulwahn@34965
    55
bulwahn@34965
    56
   fun add (i, j) xs = (case get_numbers xs of
bulwahn@34965
    57
         NONE => (i, j)
bulwahn@34965
    58
       | SOME (i', j', xs') => add (i+i', j+j') xs')
bulwahn@34965
    59
 in add (0,0) (strip (explode s)) end;
bulwahn@34965
    60
*}
bulwahn@34965
    61
bulwahn@34965
    62
(*
bulwahn@34965
    63
ML {*
wenzelm@36610
    64
Quickcheck.test_term (ProofContext.init_global @{theory})
bulwahn@34965
    65
 false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
bulwahn@34965
    66
*}
bulwahn@34965
    67
bulwahn@34965
    68
ML {*
bulwahn@34965
    69
fun is_executable thy th = can (Quickcheck.test_term
wenzelm@36610
    70
 (ProofContext.init_global thy) false (SOME "SML") 1 1) (prop_of th);
bulwahn@34965
    71
bulwahn@34965
    72
fun is_executable_term thy t = can (Quickcheck.test_term
wenzelm@36610
    73
 (ProofContext.init_global thy) false (SOME "SML") 1 1) t;
bulwahn@34965
    74
bulwahn@34965
    75
fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
bulwahn@34965
    76
   Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
bulwahn@34965
    77
   is_executable thy th)
bulwahn@34965
    78
 (PureThy.all_thms_of thy);
bulwahn@34965
    79
bulwahn@34965
    80
fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
bulwahn@34965
    81
   Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
bulwahn@34965
    82
   is_executable thy th)
bulwahn@34965
    83
 (PureThy.all_thms_of thy);
bulwahn@34965
    84
*}
bulwahn@34965
    85
bulwahn@34965
    86
ML {*
bulwahn@34965
    87
is_executable @{theory} (hd @{thms nibble_pair_of_char_simps})
bulwahn@34965
    88
*}
bulwahn@34965
    89
*)
bulwahn@34965
    90
bulwahn@34965
    91
ML {*
bulwahn@34965
    92
Mutabelle.mutate_mix @{term "Suc x \<noteq> 0"} @{theory} comms forbidden 1
bulwahn@34965
    93
*}
bulwahn@34965
    94
bulwahn@34965
    95
ML {*
bulwahn@34965
    96
Mutabelle.mutqc_thystat_mix is_forbidden @{theory Nat} @{theory} comms forbidden 1 [] 10 5 "/tmp/muta.out"
bulwahn@34965
    97
*}
bulwahn@34965
    98
bulwahn@34965
    99
end