(*  Title:      HOL/Metis_Examples/Type_Encodings.thy

    Author:     Jasmin Blanchette, TU Muenchen

Example that exercises Metis's (and hence Sledgehammer's) type encodings.

*)

header {*

Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings

*}

theory Type_Encodings

imports "~~/src/HOL/Sledgehammer2d"(*###*)

begin

declare [[metis_new_skolemizer]]

sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0]

text {* Setup for testing Metis exhaustively *}

lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption

ML {*

(* The commented-out type systems are too incomplete for our exhaustive

   tests. *)

val type_encs =

  ["erased",

   "poly_guards",

   "poly_guards_uniform",

   "poly_tags",

   "poly_tags_uniform",

   "poly_args",

   "mono_guards",

   "mono_guards_uniform",

   "mono_tags",

   "mono_tags_uniform",

   "mono_args",

   "mangled_guards",

   "mangled_guards_uniform",

   "mangled_tags",

   "mangled_tags_uniform",

   "mangled_args",

   "simple",

   "poly_guards?",

   "poly_guards_uniform?",

   "poly_tags?",

(* "poly_tags_uniform?", *)

   "mono_guards?",

   "mono_guards_uniform?",

   "mono_tags?",

   "mono_tags_uniform?",

   "mangled_guards?",

   "mangled_guards_uniform?",

   "mangled_tags?",

   "mangled_tags_uniform?",

   "simple?",

   "poly_guards!",

   "poly_guards_uniform!",

(* "poly_tags!", *)

   "poly_tags_uniform!",

   "mono_guards!",

   "mono_guards_uniform!",

   "mono_tags!",

   "mono_tags_uniform!",

   "mangled_guards!",

   "mangled_guards_uniform!",

   "mangled_tags!",

   "mangled_tags_uniform!",

   "simple!"]

fun metis_exhaust_tac ctxt ths =

  let

    fun tac [] st = all_tac st

      | tac (type_enc :: type_encs) st =

        st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)

           |> ((if null type_encs then all_tac else rtac @{thm fork} 1)

               THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1

               THEN COND (has_fewer_prems 2) all_tac no_tac

               THEN tac type_encs)

  in tac end

*}

method_setup metis_exhaust = {*

  Attrib.thms >>

    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs))

*} "exhaustively run the new Metis with all type encodings"

text {* Miscellaneous tests *}

lemma "x = y \<Longrightarrow> y = x"

by metis_exhaust

lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"

by (metis_exhaust last.simps)

lemma "map Suc [0] = [Suc 0]"

by (metis_exhaust map.simps)

lemma "map Suc [1 + 1] = [Suc 2]"

by (metis_exhaust map.simps nat_1_add_1)

lemma "map Suc [2] = [Suc (1 + 1)]"

by (metis_exhaust map.simps nat_1_add_1)

definition "null xs = (xs = [])"

lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"

by (metis_exhaust null_def)

lemma "(0::nat) + 0 = 0"

by (metis_exhaust arithmetic_simps(38))

end