--- a/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:56:06 2011 +0200
@@ -24,24 +24,24 @@
lemma "inc \<noteq> (\<lambda>y. 0)"
sledgehammer [expect = some] (inc_def plus_1_not_0)
-by (new_metis_exhaust 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 (new_metis_exhaust 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 (new_metis_exhaust add_swap_def)
+by (metis_exhaust add_swap_def)
definition "A = {xs\<Colon>'a list. True}"
lemma "xs \<in> A"
sledgehammer [expect = some]
-by (new_metis_exhaust 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"
@@ -51,7 +51,7 @@
lemma "B \<subseteq> C"
sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
-by (new_metis_exhaust 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 *}
@@ -78,7 +78,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "\<not> id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -90,7 +90,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -102,7 +102,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 (new_metis_exhaust 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)
@@ -114,7 +114,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
sledgehammer [type_sys = erased, expect = none] ()
@@ -139,7 +139,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -151,7 +151,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -163,7 +163,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -175,7 +175,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -187,7 +187,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 (new_metis_exhaust 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)
@@ -199,7 +199,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -211,7 +211,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -223,7 +223,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 (new_metis_exhaust 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)
@@ -235,7 +235,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -247,7 +247,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 (new_metis_exhaust 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)
@@ -259,6 +259,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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
end