author  wenzelm 
Thu, 04 Oct 2001 15:28:26 +0200  
changeset 11678  6aa3e2d26683 
parent 11096  bedfd42db838 
child 11771  b7b100a2de1d 
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 

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

8 
theory FOL = IFOL 
9487  9 
files 
10 
("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") 

11 
("simpdata.ML") ("FOL_lemmas2.ML"): 

12 

13 

14 
subsection {* The classical axiom *} 

4093  15 

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

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

17 
classical: "(~P ==> P) ==> P" 
4093  18 

9487  19 

11678  20 
subsection {* Lemmas and proof tools *} 
9487  21 

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

22 
use "FOL_lemmas1.ML" 
11678  23 
theorems case_split = case_split_thm [case_names True False] 
9525  24 

10383  25 
use "cladata.ML" 
26 
setup Cla.setup 

27 
setup clasetup 

28 

9487  29 
use "blastdata.ML" 
30 
setup Blast.setup 

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

31 
use "FOL_lemmas2.ML" 
9487  32 

33 
use "simpdata.ML" 

34 
setup simpsetup 

35 
setup "Simplifier.method_setup Splitter.split_modifiers" 

36 
setup Splitter.setup 

37 
setup Clasimp.setup 

9885  38 
setup Rulify.setup 
9487  39 

40 

11678  41 

42 
subsection {* Proof by cases and induction *} 

43 

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

45 

46 
constdefs 

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

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

49 
induct_implies :: "o => o => o" 

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

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

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

53 

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

55 
by (simp only: atomize_all induct_forall_def) 

56 

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

58 
by (simp only: atomize_imp induct_implies_def) 

59 

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

61 
by (simp only: atomize_eq induct_equal_def) 

62 

63 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq 

64 
lemmas induct_rulify1 = induct_atomize [symmetric, standard] 

65 
lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def 

66 

67 
hide const induct_forall induct_implies induct_equal 

68 

69 

70 
text {* Method setup. *} 

71 

72 
ML {* 

73 
structure InductMethod = InductMethodFun 

74 
(struct 

75 
val dest_concls = FOLogic.dest_concls; 

76 
val cases_default = thm "case_split"; 

77 
val conjI = thm "conjI"; 

78 
val atomize = thms "induct_atomize"; 

79 
val rulify1 = thms "induct_rulify1"; 

80 
val rulify2 = thms "induct_rulify2"; 

81 
end); 

82 
*} 

83 

84 
setup InductMethod.setup 

85 

86 

9487  87 
subsection {* Calculational rules *} 
88 

89 
lemma forw_subst: "a = b ==> P(b) ==> P(a)" 

90 
by (rule ssubst) 

91 

92 
lemma back_subst: "P(a) ==> a = b ==> P(b)" 

93 
by (rule subst) 

94 

95 
text {* 

96 
Note that this list of rules is in reverse order of priorities. 

97 
*} 

98 

99 
lemmas trans_rules [trans] = 

100 
forw_subst 

101 
back_subst 

102 
rev_mp 

103 
mp 

11096  104 
transitive 
9487  105 
trans 
106 

107 
lemmas [elim?] = sym 

4093  108 

4854  109 
end 