src/HOL/ATP.thy
author steckerm
Sat, 20 Sep 2014 10:44:24 +0200
changeset 58407 111d801b5d5d
parent 58406 539cc471186f
child 58889 5b7a9633cfa8
permissions -rw-r--r--
Changed proof method to auto for custom Waldmeister lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/ATP.thy
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     4
*)
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     5
39958
88c9aa5666de tuned comments
blanchet
parents: 39951
diff changeset
     6
header {* Automatic Theorem Provers (ATPs) *}
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     7
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
     8
theory ATP
57714
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
     9
imports Meson
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
    10
begin
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
    11
57263
2b6a96cc64c9 simplified code
blanchet
parents: 57262
diff changeset
    12
subsection {* ATP problems and proofs *}
2b6a96cc64c9 simplified code
blanchet
parents: 57262
diff changeset
    13
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    14
ML_file "Tools/ATP/atp_util.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    15
ML_file "Tools/ATP/atp_problem.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    16
ML_file "Tools/ATP/atp_proof.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    17
ML_file "Tools/ATP/atp_proof_redirect.ML"
57707
0242e9578828 imported patch satallax_proof_support_Sledgehammer
fleury
parents: 57263
diff changeset
    18
ML_file "Tools/ATP/atp_satallax.ML"
0242e9578828 imported patch satallax_proof_support_Sledgehammer
fleury
parents: 57263
diff changeset
    19
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    20
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    21
subsection {* Higher-order reasoning helpers *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    22
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    23
definition fFalse :: bool where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    24
"fFalse \<longleftrightarrow> False"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    25
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    26
definition fTrue :: bool where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    27
"fTrue \<longleftrightarrow> True"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    28
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    29
definition fNot :: "bool \<Rightarrow> bool" where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    30
"fNot P \<longleftrightarrow> \<not> P"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    31
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    32
definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    33
"fComp P = (\<lambda>x. \<not> P x)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    34
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    35
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    36
"fconj P Q \<longleftrightarrow> P \<and> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    37
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    38
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    39
"fdisj P Q \<longleftrightarrow> P \<or> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    40
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    41
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    42
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    43
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    44
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    45
"fAll P \<longleftrightarrow> All P"
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    46
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    47
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    48
"fEx P \<longleftrightarrow> Ex P"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    49
56946
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    50
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    51
"fequal x y \<longleftrightarrow> (x = y)"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    52
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    53
lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    54
unfolding fFalse_def fTrue_def by simp
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    55
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    56
lemma fNot_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    57
"fNot fFalse = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    58
"fNot fTrue = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    59
unfolding fFalse_def fTrue_def fNot_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    60
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    61
lemma fconj_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    62
"fconj fFalse P = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    63
"fconj P fFalse = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    64
"fconj fTrue fTrue = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    65
unfolding fFalse_def fTrue_def fconj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    66
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    67
lemma fdisj_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    68
"fdisj fTrue P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    69
"fdisj P fTrue = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    70
"fdisj fFalse fFalse = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    71
unfolding fFalse_def fTrue_def fdisj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    72
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    73
lemma fimplies_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    74
"fimplies P fTrue = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    75
"fimplies fFalse P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    76
"fimplies fTrue fFalse = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    77
unfolding fFalse_def fTrue_def fimplies_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    78
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    79
lemma fAll_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    80
"Ex (fComp P) \<or> fAll P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    81
"All P \<or> fAll P = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    82
unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    83
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    84
lemma fEx_table:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    85
"All (fComp P) \<or> fEx P = fTrue"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    86
"Ex P \<or> fEx P = fFalse"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    87
unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    88
56946
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    89
lemma fequal_table:
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    90
"fequal x x = fTrue"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    91
"x = y \<or> fequal x y = fFalse"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    92
unfolding fFalse_def fTrue_def fequal_def by auto
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    93
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    94
lemma fNot_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    95
"fNot P \<noteq> P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    96
unfolding fNot_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    97
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    98
lemma fComp_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
    99
"fComp P x \<longleftrightarrow> \<not> P x"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   100
unfolding fComp_def ..
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   101
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   102
lemma fconj_laws:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   103
"fconj P P \<longleftrightarrow> P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   104
"fconj P Q \<longleftrightarrow> fconj Q P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   105
"fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   106
unfolding fNot_def fconj_def fdisj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   107
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   108
lemma fdisj_laws:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   109
"fdisj P P \<longleftrightarrow> P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   110
"fdisj P Q \<longleftrightarrow> fdisj Q P"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   111
"fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   112
unfolding fNot_def fconj_def fdisj_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   113
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   114
lemma fimplies_laws:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   115
"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   116
"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   117
unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   118
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   119
lemma fAll_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   120
"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   121
unfolding fNot_def fComp_def fAll_def fEx_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   122
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   123
lemma fEx_law:
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   124
"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   125
unfolding fNot_def fComp_def fAll_def fEx_def by auto
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 46320
diff changeset
   126
56946
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   127
lemma fequal_laws:
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   128
"fequal x y = fequal y x"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   129
"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   130
"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   131
unfolding fFalse_def fTrue_def fequal_def by auto
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   132
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   133
57262
b2c629647a14 moved code around
blanchet
parents: 57255
diff changeset
   134
subsection {* Waldmeister helpers *}
b2c629647a14 moved code around
blanchet
parents: 57255
diff changeset
   135
58406
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   136
(* Has all needed simplification lemmas for logic. *)
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   137
lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   138
  by simp
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   139
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   140
lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
58407
111d801b5d5d Changed proof method to auto for custom Waldmeister lemma
steckerm
parents: 58406
diff changeset
   141
  by auto
58406
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   142
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   143
lemmas waldmeister_fol = boolean_equality boolean_comm
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   144
  simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc
57262
b2c629647a14 moved code around
blanchet
parents: 57255
diff changeset
   145
b2c629647a14 moved code around
blanchet
parents: 57255
diff changeset
   146
57263
2b6a96cc64c9 simplified code
blanchet
parents: 57262
diff changeset
   147
subsection {* Basic connection between ATPs and HOL *}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   148
57263
2b6a96cc64c9 simplified code
blanchet
parents: 57262
diff changeset
   149
ML_file "Tools/lambda_lifting.ML"
2b6a96cc64c9 simplified code
blanchet
parents: 57262
diff changeset
   150
ML_file "Tools/monomorph.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   151
ML_file "Tools/ATP/atp_problem_generate.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   152
ML_file "Tools/ATP/atp_proof_reconstruct.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   153
ML_file "Tools/ATP/atp_systems.ML"
57262
b2c629647a14 moved code around
blanchet
parents: 57255
diff changeset
   154
ML_file "Tools/ATP/atp_waldmeister.ML"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   155
58406
539cc471186f Minor fixes in ATP_Waldmeister
steckerm
parents: 58142
diff changeset
   156
hide_fact (open) waldmeister_fol boolean_equality boolean_comm
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   157
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   158
end