# HG changeset patch
# User blanchet
# Date 1302773045 -7200
# Node ID 721e85fd2db3aa4246139299d5cc17e67ea31705
# Parent  187354e22c7d69d13784269e2f75868f6fd3e61e
make 48170228f562 work also with "HO_Reas" examples

diff -r 187354e22c7d -r 721e85fd2db3 src/HOL/Metis.thy
--- 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 *}
 
diff -r 187354e22c7d -r 721e85fd2db3 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
@@ -378,15 +378,18 @@
       else raise THM("select_literal", i, [th])
   end;
 
-val neg_neg_imp = @{lemma "~ ~ Q ==> Q" by blast}
-
-val not_atomize =
-  @{lemma "(~ A ==> False) == Trueprop A"
-    by (cut_tac atomize_not [of "~ A"]) simp}
-
 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
-   to create double negations. *)
-val negate_head = fold (rewrite_rule o single) [not_atomize, atomize_not]
+   to create double negations. The "select" wrapper is a trick to ensure that
+   "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
+   don't use this trick in general because it makes the proof object uglier than
+   necessary. FIXME. *)
+fun negate_head th =
+  if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
+    (th RS @{thm select_FalseI})
+    |> fold (rewrite_rule o single)
+            @{thms not_atomize_select atomize_not_select}
+  else
+    th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
 
 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
 val select_literal = negate_head oo make_last