author  paulson 
Fri, 30 Aug 2002 16:42:45 +0200  
changeset 13550  5a176b8dda84 
parent 12367  1cee8a0db392 
child 14085  8dc3e532959a 
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" 
12127
219e543496a3
theorems case_split = case_split_thm [case_names True False, cases type: o];
wenzelm
parents:
11988
diff
changeset

23 
theorems case_split = case_split_thm [case_names True False, cases type: o] 
9525  24 

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

27 
setup clasetup 

28 

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

13550  31 

32 

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

34 
by blast 

35 

36 
ML {* 

37 
val ex1_functional = thm "ex1_functional"; 

38 
*} 

9487  39 

40 
use "simpdata.ML" 

41 
setup simpsetup 

42 
setup "Simplifier.method_setup Splitter.split_modifiers" 

43 
setup Splitter.setup 

44 
setup Clasimp.setup 

45 

11678  46 

47 
subsection {* Proof by cases and induction *} 

48 

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

50 

51 
constdefs 

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

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

54 
induct_implies :: "o => o => o" 

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

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

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

58 

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

60 
by (simp only: atomize_all induct_forall_def) 

61 

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

63 
by (simp only: atomize_imp induct_implies_def) 

64 

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

66 
by (simp only: atomize_eq induct_equal_def) 

67 

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

70 

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

71 
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

72 
lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq 
11678  73 
lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def 
74 

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

77 

11678  78 
hide const induct_forall induct_implies induct_equal 
79 

80 

81 
text {* Method setup. *} 

82 

83 
ML {* 

84 
structure InductMethod = InductMethodFun 

85 
(struct 

86 
val dest_concls = FOLogic.dest_concls; 

87 
val cases_default = thm "case_split"; 

11988  88 
val local_impI = thm "induct_impliesI"; 
11678  89 
val conjI = thm "conjI"; 
90 
val atomize = thms "induct_atomize"; 

91 
val rulify1 = thms "induct_rulify1"; 

92 
val rulify2 = thms "induct_rulify2"; 

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

11678  95 
end); 
96 
*} 

97 

98 
setup InductMethod.setup 

99 

4854  100 
end 