make 48170228f562 work also with "HO_Reas" examples
authorblanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 42349721e85fd2db3
parent 42348 187354e22c7d
child 42350 128dc0fa87fc
make 48170228f562 work also with "HO_Reas" examples
src/HOL/Metis.thy
src/HOL/Tools/Metis/metis_reconstruct.ML
     1.1 --- a/src/HOL/Metis.thy	Thu Apr 14 11:24:05 2011 +0200
     1.2 +++ b/src/HOL/Metis.thy	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4       ("Tools/try.ML")
     1.5  begin
     1.6  
     1.7 +
     1.8 +subsection {* Higher-order reasoning helpers *}
     1.9 +
    1.10  definition fFalse :: bool where [no_atp]:
    1.11  "fFalse \<longleftrightarrow> False"
    1.12  
    1.13 @@ -36,6 +39,26 @@
    1.14  definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.15  "fequal x y \<longleftrightarrow> (x = y)"
    1.16  
    1.17 +
    1.18 +subsection {* Literal selection helpers *}
    1.19 +
    1.20 +definition select :: "'a \<Rightarrow> 'a" where
    1.21 +[no_atp]: "select = (\<lambda>x. x)"
    1.22 +
    1.23 +lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
    1.24 +by (cut_tac atomize_not [of "\<not> A"]) simp
    1.25 +
    1.26 +lemma atomize_not_select: "(A \<Longrightarrow> select False) \<equiv> Trueprop (\<not> A)"
    1.27 +unfolding select_def by (rule atomize_not)
    1.28 +
    1.29 +lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A"
    1.30 +unfolding select_def by (rule not_atomize)
    1.31 +
    1.32 +lemma select_FalseI: "False \<Longrightarrow> select False" by simp
    1.33 +
    1.34 +
    1.35 +subsection {* Metis package *}
    1.36 +
    1.37  use "Tools/Metis/metis_translate.ML"
    1.38  use "Tools/Metis/metis_reconstruct.ML"
    1.39  use "Tools/Metis/metis_tactics.ML"
    1.40 @@ -45,9 +68,10 @@
    1.41    #> Metis_Tactics.setup
    1.42  *}
    1.43  
    1.44 -hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal
    1.45 +hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
    1.46  hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    1.47 -                 fequal_def
    1.48 +    fequal_def select_def not_atomize atomize_not_select not_atomize_select
    1.49 +    select_FalseI
    1.50  
    1.51  subsection {* Try *}
    1.52  
     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     2.3 @@ -378,15 +378,18 @@
     2.4        else raise THM("select_literal", i, [th])
     2.5    end;
     2.6  
     2.7 -val neg_neg_imp = @{lemma "~ ~ Q ==> Q" by blast}
     2.8 -
     2.9 -val not_atomize =
    2.10 -  @{lemma "(~ A ==> False) == Trueprop A"
    2.11 -    by (cut_tac atomize_not [of "~ A"]) simp}
    2.12 -
    2.13  (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
    2.14 -   to create double negations. *)
    2.15 -val negate_head = fold (rewrite_rule o single) [not_atomize, atomize_not]
    2.16 +   to create double negations. The "select" wrapper is a trick to ensure that
    2.17 +   "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
    2.18 +   don't use this trick in general because it makes the proof object uglier than
    2.19 +   necessary. FIXME. *)
    2.20 +fun negate_head th =
    2.21 +  if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
    2.22 +    (th RS @{thm select_FalseI})
    2.23 +    |> fold (rewrite_rule o single)
    2.24 +            @{thms not_atomize_select atomize_not_select}
    2.25 +  else
    2.26 +    th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
    2.27  
    2.28  (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
    2.29  val select_literal = negate_head oo make_last