isabelle: src/HOL/Metis_Examples/HO_Reas.thy@a7dff503ffab (annotated)

41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	1	(* Title: HOL/Metis_Examples/HO_Reas.thy
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
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	4	Testing Metis's and Sledgehammer's higher-order reasoning capabilities.
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	5	*)
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	theory HO_Reas
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	8	imports Main
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	9	begin
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	10
42103 6066a35f6678 Metis examples use the new Skolemizer to test it blanchet parents: 41145 diff changeset	11	declare [[metis_new_skolemizer]]
6066a35f6678 Metis examples use the new Skolemizer to test it blanchet parents: 41145 diff changeset	12
42555 2570e1a5ddfb more higher-order tests for Sledgehammer/ATP blanchet parents: 42103 diff changeset	13	sledgehammer_params [prover = e, blocking, timeout = 10]
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	14
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	15	lemma "id True"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	16	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	17	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	18	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	19	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	20	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	21	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	22	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	23	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	24
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	25	lemma "\<not> id False"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	26	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	27	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	28	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	29	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	30	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	31	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	32	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	33	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	34
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	35	lemma "x = id True \<or> x = id False"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	36	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	37	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	38	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	39	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	40	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	41	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	42	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	43	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	44
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	45	lemma "id x = id True \<or> id x = id False"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	46	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	47	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	48	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	49	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	50	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	51	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	52	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	53	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	54
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	55	lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	56	sledgehammer [type_sys = erased, expect = none] ()
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	57	sledgehammer [type_sys = const_args, expect = none] ()
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	58	sledgehammer [type_sys = tags!, expect = some] ()
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	59	sledgehammer [type_sys = tags, expect = some] ()
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	60	sledgehammer [type_sys = preds!, expect = some] ()
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	61	sledgehammer [type_sys = preds, expect = some] ()
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	62	sledgehammer [type_sys = mangled_preds!, expect = some] ()
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	63	sledgehammer [type_sys = mangled_preds, expect = some] ()
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	64	by metisFT
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	65
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	66	lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	67	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	68	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	69	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	70	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	71	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	72	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	73	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	74	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	75
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	76	lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	77	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	78	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	79	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	80	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	81	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	82	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	83	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
42555 2570e1a5ddfb more higher-order tests for Sledgehammer/ATP blanchet parents: 42103 diff changeset	84	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	85
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	86	lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	87	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	88	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	89	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	90	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	91	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	92	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	93	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	94	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	95
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	96	lemma "id (a \<and> b) \<Longrightarrow> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	97	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	98	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	99	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	100	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	101	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	102	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	103	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	104	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	105
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	106	lemma "id (a \<and> b) \<Longrightarrow> id b"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	107	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	108	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	109	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	110	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	111	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	112	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	113	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	114	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	115
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	116	lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	117	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	118	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	119	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	120	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	121	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	122	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	123	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	124	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	125
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	126	lemma "id a \<Longrightarrow> id (a \<or> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	127	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	128	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	129	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	130	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	131	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	132	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	133	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	134	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	135
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	136	lemma "id b \<Longrightarrow> id (a \<or> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	137	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	138	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	139	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	140	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	141	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	142	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	143	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	144	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	145
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	146	lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	147	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	148	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	149	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	150	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	151	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	152	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	153	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	154	by (metis id_apply)
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> a) \<Longrightarrow> id (a \<longrightarrow> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	157	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	158	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	159	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	160	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	161	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	162	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	163	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	164	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	165
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	166	lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	167	sledgehammer [type_sys = erased, expect = some] (id_apply)
42580 04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	168	sledgehammer [type_sys = tags!, expect = some] (id_apply)
04cae06f0b99 use new type system syntax blanchet parents: 42555 diff changeset	169	sledgehammer [type_sys = tags, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	170	sledgehammer [type_sys = preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	171	sledgehammer [type_sys = preds, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	172	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	173	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	174	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	175
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	176	end

author	blanchet
	Mon, 02 May 2011 12:09:33 +0200
changeset 42603	a7dff503ffab
parent 42590	03834570af86
child 42686	7206f5688cad
permissions	-rw-r--r--