# HG changeset patch
# User blanchet
# Date 1304544071 -7200
# Node ID 7206f5688cade5fa183f647261e761ac1c3bc0d6
# Parent  7a5116bd63b75ed4a566a9ac04c0ed9f744f2618
compile + added monotonicity tests

diff -r 7a5116bd63b7 -r 7206f5688cad src/HOL/Metis_Examples/HO_Reas.thy
--- a/src/HOL/Metis_Examples/HO_Reas.thy	Wed May 04 23:18:28 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Wed May 04 23:21:11 2011 +0200
@@ -15,161 +15,209 @@
 lemma "id True"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 "P True \<Longrightarrow> P False \<Longrightarrow> P x"
 sledgehammer [type_sys = erased, expect = none] ()
-sledgehammer [type_sys = const_args, expect = none] ()
+sledgehammer [type_sys = args, expect = none] ()
 sledgehammer [type_sys = tags!, expect = some] ()
+sledgehammer [type_sys = tags?, expect = some] ()
 sledgehammer [type_sys = tags, expect = some] ()
 sledgehammer [type_sys = preds!, expect = some] ()
+sledgehammer [type_sys = preds?, expect = some] ()
 sledgehammer [type_sys = preds, expect = some] ()
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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 = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
 sledgehammer [type_sys = tags, expect = some] (id_apply)
 sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
 sledgehammer [type_sys = preds, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds!, 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)