src/HOL/ATP.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 60758 d8d85a8172b5 child 66364 fa3247e6ee4b permissions -rw-r--r--
generalize more theorems to support enat and ennreal
```     1 (*  Title:      HOL/ATP.thy
```
```     2     Author:     Fabian Immler, TU Muenchen
```
```     3     Author:     Jasmin Blanchette, TU Muenchen
```
```     4 *)
```
```     5
```
```     6 section \<open>Automatic Theorem Provers (ATPs)\<close>
```
```     7
```
```     8 theory ATP
```
```     9 imports Meson
```
```    10 begin
```
```    11
```
```    12 subsection \<open>ATP problems and proofs\<close>
```
```    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 \<open>Higher-order reasoning helpers\<close>
```
```    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 \<open>Waldmeister helpers\<close>
```
```   135
```
```   136 (* Has all needed simplification lemmas for logic. *)
```
```   137 lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
```
```   138   by simp
```
```   139
```
```   140 lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
```
```   141   by auto
```
```   142
```
```   143 lemmas waldmeister_fol = boolean_equality boolean_comm
```
```   144   simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc
```
```   145
```
```   146
```
```   147 subsection \<open>Basic connection between ATPs and HOL\<close>
```
```   148
```
```   149 ML_file "Tools/lambda_lifting.ML"
```
```   150 ML_file "Tools/monomorph.ML"
```
```   151 ML_file "Tools/ATP/atp_problem_generate.ML"
```
```   152 ML_file "Tools/ATP/atp_proof_reconstruct.ML"
```
```   153 ML_file "Tools/ATP/atp_systems.ML"
```
```   154 ML_file "Tools/ATP/atp_waldmeister.ML"
```
```   155
```
```   156 hide_fact (open) waldmeister_fol boolean_equality boolean_comm
```
```   157
```
```   158 end
```