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