src/HOL/Mirabelle.thy
author paulson <lp15@cam.ac.uk>
Tue, 30 May 2023 12:33:06 +0100
changeset 78127 24b70433c2e8
parent 74986 fc664e4fbf6d
child 79941 6a3212bedfad
permissions -rw-r--r--
New HOL Light material on metric spaces and topological spaces
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73684
diff changeset
     1
(*  Title:      HOL/Mirabelle.thy
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
     2
    Author:     Jasmin Blanchette, TU Munich
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
     3
    Author:     Sascha Boehme, TU Munich
73696
03e134d5f867 reactive "sledgehammer_filter": statically correct, but untested (no proof_file);
wenzelm
parents: 73691
diff changeset
     4
    Author:     Makarius
74516
2c093a3167d1 added Mirabelle action presburger
desharna
parents: 73847
diff changeset
     5
    Author:     Martin Desharnais, UniBw Munich, MPI-INF Saarbrücken
32381
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     6
*)
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     7
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     8
theory Mirabelle
74516
2c093a3167d1 added Mirabelle action presburger
desharna
parents: 73847
diff changeset
     9
  imports Sledgehammer Predicate_Compile Presburger
32381
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    10
begin
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    11
74986
fc664e4fbf6d added Mirabelle option -r to randomize the goals before selection
desharna
parents: 74948
diff changeset
    12
ML_file \<open>Tools/Mirabelle/mirabelle_util.ML\<close>
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73684
diff changeset
    13
ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close>
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
    14
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
    15
ML \<open>
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
    16
signature MIRABELLE_ACTION = sig
74948
15ce207f69c8 added support for initialization messages to Mirabelle
desharna
parents: 74516
diff changeset
    17
  val make_action : Mirabelle.action_context -> string * Mirabelle.action
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
    18
end
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
    19
\<close>
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73697
diff changeset
    20
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73684
diff changeset
    21
ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73684
diff changeset
    22
ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
74516
2c093a3167d1 added Mirabelle action presburger
desharna
parents: 73847
diff changeset
    23
ML_file \<open>Tools/Mirabelle/mirabelle_presburger.ML\<close>
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73684
diff changeset
    24
ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
74516
2c093a3167d1 added Mirabelle action presburger
desharna
parents: 73847
diff changeset
    25
ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73684
diff changeset
    26
ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73684
diff changeset
    27
ML_file \<open>Tools/Mirabelle/mirabelle_try0.ML\<close>
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    28
74516
2c093a3167d1 added Mirabelle action presburger
desharna
parents: 73847
diff changeset
    29
end