# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 6b7ef9b724fdf40edf77e4ac42e9f9a74e3fbe74
# Parent  4603154a301858c252b1d43ec2ed26554a280738
added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around

diff -r 4603154a3018 -r 6b7ef9b724fd src/HOL/Metis_Examples/Clausify.thy
--- a/src/HOL/Metis_Examples/Clausify.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Metis_Examples/Clausify.thy	Thu May 12 15:29:19 2011 +0200
@@ -12,36 +12,6 @@
 declare [[unify_search_bound = 100]]
 declare [[unify_trace_bound = 100]]
 
-sledgehammer_params [prover = e, blocking, timeout = 10]
-
-
-text {* Extensionality *}
-
-lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
-by simp
-
-definition inc :: "nat \<Rightarrow> nat" where
-"inc x = x + 1"
-
-lemma "inc \<noteq> (\<lambda>y. 0)"
-sledgehammer [expect = some] (inc_def plus_1_not_0)
-by (metis inc_def plus_1_not_0)
-
-lemma "inc = (\<lambda>y. y + 1)"
-sledgehammer [expect = some] (inc_def)
-by (metis inc_def)
-
-lemma "(\<lambda>y. y + 1) = inc"
-sledgehammer [expect = some] (inc_def)
-by (metis inc_def)
-
-definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-"add_swap = (\<lambda>x y. y + x)"
-
-lemma "add_swap m n = n + m"
-sledgehammer [expect = some] (add_swap_def)
-by (metis add_swap_def)
-
 
 text {* Definitional CNF for facts *}
 
diff -r 4603154a3018 -r 6b7ef9b724fd src/HOL/Metis_Examples/HO_Reas.thy
--- a/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
@@ -12,13 +12,56 @@
 
 sledgehammer_params [prover = e, blocking, timeout = 10]
 
+text {* Extensionality and set constants *}
+
+lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
+by simp
+
+definition inc :: "nat \<Rightarrow> nat" where
+"inc x = x + 1"
+
+lemma "inc \<noteq> (\<lambda>y. 0)"
+sledgehammer [expect = some] (inc_def plus_1_not_0)
+by (metis inc_def plus_1_not_0)
+
+lemma "inc = (\<lambda>y. y + 1)"
+sledgehammer [expect = some] (inc_def)
+by (metis inc_def)
+
+lemma "(\<lambda>y. y + 1) = inc"
+sledgehammer [expect = some] (inc_def)
+by (metis inc_def)
+
+definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add_swap = (\<lambda>x y. y + x)"
+
+lemma "add_swap m n = n + m"
+sledgehammer [expect = some] (add_swap_def)
+by (metis add_swap_def)
+
+definition "A = {xs\<Colon>'a list. True}"
+
+lemma "xs \<in> A"
+sledgehammer [expect = some]
+by (metis A_def Collect_def mem_def)
+
+definition "B (y::int) \<equiv> y \<le> 0"
+definition "C (y::int) \<equiv> y \<le> 1"
+
+lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
+by linarith
+
+lemma "B \<subseteq> C"
+sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
+by (metis B_def C_def int_le_0_imp_le_1 predicate1I)
+
+
+text {* Proxies for logical constants *}
+
 lemma "id True"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -28,10 +71,7 @@
 lemma "\<not> id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -41,11 +81,8 @@
 lemma "x = id True \<or> x = id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -54,10 +91,7 @@
 lemma "id x = id True \<or> id x = id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -68,10 +102,7 @@
 sledgehammer [type_sys = erased, expect = none] ()
 sledgehammer [type_sys = poly_args, expect = none] ()
 sledgehammer [type_sys = poly_tags!, expect = some] ()
-sledgehammer [type_sys = poly_tags?, expect = some] ()
 sledgehammer [type_sys = poly_tags, expect = some] ()
-sledgehammer [type_sys = poly_preds!, expect = some] ()
-sledgehammer [type_sys = poly_preds?, expect = some] ()
 sledgehammer [type_sys = poly_preds, expect = some] ()
 sledgehammer [type_sys = mangled_preds!, expect = some] ()
 sledgehammer [type_sys = mangled_preds?, expect = some] ()
@@ -81,10 +112,7 @@
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -94,10 +122,7 @@
 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -107,10 +132,7 @@
 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -120,10 +142,7 @@
 lemma "id (a \<and> b) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -133,10 +152,7 @@
 lemma "id (a \<and> b) \<Longrightarrow> id b"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -146,10 +162,7 @@
 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -159,10 +172,7 @@
 lemma "id a \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -172,10 +182,7 @@
 lemma "id b \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -185,10 +192,7 @@
 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
@@ -198,11 +202,8 @@
 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
@@ -211,10 +212,7 @@
 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)