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

41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	1	(* Title: HOL/Metis_Examples/HO_Reas.thy
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	3
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	4	Testing Metis's and Sledgehammer's higher-order reasoning capabilities.
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	5	*)
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	6
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	7	theory HO_Reas
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	8	imports Main
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	9	begin
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	10
42103 6066a35f6678 Metis examples use the new Skolemizer to test it blanchet parents: 41145 diff changeset	11	declare [[metis_new_skolemizer]]
6066a35f6678 Metis examples use the new Skolemizer to test it blanchet parents: 41145 diff changeset	12
42555 2570e1a5ddfb more higher-order tests for Sledgehammer/ATP blanchet parents: 42103 diff changeset	13	sledgehammer_params [prover = e, blocking, timeout = 10]
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	14
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	15	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	16
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	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	18	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	19
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	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	21	"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	22
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	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	24	sledgehammer [expect = some] (inc_def plus_1_not_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	25	by (metis inc_def plus_1_not_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
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	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	28	sledgehammer [expect = some] (inc_def)
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	by (metis inc_def)
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
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	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	32	"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	33
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	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	35	sledgehammer [expect = some] (add_swap_def)
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	by (metis add_swap_def)
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
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	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	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	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	41	sledgehammer [expect = some]
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	by (metis A_def Collect_def mem_def)
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
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	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	45	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	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	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	48	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	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 "B \<subseteq> C"
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	sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
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	by (metis B_def C_def int_le_0_imp_le_1 predicate1I)
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
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
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	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	56
42758 865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	57	lemma "id (op =) x x"
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	58	sledgehammer [type_sys = erased, expect = none] (id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	59	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	60	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	61	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	62	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	63	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	64	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	65	by (metis id_apply)
865ce93ce025 handle equality proxy in a more backward-compatible way blanchet parents: 42756 diff changeset	66
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	67	lemma "id True"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	68	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	69	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	70	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	71	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	72	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	73	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	74	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	75	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	76
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	77	lemma "\<not> id False"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	78	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	79	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	80	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	81	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	82	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	83	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	84	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	85	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	86
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	87	lemma "x = id True \<or> x = id False"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	88	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	89	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	90	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	91	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	92	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	93	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	94	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	95	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	96
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	97	lemma "id x = id True \<or> id x = id False"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	98	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	99	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	100	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	101	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	102	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	103	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	104	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	105	by (metis 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 "P True \<Longrightarrow> P False \<Longrightarrow> P x"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	108	sledgehammer [type_sys = erased, expect = none] ()
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	109	sledgehammer [type_sys = poly_args, expect = none] ()
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	110	sledgehammer [type_sys = poly_tags!, expect = some] ()
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	111	sledgehammer [type_sys = poly_tags, expect = some] ()
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	112	sledgehammer [type_sys = poly_preds, expect = some] ()
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	113	sledgehammer [type_sys = mangled_preds!, expect = some] ()
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	114	sledgehammer [type_sys = mangled_preds?, expect = some] ()
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	115	sledgehammer [type_sys = mangled_preds, expect = some] ()
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	116	by metisFT
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	117
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	118	lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	119	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	120	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	121	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	122	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	123	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	124	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	125	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	126	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	127
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	128	lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	129	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	130	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	131	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	132	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	133	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	134	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	135	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
42555 2570e1a5ddfb more higher-order tests for Sledgehammer/ATP blanchet parents: 42103 diff changeset	136	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	137
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	138	lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	139	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	140	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	141	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	142	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	143	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	144	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	145	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	146	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	147
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	148	lemma "id (a \<and> b) \<Longrightarrow> id a"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	149	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	150	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	151	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	152	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	153	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	154	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	155	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	156	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	157
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	158	lemma "id (a \<and> b) \<Longrightarrow> id b"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	159	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	160	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	161	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	162	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	163	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	164	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	165	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	166	by (metis 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 \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	169	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	170	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	171	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	172	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	173	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	174	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	175	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	176	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	177
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	178	lemma "id a \<Longrightarrow> id (a \<or> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	179	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	180	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	181	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	182	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	183	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	184	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	185	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	186	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	187
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	188	lemma "id b \<Longrightarrow> id (a \<or> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	189	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	190	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	191	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	192	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	193	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	194	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	195	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	196	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	197
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	198	lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	199	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	200	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	201	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	202	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	203	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	204	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	205	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	206	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	207
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	208	lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	209	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	210	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	211	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	212	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	213	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	214	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	215	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	216	by (metis id_apply)
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	217
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: diff changeset	218	lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	219	sledgehammer [type_sys = erased, expect = some] (id_apply)
42722 626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	220	sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	221	sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
626e292d22a7 renamed type systems for more consistency blanchet parents: 42686 diff changeset	222	sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	223	sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
42686 7206f5688cad compile + added monotonicity tests blanchet parents: 42590 diff changeset	224	sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
42590 03834570af86 adapt to new type system names blanchet parents: 42580 diff changeset	225	sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
41144 509e51b7509a example tuning blanchet parents: 41141 diff changeset	226	by (metis 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	end

author	wenzelm
	Fri, 13 May 2011 23:58:40 +0200
changeset 42795	66fcc9882784
parent 42760	d83802e7348e
child 42889	412fe70f41a4
permissions	-rw-r--r--