src/HOL/Metis.thy
changeset 42349 721e85fd2db3
parent 41140 9c68004b8c9d
child 42616 92715b528e78
     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