isabelle: src/HOL/Metis_Examples/Proxies.thy@d9f3d91208af (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)"
47831 1d25deb1f185 Sledgehammer can do it blanchet parents: 46733 diff changeset	30	sledgehammer [expect = some]
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"
47892 e389889da7df prevent spurious timeouts blanchet parents: 47831 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"
46072 291c14a01b6d reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter blanchet parents: 46062 diff changeset	43	(* The "add:" argument is unfortunate. *)
291c14a01b6d reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter blanchet parents: 46062 diff changeset	44	sledgehammer [expect = some] (add: A_def mem_Collect_eq)
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 44768 diff changeset	45	by (metis_exhaust A_def mem_Collect_eq)
42756 6b7ef9b724fd added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around blanchet parents: 42722 diff changeset	46
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 "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	48	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	49
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	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	51	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	52
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 44768 diff changeset	53	lemma "B \<le> C"
46733 4a03b30e04cb use SPASS instead of E for Metis examples -- it's seems faster for these small problems blanchet parents: 46072 diff changeset	54	sledgehammer [expect = some]
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	55	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	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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	61	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	62	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	63	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	64	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	65	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	66	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	67	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	68	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43228 2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be blanchet parents: 43213 diff changeset	69	by (metis (full_types) id_apply)
42758 865ce93ce025 handle equality proxy in a more 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	73	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	74	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	75	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	76	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	77	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	78	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	79	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	80	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	85	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	86	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	87	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	88	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	89	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	90	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	91	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	92	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	97	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	98	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	99	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	100	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	101	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	102	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	103	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	104	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	109	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	110	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	111	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	112	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	113	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	114	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	115	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	116	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	122	sledgehammer [type_enc = poly_tags??, expect = some] ()
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	123	sledgehammer [type_enc = poly_tags, expect = some] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	124	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	125	sledgehammer [type_enc = poly_guards, expect = some] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	126	sledgehammer [type_enc = mono_tags??, expect = some] ()
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	127	sledgehammer [type_enc = mono_tags, expect = some] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	128	sledgehammer [type_enc = mono_guards??, expect = some] ()
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	129	sledgehammer [type_enc = mono_guards, expect = some] ()
43228 2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be blanchet parents: 43213 diff changeset	130	by (metis (full_types))
41141 ad923cdd4a5d added example to exercise 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	134	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	135	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	136	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	137	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	138	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	139	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	140	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	141	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	146	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	147	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	148	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	149	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	150	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	151	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	152	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	153	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 44768 diff changeset	154	by metis_exhaust
41141 ad923cdd4a5d added example to exercise 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	158	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	159	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	160	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	161	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	162	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	163	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	164	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	165	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	170	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	171	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	172	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	173	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	174	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	175	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	176	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	177	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	182	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	183	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	184	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	185	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	186	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	187	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	188	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	189	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	194	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	195	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	196	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	197	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	198	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	199	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	200	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	201	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	206	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	207	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	208	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	209	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	210	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	211	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	212	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	213	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	218	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	219	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	220	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	221	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	222	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	223	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	224	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	225	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	230	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	231	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	232	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	233	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	234	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	235	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	236	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	237	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	242	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	243	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	244	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	245	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	246	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	247	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	248	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	249	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	254	sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	255	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	256	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	257	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	258	sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	259	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	260	sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
44494 a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono blanchet parents: 43989 diff changeset	261	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 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	wenzelm
	Wed, 27 Feb 2013 19:39:16 +0100
changeset 51297	d9f3d91208af
parent 47892	e389889da7df
child 53989	729700091556
permissions	-rw-r--r--