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