src/HOL/Mutabelle/Mutabelle.thy
author webertj
Fri, 19 Oct 2012 15:12:52 +0200
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
permissions -rw-r--r--
Renamed {left,right}_distrib to distrib_{right,left}.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46711
f745bcc4a1e5 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents: 42361
diff changeset
     1
(* FIXME dead code!?!? *)
f745bcc4a1e5 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents: 42361
diff changeset
     2
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     3
theory Mutabelle
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     4
imports Main
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     5
begin
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     6
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46711
diff changeset
     7
ML_file "mutabelle.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46711
diff changeset
     8
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
     9
ML {*
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
    10
val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    11
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    12
val forbidden =
34974
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    13
 [(@{const_name Power.power}, "'a"),
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    14
  (@{const_name HOL.induct_equal}, "'a"),
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    15
  (@{const_name HOL.induct_implies}, "'a"),
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    16
  (@{const_name HOL.induct_conj}, "'a"),
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    17
  (@{const_name HOL.undefined}, "'a"),
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    18
  (@{const_name HOL.default}, "'a"),
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    19
  (@{const_name dummy_pattern}, "'a::{}"),
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    20
  (@{const_name Groups.uminus}, "'a"),
34974
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34965
diff changeset
    21
  (@{const_name Nat.size}, "'a"),
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 34974
diff changeset
    22
  (@{const_name Groups.abs}, "'a")];
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    23
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    24
val forbidden_thms =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    25
 ["finite_intvl_succ_class",
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    26
  "nibble"];
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    27
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    28
val forbidden_consts =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    29
 [@{const_name nibble_pair_of_char}];
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    30
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    31
fun is_forbidden s th =
46711
f745bcc4a1e5 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents: 42361
diff changeset
    32
 exists (fn s' => s' mem Long_Name.explode s) forbidden_thms orelse
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    33
 exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    34
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    35
fun test j = List.app (fn i =>
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    36
 Mutabelle.mutqc_thystat_mix is_forbidden
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    37
   @{theory List} @{theory Main} comms forbidden 1 [] i j ("list_" ^ string_of_int i ^ ".txt"))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    38
 (1 upto 10);
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    39
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    40
fun get_numbers xs =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    41
 let
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    42
   val (_, xs1) = take_prefix (not o equal ":") xs;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    43
   val (_, xs2) = take_prefix (fn ":" => true | " " => true | _ => false) xs1;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    44
   val (xs3, xs4) = take_prefix Symbol.is_digit xs2;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    45
   val (_, xs5) = take_prefix (equal " ") xs4;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    46
   val (xs6, xs7) = take_prefix Symbol.is_digit xs5
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    47
 in
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    48
   case (xs3, xs6) of
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    49
     ([], _) => NONE
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    50
   | (_, []) => NONE
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    51
   | (ys, zs) => SOME (fst (read_int ys), fst (read_int zs), xs7)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    52
 end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    53
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    54
fun add_numbers s =
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    55
 let
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    56
   fun strip ("\n" :: "\n" :: "\n" :: xs) = xs
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    57
     | strip (_ :: xs) = strip xs;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    58
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    59
   fun add (i, j) xs = (case get_numbers xs of
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    60
         NONE => (i, j)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    61
       | SOME (i', j', xs') => add (i+i', j+j') xs')
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    62
 in add (0,0) (strip (explode s)) end;
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    63
*}
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    64
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    65
(*
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    66
ML {*
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
    67
Quickcheck.test_term (Proof_Context.init_global @{theory})
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    68
 false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    69
*}
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    70
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    71
ML {*
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    72
fun is_executable thy th = can (Quickcheck.test_term
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
    73
 (Proof_Context.init_global thy) false (SOME "SML") 1 1) (prop_of th);
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    74
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    75
fun is_executable_term thy t = can (Quickcheck.test_term
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
    76
 (Proof_Context.init_global thy) false (SOME "SML") 1 1) t;
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    77
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    78
fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    79
   Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    80
   is_executable thy th)
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38864
diff changeset
    81
 (Global_Theory.all_thms_of thy);
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    82
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    83
fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    84
   Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    85
   is_executable thy th)
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38864
diff changeset
    86
 (Global_Theory.all_thms_of thy);
34965
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    87
*}
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    88
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    89
ML {*
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    90
is_executable @{theory} (hd @{thms nibble_pair_of_char_simps})
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    91
*}
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    92
*)
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    93
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    94
ML {*
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    95
Mutabelle.mutate_mix @{term "Suc x \<noteq> 0"} @{theory} comms forbidden 1
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    96
*}
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    97
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    98
ML {*
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
    99
Mutabelle.mutqc_thystat_mix is_forbidden @{theory Nat} @{theory} comms forbidden 1 [] 10 5 "/tmp/muta.out"
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   100
*}
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   101
3b4762c1052c adding Mutabelle to repository
bulwahn
parents:
diff changeset
   102
end