--- a/src/HOL/Metis.thy Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Metis.thy Thu Apr 14 11:24:05 2011 +0200
@@ -15,6 +15,9 @@
("Tools/try.ML")
begin
+
+subsection {* Higher-order reasoning helpers *}
+
definition fFalse :: bool where [no_atp]:
"fFalse \<longleftrightarrow> False"
@@ -36,6 +39,26 @@
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
"fequal x y \<longleftrightarrow> (x = y)"
+
+subsection {* Literal selection helpers *}
+
+definition select :: "'a \<Rightarrow> 'a" where
+[no_atp]: "select = (\<lambda>x. x)"
+
+lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
+by (cut_tac atomize_not [of "\<not> A"]) simp
+
+lemma atomize_not_select: "(A \<Longrightarrow> select False) \<equiv> Trueprop (\<not> A)"
+unfolding select_def by (rule atomize_not)
+
+lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A"
+unfolding select_def by (rule not_atomize)
+
+lemma select_FalseI: "False \<Longrightarrow> select False" by simp
+
+
+subsection {* Metis package *}
+
use "Tools/Metis/metis_translate.ML"
use "Tools/Metis/metis_reconstruct.ML"
use "Tools/Metis/metis_tactics.ML"
@@ -45,9 +68,10 @@
#> Metis_Tactics.setup
*}
-hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal
+hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
- fequal_def
+ fequal_def select_def not_atomize atomize_not_select not_atomize_select
+ select_FalseI
subsection {* Try *}