src/HOL/ATP.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58142 d6a2e3567f95
child 58406 539cc471186f
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (*  Title:      HOL/ATP.thy
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 *)
     5 
     6 header {* Automatic Theorem Provers (ATPs) *}
     7 
     8 theory ATP
     9 imports Meson
    10 begin
    11 
    12 subsection {* ATP problems and proofs *}
    13 
    14 ML_file "Tools/ATP/atp_util.ML"
    15 ML_file "Tools/ATP/atp_problem.ML"
    16 ML_file "Tools/ATP/atp_proof.ML"
    17 ML_file "Tools/ATP/atp_proof_redirect.ML"
    18 ML_file "Tools/ATP/atp_satallax.ML"
    19 
    20 
    21 subsection {* Higher-order reasoning helpers *}
    22 
    23 definition fFalse :: bool where
    24 "fFalse \<longleftrightarrow> False"
    25 
    26 definition fTrue :: bool where
    27 "fTrue \<longleftrightarrow> True"
    28 
    29 definition fNot :: "bool \<Rightarrow> bool" where
    30 "fNot P \<longleftrightarrow> \<not> P"
    31 
    32 definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
    33 "fComp P = (\<lambda>x. \<not> P x)"
    34 
    35 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    36 "fconj P Q \<longleftrightarrow> P \<and> Q"
    37 
    38 definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    39 "fdisj P Q \<longleftrightarrow> P \<or> Q"
    40 
    41 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    42 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    43 
    44 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    45 "fAll P \<longleftrightarrow> All P"
    46 
    47 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    48 "fEx P \<longleftrightarrow> Ex P"
    49 
    50 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    51 "fequal x y \<longleftrightarrow> (x = y)"
    52 
    53 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
    54 unfolding fFalse_def fTrue_def by simp
    55 
    56 lemma fNot_table:
    57 "fNot fFalse = fTrue"
    58 "fNot fTrue = fFalse"
    59 unfolding fFalse_def fTrue_def fNot_def by auto
    60 
    61 lemma fconj_table:
    62 "fconj fFalse P = fFalse"
    63 "fconj P fFalse = fFalse"
    64 "fconj fTrue fTrue = fTrue"
    65 unfolding fFalse_def fTrue_def fconj_def by auto
    66 
    67 lemma fdisj_table:
    68 "fdisj fTrue P = fTrue"
    69 "fdisj P fTrue = fTrue"
    70 "fdisj fFalse fFalse = fFalse"
    71 unfolding fFalse_def fTrue_def fdisj_def by auto
    72 
    73 lemma fimplies_table:
    74 "fimplies P fTrue = fTrue"
    75 "fimplies fFalse P = fTrue"
    76 "fimplies fTrue fFalse = fFalse"
    77 unfolding fFalse_def fTrue_def fimplies_def by auto
    78 
    79 lemma fAll_table:
    80 "Ex (fComp P) \<or> fAll P = fTrue"
    81 "All P \<or> fAll P = fFalse"
    82 unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
    83 
    84 lemma fEx_table:
    85 "All (fComp P) \<or> fEx P = fTrue"
    86 "Ex P \<or> fEx P = fFalse"
    87 unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
    88 
    89 lemma fequal_table:
    90 "fequal x x = fTrue"
    91 "x = y \<or> fequal x y = fFalse"
    92 unfolding fFalse_def fTrue_def fequal_def by auto
    93 
    94 lemma fNot_law:
    95 "fNot P \<noteq> P"
    96 unfolding fNot_def by auto
    97 
    98 lemma fComp_law:
    99 "fComp P x \<longleftrightarrow> \<not> P x"
   100 unfolding fComp_def ..
   101 
   102 lemma fconj_laws:
   103 "fconj P P \<longleftrightarrow> P"
   104 "fconj P Q \<longleftrightarrow> fconj Q P"
   105 "fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
   106 unfolding fNot_def fconj_def fdisj_def by auto
   107 
   108 lemma fdisj_laws:
   109 "fdisj P P \<longleftrightarrow> P"
   110 "fdisj P Q \<longleftrightarrow> fdisj Q P"
   111 "fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
   112 unfolding fNot_def fconj_def fdisj_def by auto
   113 
   114 lemma fimplies_laws:
   115 "fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
   116 "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
   117 unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
   118 
   119 lemma fAll_law:
   120 "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
   121 unfolding fNot_def fComp_def fAll_def fEx_def by auto
   122 
   123 lemma fEx_law:
   124 "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
   125 unfolding fNot_def fComp_def fAll_def fEx_def by auto
   126 
   127 lemma fequal_laws:
   128 "fequal x y = fequal y x"
   129 "fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
   130 "fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
   131 unfolding fFalse_def fTrue_def fequal_def by auto
   132 
   133 
   134 subsection {* Waldmeister helpers *}
   135 
   136 (* Has all needed simplification lemmas for logic.
   137    "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
   138 lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
   139   eq_ac disj_comms disj_assoc conj_comms conj_assoc
   140 
   141 
   142 subsection {* Basic connection between ATPs and HOL *}
   143 
   144 ML_file "Tools/lambda_lifting.ML"
   145 ML_file "Tools/monomorph.ML"
   146 ML_file "Tools/ATP/atp_problem_generate.ML"
   147 ML_file "Tools/ATP/atp_proof_reconstruct.ML"
   148 ML_file "Tools/ATP/atp_systems.ML"
   149 ML_file "Tools/ATP/atp_waldmeister.ML"
   150 
   151 hide_fact (open) waldmeister_fol
   152 
   153 end