isabelle: src/HOL/Mirabelle.thy@05329cd9db4b (annotated)

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

author	paulson
	Fri, 17 Mar 2023 10:42:50 +0000
changeset 77685	05329cd9db4b
parent 74986	fc664e4fbf6d
child 79941	6a3212bedfad
permissions	-rw-r--r--