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