author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 51575  907efc894051 
permissions  rwrr 
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  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  12 
ML_file "Tools/lambda_lifting.ML" 
13 
ML_file "Tools/monomorph.ML" 

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 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

19 
subsection {* Higherorder reasoning helpers *} 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

20 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

21 
definition fFalse :: bool where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

22 
"fFalse \<longleftrightarrow> False" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

23 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

24 
definition fTrue :: bool where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

25 
"fTrue \<longleftrightarrow> True" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

26 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

27 
definition fNot :: "bool \<Rightarrow> bool" where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

28 
"fNot P \<longleftrightarrow> \<not> P" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

29 

47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

30 
definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

31 
"fComp P = (\<lambda>x. \<not> P x)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

32 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

33 
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

34 
"fconj P Q \<longleftrightarrow> P \<and> Q" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

35 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

36 
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

37 
"fdisj P Q \<longleftrightarrow> P \<or> Q" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

38 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

39 
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

40 
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

41 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

42 
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

43 
"fequal x y \<longleftrightarrow> (x = y)" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

44 

43678  45 
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]: 
46 
"fAll P \<longleftrightarrow> All P" 

47 

48 
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]: 

49 
"fEx P \<longleftrightarrow> Ex P" 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

50 

47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

51 
lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

52 
unfolding fFalse_def fTrue_def by simp 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

53 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

54 
lemma fNot_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

55 
"fNot fFalse = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

56 
"fNot fTrue = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

57 
unfolding fFalse_def fTrue_def fNot_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

58 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

59 
lemma fconj_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

60 
"fconj fFalse P = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

61 
"fconj P fFalse = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

62 
"fconj fTrue fTrue = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

63 
unfolding fFalse_def fTrue_def fconj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

64 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

65 
lemma fdisj_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

66 
"fdisj fTrue P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

67 
"fdisj P fTrue = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

68 
"fdisj fFalse fFalse = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

69 
unfolding fFalse_def fTrue_def fdisj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

70 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

71 
lemma fimplies_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

72 
"fimplies P fTrue = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

73 
"fimplies fFalse P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

74 
"fimplies fTrue fFalse = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

75 
unfolding fFalse_def fTrue_def fimplies_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

76 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

77 
lemma fequal_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

78 
"fequal x x = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

79 
"x = y \<or> fequal x y = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

80 
unfolding fFalse_def fTrue_def fequal_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

81 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

82 
lemma fAll_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

83 
"Ex (fComp P) \<or> fAll P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

84 
"All P \<or> fAll P = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

85 
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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

86 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

87 
lemma fEx_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

88 
"All (fComp P) \<or> fEx P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

89 
"Ex P \<or> fEx P = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

90 
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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

91 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

92 
lemma fNot_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

93 
"fNot P \<noteq> P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

94 
unfolding fNot_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

95 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

96 
lemma fComp_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

97 
"fComp P x \<longleftrightarrow> \<not> P x" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

98 
unfolding fComp_def .. 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

99 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

100 
lemma fconj_laws: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

101 
"fconj P P \<longleftrightarrow> P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

102 
"fconj P Q \<longleftrightarrow> fconj Q P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

103 
"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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

104 
unfolding fNot_def fconj_def fdisj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

105 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

106 
lemma fdisj_laws: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

107 
"fdisj P P \<longleftrightarrow> P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

108 
"fdisj P Q \<longleftrightarrow> fdisj Q P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

109 
"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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

110 
unfolding fNot_def fconj_def fdisj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

111 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

112 
lemma fimplies_laws: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

113 
"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

114 
"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

115 
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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

116 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

117 
lemma fequal_laws: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

118 
"fequal x y = fequal y x" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

119 
"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

120 
"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

121 
unfolding fFalse_def fTrue_def fequal_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder 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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

123 
lemma fAll_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

124 
"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder 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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

126 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

127 
lemma fEx_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

128 
"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

129 
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 higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

130 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

131 
subsection {* Setup *} 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

132 

48891  133 
ML_file "Tools/ATP/atp_problem_generate.ML" 
134 
ML_file "Tools/ATP/atp_proof_reconstruct.ML" 

135 
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

136 

39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

137 
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

138 

ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

139 
end 