more through tests of new Metis

--- a/src/HOL/Metis_Examples/HO_Reas.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory HO_Reas
-imports Main
+imports Typings
 begin
 
 declare [[metis_new_skolemizer]]
@@ -22,24 +22,24 @@
 
 lemma "inc \<noteq> (\<lambda>y. 0)"
 sledgehammer [expect = some] (inc_def plus_1_not_0)
-by (metis inc_def plus_1_not_0)
+by (metis_eXhaust inc_def plus_1_not_0)
 
 lemma "inc = (\<lambda>y. y + 1)"
 sledgehammer [expect = some] (inc_def)
-by (metis inc_def)
+by (metis_eXhaust 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)
+by (metis_eXhaust 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)
+by (metis_eXhaust A_def Collect_def mem_def)
 
 definition "B (y::int) \<equiv> y \<le> 0"
 definition "C (y::int) \<equiv> y \<le> 1"
@@ -49,7 +49,7 @@
 
 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)
+by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I)
 
 
 text {* Proxies for logical constants *}
@@ -64,7 +64,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metisX id_apply)
 
 lemma "id True"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -76,7 +76,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "\<not> id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -88,7 +88,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "x = id True \<or> x = id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -100,7 +100,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id x = id True \<or> id x = id False"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -112,7 +112,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
 sledgehammer [type_sys = erased, expect = none] ()
@@ -125,7 +125,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] ()
 sledgehammer [type_sys = mangled_preds?, expect = some] ()
 sledgehammer [type_sys = mangled_preds, expect = some] ()
-by metisFT
+by metisX
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -137,7 +137,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -149,7 +149,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -161,7 +161,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -173,7 +173,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id b"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -185,7 +185,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -197,7 +197,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id a \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -209,7 +209,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id b \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -221,7 +221,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -233,7 +233,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -245,7 +245,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -257,6 +257,6 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis id_apply)
+by (metis_eXhaust id_apply)
 
 end

--- a/src/HOL/Metis_Examples/Typings.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Typings.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -22,6 +22,10 @@
 val type_syss =
   (levels |> map Simple_Types) @
   (map_product pair levels heaviness
+   (* The following two families of type systems are too incomplete for our
+      tests. *)
+   |> remove (op =) (Nonmonotonic_Types, Heavyweight)
+   |> remove (op =) (Finite_Types, Heavyweight)
    |> map_product pair polymorphisms
    |> map_product (fn constr => fn (poly, (level, heaviness)) =>
                       constr (poly, level, heaviness))