src/FOLP/FOLP.thy
 author blanchet Mon May 19 23:43:53 2014 +0200 (2014-05-19) changeset 57009 8cb6a5f1ae84 parent 48891 c0eafbd55de3 child 58889 5b7a9633cfa8 permissions -rw-r--r--
1 (*  Title:      FOLP/FOLP.thy
2     Author:     Martin D Coen, Cambridge University Computer Laboratory
3     Copyright   1992  University of Cambridge
4 *)
6 header {* Classical First-Order Logic with Proofs *}
8 theory FOLP
9 imports IFOLP
10 begin
12 axiomatization cla :: "[p=>p]=>p"
13   where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
16 (*** Classical introduction rules for | and EX ***)
18 schematic_lemma disjCI:
19   assumes "!!x. x:~Q ==> f(x):P"
20   shows "?p : P|Q"
21   apply (rule classical)
22   apply (assumption | rule assms disjI1 notI)+
23   apply (assumption | rule disjI2 notE)+
24   done
26 (*introduction rule involving only EX*)
27 schematic_lemma ex_classical:
28   assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
29   shows "?p : EX x. P(x)"
30   apply (rule classical)
31   apply (rule exI, rule assms, assumption)
32   done
34 (*version of above, simplifying ~EX to ALL~ *)
35 schematic_lemma exCI:
36   assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
37   shows "?p : EX x. P(x)"
38   apply (rule ex_classical)
39   apply (rule notI [THEN allI, THEN assms])
40   apply (erule notE)
41   apply (erule exI)
42   done
44 schematic_lemma excluded_middle: "?p : ~P | P"
45   apply (rule disjCI)
46   apply assumption
47   done
50 (*** Special elimination rules *)
52 (*Classical implies (-->) elimination. *)
53 schematic_lemma impCE:
54   assumes major: "p:P-->Q"
55     and r1: "!!x. x:~P ==> f(x):R"
56     and r2: "!!y. y:Q ==> g(y):R"
57   shows "?p : R"
58   apply (rule excluded_middle [THEN disjE])
59    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
60        resolve_tac [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})
61   done
63 (*Double negation law*)
64 schematic_lemma notnotD: "p:~~P ==> ?p : P"
65   apply (rule classical)
66   apply (erule notE)
67   apply assumption
68   done
71 (*** Tactics for implication and contradiction ***)
73 (*Classical <-> elimination.  Proof substitutes P=Q in
74     ~P ==> ~Q    and    P ==> Q  *)
75 schematic_lemma iffCE:
76   assumes major: "p:P<->Q"
77     and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
78     and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
79   shows "?p : R"
80   apply (insert major)
81   apply (unfold iff_def)
82   apply (rule conjE)
83   apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE
84       eresolve_tac [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE
85       resolve_tac [@{thm r1}, @{thm r2}] 1) *})+
86   done
89 (*Should be used as swap since ~P becomes redundant*)
90 schematic_lemma swap:
91   assumes major: "p:~P"
92     and r: "!!x. x:~Q ==> f(x):P"
93   shows "?p : Q"
94   apply (rule classical)
95   apply (rule major [THEN notE])
96   apply (rule r)
97   apply assumption
98   done
100 ML_file "classical.ML"      (* Patched because matching won't instantiate proof *)
101 ML_file "simp.ML"           (* Patched because matching won't instantiate proof *)
103 ML {*
104 structure Cla = Classical
105 (
106   val sizef = size_of_thm
107   val mp = @{thm mp}
108   val not_elim = @{thm notE}
109   val swap = @{thm swap}
110   val hyp_subst_tacs = [hyp_subst_tac]
111 );
112 open Cla;
114 (*Propositional rules
115   -- iffCE might seem better, but in the examples in ex/cla
116      run about 7% slower than with iffE*)
117 val prop_cs =
118   empty_cs addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI},
119       @{thm impI}, @{thm notI}, @{thm iffI}]
120     addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffE}];
122 (*Quantifier rules*)
123 val FOLP_cs =