isabelle: src/HOL/Metis_Examples/Proxies.thy@030610b1e5a8 (annotated)

43197 c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	1	(* Title: HOL/Metis_Examples/Proxies.thy
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	3
43197 c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	4	Example that exercises Metis's and Sledgehammer's logical symbol proxies for
c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	5	rudimentary higher-order reasoning.
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	6	*)
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	7
43197 c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	8	header {*
c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	9	Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	10	Rudimentary Higher-Order Reasoning.
c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	11	*}
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	12
43197 c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	13	theory Proxies
c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	14	imports Type_Encodings
c71657bbdbc0 tuned Metis examples blanchet parents: 43196 diff changeset	15	begin
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	16
42756 6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	17	text {* Extensionality and set constants *}
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	18
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	19	lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	20	by simp
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	21
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	22	definition inc :: "nat \<Rightarrow> nat" where
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	23	"inc x = x + 1"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	24
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	25	lemma "inc \<noteq> (\<lambda>y. 0)"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	26	sledgehammer [expect = some] (inc_def plus_1_not_0)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	27	by (metis_exhaust inc_def plus_1_not_0)
42756 6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	28
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	29	lemma "inc = (\<lambda>y. y + 1)"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	30	sledgehammer [expect = some] (inc_def)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	31	by (metis_exhaust inc_def)
42756 6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	32
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	33	definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	34	"add_swap = (\<lambda>x y. y + x)"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	35
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	36	lemma "add_swap m n = n + m"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	37	sledgehammer [expect = some] (add_swap_def)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	38	by (metis_exhaust add_swap_def)
42756 6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	39
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	40	definition "A = {xs\<Colon>'a list. True}"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	41
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	42	lemma "xs \<in> A"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	43	sledgehammer [expect = some]
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	44	by (metis_exhaust A_def Collect_def mem_def)
42756 6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	45
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	46	definition "B (y::int) \<equiv> y \<le> 0"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	47	definition "C (y::int) \<equiv> y \<le> 1"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	48
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	49	lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	50	by linarith
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	51
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	52	lemma "B \<subseteq> C"
43629 030610b1e5a8 test a few more type encodings blanchet parents: 43626 diff changeset	53	sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	54	by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
42756 6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	55
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	56
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	57	text {* Proxies for logical constants *}
6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	58
42758 865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	59	lemma "id (op =) x x"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	60	sledgehammer [type_enc = erased, expect = none] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	61	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	63	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	64	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	65	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	66	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	67	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	68	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43228 2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be blanchet parents: 43213 diff changeset	69	by (metis (full_types) id_apply)
42758 865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	70
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	71	lemma "id True"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	72	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	73	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	75	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	76	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	77	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	78	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	79	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	80	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	81	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	82
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	83	lemma "\<not> id False"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	84	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	85	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	87	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	88	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	89	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	90	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	91	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	92	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	93	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	94
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	95	lemma "x = id True \<or> x = id False"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	96	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	97	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	99	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	100	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	101	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	102	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	103	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	104	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	105	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	106
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	107	lemma "id x = id True \<or> id x = id False"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	108	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	109	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	111	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	112	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	113	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	114	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	115	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	116	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	117	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	118
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	119	lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	120	sledgehammer [type_enc = erased, expect = none] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	121	sledgehammer [type_enc = poly_args, expect = none] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	122	sledgehammer [type_enc = poly_tags?, expect = some] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	123	sledgehammer [type_enc = poly_tags, expect = some] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	124	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	125	sledgehammer [type_enc = poly_preds, expect = some] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	126	sledgehammer [type_enc = mangled_tags?, expect = some] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	127	sledgehammer [type_enc = mangled_tags, expect = some] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	128	sledgehammer [type_enc = mangled_preds?, expect = some] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	129	sledgehammer [type_enc = mangled_preds, expect = some] ()
43228 2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be blanchet parents: 43213 diff changeset	130	by (metis (full_types))
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	131
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	132	lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	133	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	134	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	136	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	137	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	138	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	139	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	140	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	141	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	142	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	143
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	144	lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	145	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	146	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	148	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	149	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	150	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	151	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	152	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	153	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	154	by (metis_exhaust 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> (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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	158	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	160	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	161	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	162	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	163	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	164	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	165	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	166	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	167
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	168	lemma "id (a \<and> b) \<Longrightarrow> id a"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	169	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	170	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	172	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	173	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	174	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	175	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	176	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	177	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	178	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	179
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	180	lemma "id (a \<and> b) \<Longrightarrow> id b"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	181	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	182	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	184	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	185	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	186	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	187	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	188	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	189	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	190	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	191
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	192	lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	193	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	194	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	196	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	197	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	198	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	199	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	200	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	201	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	202	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	203
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	204	lemma "id a \<Longrightarrow> id (a \<or> b)"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	205	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	206	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	208	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	209	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	210	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	211	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	212	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	213	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	214	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	215
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	216	lemma "id b \<Longrightarrow> id (a \<or> b)"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	217	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	218	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	220	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	221	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	222	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	223	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	224	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	225	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	226	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	227
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	228	lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	229	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	230	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	232	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	233	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	234	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	235	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	236	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	237	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	238	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	239
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	240	lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	241	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	242	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	244	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	245	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	246	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	247	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	248	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	249	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	250	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	251
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	252	lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	253	sledgehammer [type_enc = erased, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	254	sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
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)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	256	sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	257	sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	258	sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	259	sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	260	sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	261	sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	262	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	263
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	264	end

author	blanchet
	Fri, 01 Jul 2011 15:53:38 +0200
changeset 43629	030610b1e5a8
parent 43626	a867ebb12209
child 43989	eb763b3ff9ed
permissions	-rw-r--r--