--- a/src/HOL/Metis_Examples/Proxies.thy Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Thu Aug 25 14:25:07 2011 +0200
@@ -62,10 +62,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis (full_types) id_apply)
lemma "id True"
@@ -74,10 +74,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "\<not> id False"
@@ -86,10 +86,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
@@ -98,10 +98,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id x = id True \<or> id x = id False"
@@ -110,10 +110,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
@@ -123,10 +123,10 @@
sledgehammer [type_enc = poly_tags, expect = some] ()
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] ()
-sledgehammer [type_enc = mangled_tags?, expect = some] ()
-sledgehammer [type_enc = mangled_tags, expect = some] ()
-sledgehammer [type_enc = mangled_guards?, expect = some] ()
-sledgehammer [type_enc = mangled_guards, expect = some] ()
+sledgehammer [type_enc = mono_tags?, expect = some] ()
+sledgehammer [type_enc = mono_tags, expect = some] ()
+sledgehammer [type_enc = mono_guards?, expect = some] ()
+sledgehammer [type_enc = mono_guards, expect = some] ()
by (metis (full_types))
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
@@ -135,10 +135,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
@@ -147,10 +147,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
@@ -159,10 +159,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
@@ -171,10 +171,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
@@ -183,10 +183,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
@@ -195,10 +195,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
@@ -207,10 +207,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
@@ -219,10 +219,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
@@ -231,10 +231,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
@@ -243,10 +243,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
@@ -255,10 +255,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
end