src/HOL/ATP.thy
author boehmes
Thu Mar 28 23:44:41 2013 +0100 (2013-03-28)
changeset 51575 907efc894051
parent 48891 c0eafbd55de3
child 53479 f7d8224641de
permissions -rw-r--r--
new, simpler implementation of monomorphization;
old monomorphization code is still available as Legacy_Monomorphization;
modified SMT integration to use the new monomorphization code
     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 ML_file "Tools/lambda_lifting.ML"
    13 ML_file "Tools/monomorph.ML"
    14 ML_file "Tools/legacy_monomorph.ML"
    15 ML_file "Tools/ATP/atp_util.ML"
    16 ML_file "Tools/ATP/atp_problem.ML"
    17 ML_file "Tools/ATP/atp_proof.ML"
    18 ML_file "Tools/ATP/atp_proof_redirect.ML"
    19 
    20 subsection {* Higher-order reasoning helpers *}
    21 
    22 definition fFalse :: bool where [no_atp]:
    23 "fFalse \<longleftrightarrow> False"
    24 
    25 definition fTrue :: bool where [no_atp]:
    26 "fTrue \<longleftrightarrow> True"
    27 
    28 definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
    29 "fNot P \<longleftrightarrow> \<not> P"
    30 
    31 definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    32 "fComp P = (\<lambda>x. \<not> P x)"
    33 
    34 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    35 "fconj P Q \<longleftrightarrow> P \<and> Q"
    36 
    37 definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    38 "fdisj P Q \<longleftrightarrow> P \<or> Q"
    39 
    40 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    41 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    42 
    43 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    44 "fequal x y \<longleftrightarrow> (x = y)"
    45 
    46 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    47 "fAll P \<longleftrightarrow> All P"
    48 
    49 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    50 "fEx P \<longleftrightarrow> Ex P"
    51 
    52 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
    53 unfolding fFalse_def fTrue_def by simp
    54 
    55 lemma fNot_table:
    56 "fNot fFalse = fTrue"
    57 "fNot fTrue = fFalse"
    58 unfolding fFalse_def fTrue_def fNot_def by auto
    59 
    60 lemma fconj_table:
    61 "fconj fFalse P = fFalse"
    62 "fconj P fFalse = fFalse"
    63 "fconj fTrue fTrue = fTrue"
    64 unfolding fFalse_def fTrue_def fconj_def by auto
    65 
    66 lemma fdisj_table:
    67 "fdisj fTrue P = fTrue"
    68 "fdisj P fTrue = fTrue"
    69 "fdisj fFalse fFalse = fFalse"
    70 unfolding fFalse_def fTrue_def fdisj_def by auto
    71 
    72 lemma fimplies_table:
    73 "fimplies P fTrue = fTrue"
    74 "fimplies fFalse P = fTrue"
    75 "fimplies fTrue fFalse = fFalse"
    76 unfolding fFalse_def fTrue_def fimplies_def by auto
    77 
    78 lemma fequal_table:
    79 "fequal x x = fTrue"
    80 "x = y \<or> fequal x y = fFalse"
    81 unfolding fFalse_def fTrue_def fequal_def by auto
    82 
    83 lemma fAll_table:
    84 "Ex (fComp P) \<or> fAll P = fTrue"
    85 "All P \<or> fAll P = fFalse"
    86 unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
    87 
    88 lemma fEx_table:
    89 "All (fComp P) \<or> fEx P = fTrue"
    90 "Ex P \<or> fEx P = fFalse"
    91 unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
    92 
    93 lemma fNot_law:
    94 "fNot P \<noteq> P"
    95 unfolding fNot_def by auto
    96 
    97 lemma fComp_law:
    98 "fComp P x \<longleftrightarrow> \<not> P x"
    99 unfolding fComp_def ..
   100 
   101 lemma fconj_laws:
   102 "fconj P P \<longleftrightarrow> P"
   103 "fconj P Q \<longleftrightarrow> fconj Q P"
   104 "fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
   105 unfolding fNot_def fconj_def fdisj_def by auto
   106 
   107 lemma fdisj_laws:
   108 "fdisj P P \<longleftrightarrow> P"
   109 "fdisj P Q \<longleftrightarrow> fdisj Q P"
   110 "fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
   111 unfolding fNot_def fconj_def fdisj_def by auto
   112 
   113 lemma fimplies_laws:
   114 "fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
   115 "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
   116 unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
   117 
   118 lemma fequal_laws:
   119 "fequal x y = fequal y x"
   120 "fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
   121 "fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
   122 unfolding fFalse_def fTrue_def fequal_def by auto
   123 
   124 lemma fAll_law:
   125 "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
   126 unfolding fNot_def fComp_def fAll_def fEx_def by auto
   127 
   128 lemma fEx_law:
   129 "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
   130 unfolding fNot_def fComp_def fAll_def fEx_def by auto
   131 
   132 subsection {* Setup *}
   133 
   134 ML_file "Tools/ATP/atp_problem_generate.ML"
   135 ML_file "Tools/ATP/atp_proof_reconstruct.ML"
   136 ML_file "Tools/ATP/atp_systems.ML"
   137 
   138 setup ATP_Systems.setup
   139 
   140 end