--- a/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:38 2011 +0200
@@ -50,215 +50,215 @@
by linarith
lemma "B \<subseteq> C"
-sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
+sledgehammer [type_enc = poly_args, max_relevant = 200, expect = some]
by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
text {* Proxies for logical constants *}
lemma "id (op =) x x"
-sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = none] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis (full_types) id_apply)
lemma "id True"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "\<not> id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (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)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
-sledgehammer [type_sys = erased, expect = none] ()
-sledgehammer [type_sys = poly_args, expect = none] ()
-sledgehammer [type_sys = poly_tags?, expect = some] ()
-sledgehammer [type_sys = poly_tags, expect = some] ()
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] ()
-sledgehammer [type_sys = mangled_tags?, expect = some] ()
-sledgehammer [type_sys = mangled_tags, expect = some] ()
-sledgehammer [type_sys = mangled_preds?, expect = some] ()
-sledgehammer [type_sys = mangled_preds, expect = some] ()
+sledgehammer [type_enc = erased, expect = none] ()
+sledgehammer [type_enc = poly_args, expect = none] ()
+sledgehammer [type_enc = poly_tags?, expect = some] ()
+sledgehammer [type_enc = poly_tags, expect = some] ()
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] ()
+sledgehammer [type_enc = mangled_tags?, expect = some] ()
+sledgehammer [type_enc = mangled_tags, expect = some] ()
+sledgehammer [type_enc = mangled_preds?, expect = some] ()
+sledgehammer [type_enc = mangled_preds, expect = some] ()
by (metis (full_types))
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (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)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (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)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (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)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-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)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, 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_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
end
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 15:53:38 2011 +0200
@@ -24,7 +24,7 @@
ML {*
(* The commented-out type systems are too incomplete for our exhaustive
tests. *)
-val type_syss =
+val type_encs =
["erased",
"poly_preds",
"poly_preds_heavy",
@@ -72,18 +72,18 @@
fun metis_exhaust_tac ctxt ths =
let
fun tac [] st = all_tac st
- | tac (type_sys :: type_syss) st =
- st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
- |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
- THEN Metis_Tactics.metis_tac [type_sys] ctxt ths 1
+ | tac (type_enc :: type_encs) st =
+ st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
+ |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
+ THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1
THEN COND (has_fewer_prems 2) all_tac no_tac
- THEN tac type_syss)
+ THEN tac type_encs)
in tac end
*}
method_setup metis_exhaust = {*
Attrib.thms >>
- (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss))
+ (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs))
*} "exhaustively run the new Metis with all type encodings"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 01 15:53:38 2011 +0200
@@ -8,7 +8,7 @@
val proverK = "prover"
val prover_timeoutK = "prover_timeout"
val keepK = "keep"
-val type_sysK = "type_sys"
+val type_encK = "type_enc"
val slicingK = "slicing"
val e_weight_methodK = "e_weight_method"
val spass_force_sosK = "spass_force_sos"
@@ -353,7 +353,7 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
vampire_force_sos hard_timeout timeout dir st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
@@ -377,7 +377,7 @@
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
- ("type_sys", type_sys),
+ ("type_enc", type_enc),
("max_relevant", max_relevant),
("slicing", slicing),
("timeout", string_of_int timeout)]
@@ -452,7 +452,7 @@
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
val (prover_name, prover) = get_prover (Proof.context_of st) args
- val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
+ val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
val e_weight_method = AList.lookup (op =) args e_weight_methodK
@@ -466,7 +466,7 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+ run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
vampire_force_sos hard_timeout timeout dir st
in
case result of
@@ -503,7 +503,7 @@
val ctxt = Proof.context_of st
val n0 = length (these (!named_thms))
val (prover_name, _) = get_prover ctxt args
- val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
+ val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
@@ -511,7 +511,7 @@
val params = Sledgehammer_Isar.default_params ctxt
[("provers", prover_name),
("verbose", "true"),
- ("type_sys", type_sys),
+ ("type_enc", type_enc),
("timeout", string_of_int timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
@@ -546,9 +546,9 @@
else if !reconstructor = "smt" then
SMT_Solver.smt_tac
else if full orelse !reconstructor = "metis (full_types)" then
- Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
else if !reconstructor = "metis (no_types)" then
- Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
else
Metis_Tactics.metis_tac []) ctxt thms
fun apply_reconstructor thms =
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 01 15:53:38 2011 +0200
@@ -386,8 +386,8 @@
prem_kind = prem_kind,
formats = formats,
best_slices = fn ctxt =>
- let val (max_relevant, type_sys) = best_slice ctxt in
- [(1.0, (false, (max_relevant, type_sys, "")))]
+ let val (max_relevant, type_enc) = best_slice ctxt in
+ [(1.0, (false, (max_relevant, type_enc, "")))]
end}
fun remotify_config system_name system_versions best_slice
--- a/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:38 2011 +0200
@@ -26,7 +26,7 @@
No_Types
datatype type_heaviness = Heavyweight | Lightweight
- datatype type_sys =
+ datatype type_enc =
Simple_Types of order * type_level |
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
@@ -75,12 +75,12 @@
val atp_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_locality_global : locality -> bool
- val type_sys_from_string : string -> type_sys
- val polymorphism_of_type_sys : type_sys -> polymorphism
- val level_of_type_sys : type_sys -> type_level
- val is_type_sys_virtually_sound : type_sys -> bool
- val is_type_sys_fairly_sound : type_sys -> bool
- val choose_format : format list -> type_sys -> format * type_sys
+ val type_enc_from_string : string -> type_enc
+ val polymorphism_of_type_enc : type_enc -> polymorphism
+ val level_of_type_enc : type_enc -> type_level
+ val is_type_enc_virtually_sound : type_enc -> bool
+ val is_type_enc_fairly_sound : type_enc -> bool
+ val choose_format : format list -> type_enc -> format * type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * string fo_term list
@@ -88,7 +88,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
+ Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
-> bool -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -509,7 +509,7 @@
No_Types
datatype type_heaviness = Heavyweight | Lightweight
-datatype type_sys =
+datatype type_enc =
Simple_Types of order * type_level |
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
@@ -517,7 +517,7 @@
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
-fun type_sys_from_string s =
+fun type_enc_from_string s =
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
| NONE =>
@@ -557,29 +557,29 @@
| _ => raise Same.SAME)
handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
-fun is_type_sys_higher_order (Simple_Types (Higher_Order, _)) = true
- | is_type_sys_higher_order _ = false
+fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
+ | is_type_enc_higher_order _ = false
-fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
- | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
- | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
+fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
+ | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
+ | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
-fun level_of_type_sys (Simple_Types (_, level)) = level
- | level_of_type_sys (Preds (_, level, _)) = level
- | level_of_type_sys (Tags (_, level, _)) = level
+fun level_of_type_enc (Simple_Types (_, level)) = level
+ | level_of_type_enc (Preds (_, level, _)) = level
+ | level_of_type_enc (Tags (_, level, _)) = level
-fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
- | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
- | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
+fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
+ | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
+ | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
fun is_type_level_virtually_sound level =
level = All_Types orelse level = Noninf_Nonmono_Types
-val is_type_sys_virtually_sound =
- is_type_level_virtually_sound o level_of_type_sys
+val is_type_enc_virtually_sound =
+ is_type_level_virtually_sound o level_of_type_enc
fun is_type_level_fairly_sound level =
is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
-val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
+val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
fun choose_format formats (Simple_Types (order, level)) =
if member (op =) formats THF then
@@ -588,15 +588,15 @@
(TFF, Simple_Types (First_Order, level))
else
choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
- | choose_format formats type_sys =
+ | choose_format formats type_enc =
(case hd formats of
CNF_UEQ =>
- (CNF_UEQ, case type_sys of
+ (CNF_UEQ, case type_enc of
Preds stuff =>
- (if is_type_sys_fairly_sound type_sys then Tags else Preds)
+ (if is_type_enc_fairly_sound type_enc then Tags else Preds)
stuff
- | _ => type_sys)
- | format => (format, type_sys))
+ | _ => type_enc)
+ | format => (format, type_enc))
type translated_formula =
{name : string,
@@ -628,30 +628,30 @@
fun should_drop_arg_type_args (Simple_Types _) =
false (* since TFF doesn't support overloading *)
- | should_drop_arg_type_args type_sys =
- level_of_type_sys type_sys = All_Types andalso
- heaviness_of_type_sys type_sys = Heavyweight
+ | should_drop_arg_type_args type_enc =
+ level_of_type_enc type_enc = All_Types andalso
+ heaviness_of_type_enc type_enc = Heavyweight
fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
- | general_type_arg_policy type_sys =
- if level_of_type_sys type_sys = No_Types then
+ | general_type_arg_policy type_enc =
+ if level_of_type_enc type_enc = No_Types then
No_Type_Args
- else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
- Mangled_Type_Args (should_drop_arg_type_args type_sys)
+ else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+ Mangled_Type_Args (should_drop_arg_type_args type_enc)
else
- Explicit_Type_Args (should_drop_arg_type_args type_sys)
+ Explicit_Type_Args (should_drop_arg_type_args type_enc)
-fun type_arg_policy type_sys s =
+fun type_arg_policy type_enc s =
if s = @{const_name HOL.eq} orelse
- (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
+ (s = app_op_name andalso level_of_type_enc type_enc = Const_Arg_Types) then
No_Type_Args
else if s = type_tag_name then
- (if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
+ (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
Mangled_Type_Args
else
Explicit_Type_Args) false
else
- general_type_arg_policy type_sys
+ general_type_arg_policy type_enc
(*Make literals for sorted type variables*)
fun generic_add_sorts_on_type (_, []) = I
@@ -669,8 +669,8 @@
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
| add_sorts_on_tvar _ = I
-fun type_literals_for_types type_sys add_sorts_on_typ Ts =
- [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
+fun type_literals_for_types type_enc add_sorts_on_typ Ts =
+ [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
fun mk_aconns c phis =
let val (phis', phi') = split_last phis in
@@ -705,10 +705,10 @@
val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
val homo_infinite_type = Type (homo_infinite_type_name, [])
-fun fo_term_from_typ format type_sys =
+fun fo_term_from_typ format type_enc =
let
fun term (Type (s, Ts)) =
- ATerm (case (is_type_sys_higher_order type_sys, s) of
+ ATerm (case (is_type_enc_higher_order type_enc, s) of
(true, @{type_name bool}) => `I tptp_bool_type
| (true, @{type_name fun}) => `I tptp_fun_type
| _ => if s = homo_infinite_type_name andalso
@@ -722,8 +722,8 @@
ATerm ((make_schematic_type_var x, s), [])
in term end
-fun fo_term_for_type_arg format type_sys T =
- if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
+fun fo_term_for_type_arg format type_enc T =
+ if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
(* This shouldn't clash with anything else. *)
val mangled_type_sep = "\000"
@@ -742,7 +742,7 @@
else
simple_type_prefix ^ ascii_of s
-fun ho_type_from_fo_term type_sys pred_sym ary =
+fun ho_type_from_fo_term type_enc pred_sym ary =
let
fun to_atype ty =
AType ((make_simple_type (generic_mangled_type_name fst ty),
@@ -752,15 +752,15 @@
| to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
fun to_ho (ty as ATerm ((s, _), tys)) =
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
- in if is_type_sys_higher_order type_sys then to_ho else to_fo ary end
+ in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
-fun mangled_type format type_sys pred_sym ary =
- ho_type_from_fo_term type_sys pred_sym ary
- o fo_term_from_typ format type_sys
+fun mangled_type format type_enc pred_sym ary =
+ ho_type_from_fo_term type_enc pred_sym ary
+ o fo_term_from_typ format type_enc
-fun mangled_const_name format type_sys T_args (s, s') =
+fun mangled_const_name format type_enc T_args (s, s') =
let
- val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
+ val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
fun type_suffix f g =
fold_rev (curry (op ^) o g o prefix mangled_type_sep
o generic_mangled_type_name f) ty_args ""
@@ -789,14 +789,14 @@
(hd ss, map unmangled_type (tl ss))
end
-fun introduce_proxies type_sys =
+fun introduce_proxies type_enc =
let
fun intro top_level (CombApp (tm1, tm2)) =
CombApp (intro top_level tm1, intro false tm2)
| intro top_level (CombConst (name as (s, _), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
- if top_level orelse is_type_sys_higher_order type_sys then
+ if top_level orelse is_type_enc_higher_order type_enc then
case (top_level, s) of
(_, "c_False") => (`I tptp_false, [])
| (_, "c_True") => (`I tptp_true, [])
@@ -815,11 +815,11 @@
| intro _ tm = tm
in intro true end
-fun combformula_from_prop thy type_sys eq_as_iff =
+fun combformula_from_prop thy type_enc eq_as_iff =
let
fun do_term bs t atomic_types =
combterm_from_term thy bs (Envir.eta_contract t)
- |>> (introduce_proxies type_sys #> AAtom)
+ |>> (introduce_proxies type_enc #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q s T t' =
let val s = singleton (Name.variant_list (map fst bs)) s in
@@ -940,27 +940,27 @@
end
(* making fact and conjecture formulas *)
-fun make_formula thy type_sys eq_as_iff name loc kind t =
+fun make_formula thy type_enc eq_as_iff name loc kind t =
let
val (combformula, atomic_types) =
- combformula_from_prop thy type_sys eq_as_iff t []
+ combformula_from_prop thy type_enc eq_as_iff t []
in
{name = name, locality = loc, kind = kind, combformula = combformula,
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
- |> make_formula thy type_sys (eq_as_iff andalso format <> CNF) name
+ |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
loc Axiom of
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula
end
-fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
+fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
let
val thy = Proof_Context.theory_of ctxt
val last = length ts - 1
@@ -977,7 +977,7 @@
in
t |> preproc ?
(preprocess_prop ctxt presimp_consts kind #> freeze_term)
- |> make_formula thy type_sys (format <> CNF) (string_of_int j)
+ |> make_formula thy type_enc (format <> CNF) (string_of_int j)
Local kind
|> maybe_negate
end)
@@ -1231,7 +1231,7 @@
end
handle TYPE _ => T_args
-fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
+fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
let
val thy = Proof_Context.theory_of ctxt
fun aux arity (CombApp (tm1, tm2)) =
@@ -1245,11 +1245,11 @@
fun filtered_T_args false = T_args
| filtered_T_args true = filter_type_args thy s'' arity T_args
in
- case type_arg_policy type_sys s'' of
+ case type_arg_policy type_enc s'' of
Explicit_Type_Args drop_args =>
(name, filtered_T_args drop_args)
| Mangled_Type_Args drop_args =>
- (mangled_const_name format type_sys (filtered_T_args drop_args)
+ (mangled_const_name format type_enc (filtered_T_args drop_args)
name, [])
| No_Type_Args => (name, [])
end)
@@ -1257,14 +1257,14 @@
| aux _ tm = tm
in aux 0 end
-fun repair_combterm ctxt format type_sys sym_tab =
- not (is_type_sys_higher_order type_sys)
+fun repair_combterm ctxt format type_enc sym_tab =
+ not (is_type_enc_higher_order type_enc)
? (introduce_explicit_apps_in_combterm sym_tab
#> introduce_predicators_in_combterm sym_tab)
- #> enforce_type_arg_policy_in_combterm ctxt format type_sys
-fun repair_fact ctxt format type_sys sym_tab =
+ #> enforce_type_arg_policy_in_combterm ctxt format type_enc
+fun repair_fact ctxt format type_enc sym_tab =
update_combformula (formula_map
- (repair_combterm ctxt format type_sys sym_tab))
+ (repair_combterm ctxt format type_enc sym_tab))
(** Helper facts **)
@@ -1313,12 +1313,12 @@
|> close_formula_universally, simp_info, NONE)
end
-fun should_specialize_helper type_sys t =
- case general_type_arg_policy type_sys of
+fun should_specialize_helper type_enc t =
+ case general_type_arg_policy type_enc of
Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
| _ => false
-fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -1331,14 +1331,14 @@
else untyped_helper_suffix),
Helper),
let val t = th |> prop_of in
- t |> should_specialize_helper type_sys t
+ t |> should_specialize_helper type_enc t
? (case types of
[T] => specialize_type thy (invert_const unmangled_s, T)
| _ => I)
end)
val make_facts =
- map_filter (make_fact ctxt format type_sys false false [])
- val fairly_sound = is_type_sys_fairly_sound type_sys
+ map_filter (make_fact ctxt format type_enc false false [])
+ val fairly_sound = is_type_enc_fairly_sound type_enc
in
helper_table
|> maps (fn ((helper_s, needs_fairly_sound), ths) =>
@@ -1351,8 +1351,8 @@
|> make_facts)
end
| NONE => []
-fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
- Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
+fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
+ Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
[]
(***************************************************************)
@@ -1393,13 +1393,13 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
-fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
+fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
facts =
let
val thy = Proof_Context.theory_of ctxt
val fact_ts = facts |> map snd
val presimp_consts = Meson.presimplified_consts ctxt
- val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
+ val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
val (facts, fact_names) =
facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
|> map_filter (try (apfst the))
@@ -1416,9 +1416,9 @@
val tycons = type_constrs_of_terms thy all_ts
val conjs =
hyp_ts @ [concl_t]
- |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
+ |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
val (supers', arity_clauses) =
- if level_of_type_sys type_sys = No_Types then ([], [])
+ if level_of_type_enc type_enc = No_Types then ([], [])
else make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
@@ -1434,9 +1434,9 @@
val type_pred = `make_fixed_const type_pred_name
-fun type_pred_combterm ctxt format type_sys T tm =
+fun type_pred_combterm ctxt format type_enc T tm =
CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
- |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
+ |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
| is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
@@ -1445,15 +1445,15 @@
formula_fold pos (is_var_positively_naked_in_term name) phi false
| should_predicate_on_var_in_formula _ _ _ _ = true
-fun mk_const_aterm format type_sys x T_args args =
- ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
+fun mk_const_aterm format type_enc x T_args args =
+ ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
-fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
+fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
CombConst (type_tag, T --> T, [T])
- |> enforce_type_arg_policy_in_combterm ctxt format type_sys
- |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
+ |> enforce_type_arg_policy_in_combterm ctxt format type_enc
+ |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
-and term_from_combterm ctxt format nonmono_Ts type_sys =
+and term_from_combterm ctxt format nonmono_Ts type_enc =
let
fun aux site u =
let
@@ -1469,32 +1469,32 @@
(pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
| Eq_Arg pos => (pos, Elsewhere)
| Elsewhere => (NONE, Elsewhere)
- val t = mk_const_aterm format type_sys x T_args
+ val t = mk_const_aterm format type_enc x T_args
(map (aux arg_site) args)
val T = combtyp_of u
in
- t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
- tag_with_type ctxt format nonmono_Ts type_sys pos T
+ t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
+ tag_with_type ctxt format nonmono_Ts type_enc pos T
else
I)
end
in aux end
-and formula_from_combformula ctxt format nonmono_Ts type_sys
+and formula_from_combformula ctxt format nonmono_Ts type_enc
should_predicate_on_var =
let
fun do_term pos =
- term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
+ term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
val do_bound_type =
- case type_sys of
+ case type_enc of
Simple_Types (_, level) =>
homogenized_type ctxt nonmono_Ts level 0
- #> mangled_type format type_sys false 0 #> SOME
+ #> mangled_type format type_enc false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
- if should_predicate_on_type ctxt nonmono_Ts type_sys
+ if should_predicate_on_type ctxt nonmono_Ts type_enc
(fn () => should_predicate_on_var pos phi universal name) T then
CombVar (name, T)
- |> type_pred_combterm ctxt format type_sys T
+ |> type_pred_combterm ctxt format type_enc T
|> do_term pos |> AAtom |> SOME
else
NONE
@@ -1517,23 +1517,23 @@
| do_formula pos (AAtom tm) = AAtom (do_term pos tm)
in do_formula end
-fun bound_tvars type_sys Ts =
+fun bound_tvars type_enc Ts =
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
- (type_literals_for_types type_sys add_sorts_on_tvar Ts))
+ (type_literals_for_types type_enc add_sorts_on_tvar Ts))
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
- type_sys (j, {name, locality, kind, combformula, atomic_types}) =
+ type_enc (j, {name, locality, kind, combformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
kind,
combformula
|> close_combformula_universally
- |> formula_from_combformula ctxt format nonmono_Ts type_sys
+ |> formula_from_combformula ctxt format nonmono_Ts type_enc
should_predicate_on_var_in_formula
(if pos then SOME true else NONE)
- |> bound_tvars type_sys atomic_types
+ |> bound_tvars type_enc atomic_types
|> close_formula_universally,
NONE,
case locality of
@@ -1566,45 +1566,45 @@
(fo_literal_from_arity_literal concl_lits))
|> close_formula_universally, intro_info, NONE)
-fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
+fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
({name, kind, combformula, atomic_types, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
- formula_from_combformula ctxt format nonmono_Ts type_sys
+ formula_from_combformula ctxt format nonmono_Ts type_enc
should_predicate_on_var_in_formula (SOME false)
(close_combformula_universally combformula)
- |> bound_tvars type_sys atomic_types
+ |> bound_tvars type_enc atomic_types
|> close_formula_universally, NONE, NONE)
-fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
- atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
+fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
+ atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
|> map fo_literal_from_type_literal
fun formula_line_for_free_type j lit =
Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types type_sys facts =
+fun formula_lines_for_free_types type_enc facts =
let
- val litss = map (free_type_literals type_sys) facts
+ val litss = map (free_type_literals type_enc) facts
val lits = fold (union (op =)) litss []
in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
(** Symbol declarations **)
-fun should_declare_sym type_sys pred_sym s =
+fun should_declare_sym type_enc pred_sym s =
is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
- (case type_sys of
+ (case type_enc of
Simple_Types _ => true
| Tags (_, _, Lightweight) => true
| _ => not pred_sym)
-fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
+fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
let
fun add_combterm in_conj tm =
let val (head, args) = strip_combterm_comb tm in
(case head of
CombConst ((s, s'), T, T_args) =>
let val pred_sym = is_pred_sym repaired_sym_tab s in
- if should_declare_sym type_sys pred_sym s then
+ if should_declare_sym type_enc pred_sym s then
Symtab.map_default (s, [])
(insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
in_conj))
@@ -1618,7 +1618,7 @@
fact_lift (formula_fold NONE (K (add_combterm in_conj)))
in
Symtab.empty
- |> is_type_sys_fairly_sound type_sys
+ |> is_type_enc_fairly_sound type_enc
? (fold (add_fact true) conjs #> fold (add_fact false) facts)
end
@@ -1641,8 +1641,8 @@
formula_fold (SOME (kind <> Conjecture))
(add_combterm_nonmonotonic_types ctxt level sound locality)
combformula
-fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
- let val level = level_of_type_sys type_sys in
+fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
+ let val level = level_of_type_enc type_enc in
if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
[] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
(* We must add "bool" in case the helper "True_or_False" is added
@@ -1653,21 +1653,21 @@
[]
end
-fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
+fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
(s', T_args, T, pred_sym, ary, _) =
let
val (T_arg_Ts, level) =
- case type_sys of
+ case type_enc of
Simple_Types (_, level) => ([], level)
| _ => (replicate (length T_args) homo_infinite_type, No_Types)
in
Decl (sym_decl_prefix ^ s, (s, s'),
(T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
- |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
+ |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
end
fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
+ poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
let
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
@@ -1681,7 +1681,7 @@
val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
fun should_keep_arg_type T =
sym_needs_arg_types orelse
- not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
+ not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
val bound_Ts =
arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
in
@@ -1689,18 +1689,18 @@
(if n > 1 then "_" ^ string_of_int j else ""), kind,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bounds
- |> type_pred_combterm ctxt format type_sys res_T
+ |> type_pred_combterm ctxt format type_enc res_T
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
+ |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
(K (K (K (K true)))) (SOME true)
- |> n > 1 ? bound_tvars type_sys (atyps_of T)
+ |> n > 1 ? bound_tvars type_enc (atyps_of T)
|> close_formula_universally
|> maybe_negate,
intro_info, NONE)
end
fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
- poly_nonmono_Ts type_sys n s
+ poly_nonmono_Ts type_enc n s
(j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val ident_base =
@@ -1713,22 +1713,22 @@
val bound_names =
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
- val cst = mk_const_aterm format type_sys (s, s') T_args
+ val cst = mk_const_aterm format type_enc (s, s') T_args
val atomic_Ts = atyps_of T
fun eq tms =
(if pred_sym then AConn (AIff, map AAtom tms)
else AAtom (ATerm (`I tptp_equal, tms)))
- |> bound_tvars type_sys atomic_Ts
+ |> bound_tvars type_enc atomic_Ts
|> close_formula_universally
|> maybe_negate
(* See also "should_tag_with_type". *)
fun should_encode T =
should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
- (case type_sys of
+ (case type_enc of
Tags (Polymorphic, level, Lightweight) =>
level <> All_Types andalso Monomorph.typ_has_tvars T
| _ => false)
- val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
+ val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
val add_formula_for_res =
if should_encode res_T then
cons (Formula (ident_base ^ "_res", kind,
@@ -1757,10 +1757,10 @@
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys (s, decls) =
- case type_sys of
+ poly_nonmono_Ts type_enc (s, decls) =
+ case type_enc of
Simple_Types _ =>
- decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
+ decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
| Preds _ =>
let
val decls =
@@ -1776,13 +1776,13 @@
| _ => decls
val n = length decls
val decls =
- decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
+ decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
(K true)
o result_type_of_decl)
in
(0 upto length decls - 1, decls)
|-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
- nonmono_Ts poly_nonmono_Ts type_sys n s)
+ nonmono_Ts poly_nonmono_Ts type_enc n s)
end
| Tags (_, _, heaviness) =>
(case heaviness of
@@ -1791,17 +1791,17 @@
let val n = length decls in
(0 upto n - 1 ~~ decls)
|> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
- conj_sym_kind poly_nonmono_Ts type_sys n s)
+ conj_sym_kind poly_nonmono_Ts type_enc n s)
end)
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys sym_decl_tab =
+ poly_nonmono_Ts type_enc sym_decl_tab =
sym_decl_tab
|> Symtab.dest
|> sort_wrt fst
|> rpair []
|-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
- nonmono_Ts poly_nonmono_Ts type_sys)
+ nonmono_Ts poly_nonmono_Ts type_enc)
fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
poly <> Mangled_Monomorphic andalso
@@ -1825,39 +1825,39 @@
val explicit_apply = NONE (* for experimental purposes *)
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
exporter readable_names preproc hyp_ts concl_t facts =
let
- val (format, type_sys) = choose_format [format] type_sys
+ val (format, type_enc) = choose_format [format] type_enc
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
+ translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val nonmono_Ts =
- conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
- val repair = repair_fact ctxt format type_sys sym_tab
+ conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
+ val repair = repair_fact ctxt format type_enc sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab =
conjs @ facts |> sym_table_for_facts ctxt (SOME false)
val helpers =
- repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
+ repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
|> map repair
val poly_nonmono_Ts =
if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
- polymorphism_of_type_sys type_sys <> Polymorphic then
+ polymorphism_of_type_enc type_enc <> Polymorphic then
nonmono_Ts
else
[TVar (("'a", 0), HOLogic.typeS)]
val sym_decl_lines =
(conjs, helpers @ facts)
- |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
+ |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
|> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys
+ poly_nonmono_Ts type_enc
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt format helper_prefix I false true
- poly_nonmono_Ts type_sys)
- |> (if needs_type_tag_idempotence type_sys then
+ poly_nonmono_Ts type_enc)
+ |> (if needs_type_tag_idempotence type_enc then
cons (type_tag_idempotence_fact ())
else
I)
@@ -1868,15 +1868,15 @@
(factsN,
map (formula_line_for_fact ctxt format fact_prefix ascii_of
(not exporter) (not exporter) nonmono_Ts
- type_sys)
+ type_enc)
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
(helpersN, helper_lines),
(conjsN,
- map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
+ map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
conjs),
- (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
+ (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
val problem =
problem
|> (case format of
--- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri Jul 01 15:53:38 2011 +0200
@@ -13,10 +13,10 @@
val full_typesN : string
val partial_typesN : string
val no_typesN : string
- val really_full_type_sys : string
- val full_type_sys : string
- val partial_type_sys : string
- val no_type_sys : string
+ val really_full_type_enc : string
+ val full_type_enc : string
+ val partial_type_enc : string
+ val no_type_enc : string
val full_type_syss : string list
val partial_type_syss : string list
val trace : bool Config.T
@@ -39,22 +39,22 @@
val partial_typesN = "partial_types"
val no_typesN = "no_types"
-val really_full_type_sys = "poly_tags_heavy"
-val full_type_sys = "poly_preds_heavy_query"
-val partial_type_sys = "poly_args"
-val no_type_sys = "erased"
+val really_full_type_enc = "poly_tags_heavy"
+val full_type_enc = "poly_preds_heavy_query"
+val partial_type_enc = "poly_args"
+val no_type_enc = "erased"
-val full_type_syss = [full_type_sys, really_full_type_sys]
-val partial_type_syss = partial_type_sys :: full_type_syss
+val full_type_syss = [full_type_enc, really_full_type_enc]
+val partial_type_syss = partial_type_enc :: full_type_syss
-val type_sys_aliases =
+val type_enc_aliases =
[(full_typesN, full_type_syss),
(partial_typesN, partial_type_syss),
- (no_typesN, [no_type_sys])]
+ (no_typesN, [no_type_enc])]
-fun method_call_for_type_sys type_syss =
+fun method_call_for_type_enc type_syss =
metisN ^ " (" ^
- (case AList.find (op =) type_sys_aliases type_syss of
+ (case AList.find (op =) type_enc_aliases type_syss of
[alias] => alias
| _ => hd type_syss) ^ ")"
@@ -102,7 +102,7 @@
val resolution_params = {active = active_params, waiting = waiting_params}
(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
+fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
val new_skolemizer =
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
@@ -118,7 +118,7 @@
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
val (sym_tab, axioms, old_skolems) =
- prepare_metis_problem ctxt type_sys cls ths
+ prepare_metis_problem ctxt type_enc cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
| get_isa_thm _ (Isa_Raw ith) = ith
@@ -126,7 +126,7 @@
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
val thms = axioms |> map fst
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
- val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
+ val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
in
case filter (fn t => prop_of t aconv @{prop False}) cls of
@@ -186,7 +186,7 @@
| _ =>
(verbose_warning ctxt
("Falling back on " ^
- quote (method_call_for_type_sys fallback_type_syss) ^ "...");
+ quote (method_call_for_type_enc fallback_type_syss) ^ "...");
FOL_SOLVE fallback_type_syss ctxt cls ths0)
val neg_clausify =
@@ -249,7 +249,7 @@
fun setup_method (binding, type_syss) =
((Args.parens (Scan.repeat Parse.short_ident)
- >> maps (fn s => case AList.lookup (op =) type_sys_aliases s of
+ >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of
SOME tss => tss
| NONE => [s]))
|> Scan.option |> Scan.lift)
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Jul 01 15:53:38 2011 +0200
@@ -165,11 +165,11 @@
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
let
- val type_sys = type_sys_from_string type_sys
+ val type_enc = type_enc_from_string type_enc
val (conj_clauses, fact_clauses) =
- if polymorphism_of_type_sys type_sys = Polymorphic then
+ if polymorphism_of_type_enc type_enc = Polymorphic then
(conj_clauses, fact_clauses)
else
conj_clauses @ fact_clauses
@@ -196,7 +196,7 @@
tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false
false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 01 15:53:38 2011 +0200
@@ -84,7 +84,7 @@
("verbose", "false"),
("overlord", "false"),
("blocking", "false"),
- ("type_sys", "smart"),
+ ("type_enc", "smart"),
("sound", "false"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
@@ -107,7 +107,7 @@
("no_slicing", "slicing")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
+ ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
"max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
"preplay_timeout"]
@@ -124,15 +124,15 @@
ss as _ :: _ => forall (is_prover_supported ctxt) ss
| _ => false
-(* "provers =" and "type_sys =" can be left out. The latter is a secret
+(* "provers =" and "type_enc =" can be left out. The latter is a secret
feature. *)
fun check_and_repair_raw_param ctxt (name, value) =
if is_known_raw_param name then
(name, value)
else if is_prover_list ctxt name andalso null value then
("provers", [name])
- else if can type_sys_from_string name andalso null value then
- ("type_sys", [name])
+ else if can type_enc_from_string name andalso null value then
+ ("type_enc", [name])
else
error ("Unknown parameter: " ^ quote name ^ ".")
@@ -264,12 +264,12 @@
lookup_bool "blocking"
val provers = lookup_string "provers" |> space_explode " "
|> mode = Auto_Try ? single o hd
- val type_sys =
+ val type_enc =
if mode = Auto_Try then
NONE
- else case lookup_string "type_sys" of
+ else case lookup_string "type_enc" of
"smart" => NONE
- | s => SOME (type_sys_from_string s)
+ | s => SOME (type_enc_from_string s)
val sound = mode = Auto_Try orelse lookup_bool "sound"
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
@@ -288,7 +288,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
- max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
+ max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
sound = sound, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slicing = slicing,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 01 15:53:38 2011 +0200
@@ -47,7 +47,7 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
- max_new_mono_instances, type_sys, isar_proof,
+ max_new_mono_instances, type_enc, isar_proof,
isar_shrink_factor, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
@@ -59,7 +59,7 @@
val {goal, ...} = Proof.goal state
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
- provers = provers, type_sys = type_sys, sound = true,
+ provers = provers, type_enc = type_enc, sound = true,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 01 15:53:38 2011 +0200
@@ -10,7 +10,7 @@
sig
type failure = ATP_Proof.failure
type locality = ATP_Translate.locality
- type type_sys = ATP_Translate.type_sys
+ type type_enc = ATP_Translate.type_enc
type reconstructor = ATP_Reconstruct.reconstructor
type play = ATP_Reconstruct.play
type minimize_command = ATP_Reconstruct.minimize_command
@@ -24,7 +24,7 @@
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: type_sys option,
+ type_enc: type_enc option,
sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -289,7 +289,7 @@
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: type_sys option,
+ type_enc: type_enc option,
sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -407,11 +407,11 @@
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
fun tac_for_reconstructor Metis =
- Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc]
| tac_for_reconstructor Metis_Full_Types =
Metis_Tactics.metis_tac Metis_Tactics.full_type_syss
| tac_for_reconstructor Metis_No_Types =
- Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
| tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
fun timed_reconstructor reconstructor debug timeout ths =
@@ -504,10 +504,10 @@
them each time. *)
val atp_important_message_keep_quotient = 10
-fun choose_format_and_type_sys best_type_sys formats type_sys_opt =
- (case type_sys_opt of
+fun choose_format_and_type_enc best_type_enc formats type_enc_opt =
+ (case type_enc_opt of
SOME ts => ts
- | NONE => type_sys_from_string best_type_sys)
+ | NONE => type_enc_from_string best_type_enc)
|> choose_format formats
val metis_minimize_max_time = seconds 2.0
@@ -530,7 +530,7 @@
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
- ({debug, verbose, overlord, type_sys, sound, max_relevant,
+ ({debug, verbose, overlord, type_enc, sound, max_relevant,
max_mono_iters, max_new_mono_instances, isar_proof,
isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
minimize_command
@@ -598,21 +598,21 @@
|> maps (fn (name, rths) => map (pair name o snd) rths)
end
fun run_slice (slice, (time_frac, (complete,
- (best_max_relevant, best_type_sys, extra))))
+ (best_max_relevant, best_type_enc, extra))))
time_left =
let
val num_facts =
length facts |> is_none max_relevant
? Integer.min best_max_relevant
- val (format, type_sys) =
- choose_format_and_type_sys best_type_sys formats type_sys
- val fairly_sound = is_type_sys_fairly_sound type_sys
+ val (format, type_enc) =
+ choose_format_and_type_enc best_type_enc formats type_enc
+ val fairly_sound = is_type_enc_fairly_sound type_enc
val facts =
facts |> map untranslated_fact
|> not fairly_sound
? filter_out (is_dangerous_prop ctxt o prop_of o snd)
|> take num_facts
- |> polymorphism_of_type_sys type_sys <> Polymorphic
+ |> polymorphism_of_type_enc type_enc <> Polymorphic
? monomorphize_facts
|> map (apsnd prop_of)
val real_ms = Real.fromInt o Time.toMilliseconds
@@ -635,7 +635,7 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_sys sound false (Config.get ctxt atp_readable_names)
+ type_enc sound false (Config.get ctxt atp_readable_names)
true hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
@@ -675,7 +675,7 @@
used_facts_in_unsound_atp_proof ctxt
conjecture_shape facts_offset fact_names atp_proof
|> Option.map (fn facts =>
- UnsoundProof (is_type_sys_virtually_sound type_sys,
+ UnsoundProof (is_type_enc_virtually_sound type_enc,
facts |> sort string_ord))
| _ => outcome
in
--- a/src/HOL/ex/atp_export.ML Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Fri Jul 01 15:53:38 2011 +0200
@@ -149,17 +149,17 @@
if heading = factsN then (heading, order_facts ord lines) :: problem
else (heading, lines) :: order_problem_facts ord problem
-fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name =
+fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
let
val format = FOF
- val type_sys = type_sys |> type_sys_from_string
+ val type_enc = type_enc |> type_enc_from_string
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
val (atp_problem, _, _, _, _, _, _) =
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
- |> prepare_atp_problem ctxt format Axiom Axiom type_sys true true false
+ |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false
true [] @{prop False}
val atp_problem =
atp_problem