src/HOL/Mutabelle/mutabelle_extra.ML
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 44064 5bce8ff0d9ae
child 44845 5e51075cbd97
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
     1 (*  Title:      HOL/Mutabelle/mutabelle_extra.ML
     2     Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
     3 
     4 Invokation of Counterexample generators.
     5 *)
     6 
     7 signature MUTABELLE_EXTRA =
     8 sig
     9 
    10 val take_random : int -> 'a list -> 'a list
    11 
    12 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
    13 type timings = (string * int) list
    14 
    15 type mtd = string * (theory -> term -> outcome * timings)
    16 
    17 type mutant_subentry = term * (string * (outcome * timings)) list
    18 type detailed_entry = string * bool * term * mutant_subentry list
    19 
    20 type subentry = string * int * int * int * int * int * int
    21 type entry = string * bool * subentry list
    22 type report = entry list
    23 
    24 val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
    25 
    26 val solve_direct_mtd : mtd
    27 val try_methods_mtd : mtd
    28 (*
    29 val sledgehammer_mtd : mtd
    30 *)
    31 val nitpick_mtd : mtd
    32 
    33 (*
    34 val refute_mtd : mtd
    35 *)
    36 
    37 val freezeT : term -> term
    38 val thms_of : bool -> theory -> thm list
    39 
    40 val string_for_report : report -> string
    41 val write_report : string -> report -> unit
    42 val mutate_theorems_and_write_report :
    43   theory -> mtd list -> thm list -> string -> unit
    44 
    45 val random_seed : real Unsynchronized.ref
    46 end;
    47 
    48 structure MutabelleExtra : MUTABELLE_EXTRA =
    49 struct
    50 
    51 (* Own seed; can't rely on the Isabelle one to stay the same *)
    52 val random_seed = Unsynchronized.ref 1.0;
    53 
    54 
    55 (* mutation options *)
    56 (*val max_mutants = 4
    57 val num_mutations = 1*)
    58 (* soundness check: *)
    59 val max_mutants =  10
    60 val num_mutations = 1
    61 
    62 (* quickcheck options *)
    63 (*val quickcheck_generator = "SML"*)
    64 
    65 (* Another Random engine *)
    66 
    67 exception RANDOM;
    68 
    69 fun rmod x y = x - y * Real.realFloor (x / y);
    70 
    71 local
    72   val a = 16807.0;
    73   val m = 2147483647.0;
    74 in
    75 
    76 fun random () = CRITICAL (fn () =>
    77   let val r = rmod (a * ! random_seed) m
    78   in (random_seed := r; r) end);
    79 
    80 end;
    81 
    82 fun random_range l h =
    83   if h < l orelse l < 0 then raise RANDOM
    84   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    85 
    86 fun take_random 0 _ = []
    87   | take_random _ [] = []
    88   | take_random n xs =
    89     let val j = random_range 0 (length xs - 1) in
    90       Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
    91     end
    92   
    93 (* possible outcomes *)
    94 
    95 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
    96 
    97 fun string_of_outcome GenuineCex = "GenuineCex"
    98   | string_of_outcome PotentialCex = "PotentialCex"
    99   | string_of_outcome NoCex = "NoCex"
   100   | string_of_outcome Donno = "Donno"
   101   | string_of_outcome Timeout = "Timeout"
   102   | string_of_outcome Error = "Error"
   103   | string_of_outcome Solved = "Solved"
   104   | string_of_outcome Unsolved = "Unsolved"
   105 
   106 type timings = (string * int) list
   107 
   108 type mtd = string * (theory -> term -> outcome * timings)
   109 
   110 type mutant_subentry = term * (string * (outcome * timings)) list
   111 type detailed_entry = string * bool * term * mutant_subentry list
   112 
   113 type subentry = string * int * int * int * int * int * int
   114 type entry = string * bool * subentry list
   115 type report = entry list
   116 
   117 (* possible invocations *)
   118 
   119 (** quickcheck **)
   120 
   121 fun invoke_quickcheck change_options quickcheck_generator thy t =
   122   TimeLimit.timeLimit (seconds (!Try.auto_time_limit))
   123       (fn _ =>
   124           let
   125             val SOME [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy))
   126               (false, false) [] [(t, [])]
   127           in
   128             case Quickcheck.counterexample_of result of 
   129               NONE => (NoCex, Quickcheck.timings_of result)
   130             | SOME _ => (GenuineCex, Quickcheck.timings_of result)
   131           end) ()
   132   handle TimeLimit.TimeOut =>
   133          (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
   134 
   135 fun quickcheck_mtd change_options quickcheck_generator =
   136   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
   137 
   138 (** solve direct **)
   139  
   140 fun invoke_solve_direct thy t =
   141   let
   142     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) 
   143   in
   144     case Solve_Direct.solve_direct state of
   145       (true, _) => (Solved, [])
   146     | (false, _) => (Unsolved, [])
   147   end
   148 
   149 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
   150 
   151 (** try **)
   152 
   153 fun invoke_try_methods thy t =
   154   let
   155     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
   156   in
   157     case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of
   158       true => (Solved, [])
   159     | false => (Unsolved, [])
   160   end
   161 
   162 val try_methods_mtd = ("try_methods", invoke_try_methods)
   163 
   164 (** sledgehammer **)
   165 (*
   166 fun invoke_sledgehammer thy t =
   167   if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
   168       (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
   169     (Solved, ([], NONE))
   170   else
   171     (Unsolved, ([], NONE))
   172 
   173 val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
   174 *)
   175 (*
   176 fun invoke_refute thy t =
   177   let
   178     val res = MyRefute.refute_term thy [] t
   179     val _ = Output.urgent_message ("Refute: " ^ res)
   180   in
   181     case res of
   182       "genuine" => GenuineCex
   183     | "likely_genuine" => GenuineCex
   184     | "potential" => PotentialCex
   185     | "none" => NoCex
   186     | "unknown" => Donno
   187     | _ => Error
   188   end
   189   handle MyRefute.REFUTE (loc, details) =>
   190          (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
   191                    "."))
   192 val refute_mtd = ("refute", invoke_refute)
   193 *)
   194 
   195 (** nitpick **)
   196 
   197 fun invoke_nitpick thy t =
   198   let
   199     val ctxt = Proof_Context.init_global thy
   200     val state = Proof.init ctxt
   201     val (res, _) = Nitpick.pick_nits_in_term state
   202       (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t
   203     val _ = Output.urgent_message ("Nitpick: " ^ res)
   204   in
   205     (rpair []) (case res of
   206       "genuine" => GenuineCex
   207     | "likely_genuine" => GenuineCex
   208     | "potential" => PotentialCex
   209     | "none" => NoCex
   210     | "unknown" => Donno
   211     | _ => Error)
   212   end
   213 
   214 val nitpick_mtd = ("nitpick", invoke_nitpick)
   215 
   216 (* filtering forbidden theorems and mutants *)
   217 
   218 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
   219 
   220 val forbidden =
   221  [(* (@{const_name "power"}, "'a"), *)
   222   (*(@{const_name induct_equal}, "'a"),
   223   (@{const_name induct_implies}, "'a"),
   224   (@{const_name induct_conj}, "'a"),*)
   225   (@{const_name "undefined"}, "'a"),
   226   (@{const_name "default"}, "'a"),
   227   (@{const_name "dummy_pattern"}, "'a::{}"),
   228   (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
   229   (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
   230   (@{const_name "top_fun_inst.top_fun"}, "'a"),
   231   (@{const_name "Pure.term"}, "'a"),
   232   (@{const_name "top_class.top"}, "'a"),
   233   (@{const_name "Quotient.Quot_True"}, "'a")(*,
   234   (@{const_name "uminus"}, "'a"),
   235   (@{const_name "Nat.size"}, "'a"),
   236   (@{const_name "Groups.abs"}, "'a") *)]
   237 
   238 val forbidden_thms =
   239  ["finite_intvl_succ_class",
   240   "nibble"]
   241 
   242 val forbidden_consts =
   243  [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
   244 
   245 fun is_forbidden_theorem (s, th) =
   246   let val consts = Term.add_const_names (prop_of th) [] in
   247     exists (member (op =) (space_explode "." s)) forbidden_thms orelse
   248     exists (member (op =) forbidden_consts) consts orelse
   249     length (space_explode "." s) <> 2 orelse
   250     String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
   251     String.isSuffix "_def" s orelse
   252     String.isSuffix "_raw" s orelse
   253     String.isPrefix "term_of" (List.last (space_explode "." s))
   254   end
   255 
   256 val forbidden_mutant_constnames =
   257  ["HOL.induct_equal",
   258   "HOL.induct_implies",
   259   "HOL.induct_conj",
   260  @{const_name undefined},
   261  @{const_name default},
   262  @{const_name dummy_pattern},
   263  @{const_name "HOL.simp_implies"},
   264  @{const_name "bot_fun_inst.bot_fun"},
   265  @{const_name "top_fun_inst.top_fun"},
   266  @{const_name "Pure.term"},
   267  @{const_name "top_class.top"},
   268  (*@{const_name "HOL.equal"},*)
   269  @{const_name "Quotient.Quot_True"},
   270  @{const_name "equal_fun_inst.equal_fun"},
   271  @{const_name "equal_bool_inst.equal_bool"},
   272  @{const_name "ord_fun_inst.less_eq_fun"},
   273  @{const_name "ord_fun_inst.less_fun"},
   274  @{const_name Meson.skolem},
   275  @{const_name ATP.fequal},
   276  @{const_name transfer_morphism},
   277  @{const_name enum_prod_inst.enum_all_prod},
   278  @{const_name enum_prod_inst.enum_ex_prod}
   279  (*@{const_name "==>"}, @{const_name "=="}*)]
   280 
   281 val forbidden_mutant_consts =
   282   [
   283    (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
   284    (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
   285    (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
   286    (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
   287    (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
   288    (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
   289    (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
   290    (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
   291    (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
   292    (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
   293    (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
   294    (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
   295    (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
   296    (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
   297    (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
   298    (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
   299    (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
   300    (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"})]
   301 
   302 fun is_forbidden_mutant t =
   303   let
   304     val const_names = Term.add_const_names t []
   305     val consts = Term.add_consts t []
   306   in
   307     exists (String.isPrefix "Nitpick") const_names orelse
   308     exists (String.isSubstring "_sumC") const_names orelse
   309     exists (member (op =) forbidden_mutant_constnames) const_names orelse
   310     exists (member (op =) forbidden_mutant_consts) consts
   311   end
   312 
   313 (* executable via quickcheck *)
   314 
   315 fun is_executable_term thy t =
   316   let
   317     val ctxt = Proof_Context.init_global thy
   318   in
   319     can (TimeLimit.timeLimit (seconds 2.0)
   320       (Quickcheck.test_goal_terms
   321         ((Config.put Quickcheck.finite_types true #>
   322           Config.put Quickcheck.finite_type_size 1 #>
   323           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
   324         (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
   325   end
   326 
   327 fun is_executable_thm thy th = is_executable_term thy (prop_of th)
   328 
   329 val freezeT =
   330   map_types (map_type_tvar (fn ((a, i), S) =>
   331     TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
   332 
   333 fun thms_of all thy =
   334   filter
   335     (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
   336       (* andalso is_executable_thm thy th *))
   337     (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
   338 
   339 fun count x = (length oo filter o equal) x
   340 
   341 fun cpu_time description e =
   342   let val ({cpu, ...}, result) = Timing.timing e ()
   343   in (result, (description, Time.toMilliseconds cpu)) end
   344 (*
   345 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   346   let
   347     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
   348     val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
   349       handle ERROR s => (tracing s; (Error, ([], NONE))))
   350     val _ = Output.urgent_message (" Done")
   351   in (res, (time :: timing, reports)) end
   352 *)  
   353 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   354   let
   355     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
   356     val (res, timing) = (*cpu_time "total time"
   357       (fn () => *)case try (invoke_mtd thy) t of
   358           SOME (res, timing) => (res, timing)
   359         | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
   360            (Error, []))
   361     val _ = Output.urgent_message (" Done")
   362   in (res, timing) end
   363 
   364 (* theory -> term list -> mtd -> subentry *)
   365 
   366 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
   367   let
   368      val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
   369   in
   370     (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
   371      count Donno res, count Timeout res, count Error res)
   372   end
   373 
   374 (* creating entries *)
   375 
   376 fun create_entry thy thm exec mutants mtds =
   377   (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
   378 
   379 fun create_detailed_entry thy thm exec mutants mtds =
   380   let
   381     fun create_mutant_subentry mutant = (mutant,
   382       map (fn (mtd_name, invoke_mtd) =>
   383         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
   384   in
   385     (Thm.get_name_hint thm, exec, prop_of thm, map create_mutant_subentry mutants)
   386   end
   387 
   388 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
   389 fun mutate_theorem create_entry thy mtds thm =
   390   let
   391     val exec = is_executable_thm thy thm
   392     val _ = tracing (if exec then "EXEC" else "NOEXEC")
   393     val mutants =
   394           (if num_mutations = 0 then
   395              [Thm.prop_of thm]
   396            else
   397              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
   398                                   num_mutations)
   399              |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
   400              |> filter_out is_forbidden_mutant
   401     val mutants =
   402       if exec then
   403         let
   404           val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
   405                             string_of_int (length mutants) ^ " MUTANTS")
   406           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
   407           val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
   408                            " vs " ^ string_of_int (length noexecs) ^ ")")
   409         in
   410           execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
   411         end
   412       else
   413         mutants
   414     val mutants = mutants
   415           |> map Mutabelle.freeze |> map freezeT
   416 (*          |> filter (not o is_forbidden_mutant) *)
   417           |> map_filter (try (Sign.cert_term thy))
   418           |> filter (is_some o try (Thm.cterm_of thy))
   419           |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
   420           |> take_random max_mutants
   421     val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   422   in
   423     create_entry thy thm exec mutants mtds
   424   end
   425 
   426 (* theory -> mtd list -> thm list -> report *)
   427 val mutate_theorems = map ooo mutate_theorem
   428 
   429 fun string_of_mutant_subentry thy thm_name (t, results) =
   430   "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
   431   space_implode "; "
   432     (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
   433   "\n"
   434 
   435 (* string -> string *)
   436 val unyxml = XML.content_of o YXML.parse_body
   437 
   438 fun string_of_mutant_subentry' thy thm_name (t, results) =
   439   let
   440    (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
   441       satisfied_assms = s, positive_concl_tests = p}) =
   442       "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
   443     fun string_of_reports NONE = ""
   444       | string_of_reports (SOME reports) =
   445         cat_lines (map (fn (size, [report]) =>
   446           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
   447     fun string_of_mtd_result (mtd_name, (outcome, timing)) =
   448       mtd_name ^ ": " ^ string_of_outcome outcome
   449       (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
   450       (*^ "\n" ^ string_of_reports reports*)
   451   in
   452     "mutant of " ^ thm_name ^ ":\n"
   453     ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
   454   end
   455 
   456 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
   457    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
   458    Syntax.string_of_term_global thy t ^ "\n" ^                                    
   459    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
   460 
   461 fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
   462   "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
   463   "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
   464   "\" \nquickcheck\noops\n"
   465 
   466 fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
   467   "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
   468   cat_lines (map_index
   469     (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
   470 
   471 (* subentry -> string *)
   472 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
   473                          timeout, error) =
   474   "    " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^
   475   string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^
   476   string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^
   477   string_of_int error ^ "!"
   478 
   479 (* entry -> string *)
   480 fun string_for_entry (thm_name, exec, subentries) =
   481   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
   482   cat_lines (map string_for_subentry subentries) ^ "\n"
   483 
   484 (* report -> string *)
   485 fun string_for_report report = cat_lines (map string_for_entry report)
   486 
   487 (* string -> report -> unit *)
   488 fun write_report file_name =
   489   File.write (Path.explode file_name) o string_for_report
   490 
   491 (* theory -> mtd list -> thm list -> string -> unit *)
   492 fun mutate_theorems_and_write_report thy mtds thms file_name =
   493   let
   494     val _ = Output.urgent_message "Starting Mutabelle..."
   495     val ctxt = Proof_Context.init_global thy
   496     val path = Path.explode file_name
   497     (* for normal report: *)
   498     (*
   499     val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
   500     *)
   501     (* for detailled report: *)
   502     val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
   503     (* for theory creation: *)
   504     (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
   505   in
   506     File.write path (
   507     "Mutation options = "  ^
   508       "max_mutants: " ^ string_of_int max_mutants ^
   509       "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
   510     "QC options = " ^
   511       (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
   512       "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
   513       "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^
   514     "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n");
   515     map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
   516     ()
   517   end
   518 
   519 end;