src/HOL/ATP.thy
author blanchet
Tue, 13 May 2014 11:10:23 +0200
changeset 56946 10d9bd4ea94f
parent 54148 c8cc5ab4a863
child 57255 488046fdda59
permissions -rw-r--r--
hide more internal names
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
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
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
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    12
ML_file "Tools/lambda_lifting.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    13
ML_file "Tools/monomorph.ML"
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"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
    18
56946
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    19
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    20
subsection {* Higher-order reasoning helpers *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    21
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    22
definition fFalse :: bool where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    23
"fFalse \<longleftrightarrow> False"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    24
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    25
definition fTrue :: bool where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    26
"fTrue \<longleftrightarrow> True"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    27
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    28
definition fNot :: "bool \<Rightarrow> bool" where
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    29
"fNot P \<longleftrightarrow> \<not> P"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    30
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    31
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
    32
"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
    33
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    34
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
    35
"fconj P Q \<longleftrightarrow> P \<and> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    36
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    37
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
    38
"fdisj P Q \<longleftrightarrow> P \<or> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    39
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    40
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
    41
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    42
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    43
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    44
"fAll P \<longleftrightarrow> All P"
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    45
54148
c8cc5ab4a863 killed more "no_atp"s
blanchet
parents: 53479
diff changeset
    46
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43108
diff changeset
    47
"fEx P \<longleftrightarrow> Ex P"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
    48
56946
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    49
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    50
"fequal x y \<longleftrightarrow> (x = y)"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    51
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
    52
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
    53
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
    54
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
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
    56
"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
    57
"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
    58
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
    59
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
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
    61
"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
    62
"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
    63
"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
    64
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
    65
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
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
    67
"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
    68
"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
    69
"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
    70
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
    71
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
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
    73
"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
    74
"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
    75
"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
    76
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
    77
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
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
    79
"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
    80
"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
    81
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
    82
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
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
    84
"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
    85
"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
    86
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
    87
56946
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    88
lemma fequal_table:
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    89
"fequal x x = fTrue"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    90
"x = y \<or> fequal x y = fFalse"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    91
unfolding fFalse_def fTrue_def fequal_def by auto
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
    92
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
    93
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
    94
"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
    95
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
    96
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
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
    98
"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
    99
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
   100
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
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
   102
"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
   103
"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
   104
"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
   105
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
   106
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
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
   108
"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
   109
"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
   110
"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
   111
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
   112
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
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
   114
"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
   115
"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
   116
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
   117
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
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
   119
"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
   120
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
   121
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
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
   123
"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
   124
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
   125
56946
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   126
lemma fequal_laws:
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   127
"fequal x y = fequal y x"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   128
"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   129
"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   130
unfolding fFalse_def fTrue_def fequal_def by auto
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   131
10d9bd4ea94f hide more internal names
blanchet
parents: 54148
diff changeset
   132
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   133
subsection {* Setup *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   134
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   135
ML_file "Tools/ATP/atp_problem_generate.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   136
ML_file "Tools/ATP/atp_proof_reconstruct.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47946
diff changeset
   137
ML_file "Tools/ATP/atp_systems.ML"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 40178
diff changeset
   138
39951
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   139
setup ATP_Systems.setup
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   140
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff changeset
   141
end