src/HOL/Metis.thy
author blanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 42349 721e85fd2db3
parent 41140 9c68004b8c9d
child 42616 92715b528e78
permissions -rw-r--r--
make 48170228f562 work also with "HO_Reas" examples
     1 (*  Title:      HOL/Metis.thy
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 *)
     6 
     7 header {* Metis Proof Method *}
     8 
     9 theory Metis
    10 imports Meson
    11 uses "~~/src/Tools/Metis/metis.ML"
    12      ("Tools/Metis/metis_translate.ML")
    13      ("Tools/Metis/metis_reconstruct.ML")
    14      ("Tools/Metis/metis_tactics.ML")
    15      ("Tools/try.ML")
    16 begin
    17 
    18 
    19 subsection {* Higher-order reasoning helpers *}
    20 
    21 definition fFalse :: bool where [no_atp]:
    22 "fFalse \<longleftrightarrow> False"
    23 
    24 definition fTrue :: bool where [no_atp]:
    25 "fTrue \<longleftrightarrow> True"
    26 
    27 definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
    28 "fNot P \<longleftrightarrow> \<not> P"
    29 
    30 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    31 "fconj P Q \<longleftrightarrow> P \<and> Q"
    32 
    33 definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    34 "fdisj P Q \<longleftrightarrow> P \<or> Q"
    35 
    36 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    37 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    38 
    39 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    40 "fequal x y \<longleftrightarrow> (x = y)"
    41 
    42 
    43 subsection {* Literal selection helpers *}
    44 
    45 definition select :: "'a \<Rightarrow> 'a" where
    46 [no_atp]: "select = (\<lambda>x. x)"
    47 
    48 lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
    49 by (cut_tac atomize_not [of "\<not> A"]) simp
    50 
    51 lemma atomize_not_select: "(A \<Longrightarrow> select False) \<equiv> Trueprop (\<not> A)"
    52 unfolding select_def by (rule atomize_not)
    53 
    54 lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A"
    55 unfolding select_def by (rule not_atomize)
    56 
    57 lemma select_FalseI: "False \<Longrightarrow> select False" by simp
    58 
    59 
    60 subsection {* Metis package *}
    61 
    62 use "Tools/Metis/metis_translate.ML"
    63 use "Tools/Metis/metis_reconstruct.ML"
    64 use "Tools/Metis/metis_tactics.ML"
    65 
    66 setup {*
    67   Metis_Reconstruct.setup
    68   #> Metis_Tactics.setup
    69 *}
    70 
    71 hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
    72 hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    73     fequal_def select_def not_atomize atomize_not_select not_atomize_select
    74     select_FalseI
    75 
    76 subsection {* Try *}
    77 
    78 use "Tools/try.ML"
    79 
    80 setup {* Try.setup *}
    81 
    82 end