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