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