# HG changeset patch
# User blanchet
# Date 1305889173 -7200
# Node ID 412fe70f41a4b221cc595c2b00f25adbf5301f5f
# Parent  4da581400b6982ab4dafb93b20b37f253ec52b40
exercise more type systems (but only sound or quasi-sound ones)

diff -r 4da581400b69 -r 412fe70f41a4 src/HOL/Metis_Examples/HO_Reas.thy
--- a/src/HOL/Metis_Examples/HO_Reas.thy	Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Fri May 20 12:59:33 2011 +0200
@@ -56,50 +56,60 @@
 
 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis id_apply)
@@ -107,120 +117,144 @@
 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_tags, expect = some] ()
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] ()
-sledgehammer [type_sys = mangled_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] ()
 by metisFT
 
 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis 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_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_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)
 by (metis id_apply)