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