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\nat) \ 0" ``` blanchet@42756 ` 20` ```by simp ``` blanchet@42756 ` 21` blanchet@42756 ` 22` ```definition inc :: "nat \ nat" where ``` blanchet@42756 ` 23` ```"inc x = x + 1" ``` blanchet@42756 ` 24` blanchet@42756 ` 25` ```lemma "inc \ (\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 = (\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 \ nat \ nat" where ``` blanchet@42756 ` 34` ```"add_swap = (\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\'a list. True}" ``` blanchet@42756 ` 41` blanchet@42756 ` 42` ```lemma "xs \ 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) \ y \ 0" ``` blanchet@42756 ` 47` ```definition "C (y::int) \ y \ 1" ``` blanchet@42756 ` 48` blanchet@42756 ` 49` ```lemma int_le_0_imp_le_1: "x \ (0::int) \ x \ 1" ``` blanchet@42756 ` 50` ```by linarith ``` blanchet@42756 ` 51` blanchet@42756 ` 52` ```lemma "B \ 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 "\ 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 \ 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 \ 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 \ P False \ 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 (\ a) \ \ 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 (\ \ a) \ 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 (\ (id (\ a))) \ 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 \ b) \ 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 \ b) \ 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 \ id b \ id (a \ 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 \ id (a \ 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 \ id (a \ 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 (\ a) \ id (\ b) \ id (\ (a \ 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 (\ a) \ id (a \ 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 \ b) \ id (\ a \ 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 ```