1477

1 
(* Title: FOLP/FOLP.thy


2 
Author: Martin D Coen, Cambridge University Computer Laboratory

1142

3 
Copyright 1992 University of Cambridge


4 
*)


5 

17480

6 
header {* Classical FirstOrder Logic with Proofs *}


7 


8 
theory FOLP


9 
imports IFOLP


10 
uses

26322

11 
("classical.ML") ("simp.ML") ("simpdata.ML")

17480

12 
begin


13 

0

14 
consts


15 
cla :: "[p=>p]=>p"

17480

16 
axioms


17 
classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"


18 

26322

19 


20 
(*** Classical introduction rules for  and EX ***)


21 

36319

22 
schematic_lemma disjCI:

26322

23 
assumes "!!x. x:~Q ==> f(x):P"


24 
shows "?p : PQ"


25 
apply (rule classical)


26 
apply (assumption  rule assms disjI1 notI)+


27 
apply (assumption  rule disjI2 notE)+


28 
done


29 


30 
(*introduction rule involving only EX*)

36319

31 
schematic_lemma ex_classical:

26322

32 
assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"


33 
shows "?p : EX x. P(x)"


34 
apply (rule classical)


35 
apply (rule exI, rule assms, assumption)


36 
done


37 


38 
(*version of above, simplifying ~EX to ALL~ *)

36319

39 
schematic_lemma exCI:

26322

40 
assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"


41 
shows "?p : EX x. P(x)"


42 
apply (rule ex_classical)


43 
apply (rule notI [THEN allI, THEN assms])


44 
apply (erule notE)


45 
apply (erule exI)


46 
done


47 

36319

48 
schematic_lemma excluded_middle: "?p : ~P  P"

26322

49 
apply (rule disjCI)


50 
apply assumption


51 
done


52 


53 


54 
(*** Special elimination rules *)

17480

55 

26322

56 
(*Classical implies (>) elimination. *)

36319

57 
schematic_lemma impCE:

26322

58 
assumes major: "p:P>Q"


59 
and r1: "!!x. x:~P ==> f(x):R"


60 
and r2: "!!y. y:Q ==> g(y):R"


61 
shows "?p : R"


62 
apply (rule excluded_middle [THEN disjE])


63 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE


64 
resolve_tac [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})


65 
done


66 


67 
(*Double negation law*)

36319

68 
schematic_lemma notnotD: "p:~~P ==> ?p : P"

26322

69 
apply (rule classical)


70 
apply (erule notE)


71 
apply assumption


72 
done


73 


74 


75 
(*** Tactics for implication and contradiction ***)

17480

76 

26322

77 
(*Classical <> elimination. Proof substitutes P=Q in


78 
~P ==> ~Q and P ==> Q *)

36319

79 
schematic_lemma iffCE:

26322

80 
assumes major: "p:P<>Q"


81 
and r1: "!!x y.[ x:P; y:Q ] ==> f(x,y):R"


82 
and r2: "!!x y.[ x:~P; y:~Q ] ==> g(x,y):R"


83 
shows "?p : R"


84 
apply (insert major)


85 
apply (unfold iff_def)


86 
apply (rule conjE)


87 
apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE


88 
eresolve_tac [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE


89 
resolve_tac [@{thm r1}, @{thm r2}] 1) *})+


90 
done


91 


92 


93 
(*Should be used as swap since ~P becomes redundant*)

36319

94 
schematic_lemma swap:

26322

95 
assumes major: "p:~P"


96 
and r: "!!x. x:~Q ==> f(x):P"


97 
shows "?p : Q"


98 
apply (rule classical)


99 
apply (rule major [THEN notE])


100 
apply (rule r)


101 
apply assumption


102 
done


103 

17480

104 
use "classical.ML" (* Patched 'cos matching won't instantiate proof *)


105 
use "simp.ML" (* Patched 'cos matching won't instantiate proof *)


106 


107 
ML {*


108 
(*** Applying ClassicalFun to create a classical prover ***)


109 
structure Classical_Data =

26322

110 
struct

17480

111 
val sizef = size_of_thm

26322

112 
val mp = @{thm mp}


113 
val not_elim = @{thm notE}


114 
val swap = @{thm swap}


115 
val hyp_subst_tacs = [hyp_subst_tac]


116 
end;

17480

117 


118 
structure Cla = ClassicalFun(Classical_Data);


119 
open Cla;


120 


121 
(*Propositional rules


122 
 iffCE might seem better, but in the examples in ex/cla


123 
run about 7% slower than with iffE*)

26322

124 
val prop_cs =


125 
empty_cs addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI},


126 
@{thm impI}, @{thm notI}, @{thm iffI}]


127 
addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffE}];

17480

128 


129 
(*Quantifier rules*)

26322

130 
val FOLP_cs =


131 
prop_cs addSIs [@{thm allI}] addIs [@{thm exI}, @{thm ex1I}]


132 
addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm allE}];

17480

133 

26322

134 
val FOLP_dup_cs =


135 
prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}]


136 
addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];


137 
*}

17480

138 

36319

139 
schematic_lemma cla_rews:

26322

140 
"?p1 : P  ~P"


141 
"?p2 : ~P  P"


142 
"?p3 : ~ ~ P <> P"


143 
"?p4 : (~P > P) <> P"


144 
apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})


145 
done

17480

146 


147 
use "simpdata.ML"


148 

0

149 
end
