author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 15481  fc075ae929e4 
child 18456  8cc35e95450a 
permissions  rwrr 
9487  1 
(* Title: FOL/FOL.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

11678  4 
*) 
9487  5 

11678  6 
header {* Classical firstorder logic *} 
4093  7 

15481  8 
theory FOL 
9 
imports IFOL 

16417  10 
uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") 
15481  11 
("eqrule_FOL_data.ML") 
12 
("~~/src/Provers/eqsubst.ML") 

13 
begin 

9487  14 

15 

16 
subsection {* The classical axiom *} 

4093  17 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset

18 
axioms 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset

19 
classical: "(~P ==> P) ==> P" 
4093  20 

9487  21 

11678  22 
subsection {* Lemmas and proof tools *} 
9487  23 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset

24 
use "FOL_lemmas1.ML" 
12127
219e543496a3
theorems case_split = case_split_thm [case_names True False, cases type: o];
wenzelm
parents:
11988
diff
changeset

25 
theorems case_split = case_split_thm [case_names True False, cases type: o] 
9525  26 

10383  27 
use "cladata.ML" 
28 
setup Cla.setup 

14156  29 
setup cla_setup 
30 
setup case_setup 

10383  31 

9487  32 
use "blastdata.ML" 
33 
setup Blast.setup 

13550  34 

35 

36 
lemma ex1_functional: "[ EX! z. P(a,z); P(a,b); P(a,c) ] ==> b = c" 

37 
by blast 

38 

39 
ML {* 

40 
val ex1_functional = thm "ex1_functional"; 

41 
*} 

9487  42 

43 
use "simpdata.ML" 

44 
setup simpsetup 

45 
setup "Simplifier.method_setup Splitter.split_modifiers" 

46 
setup Splitter.setup 

47 
setup Clasimp.setup 

48 

15481  49 

50 
subsection {* Lucas Dixon's eqstep tactic *} 

51 

52 
use "~~/src/Provers/eqsubst.ML"; 

53 
use "eqrule_FOL_data.ML"; 

54 

55 
setup EQSubstTac.setup 

56 

57 

14085  58 
subsection {* Other simple lemmas *} 
59 

60 
lemma [simp]: "((P>R) <> (Q>R)) <> ((P<>Q)  R)" 

61 
by blast 

62 

63 
lemma [simp]: "((P>Q) <> (P>R)) <> (P > (Q<>R))" 

64 
by blast 

65 

66 
lemma not_disj_iff_imp: "~P  Q <> (P>Q)" 

67 
by blast 

68 

69 
(** Monotonicity of implications **) 

70 

71 
lemma conj_mono: "[ P1>Q1; P2>Q2 ] ==> (P1&P2) > (Q1&Q2)" 

72 
by fast (*or (IntPr.fast_tac 1)*) 

73 

74 
lemma disj_mono: "[ P1>Q1; P2>Q2 ] ==> (P1P2) > (Q1Q2)" 

75 
by fast (*or (IntPr.fast_tac 1)*) 

76 

77 
lemma imp_mono: "[ Q1>P1; P2>Q2 ] ==> (P1>P2)>(Q1>Q2)" 

78 
by fast (*or (IntPr.fast_tac 1)*) 

79 

80 
lemma imp_refl: "P>P" 

81 
by (rule impI, assumption) 

82 

83 
(*The quantifier monotonicity rules are also intuitionistically valid*) 

84 
lemma ex_mono: "(!!x. P(x) > Q(x)) ==> (EX x. P(x)) > (EX x. Q(x))" 

85 
by blast 

86 

87 
lemma all_mono: "(!!x. P(x) > Q(x)) ==> (ALL x. P(x)) > (ALL x. Q(x))" 

88 
by blast 

89 

11678  90 

91 
subsection {* Proof by cases and induction *} 

92 

93 
text {* Proper handling of nonatomic rule statements. *} 

94 

95 
constdefs 

96 
induct_forall :: "('a => o) => o" 

97 
"induct_forall(P) == \<forall>x. P(x)" 

98 
induct_implies :: "o => o => o" 

99 
"induct_implies(A, B) == A > B" 

100 
induct_equal :: "'a => 'a => o" 

101 
"induct_equal(x, y) == x = y" 

102 

103 
lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" 

104 
by (simp only: atomize_all induct_forall_def) 

105 

106 
lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" 

107 
by (simp only: atomize_imp induct_implies_def) 

108 

109 
lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" 

110 
by (simp only: atomize_eq induct_equal_def) 

111 

11988  112 
lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)" 
113 
by (simp add: induct_implies_def) 

114 

12164
0b219d9e3384
induct_atomize: include atomize_conj (for mutual induction);
wenzelm
parents:
12160
diff
changeset

115 
lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq 
0b219d9e3384
induct_atomize: include atomize_conj (for mutual induction);
wenzelm
parents:
12160
diff
changeset

116 
lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq 
11678  117 
lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def 
118 

12240  119 
lemma all_conj_eq: "(ALL x. P(x)) & (ALL y. Q(y)) == (ALL x y. P(x) & Q(y))" 
120 
by simp 

121 

11678  122 
hide const induct_forall induct_implies induct_equal 
123 

124 

125 
text {* Method setup. *} 

126 

127 
ML {* 

128 
structure InductMethod = InductMethodFun 

129 
(struct 

130 
val dest_concls = FOLogic.dest_concls; 

131 
val cases_default = thm "case_split"; 

11988  132 
val local_impI = thm "induct_impliesI"; 
11678  133 
val conjI = thm "conjI"; 
134 
val atomize = thms "induct_atomize"; 

135 
val rulify1 = thms "induct_rulify1"; 

136 
val rulify2 = thms "induct_rulify2"; 

12240  137 
val localize = [Thm.symmetric (thm "induct_implies_def"), 
138 
Thm.symmetric (thm "atomize_all"), thm "all_conj_eq"]; 

11678  139 
end); 
140 
*} 

141 

142 
setup InductMethod.setup 

143 

4854  144 
end 