author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46733  4a03b30e04cb 
child 47831  1d25deb1f185 
permissions  rwrr 
43197  1 
(* Title: HOL/Metis_Examples/Proxies.thy 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

3 

43197  4 
Example that exercises Metis's and Sledgehammer's logical symbol proxies for 
5 
rudimentary higherorder reasoning. 

41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

6 
*) 
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

7 

43197  8 
header {* 
9 
Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for 

10 
Rudimentary HigherOrder Reasoning. 

11 
*} 

41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

12 

43197  13 
theory Proxies 
14 
imports Type_Encodings 

15 
begin 

41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

16 

42756
6b7ef9b724fd
added two mildly higherorder 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 higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

18 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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 higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

21 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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 higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

24 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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  27 
by (metis_exhaust inc_def plus_1_not_0) 
42756
6b7ef9b724fd
added two mildly higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

28 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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  31 
by (metis_exhaust inc_def) 
42756
6b7ef9b724fd
added two mildly higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

32 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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 higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

35 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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  38 
by (metis_exhaust add_swap_def) 
42756
6b7ef9b724fd
added two mildly higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

39 

6b7ef9b724fd
added two mildly higherorder 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 higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

41 

6b7ef9b724fd
added two mildly higherorder 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 higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

46 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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 higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

49 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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 higherorder 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  55 
by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) 
42756
6b7ef9b724fd
added two mildly higherorder examples contributed by TN, removed references to obsoleted type systems, and moved things around
blanchet
parents:
42722
diff
changeset

56 

6b7ef9b724fd
added two mildly higherorder 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 higherorder 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 backwardcompatible 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  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  63 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  64 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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 backwardcompatible way
blanchet
parents:
42756
diff
changeset

70 

41141
ad923cdd4a5d
added example to exercise higherorder 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  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  75 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  76 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  81 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

82 

ad923cdd4a5d
added example to exercise higherorder 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  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  87 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  88 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  93 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

94 

ad923cdd4a5d
added example to exercise higherorder 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  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  99 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  100 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  105 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

106 

ad923cdd4a5d
added example to exercise higherorder 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  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  111 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  112 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  117 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

118 

ad923cdd4a5d
added example to exercise higherorder 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  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  124 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  125 
sledgehammer [type_enc = poly_guards, expect = some] () 
44768  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  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 higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

131 

ad923cdd4a5d
added example to exercise higherorder 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  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  136 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  137 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  142 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

143 

ad923cdd4a5d
added example to exercise higherorder 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  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  148 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  149 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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 higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

155 

ad923cdd4a5d
added example to exercise higherorder 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  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  160 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  161 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  166 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

167 

ad923cdd4a5d
added example to exercise higherorder 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  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  172 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  173 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  178 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

179 

ad923cdd4a5d
added example to exercise higherorder 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  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  184 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  185 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  190 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

191 

ad923cdd4a5d
added example to exercise higherorder 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  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  196 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  197 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  202 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

203 

ad923cdd4a5d
added example to exercise higherorder 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  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  208 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  209 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  214 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

215 

ad923cdd4a5d
added example to exercise higherorder 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  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  220 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  221 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  226 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

227 

ad923cdd4a5d
added example to exercise higherorder 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  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  232 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  233 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  238 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

239 

ad923cdd4a5d
added example to exercise higherorder 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  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  244 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  245 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  250 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

251 

ad923cdd4a5d
added example to exercise higherorder 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  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  256 
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply) 
43989  257 
sledgehammer [type_enc = poly_guards, expect = some] (id_apply) 
44768  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  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  262 
by (metis_exhaust id_apply) 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

263 

ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
diff
changeset

264 
end 