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