src/HOL/Metis_Examples/Type_Encodings.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61076 bdc1e2f0a86a
child 63167 0909deb8059b
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Metis_Examples/Type_Encodings.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Example that exercises Metis's (and hence Sledgehammer's) type encodings.
     5 *)
     6 
     7 section {*
     8 Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings
     9 *}
    10 
    11 theory Type_Encodings
    12 imports Main
    13 begin
    14 
    15 declare [[metis_new_skolem]]
    16 
    17 text {* Setup for testing Metis exhaustively *}
    18 
    19 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
    20 
    21 ML {*
    22 val type_encs =
    23   ["erased",
    24    "poly_guards",
    25    "poly_guards?",
    26    "poly_guards??",
    27    "poly_guards@",
    28    "poly_tags",
    29    "poly_tags?",
    30    "poly_tags??",
    31    "poly_tags@",
    32    "poly_args",
    33    "poly_args?",
    34    "raw_mono_guards",
    35    "raw_mono_guards?",
    36    "raw_mono_guards??",
    37    "raw_mono_guards@",
    38    "raw_mono_tags",
    39    "raw_mono_tags?",
    40    "raw_mono_tags??",
    41    "raw_mono_tags@",
    42    "raw_mono_args",
    43    "raw_mono_args?",
    44    "mono_guards",
    45    "mono_guards?",
    46    "mono_guards??",
    47    "mono_tags",
    48    "mono_tags?",
    49    "mono_tags??",
    50    "mono_args"]
    51 
    52 fun metis_exhaust_tac ctxt ths =
    53   let
    54     fun tac [] st = all_tac st
    55       | tac (type_enc :: type_encs) st =
    56         st (* |> tap (fn _ => tracing (@{make_string} type_enc)) *)
    57            |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1)
    58                THEN Metis_Tactic.metis_tac [type_enc]
    59                     ATP_Problem_Generate.combsN ctxt ths 1
    60                THEN COND (has_fewer_prems 2) all_tac no_tac
    61                THEN tac type_encs)
    62   in tac type_encs end
    63 *}
    64 
    65 method_setup metis_exhaust = {*
    66   Attrib.thms >>
    67     (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths))
    68 *} "exhaustively run Metis with all type encodings"
    69 
    70 text {* Miscellaneous tests *}
    71 
    72 lemma "x = y \<Longrightarrow> y = x"
    73 by metis_exhaust
    74 
    75 lemma "[a] = [Suc 0] \<Longrightarrow> a = 1"
    76 by (metis_exhaust last.simps One_nat_def)
    77 
    78 lemma "map Suc [0] = [Suc 0]"
    79 by (metis_exhaust list.map)
    80 
    81 lemma "map Suc [1 + 1] = [Suc 2]"
    82 by (metis_exhaust list.map nat_1_add_1)
    83 
    84 lemma "map Suc [2] = [Suc (1 + 1)]"
    85 by (metis_exhaust list.map nat_1_add_1)
    86 
    87 definition "null xs = (xs = [])"
    88 
    89 lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
    90 by (metis_exhaust null_def)
    91 
    92 lemma "(0::nat) + 0 = 0"
    93 by (metis_exhaust add_0_left)
    94 
    95 end