author  wenzelm 
Fri, 30 Dec 2005 16:56:56 +0100  
changeset 18522  9bdfb6eaf8ab 
parent 18511  beed2bc052a3 
child 18531  ce7b80b7c84e 
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 

18456  8 
theory FOL 
15481  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") 

18456  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 

18522  27 
lemma cla_dist_concl: 
28 
assumes x: "~Z_Z ==> PROP X_X" 

29 
and z: "PROP Y_Y ==> Z_Z" 

30 
and y: "PROP X_X ==> PROP Y_Y" 

31 
shows Z_Z 

32 
apply (rule classical) 

33 
apply (erule x [THEN y, THEN z]) 

34 
done 

35 

10383  36 
use "cladata.ML" 
37 
setup Cla.setup 

14156  38 
setup cla_setup 
39 
setup case_setup 

10383  40 

9487  41 
use "blastdata.ML" 
42 
setup Blast.setup 

13550  43 

44 

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

46 
by blast 

47 

48 
ML {* 

49 
val ex1_functional = thm "ex1_functional"; 

50 
*} 

9487  51 

52 
use "simpdata.ML" 

53 
setup simpsetup 

54 
setup "Simplifier.method_setup Splitter.split_modifiers" 

55 
setup Splitter.setup 

56 
setup Clasimp.setup 

57 

15481  58 

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

60 

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

62 
use "eqrule_FOL_data.ML"; 

63 

64 
setup EQSubstTac.setup 

65 

66 

14085  67 
subsection {* Other simple lemmas *} 
68 

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

70 
by blast 

71 

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

73 
by blast 

74 

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

76 
by blast 

77 

78 
(** Monotonicity of implications **) 

79 

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

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

82 

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

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

85 

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

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

88 

89 
lemma imp_refl: "P>P" 

90 
by (rule impI, assumption) 

91 

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

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

94 
by blast 

95 

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

97 
by blast 

98 

11678  99 

100 
subsection {* Proof by cases and induction *} 

101 

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

103 

104 
constdefs 

18456  105 
induct_forall where "induct_forall(P) == \<forall>x. P(x)" 
106 
induct_implies where "induct_implies(A, B) == A \<longrightarrow> B" 

107 
induct_equal where "induct_equal(x, y) == x = y" 

108 
induct_conj where "induct_conj(A, B) == A \<and> B" 

11678  109 

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

18456  111 
by (unfold atomize_all induct_forall_def) 
11678  112 

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

18456  114 
by (unfold atomize_imp induct_implies_def) 
11678  115 

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

18456  117 
by (unfold atomize_eq induct_equal_def) 
11678  118 

18456  119 
lemma induct_conj_eq: 
120 
includes meta_conjunction_syntax 

121 
shows "(A && B) == Trueprop(induct_conj(A, B))" 

122 
by (unfold atomize_conj induct_conj_def) 

11988  123 

18456  124 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
125 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

126 
lemmas induct_rulify_fallback = 

127 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  128 

18456  129 
hide const induct_forall induct_implies induct_equal induct_conj 
11678  130 

131 

132 
text {* Method setup. *} 

133 

134 
ML {* 

135 
structure InductMethod = InductMethodFun 

136 
(struct 

137 
val cases_default = thm "case_split"; 

138 
val atomize = thms "induct_atomize"; 

18456  139 
val rulify = thms "induct_rulify"; 
140 
val rulify_fallback = thms "induct_rulify_fallback"; 

11678  141 
end); 
142 
*} 

143 

144 
setup InductMethod.setup 

145 

4854  146 
end 