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