src/HOL/Metis_Examples/Type_Encodings.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 58889 5b7a9633cfa8 child 60754 02924903a6fd permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
```     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 rtac @{thm 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\<Colon>nat) + 0 = 0"
```
```    93 by (metis_exhaust add_0_left)
```
```    94
```
```    95 end
```