(* Title: FOLP/FOLP.thy Author: Martin D Coen, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) header {* Classical First-Order Logic with Proofs *} theory FOLP imports IFOLP begin axiomatization cla :: "[p=>p]=>p" where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P" (*** Classical introduction rules for | and EX ***) schematic_lemma disjCI: assumes "!!x. x:~Q ==> f(x):P" shows "?p : P|Q" apply (rule classical) apply (assumption | rule assms disjI1 notI)+ apply (assumption | rule disjI2 notE)+ done (*introduction rule involving only EX*) schematic_lemma ex_classical: assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)" shows "?p : EX x. P(x)" apply (rule classical) apply (rule exI, rule assms, assumption) done (*version of above, simplifying ~EX to ALL~ *) schematic_lemma exCI: assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)" shows "?p : EX x. P(x)" apply (rule ex_classical) apply (rule notI [THEN allI, THEN assms]) apply (erule notE) apply (erule exI) done schematic_lemma excluded_middle: "?p : ~P | P" apply (rule disjCI) apply assumption done (*** Special elimination rules *) (*Classical implies (-->) elimination. *) schematic_lemma impCE: assumes major: "p:P-->Q" and r1: "!!x. x:~P ==> f(x):R" and r2: "!!y. y:Q ==> g(y):R" shows "?p : R" apply (rule excluded_middle [THEN disjE]) apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE resolve_tac [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *}) done (*Double negation law*) schematic_lemma notnotD: "p:~~P ==> ?p : P" apply (rule classical) apply (erule notE) apply assumption done (*** Tactics for implication and contradiction ***) (*Classical <-> elimination. Proof substitutes P=Q in ~P ==> ~Q and P ==> Q *) schematic_lemma iffCE: assumes major: "p:P<->Q" and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R" and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R" shows "?p : R" apply (insert major) apply (unfold iff_def) apply (rule conjE) apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE eresolve_tac [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE resolve_tac [@{thm r1}, @{thm r2}] 1) *})+ done (*Should be used as swap since ~P becomes redundant*) schematic_lemma swap: assumes major: "p:~P" and r: "!!x. x:~Q ==> f(x):P" shows "?p : Q" apply (rule classical) apply (rule major [THEN notE]) apply (rule r) apply assumption done ML_file "classical.ML" (* Patched because matching won't instantiate proof *) ML_file "simp.ML" (* Patched because matching won't instantiate proof *) ML {* structure Cla = Classical ( val sizef = size_of_thm val mp = @{thm mp} val not_elim = @{thm notE} val swap = @{thm swap} val hyp_subst_tacs = [hyp_subst_tac] ); open Cla; (*Propositional rules -- iffCE might seem better, but in the examples in ex/cla run about 7% slower than with iffE*) val prop_cs = empty_cs addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI}, @{thm notI}, @{thm iffI}] addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffE}]; (*Quantifier rules*) val FOLP_cs = prop_cs addSIs [@{thm allI}] addIs [@{thm exI}, @{thm ex1I}] addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm allE}]; val FOLP_dup_cs = prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}] addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}]; *} schematic_lemma cla_rews: "?p1 : P | ~P" "?p2 : ~P | P" "?p3 : ~ ~ P <-> P" "?p4 : (~P --> P) <-> P" apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *}) done ML_file "simpdata.ML" end