src/HOL/Metis_Examples/Proxies.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46733 4a03b30e04cb
child 47831 1d25deb1f185
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
     1
(*  Title:      HOL/Metis_Examples/Proxies.thy
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
     3
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
     4
Example that exercises Metis's and Sledgehammer's logical symbol proxies for
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
     5
rudimentary higher-order reasoning.
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
     6
*)
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
     7
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
     8
header {*
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
     9
Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
    10
Rudimentary Higher-Order Reasoning.
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
    11
*}
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
    12
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
    13
theory Proxies
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
    14
imports Type_Encodings
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43196
diff changeset
    15
begin
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
    16
42756
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    17
text {* Extensionality and set constants *}
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    18
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    19
lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    20
by simp
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    21
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    22
definition inc :: "nat \<Rightarrow> nat" where
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    23
"inc x = x + 1"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    24
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    25
lemma "inc \<noteq> (\<lambda>y. 0)"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    26
sledgehammer [expect = some] (inc_def plus_1_not_0)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
    27
by (metis_exhaust inc_def plus_1_not_0)
42756
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    28
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    29
lemma "inc = (\<lambda>y. y + 1)"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    30
sledgehammer [expect = some] (inc_def)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
    31
by (metis_exhaust inc_def)
42756
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    32
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    33
definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    34
"add_swap = (\<lambda>x y. y + x)"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    35
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    36
lemma "add_swap m n = n + m"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    37
sledgehammer [expect = some] (add_swap_def)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
    38
by (metis_exhaust add_swap_def)
42756
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    39
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    40
definition "A = {xs\<Colon>'a list. True}"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    41
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    42
lemma "xs \<in> A"
46072
291c14a01b6d reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter
blanchet
parents: 46062
diff changeset
    43
(* The "add:" argument is unfortunate. *)
291c14a01b6d reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter
blanchet
parents: 46062
diff changeset
    44
sledgehammer [expect = some] (add: A_def mem_Collect_eq)
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 44768
diff changeset
    45
by (metis_exhaust A_def mem_Collect_eq)
42756
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    46
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    47
definition "B (y::int) \<equiv> y \<le> 0"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    48
definition "C (y::int) \<equiv> y \<le> 1"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    49
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    50
lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    51
by linarith
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    52
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 44768
diff changeset
    53
lemma "B \<le> C"
46733
4a03b30e04cb use SPASS instead of E for Metis examples -- it's seems faster for these small problems
blanchet
parents: 46072
diff changeset
    54
sledgehammer [expect = some]
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
    55
by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
42756
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    56
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    57
text {* Proxies for logical constants *}
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents: 42722
diff changeset
    58
42758
865ce93ce025 handle equality proxy in a more backward-compatible way
blanchet
parents: 42756
diff changeset
    59
lemma "id (op =) x x"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    60
sledgehammer [type_enc = erased, expect = none] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    61
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    62
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    63
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
    64
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    65
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
    66
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    67
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
    68
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43213
diff changeset
    69
by (metis (full_types) id_apply)
42758
865ce93ce025 handle equality proxy in a more backward-compatible way
blanchet
parents: 42756
diff changeset
    70
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
    71
lemma "id True"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    72
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    73
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    74
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    75
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
    76
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    77
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
    78
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    79
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
    80
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
    81
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
    82
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
    83
lemma "\<not> id False"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    84
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    85
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    86
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    87
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
    88
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    89
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
    90
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    91
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
    92
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
    93
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
    94
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
    95
lemma "x = id True \<or> x = id False"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    96
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    97
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
    98
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
    99
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   100
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   101
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   102
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   103
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   104
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   105
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   106
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   107
lemma "id x = id True \<or> id x = id False"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   108
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   109
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   110
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   111
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   112
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   113
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   114
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   115
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   116
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   117
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   118
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   119
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   120
sledgehammer [type_enc = erased, expect = none] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   121
sledgehammer [type_enc = poly_args, expect = none] ()
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   122
sledgehammer [type_enc = poly_tags??, expect = some] ()
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   123
sledgehammer [type_enc = poly_tags, expect = some] ()
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   124
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   125
sledgehammer [type_enc = poly_guards, expect = some] ()
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   126
sledgehammer [type_enc = mono_tags??, expect = some] ()
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   127
sledgehammer [type_enc = mono_tags, expect = some] ()
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   128
sledgehammer [type_enc = mono_guards??, expect = some] ()
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   129
sledgehammer [type_enc = mono_guards, expect = some] ()
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43213
diff changeset
   130
by (metis (full_types))
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   131
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   132
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   133
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   134
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   135
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   136
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   137
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   138
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   139
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   140
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   141
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   142
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   143
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   144
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   145
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   146
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   147
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   148
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   149
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   150
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   151
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   152
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   153
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 44768
diff changeset
   154
by metis_exhaust
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   155
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   156
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   157
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   158
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   159
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   160
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   161
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   162
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   163
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   164
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   165
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   166
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   167
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   168
lemma "id (a \<and> b) \<Longrightarrow> id a"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   169
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   170
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   171
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   172
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   173
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   174
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   175
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   176
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   177
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   178
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   179
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   180
lemma "id (a \<and> b) \<Longrightarrow> id b"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   181
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   182
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   183
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   184
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   185
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   186
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   187
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   188
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   189
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   190
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   191
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   192
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   193
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   194
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   195
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   196
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   197
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   198
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   199
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   200
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   201
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   202
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   203
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   204
lemma "id a \<Longrightarrow> id (a \<or> b)"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   205
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   206
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   207
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   208
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   209
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   210
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   211
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   212
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   213
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   214
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   215
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   216
lemma "id b \<Longrightarrow> id (a \<or> b)"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   217
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   218
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   219
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   220
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   221
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   222
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   223
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   224
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   225
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   226
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   227
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   228
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   229
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   230
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   231
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   232
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   233
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   234
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   235
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   236
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   237
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   238
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   239
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   240
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   241
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   242
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   243
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   244
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   245
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   246
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   247
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   248
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   249
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   250
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   251
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   252
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   253
sledgehammer [type_enc = erased, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   254
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43228
diff changeset
   255
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   256
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43629
diff changeset
   257
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   258
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   259
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44494
diff changeset
   260
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 43989
diff changeset
   261
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43205
diff changeset
   262
by (metis_exhaust id_apply)
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   263
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
diff changeset
   264
end