# HG changeset patch
# User blanchet
# Date 1292408788 -3600
# Node ID ad923cdd4a5d9e625e6851b83216a5d6520945f3
# Parent  9c68004b8c9df1c7b6bdf00f76b50f074f27a2af
added example to exercise higher-order reasoning with Sledgehammer and Metis

diff -r 9c68004b8c9d -r ad923cdd4a5d src/HOL/Metis_Examples/BT.thy
--- a/src/HOL/Metis_Examples/BT.thy	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/BT.thy	Wed Dec 15 11:26:28 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MetisTest/BT.thy
+(*  Title:      HOL/Metis_Examples/BT.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
diff -r 9c68004b8c9d -r ad923cdd4a5d src/HOL/Metis_Examples/HO_Reas.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Wed Dec 15 11:26:28 2010 +0100
@@ -0,0 +1,81 @@
+(*  Title:      HOL/Metis_Examples/HO_Reas.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Testing Metis's and Sledgehammer's higher-order reasoning capabilities.
+*)
+
+theory HO_Reas
+imports Main
+begin
+
+sledgehammer_params [prover = e, blocking, isar_proof, timeout = 10]
+
+hide_const id
+definition id where "id (x::bool) = x"
+
+lemma "id True"
+sledgehammer [expect = some] (add: id_def)
+by (metis id_def)
+
+lemma "\<not> id False"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "x = id True \<or> x = id False"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id x = id True \<or> id x = id False"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
+sledgehammer [expect = none] ()
+sledgehammer [full_types, expect = some] ()
+by metisFT
+
+lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
+sledgehammer [expect = some] ()
+by metis
+
+lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id (a \<and> b) \<Longrightarrow> id a"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id (a \<and> b) \<Longrightarrow> id b"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id a \<Longrightarrow> id (a \<or> b)"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id b \<Longrightarrow> id (a \<or> b)"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
+sledgehammer [expect = some] (id_def)
+by (metis id_def)
+
+end
diff -r 9c68004b8c9d -r ad923cdd4a5d src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Wed Dec 15 11:26:28 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MetisTest/Message.thy
+(*  Title:      HOL/Metis_Examples/Message.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method.
diff -r 9c68004b8c9d -r ad923cdd4a5d src/HOL/Metis_Examples/ROOT.ML
--- a/src/HOL/Metis_Examples/ROOT.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/ROOT.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -1,8 +1,9 @@
 (*  Title:      HOL/Metis_Examples/ROOT.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Jasmin Blanchette, TU Muenchen
 
-Testing the metis method.
+Testing Metis and Sledgehammer.
 *)
 
-use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];
-
+use_thys ["set", "Abstraction", "BigO", "BT", "HO_Reas", "Message", "Tarski",
+          "TransClosure"];
diff -r 9c68004b8c9d -r ad923cdd4a5d src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Wed Dec 15 11:26:28 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MetisTest/Tarski.thy
+(*  Title:      HOL/Metis_Examples/Tarski.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method.
diff -r 9c68004b8c9d -r ad923cdd4a5d src/HOL/Metis_Examples/TransClosure.thy
--- a/src/HOL/Metis_Examples/TransClosure.thy	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/TransClosure.thy	Wed Dec 15 11:26:28 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MetisTest/TransClosure.thy
+(*  Title:      HOL/Metis_Examples/TransClosure.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method