isabelle: src/HOL/Metis_Examples/Proxies.thy@67360d50ebb3 (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 61314 diff changeset	8	section \<open>
43197 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.
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 61314 diff changeset	11	\<close>
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
61314 07eb540da4ab adapted example blanchet parents: 61076 diff changeset	17	sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,
07eb540da4ab adapted example blanchet parents: 61076 diff changeset	18	dont_minimize]
53989 729700091556 minor tweak to error message blanchet parents: 47892 diff changeset	19
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 61314 diff changeset	20	text \<open>Extensionality and set constants\<close>
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	21
61076 bdc1e2f0a86a eliminated \<Colon>; wenzelm parents: 58889 diff changeset	22	lemma plus_1_not_0: "n + (1::nat) \<noteq> 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	23	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	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	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	26	"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	27
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	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	29	sledgehammer [expect = some] (inc_def plus_1_not_0)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	30	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	31
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	lemma "inc = (\<lambda>y. y + 1)"
47831 1d25deb1f185 Sledgehammer can do it blanchet parents: 46733 diff changeset	33	sledgehammer [expect = some]
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	34	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	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	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	37	"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	38
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	lemma "add_swap m n = n + m"
47892 e389889da7df prevent spurious timeouts blanchet parents: 47831 diff changeset	40	sledgehammer [expect = some] (add_swap_def)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	41	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	42
61076 bdc1e2f0a86a eliminated \<Colon>; wenzelm parents: 58889 diff changeset	43	definition "A = {xs::'a list. True}"
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	44
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	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	46	(* 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	47	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	48	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	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	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	51	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	52
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	53	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	54	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	55
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 44768 diff changeset	56	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	57	sledgehammer [expect = some]
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	58	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	59
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 61314 diff changeset	60	text \<open>Proxies for logical constants\<close>
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	61
67399 eab6ce8368fa ran isabelle update_op on all sources nipkow parents: 63167 diff changeset	62	lemma "id (=) x x"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	63	sledgehammer [type_enc = erased, expect = none] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	64	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	65	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	66	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	67	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	68	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	69	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	70	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	71	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	72	by (metis (full_types) id_apply)
42758 865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	73
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	74	lemma "id True"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	75	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	76	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	77	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	78	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	79	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	80	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	81	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	82	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	83	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	84	by (metis_exhaust 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 "\<not> id False"
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	87	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	88	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	89	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	90	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	91	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	92	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	93	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	94	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	95	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	96	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	97
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	98	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	99	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	100	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	101	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	102	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	103	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	104	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	105	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	106	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	107	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	108	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	109
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	110	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	111	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	112	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	113	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	114	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	115	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	116	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	117	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	118	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	119	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	120	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	121
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	122	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	123	sledgehammer [type_enc = erased, expect = none] ()
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	124	sledgehammer [type_enc = poly_args, expect = none] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	125	sledgehammer [type_enc = poly_tags??, expect = some] ()
43626 a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate blanchet parents: 43228 diff changeset	126	sledgehammer [type_enc = poly_tags, expect = some] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	127	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	128	sledgehammer [type_enc = poly_guards, expect = some] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	129	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	130	sledgehammer [type_enc = mono_tags, expect = some] ()
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	131	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	132	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	133	by (metis (full_types))
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	134
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	135	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	136	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	137	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	138	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	139	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	140	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	141	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	142	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	143	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	144	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	145	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	146
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	147	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	148	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	149	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	150	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	151	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	152	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	153	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	154	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	155	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	156	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	157	by metis_exhaust
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	158
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	159	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	160	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	161	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	162	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	163	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	164	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	165	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	166	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	167	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	168	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	169	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	170
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	171	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	172	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	173	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	174	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	175	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	176	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	177	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	178	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	179	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	180	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	181	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	182
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	183	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	184	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	185	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	186	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	187	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	188	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	189	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	190	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	191	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	192	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	193	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	194
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	195	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	196	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	197	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	198	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	199	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	200	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	201	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	202	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	203	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	204	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	205	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	206
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	207	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	208	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	209	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	210	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	211	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	212	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	213	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	214	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	215	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	216	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	217	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	218
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	219	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	220	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	221	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	222	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	223	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	224	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	225	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	226	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	227	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	228	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	229	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	230
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	231	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	232	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	233	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	234	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	235	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	236	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	237	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	238	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	239	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	240	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	241	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	242
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	243	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	244	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	245	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	246	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	247	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	248	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	249	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	250	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	251	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	252	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	253	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	254
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	255	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	256	sledgehammer [type_enc = erased, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	257	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	258	sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	259	sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
43989 eb763b3ff9ed renamed "preds" encodings to "guards" blanchet parents: 43629 diff changeset	260	sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	261	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	262	sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
44768 a7bc1bdb8bb4 rationalize uniform encodings blanchet parents: 44494 diff changeset	263	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	264	sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
43212 050a03afe024 Metis code cleanup blanchet parents: 43205 diff changeset	265	by (metis_exhaust id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	266
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	267	end

author	paulson
	Thu, 12 Sep 2019 14:51:50 +0100
changeset 70689	67360d50ebb3
parent 67399	eab6ce8368fa
child 75043	46a94aa3ec8e
permissions	-rw-r--r--