# HG changeset patch
# User blanchet
# Date 1307385394 -7200
# Node ID 9a8acc5adfa35b8f65316e7c488f8c1f2e7b50f4
# Parent  27dcda8fc89b3c6d01bf300c984c7717400f80af
added Metis examples to test the new type encodings

diff -r 27dcda8fc89b -r 9a8acc5adfa3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/IsaMakefile	Mon Jun 06 20:36:34 2011 +0200
@@ -710,7 +710,7 @@
   Metis_Examples/BT.thy Metis_Examples/Clausify.thy \
   Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \
   Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
-  Metis_Examples/set.thy
+  Metis_Examples/Typings.thy Metis_Examples/set.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
 
 
diff -r 27dcda8fc89b -r 9a8acc5adfa3 src/HOL/Metis_Examples/ROOT.ML
--- a/src/HOL/Metis_Examples/ROOT.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Metis_Examples/ROOT.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -6,4 +6,4 @@
 *)
 
 use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message",
-          "Tarski", "TransClosure", "set"];
+          "Tarski", "TransClosure", "Typings", "set"];
diff -r 27dcda8fc89b -r 9a8acc5adfa3 src/HOL/Metis_Examples/Typings.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Typings.thy	Mon Jun 06 20:36:34 2011 +0200
@@ -0,0 +1,73 @@
+(*  Title:      HOL/Metis_Examples/Typings.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Testing the new Metis's (and hence Sledgehammer's) type translations.
+*)
+
+theory Typings
+imports Main
+begin
+
+
+text {* Setup for testing Metis exhaustively *}
+
+lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
+
+ML {*
+open ATP_Translate
+
+val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic]
+val levels =
+  [All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types]
+val heaviness = [Heavyweight, Lightweight]
+val type_syss =
+  (levels |> map Simple_Types) @
+  (map_product pair levels heaviness
+   |> map_product pair polymorphisms
+   |> map_product (fn constr => fn (poly, (level, heaviness)) =>
+                      constr (poly, level, heaviness))
+                  [Preds, Tags])
+
+fun metis_exhaust_tac ctxt ths =
+  let
+    fun tac [] = all_tac
+      | tac (type_sys :: type_syss) =
+        (if null type_syss then all_tac else rtac @{thm fork} 1)
+        THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1
+        THEN COND (has_fewer_prems 2) all_tac no_tac
+        THEN tac type_syss
+  in tac end
+*}
+
+method_setup metis_exhaust = {*
+  Attrib.thms >>
+    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss))
+*} "exhaustively run the new Metis with all type encodings"
+
+
+text {* Metis tests *}
+
+lemma "x = y \<Longrightarrow> y = x"
+by metis_exhaust
+
+lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
+by (metis_exhaust last.simps)
+
+lemma "map Suc [0] = [Suc 0]"
+by (metis_exhaust map.simps)
+
+lemma "map Suc [1 + 1] = [Suc 2]"
+by (metis_exhaust map.simps nat_1_add_1)
+
+lemma "map Suc [2] = [Suc (1 + 1)]"
+by (metis_exhaust map.simps nat_1_add_1)
+
+definition "null xs = (xs = [])"
+
+lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
+by (metis_exhaust null_def)
+
+lemma "(0::nat) + 0 = 0"
+by (metis_exhaust arithmetic_simps(38))
+
+end
diff -r 27dcda8fc89b -r 9a8acc5adfa3 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -789,8 +789,7 @@
   end
 
 fun fix_exists_tac t =
-  etac @{thm exE}
-  THEN' rename_tac [t |> dest_Var |> fst |> fst]
+  etac @{thm exE} THEN' rename_tac [t |> dest_Var |> fst |> fst]
 
 fun release_quantifier_tac thy (skolem, t) =
   (if skolem then fix_exists_tac else instantiate_forall_tac thy) t