src/HOL/Metis_Examples/Proxies.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 63167 0909deb8059b child 67399 eab6ce8368fa permissions -rw-r--r--
executable domain membership checks
```     1 (*  Title:      HOL/Metis_Examples/Proxies.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3
```
```     4 Example that exercises Metis's and Sledgehammer's logical symbol proxies for
```
```     5 rudimentary higher-order reasoning.
```
```     6 *)
```
```     7
```
```     8 section \<open>
```
```     9 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
```
```    10 Rudimentary Higher-Order Reasoning.
```
```    11 \<close>
```
```    12
```
```    13 theory Proxies
```
```    14 imports Type_Encodings
```
```    15 begin
```
```    16
```
```    17 sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,
```
```    18   dont_minimize]
```
```    19
```
```    20 text \<open>Extensionality and set constants\<close>
```
```    21
```
```    22 lemma plus_1_not_0: "n + (1::nat) \<noteq> 0"
```
```    23 by simp
```
```    24
```
```    25 definition inc :: "nat \<Rightarrow> nat" where
```
```    26 "inc x = x + 1"
```
```    27
```
```    28 lemma "inc \<noteq> (\<lambda>y. 0)"
```
```    29 sledgehammer [expect = some] (inc_def plus_1_not_0)
```
```    30 by (metis_exhaust inc_def plus_1_not_0)
```
```    31
```
```    32 lemma "inc = (\<lambda>y. y + 1)"
```
```    33 sledgehammer [expect = some]
```
```    34 by (metis_exhaust inc_def)
```
```    35
```
```    36 definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
```
```    37 "add_swap = (\<lambda>x y. y + x)"
```
```    38
```
```    39 lemma "add_swap m n = n + m"
```
```    40 sledgehammer [expect = some] (add_swap_def)
```
```    41 by (metis_exhaust add_swap_def)
```
```    42
```
```    43 definition "A = {xs::'a list. True}"
```
```    44
```
```    45 lemma "xs \<in> A"
```
```    46 (* The "add:" argument is unfortunate. *)
```
```    47 sledgehammer [expect = some] (add: A_def mem_Collect_eq)
```
```    48 by (metis_exhaust A_def mem_Collect_eq)
```
```    49
```
```    50 definition "B (y::int) \<equiv> y \<le> 0"
```
```    51 definition "C (y::int) \<equiv> y \<le> 1"
```
```    52
```
```    53 lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
```
```    54 by linarith
```
```    55
```
```    56 lemma "B \<le> C"
```
```    57 sledgehammer [expect = some]
```
```    58 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
```
```    59
```
```    60 text \<open>Proxies for logical constants\<close>
```
```    61
```
```    62 lemma "id (op =) x x"
```
```    63 sledgehammer [type_enc = erased, expect = none] (id_apply)
```
```    64 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```    65 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```    66 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```    67 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```    68 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```    69 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```    70 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```    71 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```    72 by (metis (full_types) id_apply)
```
```    73
```
```    74 lemma "id True"
```
```    75 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```    76 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```    77 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```    78 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```    79 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```    80 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```    81 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```    82 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```    83 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```    84 by (metis_exhaust id_apply)
```
```    85
```
```    86 lemma "\<not> id False"
```
```    87 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```    88 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```    89 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```    90 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```    91 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```    92 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```    93 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```    94 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```    95 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```    96 by (metis_exhaust id_apply)
```
```    97
```
```    98 lemma "x = id True \<or> x = id False"
```
```    99 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   100 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   101 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   102 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   103 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   104 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   105 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   106 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   107 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   108 by (metis_exhaust id_apply)
```
```   109
```
```   110 lemma "id x = id True \<or> id x = id False"
```
```   111 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   112 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   113 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   114 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   115 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   116 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   117 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   118 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   119 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   120 by (metis_exhaust id_apply)
```
```   121
```
```   122 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
```
```   123 sledgehammer [type_enc = erased, expect = none] ()
```
```   124 sledgehammer [type_enc = poly_args, expect = none] ()
```
```   125 sledgehammer [type_enc = poly_tags??, expect = some] ()
```
```   126 sledgehammer [type_enc = poly_tags, expect = some] ()
```
```   127 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   128 sledgehammer [type_enc = poly_guards, expect = some] ()
```
```   129 sledgehammer [type_enc = mono_tags??, expect = some] ()
```
```   130 sledgehammer [type_enc = mono_tags, expect = some] ()
```
```   131 sledgehammer [type_enc = mono_guards??, expect = some] ()
```
```   132 sledgehammer [type_enc = mono_guards, expect = some] ()
```
```   133 by (metis (full_types))
```
```   134
```
```   135 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
```
```   136 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   137 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   138 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   139 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   140 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   141 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   142 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   143 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   144 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   145 by (metis_exhaust id_apply)
```
```   146
```
```   147 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
```
```   148 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   149 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   150 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   151 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   152 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   153 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   154 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   155 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   156 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   157 by metis_exhaust
```
```   158
```
```   159 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
```
```   160 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   161 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   162 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   163 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   164 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   165 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   166 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   167 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   168 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   169 by (metis_exhaust id_apply)
```
```   170
```
```   171 lemma "id (a \<and> b) \<Longrightarrow> id a"
```
```   172 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   173 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   174 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   175 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   176 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   177 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   178 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   179 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   180 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   181 by (metis_exhaust id_apply)
```
```   182
```
```   183 lemma "id (a \<and> b) \<Longrightarrow> id b"
```
```   184 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   185 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   186 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   187 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   188 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   189 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   190 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   191 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   192 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   193 by (metis_exhaust id_apply)
```
```   194
```
```   195 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
```
```   196 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   197 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   198 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   199 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   200 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   201 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   202 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   203 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   204 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   205 by (metis_exhaust id_apply)
```
```   206
```
```   207 lemma "id a \<Longrightarrow> id (a \<or> b)"
```
```   208 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   209 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   210 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   211 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   212 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   213 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   214 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   215 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   216 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   217 by (metis_exhaust id_apply)
```
```   218
```
```   219 lemma "id b \<Longrightarrow> id (a \<or> b)"
```
```   220 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   221 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   222 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   223 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   224 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   225 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   226 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   227 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   228 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   229 by (metis_exhaust id_apply)
```
```   230
```
```   231 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
```
```   232 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   233 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   234 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   235 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   236 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   237 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   238 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   239 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   240 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   241 by (metis_exhaust id_apply)
```
```   242
```
```   243 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
```
```   244 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   245 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   246 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   247 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   248 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   249 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   250 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   251 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   252 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   253 by (metis_exhaust id_apply)
```
```   254
```
```   255 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
```
```   256 sledgehammer [type_enc = erased, expect = some] (id_apply)
```
```   257 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
```
```   258 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
```
```   259 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
```
```   260 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
```
```   261 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
```
```   262 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
```
```   263 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
```
```   264 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
```
```   265 by (metis_exhaust id_apply)
```
```   266
```
```   267 end
```