--- a/src/FOLP/FOLP.thy Tue Mar 18 21:57:36 2008 +0100
+++ b/src/FOLP/FOLP.thy Tue Mar 18 22:19:18 2008 +0100
@@ -9,8 +9,7 @@
theory FOLP
imports IFOLP
uses
- ("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")
- ("simp.ML") ("intprover.ML") ("simpdata.ML")
+ ("classical.ML") ("simp.ML") ("simpdata.ML")
begin
consts
@@ -18,52 +17,104 @@
axioms
classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
-ML {* use_legacy_bindings (the_context ()) *}
+
+(*** Classical introduction rules for | and EX ***)
+
+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*)
+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~ *)
+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
+
+lemma excluded_middle: "?p : ~P | P"
+ apply (rule disjCI)
+ apply assumption
+ done
+
+
+(*** Special elimination rules *)
-use "FOLP_lemmas.ML"
+(*Classical implies (-->) elimination. *)
+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*)
+lemma notnotD: "p:~~P ==> ?p : P"
+ apply (rule classical)
+ apply (erule notE)
+ apply assumption
+ done
+
+
+(*** Tactics for implication and contradiction ***)
-use "hypsubst.ML"
+(*Classical <-> elimination. Proof substitutes P=Q in
+ ~P ==> ~Q and P ==> Q *)
+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*)
+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
+
use "classical.ML" (* Patched 'cos matching won't instantiate proof *)
use "simp.ML" (* Patched 'cos matching won't instantiate proof *)
ML {*
-
-(*** Applying HypsubstFun to generate hyp_subst_tac ***)
-
-structure Hypsubst_Data =
- struct
- (*Take apart an equality judgement; otherwise raise Match!*)
- fun dest_eq (Const("Proof",_) $ (Const("op =",_) $ t $ u) $ _) = (t,u);
-
- val imp_intr = impI
-
- (*etac rev_cut_eq moves an equality to be the last premise. *)
- val rev_cut_eq = prove_goal @{theory}
- "[| p:a=b; !!x. x:a=b ==> f(x):R |] ==> ?p:R"
- (fn prems => [ REPEAT(resolve_tac prems 1) ]);
-
- val rev_mp = rev_mp
- val subst = subst
- val sym = sym
- val thin_refl = prove_goal @{theory} "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
- end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-open Hypsubst;
-*}
-
-use "intprover.ML"
-
-ML {*
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
- struct
+struct
val sizef = size_of_thm
- val mp = mp
- val not_elim = notE
- val swap = swap
- val hyp_subst_tacs=[hyp_subst_tac]
- end;
+ val mp = @{thm mp}
+ val not_elim = @{thm notE}
+ val swap = @{thm swap}
+ val hyp_subst_tacs = [hyp_subst_tac]
+end;
structure Cla = ClassicalFun(Classical_Data);
open Cla;
@@ -71,17 +122,28 @@
(*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 [refl,TrueI,conjI,disjCI,impI,notI,iffI]
- addSEs [conjE,disjE,impCE,FalseE,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 [allI] addIs [exI,ex1I]
- addSEs [exE,ex1E] addEs [allE];
+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 [allI] addIs [exCI,ex1I]
- addSEs [exE,ex1E] addEs [all_dupE];
+val FOLP_dup_cs =
+ prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}]
+ addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
+*}
-*}
+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
use "simpdata.ML"
--- a/src/FOLP/FOLP_lemmas.ML Tue Mar 18 21:57:36 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(* Title: FOLP/FOLP_lemmas.ML
- ID: $Id$
- Author: Martin D Coen, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-*)
-
-(*** Classical introduction rules for | and EX ***)
-
-val prems= goal (the_context ())
- "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
-by (rtac classical 1);
-by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
-by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
-qed "disjCI";
-
-(*introduction rule involving only EX*)
-val prems= goal (the_context ())
- "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
-by (rtac classical 1);
-by (eresolve_tac (prems RL [exI]) 1) ;
-qed "ex_classical";
-
-(*version of above, simplifying ~EX to ALL~ *)
-val [prem]= goal (the_context ())
- "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
-by (rtac ex_classical 1);
-by (resolve_tac [notI RS allI RS prem] 1);
-by (etac notE 1);
-by (etac exI 1) ;
-qed "exCI";
-
-val excluded_middle = prove_goal (the_context ()) "?p : ~P | P"
- (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
-
-
-(*** Special elimination rules *)
-
-
-(*Classical implies (-->) elimination. *)
-val major::prems= goal (the_context ())
- "[| p:P-->Q; !!x. x:~P ==> f(x):R; !!y. y:Q ==> g(y):R |] ==> ?p : R";
-by (resolve_tac [excluded_middle RS disjE] 1);
-by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
-qed "impCE";
-
-(*Double negation law*)
-Goal "p:~~P ==> ?p : P";
-by (rtac classical 1);
-by (etac notE 1);
-by (assume_tac 1);
-qed "notnotD";
-
-
-(*** Tactics for implication and contradiction ***)
-
-(*Classical <-> elimination. Proof substitutes P=Q in
- ~P ==> ~Q and P ==> Q *)
-val prems = goalw (the_context ()) [iff_def]
- "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R; \
-\ !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
-by (rtac conjE 1);
-by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
- ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ;
-qed "iffCE";
-
-
-(*Should be used as swap since ~P becomes redundant*)
-val major::prems= goal (the_context ())
- "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
-by (rtac classical 1);
-by (rtac (major RS notE) 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "swap";
--- a/src/FOLP/IFOLP.ML Tue Mar 18 21:57:36 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,370 +0,0 @@
-(* Title: FOLP/IFOLP.ML
- ID: $Id$
- Author: Martin D Coen, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-*)
-
-(*** Sequent-style elimination rules for & --> and ALL ***)
-
-val prems= Goal
- "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R";
-by (REPEAT (resolve_tac prems 1
- ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ;
-qed "conjE";
-
-val prems= Goal
- "[| p:P-->Q; q:P; !!x. x:Q ==> r(x):R |] ==> ?p:R";
-by (REPEAT (resolve_tac (prems@[mp]) 1)) ;
-qed "impE";
-
-val prems= Goal
- "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R";
-by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
-qed "allE";
-
-(*Duplicates the quantifier; for use with eresolve_tac*)
-val prems= Goal
- "[| p:ALL x. P(x); !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
-\ |] ==> ?p:R";
-by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
-qed "all_dupE";
-
-
-(*** Negation rules, which translate between ~P and P-->False ***)
-
-bind_thm ("notI", prove_goalw (the_context ()) [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P"
- (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]));
-
-bind_thm ("notE", prove_goalw (the_context ()) [not_def] "[| p:~P; q:P |] ==> ?p:R"
- (fn prems=>
- [ (resolve_tac [mp RS FalseE] 1),
- (REPEAT (resolve_tac prems 1)) ]));
-
-(*This is useful with the special implication rules for each kind of P. *)
-val prems= Goal
- "[| p:~P; !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q";
-by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ;
-qed "not_to_imp";
-
-
-(* For substitution int an assumption P, reduce Q to P-->Q, substitute into
- this implication, then apply impI to move P back into the assumptions.
- To specify P use something like
- eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *)
-Goal "[| p:P; q:P --> Q |] ==> ?p:Q";
-by (REPEAT (ares_tac [mp] 1)) ;
-qed "rev_mp";
-
-
-(*Contrapositive of an inference rule*)
-val [major,minor]= Goal "[| p:~Q; !!y. y:P==>q(y):Q |] ==> ?a:~P";
-by (rtac (major RS notE RS notI) 1);
-by (etac minor 1) ;
-qed "contrapos";
-
-(** Unique assumption tactic.
- Ignores proof objects.
- Fails unless one assumption is equal and exactly one is unifiable
-**)
-
-local
- fun discard_proof (Const("Proof",_) $ P $ _) = P;
-in
-val uniq_assume_tac =
- SUBGOAL
- (fn (prem,i) =>
- let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
- and concl = discard_proof (Logic.strip_assums_concl prem)
- in
- if exists (fn hyp => hyp aconv concl) hyps
- then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
- [_] => assume_tac i
- | _ => no_tac
- else no_tac
- end);
-end;
-
-
-(*** Modus Ponens Tactics ***)
-
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = eresolve_tac [notE,make_elim mp] i THEN assume_tac i;
-
-(*Like mp_tac but instantiates no variables*)
-fun int_uniq_mp_tac i = eresolve_tac [notE,impE] i THEN uniq_assume_tac i;
-
-
-(*** If-and-only-if ***)
-
-bind_thm ("iffI", prove_goalw (the_context ()) [iff_def]
- "[| !!x. x:P ==> q(x):Q; !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
- (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]));
-
-
-(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
-bind_thm ("iffE", prove_goalw (the_context ()) [iff_def]
- "[| p:P <-> Q; !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R"
- (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]));
-
-(* Destruct rules for <-> similar to Modus Ponens *)
-
-bind_thm ("iffD1", prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q; q:P |] ==> ?p:Q"
- (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]));
-
-bind_thm ("iffD2", prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q; q:Q |] ==> ?p:P"
- (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]));
-
-Goal "?p:P <-> P";
-by (REPEAT (ares_tac [iffI] 1)) ;
-qed "iff_refl";
-
-Goal "p:Q <-> P ==> ?p:P <-> Q";
-by (etac iffE 1);
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [asm_rl,mp] 1)) ;
-qed "iff_sym";
-
-Goal "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ;
-qed "iff_trans";
-
-
-(*** Unique existence. NOTE THAT the following 2 quantifications
- EX!x such that [EX!y such that P(x,y)] (sequential)
- EX!x,y such that P(x,y) (simultaneous)
- do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
-***)
-
-val prems = goalw (the_context ()) [ex1_def]
- "[| p:P(a); !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)";
-by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
-qed "ex1I";
-
-val prems = goalw (the_context ()) [ex1_def]
- "[| p:EX! x. P(x); \
-\ !!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
-\ ?a : R";
-by (cut_facts_tac prems 1);
-by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ;
-qed "ex1E";
-
-
-(*** <-> congruence rules for simplification ***)
-
-(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*)
-fun iff_tac prems i =
- resolve_tac (prems RL [iffE]) i THEN
- REPEAT1 (eresolve_tac [asm_rl,mp] i);
-
-bind_thm ("conj_cong", prove_goal (the_context ())
- "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
- (fn prems =>
- [ (cut_facts_tac prems 1),
- (REPEAT (ares_tac [iffI,conjI] 1
- ORELSE eresolve_tac [iffE,conjE,mp] 1
- ORELSE iff_tac prems 1)) ]));
-
-bind_thm ("disj_cong", prove_goal (the_context ())
- "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
- (fn prems =>
- [ (cut_facts_tac prems 1),
- (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1
- ORELSE ares_tac [iffI] 1
- ORELSE mp_tac 1)) ]));
-
-bind_thm ("imp_cong", prove_goal (the_context ())
- "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
- (fn prems =>
- [ (cut_facts_tac prems 1),
- (REPEAT (ares_tac [iffI,impI] 1
- ORELSE etac iffE 1
- ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]));
-
-bind_thm ("iff_cong", prove_goal (the_context ())
- "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
- (fn prems =>
- [ (cut_facts_tac prems 1),
- (REPEAT (etac iffE 1
- ORELSE ares_tac [iffI] 1
- ORELSE mp_tac 1)) ]));
-
-bind_thm ("not_cong", prove_goal (the_context ())
- "p:P <-> P' ==> ?p:~P <-> ~P'"
- (fn prems =>
- [ (cut_facts_tac prems 1),
- (REPEAT (ares_tac [iffI,notI] 1
- ORELSE mp_tac 1
- ORELSE eresolve_tac [iffE,notE] 1)) ]));
-
-bind_thm ("all_cong", prove_goal (the_context ())
- "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
- (fn prems =>
- [ (REPEAT (ares_tac [iffI,allI] 1
- ORELSE mp_tac 1
- ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]));
-
-bind_thm ("ex_cong", prove_goal (the_context ())
- "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
- (fn prems =>
- [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1
- ORELSE mp_tac 1
- ORELSE iff_tac prems 1)) ]));
-
-(*NOT PROVED
-bind_thm ("ex1_cong", prove_goal (the_context ())
- "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
- (fn prems =>
- [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
- ORELSE mp_tac 1
- ORELSE iff_tac prems 1)) ]));
-*)
-
-(*** Equality rules ***)
-
-bind_thm ("refl", ieqI);
-
-bind_thm ("subst", prove_goal (the_context ()) "[| p:a=b; q:P(a) |] ==> ?p : P(b)"
- (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),
- rtac impI 1, atac 1 ]));
-
-Goal "q:a=b ==> ?c:b=a";
-by (etac subst 1);
-by (rtac refl 1) ;
-qed "sym";
-
-Goal "[| p:a=b; q:b=c |] ==> ?d:a=c";
-by (etac subst 1 THEN assume_tac 1);
-qed "trans";
-
-(** ~ b=a ==> ~ a=b **)
-Goal "p:~ b=a ==> ?q:~ a=b";
-by (etac contrapos 1);
-by (etac sym 1) ;
-qed "not_sym";
-
-(*calling "standard" reduces maxidx to 0*)
-bind_thm ("ssubst", standard (sym RS subst));
-
-(*A special case of ex1E that would otherwise need quantifier expansion*)
-Goal "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b";
-by (etac ex1E 1);
-by (rtac trans 1);
-by (rtac sym 2);
-by (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ;
-qed "ex1_equalsE";
-
-(** Polymorphic congruence rules **)
-
-Goal "[| p:a=b |] ==> ?d:t(a)=t(b)";
-by (etac ssubst 1);
-by (rtac refl 1) ;
-qed "subst_context";
-
-Goal "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)";
-by (REPEAT (etac ssubst 1));
-by (rtac refl 1) ;
-qed "subst_context2";
-
-Goal "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)";
-by (REPEAT (etac ssubst 1));
-by (rtac refl 1) ;
-qed "subst_context3";
-
-(*Useful with eresolve_tac for proving equalties from known equalities.
- a = b
- | |
- c = d *)
-Goal "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d";
-by (rtac trans 1);
-by (rtac trans 1);
-by (rtac sym 1);
-by (REPEAT (assume_tac 1)) ;
-qed "box_equals";
-
-(*Dual of box_equals: for proving equalities backwards*)
-Goal "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b";
-by (rtac trans 1);
-by (rtac trans 1);
-by (REPEAT (eresolve_tac [asm_rl, sym] 1)) ;
-qed "simp_equals";
-
-(** Congruence rules for predicate letters **)
-
-Goal "p:a=a' ==> ?p:P(a) <-> P(a')";
-by (rtac iffI 1);
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
-qed "pred1_cong";
-
-Goal "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')";
-by (rtac iffI 1);
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
-qed "pred2_cong";
-
-Goal "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')";
-by (rtac iffI 1);
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
-qed "pred3_cong";
-
-(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
-
-bind_thms ("pred_congs",
- List.concat (map (fn c =>
- map (fn th => read_instantiate [("P",c)] th)
- [pred1_cong,pred2_cong,pred3_cong])
- (explode"PQRS")));
-
-(*special case for the equality predicate!*)
-bind_thm ("eq_cong", read_instantiate [("P","op =")] pred2_cong);
-
-
-(*** Simplifications of assumed implications.
- Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
- used with mp_tac (restricted to atomic formulae) is COMPLETE for
- intuitionistic propositional logic. See
- R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
- (preprint, University of St Andrews, 1991) ***)
-
-val major::prems= Goal
- "[| p:(P&Q)-->S; !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R";
-by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ;
-qed "conj_impE";
-
-val major::prems= Goal
- "[| p:(P|Q)-->S; !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R";
-by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ;
-qed "disj_impE";
-
-(*Simplifies the implication. Classical version is stronger.
- Still UNSAFE since Q must be provable -- backtracking needed. *)
-val major::prems= Goal
- "[| p:(P-->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; !!x. x:S ==> r(x):R |] ==> \
-\ ?p:R";
-by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ;
-qed "imp_impE";
-
-(*Simplifies the implication. Classical version is stronger.
- Still UNSAFE since ~P must be provable -- backtracking needed. *)
-val major::prems= Goal
- "[| p:~P --> S; !!y. y:P ==> q(y):False; !!y. y:S ==> r(y):R |] ==> ?p:R";
-by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ;
-qed "not_impE";
-
-(*Simplifies the implication. UNSAFE. *)
-val major::prems= Goal
- "[| p:(P<->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; \
-\ !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P; !!x. x:S ==> s(x):R |] ==> ?p:R";
-by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ;
-qed "iff_impE";
-
-(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
-val major::prems= Goal
- "[| p:(ALL x. P(x))-->S; !!x. q:P(x); !!y. y:S ==> r(y):R |] ==> ?p:R";
-by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ;
-qed "all_impE";
-
-(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *)
-val major::prems= Goal
- "[| p:(EX x. P(x))-->S; !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R";
-by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ;
-qed "ex_impE";
--- a/src/FOLP/IFOLP.thy Tue Mar 18 21:57:36 2008 +0100
+++ b/src/FOLP/IFOLP.thy Tue Mar 18 22:19:18 2008 +0100
@@ -8,6 +8,7 @@
theory IFOLP
imports Pure
+uses ("hypsubst.ML") ("intprover.ML")
begin
global
@@ -69,7 +70,7 @@
(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
val show_proofs = ref false;
-fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
+fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
fun proof_tr' [P,p] =
if !show_proofs then Const("@Proof",dummyT) $ p $ P
@@ -154,8 +155,555 @@
norm_eq: "nrm : norm(x) = x"
NORM_iff: "NRM : NORM(P) <-> P"
-ML {* use_legacy_bindings (the_context ()) *}
+(*** Sequent-style elimination rules for & --> and ALL ***)
+
+lemma conjE:
+ assumes "p:P&Q"
+ and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
+ shows "?a:R"
+ apply (rule assms(2))
+ apply (rule conjunct1 [OF assms(1)])
+ apply (rule conjunct2 [OF assms(1)])
+ done
+
+lemma impE:
+ assumes "p:P-->Q"
+ and "q:P"
+ and "!!x. x:Q ==> r(x):R"
+ shows "?p:R"
+ apply (rule assms mp)+
+ done
+
+lemma allE:
+ assumes "p:ALL x. P(x)"
+ and "!!y. y:P(x) ==> q(y):R"
+ shows "?p:R"
+ apply (rule assms spec)+
+ done
+
+(*Duplicates the quantifier; for use with eresolve_tac*)
+lemma all_dupE:
+ assumes "p:ALL x. P(x)"
+ and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
+ shows "?p:R"
+ apply (rule assms spec)+
+ done
+
+
+(*** Negation rules, which translate between ~P and P-->False ***)
+
+lemma notI:
+ assumes "!!x. x:P ==> q(x):False"
+ shows "?p:~P"
+ unfolding not_def
+ apply (assumption | rule assms impI)+
+ done
+
+lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
+ unfolding not_def
+ apply (drule (1) mp)
+ apply (erule FalseE)
+ done
+
+(*This is useful with the special implication rules for each kind of P. *)
+lemma not_to_imp:
+ assumes "p:~P"
+ and "!!x. x:(P-->False) ==> q(x):Q"
+ shows "?p:Q"
+ apply (assumption | rule assms impI notE)+
+ done
+
+(* For substitution int an assumption P, reduce Q to P-->Q, substitute into
+ this implication, then apply impI to move P back into the assumptions.
+ To specify P use something like
+ eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *)
+lemma rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q"
+ apply (assumption | rule mp)+
+ done
+
+
+(*Contrapositive of an inference rule*)
+lemma contrapos:
+ assumes major: "p:~Q"
+ and minor: "!!y. y:P==>q(y):Q"
+ shows "?a:~P"
+ apply (rule major [THEN notE, THEN notI])
+ apply (erule minor)
+ done
+
+(** Unique assumption tactic.
+ Ignores proof objects.
+ Fails unless one assumption is equal and exactly one is unifiable
+**)
+
+ML {*
+local
+ fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P;
+in
+val uniq_assume_tac =
+ SUBGOAL
+ (fn (prem,i) =>
+ let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
+ and concl = discard_proof (Logic.strip_assums_concl prem)
+ in
+ if exists (fn hyp => hyp aconv concl) hyps
+ then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
+ [_] => assume_tac i
+ | _ => no_tac
+ else no_tac
+ end);
+end;
+*}
+
+
+(*** Modus Ponens Tactics ***)
+
+(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+ML {*
+ fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac i
+*}
+
+(*Like mp_tac but instantiates no variables*)
+ML {*
+ fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac i
+*}
+
+
+(*** If-and-only-if ***)
+
+lemma iffI:
+ assumes "!!x. x:P ==> q(x):Q"
+ and "!!x. x:Q ==> r(x):P"
+ shows "?p:P<->Q"
+ unfolding iff_def
+ apply (assumption | rule assms conjI impI)+
+ done
+
+
+(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
+
+lemma iffE:
+ assumes "p:P <-> Q"
+ and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
+ shows "?p:R"
+ apply (rule conjE)
+ apply (rule assms(1) [unfolded iff_def])
+ apply (rule assms(2))
+ apply assumption+
+ done
+
+(* Destruct rules for <-> similar to Modus Ponens *)
+
+lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
+ unfolding iff_def
+ apply (rule conjunct1 [THEN mp], assumption+)
+ done
+
+lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
+ unfolding iff_def
+ apply (rule conjunct2 [THEN mp], assumption+)
+ done
+
+lemma iff_refl: "?p:P <-> P"
+ apply (rule iffI)
+ apply assumption+
+ done
+
+lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
+ apply (erule iffE)
+ apply (rule iffI)
+ apply (erule (1) mp)+
+ done
+
+lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
+ apply (rule iffI)
+ apply (assumption | erule iffE | erule (1) impE)+
+ done
+
+(*** Unique existence. NOTE THAT the following 2 quantifications
+ EX!x such that [EX!y such that P(x,y)] (sequential)
+ EX!x,y such that P(x,y) (simultaneous)
+ do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
+***)
+
+lemma ex1I:
+ assumes "p:P(a)"
+ and "!!x u. u:P(x) ==> f(u) : x=a"
+ shows "?p:EX! x. P(x)"
+ unfolding ex1_def
+ apply (assumption | rule assms exI conjI allI impI)+
+ done
+
+lemma ex1E:
+ assumes "p:EX! x. P(x)"
+ and "!!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
+ shows "?a : R"
+ apply (insert assms(1) [unfolded ex1_def])
+ apply (erule exE conjE | assumption | rule assms(1))+
+ done
+
+
+(*** <-> congruence rules for simplification ***)
+
+(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*)
+ML {*
+fun iff_tac prems i =
+ resolve_tac (prems RL [@{thm iffE}]) i THEN
+ REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
+*}
+
+lemma conj_cong:
+ assumes "p:P <-> P'"
+ and "!!x. x:P' ==> q(x):Q <-> Q'"
+ shows "?p:(P&Q) <-> (P'&Q')"
+ apply (insert assms(1))
+ apply (assumption | rule iffI conjI |
+ erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
+ done
+
+lemma disj_cong:
+ "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
+ apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
+ done
+
+lemma imp_cong:
+ assumes "p:P <-> P'"
+ and "!!x. x:P' ==> q(x):Q <-> Q'"
+ shows "?p:(P-->Q) <-> (P'-->Q')"
+ apply (insert assms(1))
+ apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} |
+ tactic {* iff_tac @{thms assms} 1 *})+
+ done
+
+lemma iff_cong:
+ "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
+ apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
+ done
+
+lemma not_cong:
+ "p:P <-> P' ==> ?p:~P <-> ~P'"
+ apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
+ done
+
+lemma all_cong:
+ assumes "!!x. f(x):P(x) <-> Q(x)"
+ shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
+ apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
+ tactic {* iff_tac @{thms assms} 1 *})+
+ done
+
+lemma ex_cong:
+ assumes "!!x. f(x):P(x) <-> Q(x)"
+ shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
+ apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
+ tactic {* iff_tac @{thms assms} 1 *})+
+ done
+
+(*NOT PROVED
+bind_thm ("ex1_cong", prove_goal (the_context ())
+ "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
+ (fn prems =>
+ [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
+ ORELSE mp_tac 1
+ ORELSE iff_tac prems 1)) ]))
+*)
+
+(*** Equality rules ***)
+
+lemmas refl = ieqI
+
+lemma subst:
+ assumes prem1: "p:a=b"
+ and prem2: "q:P(a)"
+ shows "?p : P(b)"
+ apply (rule prem2 [THEN rev_mp])
+ apply (rule prem1 [THEN ieqE])
+ apply (rule impI)
+ apply assumption
+ done
+
+lemma sym: "q:a=b ==> ?c:b=a"
+ apply (erule subst)
+ apply (rule refl)
+ done
+
+lemma trans: "[| p:a=b; q:b=c |] ==> ?d:a=c"
+ apply (erule (1) subst)
+ done
+
+(** ~ b=a ==> ~ a=b **)
+lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
+ apply (erule contrapos)
+ apply (erule sym)
+ done
+
+(*calling "standard" reduces maxidx to 0*)
+lemmas ssubst = sym [THEN subst, standard]
+
+(*A special case of ex1E that would otherwise need quantifier expansion*)
+lemma ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b"
+ apply (erule ex1E)
+ apply (rule trans)
+ apply (rule_tac [2] sym)
+ apply (assumption | erule spec [THEN mp])+
+ done
+
+(** Polymorphic congruence rules **)
+
+lemma subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)"
+ apply (erule ssubst)
+ apply (rule refl)
+ done
+
+lemma subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)"
+ apply (erule ssubst)+
+ apply (rule refl)
+ done
+
+lemma subst_context3: "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)"
+ apply (erule ssubst)+
+ apply (rule refl)
+ done
+
+(*Useful with eresolve_tac for proving equalties from known equalities.
+ a = b
+ | |
+ c = d *)
+lemma box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d"
+ apply (rule trans)
+ apply (rule trans)
+ apply (rule sym)
+ apply assumption+
+ done
+
+(*Dual of box_equals: for proving equalities backwards*)
+lemma simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b"
+ apply (rule trans)
+ apply (rule trans)
+ apply (assumption | rule sym)+
+ done
+
+(** Congruence rules for predicate letters **)
+
+lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
+ apply (rule iffI)
+ apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
+ done
+
+lemma pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
+ apply (rule iffI)
+ apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
+ done
+
+lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
+ apply (rule iffI)
+ apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
+ done
+
+(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
+
+ML_setup {*
+ bind_thms ("pred_congs",
+ flat (map (fn c =>
+ map (fn th => read_instantiate [("P",c)] th)
+ [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
+ (explode"PQRS")))
+*}
+
+(*special case for the equality predicate!*)
+lemmas eq_cong = pred2_cong [where P = "op =", standard]
+
+
+(*** Simplifications of assumed implications.
+ Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
+ used with mp_tac (restricted to atomic formulae) is COMPLETE for
+ intuitionistic propositional logic. See
+ R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
+ (preprint, University of St Andrews, 1991) ***)
+
+lemma conj_impE:
+ assumes major: "p:(P&Q)-->S"
+ and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
+ shows "?p:R"
+ apply (assumption | rule conjI impI major [THEN mp] minor)+
+ done
+
+lemma disj_impE:
+ assumes major: "p:(P|Q)-->S"
+ and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
+ shows "?p:R"
+ apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
+ resolve_tac [@{thm disjI1}, @{thm disjI2}, @{thm impI},
+ @{thm major} RS @{thm mp}, @{thm minor}] 1) *})
+ done
+
+(*Simplifies the implication. Classical version is stronger.
+ Still UNSAFE since Q must be provable -- backtracking needed. *)
+lemma imp_impE:
+ assumes major: "p:(P-->Q)-->S"
+ and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
+ and r2: "!!x. x:S ==> r(x):R"
+ shows "?p:R"
+ apply (assumption | rule impI major [THEN mp] r1 r2)+
+ done
+
+(*Simplifies the implication. Classical version is stronger.
+ Still UNSAFE since ~P must be provable -- backtracking needed. *)
+lemma not_impE:
+ assumes major: "p:~P --> S"
+ and r1: "!!y. y:P ==> q(y):False"
+ and r2: "!!y. y:S ==> r(y):R"
+ shows "?p:R"
+ apply (assumption | rule notI impI major [THEN mp] r1 r2)+
+ done
+
+(*Simplifies the implication. UNSAFE. *)
+lemma iff_impE:
+ assumes major: "p:(P<->Q)-->S"
+ and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
+ and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
+ and r3: "!!x. x:S ==> s(x):R"
+ shows "?p:R"
+ apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
+ done
+
+(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
+lemma all_impE:
+ assumes major: "p:(ALL x. P(x))-->S"
+ and r1: "!!x. q:P(x)"
+ and r2: "!!y. y:S ==> r(y):R"
+ shows "?p:R"
+ apply (assumption | rule allI impI major [THEN mp] r1 r2)+
+ done
+
+(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *)
+lemma ex_impE:
+ assumes major: "p:(EX x. P(x))-->S"
+ and r: "!!y. y:P(a)-->S ==> q(y):R"
+ shows "?p:R"
+ apply (assumption | rule exI impI major [THEN mp] r)+
+ done
+
+
+lemma rev_cut_eq:
+ assumes "p:a=b"
+ and "!!x. x:a=b ==> f(x):R"
+ shows "?p:R"
+ apply (rule assms)+
+ done
+
+lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
+
+use "hypsubst.ML"
+
+ML {*
+
+(*** Applying HypsubstFun to generate hyp_subst_tac ***)
+
+structure Hypsubst_Data =
+struct
+ (*Take apart an equality judgement; otherwise raise Match!*)
+ fun dest_eq (Const (@{const_name Proof}, _) $
+ (Const (@{const_name "op ="}, _) $ t $ u) $ _) = (t, u);
+
+ val imp_intr = @{thm impI}
+
+ (*etac rev_cut_eq moves an equality to be the last premise. *)
+ val rev_cut_eq = @{thm rev_cut_eq}
+
+ val rev_mp = @{thm rev_mp}
+ val subst = @{thm subst}
+ val sym = @{thm sym}
+ val thin_refl = @{thm thin_refl}
+end;
+
+structure Hypsubst = HypsubstFun(Hypsubst_Data);
+open Hypsubst;
+*}
+
+use "intprover.ML"
+
+
+(*** Rewrite rules ***)
+
+lemma conj_rews:
+ "?p1 : P & True <-> P"
+ "?p2 : True & P <-> P"
+ "?p3 : P & False <-> False"
+ "?p4 : False & P <-> False"
+ "?p5 : P & P <-> P"
+ "?p6 : P & ~P <-> False"
+ "?p7 : ~P & P <-> False"
+ "?p8 : (P & Q) & R <-> P & (Q & R)"
+ apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
+ done
+
+lemma disj_rews:
+ "?p1 : P | True <-> True"
+ "?p2 : True | P <-> True"
+ "?p3 : P | False <-> P"
+ "?p4 : False | P <-> P"
+ "?p5 : P | P <-> P"
+ "?p6 : (P | Q) | R <-> P | (Q | R)"
+ apply (tactic {* IntPr.fast_tac 1 *})+
+ done
+
+lemma not_rews:
+ "?p1 : ~ False <-> True"
+ "?p2 : ~ True <-> False"
+ apply (tactic {* IntPr.fast_tac 1 *})+
+ done
+
+lemma imp_rews:
+ "?p1 : (P --> False) <-> ~P"
+ "?p2 : (P --> True) <-> True"
+ "?p3 : (False --> P) <-> True"
+ "?p4 : (True --> P) <-> P"
+ "?p5 : (P --> P) <-> True"
+ "?p6 : (P --> ~P) <-> ~P"
+ apply (tactic {* IntPr.fast_tac 1 *})+
+ done
+
+lemma iff_rews:
+ "?p1 : (True <-> P) <-> P"
+ "?p2 : (P <-> True) <-> P"
+ "?p3 : (P <-> P) <-> True"
+ "?p4 : (False <-> P) <-> ~P"
+ "?p5 : (P <-> False) <-> ~P"
+ apply (tactic {* IntPr.fast_tac 1 *})+
+ done
+
+lemma quant_rews:
+ "?p1 : (ALL x. P) <-> P"
+ "?p2 : (EX x. P) <-> P"
+ apply (tactic {* IntPr.fast_tac 1 *})+
+ done
+
+(*These are NOT supplied by default!*)
+lemma distrib_rews1:
+ "?p1 : ~(P|Q) <-> ~P & ~Q"
+ "?p2 : P & (Q | R) <-> P&Q | P&R"
+ "?p3 : (Q | R) & P <-> Q&P | R&P"
+ "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)"
+ apply (tactic {* IntPr.fast_tac 1 *})+
+ done
+
+lemma distrib_rews2:
+ "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
+ "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
+ "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
+ "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"
+ apply (tactic {* IntPr.fast_tac 1 *})+
+ done
+
+lemmas distrib_rews = distrib_rews1 distrib_rews2
+
+lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
+ apply (tactic {* IntPr.fast_tac 1 *})
+ done
+
+lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
+ apply (tactic {* IntPr.fast_tac 1 *})
+ done
end
-
-
--- a/src/FOLP/IsaMakefile Tue Mar 18 21:57:36 2008 +0100
+++ b/src/FOLP/IsaMakefile Tue Mar 18 22:19:18 2008 +0100
@@ -26,7 +26,7 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/FOLP: $(OUT)/Pure FOLP_lemmas.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
+$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML \
classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
@@ -35,8 +35,9 @@
FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
-$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/Foundation.thy \
- ex/If.thy ex/int.ML ex/Intro.thy ex/Nat.thy \
+$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy \
+ ex/If.thy ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy \
+ ex/Classical.thy \
ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
@$(ISATOOL) usedir $(OUT)/FOLP ex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/ex/Classical.thy Tue Mar 18 22:19:18 2008 +0100
@@ -0,0 +1,303 @@
+(* Title: FOLP/ex/Classical.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Classical First-Order Logic.
+*)
+
+theory Classical
+imports FOLP
+begin
+
+lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*If and only if*)
+lemma "?p : (P<->Q) <-> (Q<->P)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+lemma "?p : ~ (P <-> ~P)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+
+(*Sample problems from
+ F. J. Pelletier,
+ Seventy-Five Problems for Testing Automatic Theorem Provers,
+ J. Automated Reasoning 2 (1986), 191-216.
+ Errata, JAR 4 (1988), 236-236.
+
+The hardest problems -- judging by experience with several theorem provers,
+including matrix ones -- are 34 and 43.
+*)
+
+text "Pelletier's examples"
+(*1*)
+lemma "?p : (P-->Q) <-> (~Q --> ~P)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*2*)
+lemma "?p : ~ ~ P <-> P"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*3*)
+lemma "?p : ~(P-->Q) --> (Q-->P)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*4*)
+lemma "?p : (~P-->Q) <-> (~Q --> P)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*5*)
+lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*6*)
+lemma "?p : P | ~ P"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*7*)
+lemma "?p : P | ~ ~ ~ P"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*8. Peirce's law*)
+lemma "?p : ((P-->Q) --> P) --> P"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*9*)
+lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*10*)
+lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
+lemma "?p : P<->P"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*12. "Dijkstra's law"*)
+lemma "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*13. Distributive law*)
+lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*14*)
+lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*15*)
+lemma "?p : (P --> Q) <-> (~P | Q)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*16*)
+lemma "?p : (P-->Q) | (Q-->P)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+(*17*)
+lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+
+text "Classical Logic: examples with quantifiers"
+
+lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+lemma "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+lemma "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"
+ by (tactic "fast_tac FOLP_cs 1")
+
+lemma "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"
+ by (tactic "fast_tac FOLP_cs 1")
+
+
+text "Problems requiring quantifier duplication"
+
+(*Needs multiple instantiation of ALL.*)
+lemma "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+(*Needs double instantiation of the quantifier*)
+lemma "?p : EX x. P(x) --> P(a) & P(b)"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+lemma "?p : EX z. P(z) --> (ALL x. P(x))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+
+text "Hard examples with quantifiers"
+
+text "Problem 18"
+lemma "?p : EX y. ALL x. P(y)-->P(x)"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 19"
+lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 20"
+lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
+ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 21"
+lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 22"
+lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 23"
+lemma "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 24"
+lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
+ (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))
+ --> (EX x. P(x)&R(x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 25"
+lemma "?p : (EX x. P(x)) &
+ (ALL x. L(x) --> ~ (M(x) & R(x))) &
+ (ALL x. P(x) --> (M(x) & L(x))) &
+ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
+ --> (EX x. Q(x)&P(x))"
+ oops
+
+text "Problem 26"
+lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &
+ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))
+ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 27"
+lemma "?p : (EX x. P(x) & ~Q(x)) &
+ (ALL x. P(x) --> R(x)) &
+ (ALL x. M(x) & L(x) --> P(x)) &
+ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
+ --> (ALL x. M(x) --> ~L(x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 28. AMENDED"
+lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &
+ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
+ ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))
+ --> (ALL x. P(x) & L(x) --> M(x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 29. Essentially the same as Principia Mathematica *11.71"
+lemma "?p : (EX x. P(x)) & (EX y. Q(y))
+ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <->
+ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 30"
+lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &
+ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
+ --> (ALL x. S(x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 31"
+lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &
+ (EX x. L(x) & P(x)) &
+ (ALL x. ~ R(x) --> M(x))
+ --> (EX x. L(x) & M(x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 32"
+lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
+ (ALL x. S(x) & R(x) --> L(x)) &
+ (ALL x. M(x) --> R(x))
+ --> (ALL x. P(x) & M(x) --> L(x))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 33"
+lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <->
+ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 35"
+lemma "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 36"
+lemma
+"?p : (ALL x. EX y. J(x,y)) &
+ (ALL x. EX y. G(x,y)) &
+ (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
+ --> (ALL x. EX y. H(x,y))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 37"
+lemma "?p : (ALL z. EX w. ALL x. EX y.
+ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &
+ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &
+ ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))
+ --> (ALL x. EX y. R(x,y))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 39"
+lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 40. AMENDED"
+lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->
+ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 41"
+lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))
+ --> ~ (EX z. ALL x. f(x,z))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 44"
+lemma "?p : (ALL x. f(x) -->
+ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
+ (EX x. j(x) & (ALL y. g(y) --> h(x,y)))
+ --> (EX x. j(x) & ~f(x))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problems (mainly) involving equality or functions"
+
+text "Problem 48"
+lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 50"
+(*What has this to do with equality?*)
+lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 56"
+lemma
+ "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 57"
+lemma
+"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
+ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+text "Problem 58 NOT PROVED AUTOMATICALLY"
+lemma
+ notes f_cong = subst_context [where t = f]
+ shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
+ by (tactic {* fast_tac (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
+
+text "Problem 59"
+lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
+ by (tactic "best_tac FOLP_dup_cs 1")
+
+text "Problem 60"
+lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+ by (tactic "fast_tac FOLP_cs 1")
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/ex/Intuitionistic.thy Tue Mar 18 22:19:18 2008 +0100
@@ -0,0 +1,307 @@
+(* Title: FOLP/ex/Intuitionistic.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+Intuitionistic First-Order Logic.
+
+Single-step commands:
+by (IntPr.step_tac 1)
+by (biresolve_tac safe_brls 1);
+by (biresolve_tac haz_brls 1);
+by (assume_tac 1);
+by (IntPr.safe_tac 1);
+by (IntPr.mp_tac 1);
+by (IntPr.fast_tac 1);
+*)
+
+(*Note: for PROPOSITIONAL formulae...
+ ~A is classically provable iff it is intuitionistically provable.
+ Therefore A is classically provable iff ~~A is intuitionistically provable.
+
+Let Q be the conjuction of the propositions A|~A, one for each atom A in
+P. If P is provable classically, then clearly P&Q is provable
+intuitionistically, so ~~(P&Q) is also provable intuitionistically.
+The latter is intuitionistically equivalent to ~~P&~~Q, hence to ~~P,
+since ~~Q is intuitionistically provable. Finally, if P is a negation then
+~~P is intuitionstically equivalent to P. [Andy Pitts]
+*)
+
+theory Intuitionistic
+imports IFOLP
+begin
+
+lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : ~~~P <-> ~P"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : (P<->Q) <-> (Q<->P)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+
+subsection {* Lemmas for the propositional double-negation translation *}
+
+lemma "?p : P --> ~~P"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : ~~(~~P --> P)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+
+subsection {* The following are classically but not constructively valid *}
+
+(*The attempt to prove them terminates quickly!*)
+lemma "?p : ((P-->Q) --> P) --> P"
+ apply (tactic {* IntPr.fast_tac 1 *})?
+ oops
+
+lemma "?p : (P&Q-->R) --> (P-->R) | (Q-->R)"
+ apply (tactic {* IntPr.fast_tac 1 *})?
+ oops
+
+
+subsection {* Intuitionistic FOL: propositional problems based on Pelletier *}
+
+text "Problem ~~1"
+lemma "?p : ~~((P-->Q) <-> (~Q --> ~P))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~2"
+lemma "?p : ~~(~~P <-> P)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem 3"
+lemma "?p : ~(P-->Q) --> (Q-->P)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~4"
+lemma "?p : ~~((~P-->Q) <-> (~Q --> P))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~5"
+lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~6"
+lemma "?p : ~~(P | ~P)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~7"
+lemma "?p : ~~(P | ~~~P)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~8. Peirce's law"
+lemma "?p : ~~(((P-->Q) --> P) --> P)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem 9"
+lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem 10"
+lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "11. Proved in each direction (incorrectly, says Pelletier!!) "
+lemma "?p : P<->P"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~12. Dijkstra's law "
+lemma "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem 13. Distributive law"
+lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~14"
+lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~15"
+lemma "?p : ~~((P --> Q) <-> (~P | Q))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~16"
+lemma "?p : ~~((P-->Q) | (Q-->P))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~17"
+lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
+ by (tactic {* IntPr.fast_tac 1 *}) -- slow
+
+
+subsection {* Examples with quantifiers *}
+
+text "The converse is classical in the following implications..."
+
+lemma "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+
+text "The following are not constructively valid!"
+text "The attempt to prove them terminates quickly!"
+
+lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
+ apply (tactic {* IntPr.fast_tac 1 *})?
+ oops
+
+lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
+ apply (tactic {* IntPr.fast_tac 1 *})?
+ oops
+
+lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
+ apply (tactic {* IntPr.fast_tac 1 *})?
+ oops
+
+lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
+ apply (tactic {* IntPr.fast_tac 1 *})?
+ oops
+
+(*Classically but not intuitionistically valid. Proved by a bug in 1986!*)
+lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
+ apply (tactic {* IntPr.fast_tac 1 *})?
+ oops
+
+
+subsection "Hard examples with quantifiers"
+
+text {*
+ The ones that have not been proved are not known to be valid!
+ Some will require quantifier duplication -- not currently available.
+*}
+
+text "Problem ~~18"
+lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
+(*NOT PROVED*)
+
+text "Problem ~~19"
+lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
+(*NOT PROVED*)
+
+text "Problem 20"
+lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
+ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem 21"
+lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
+(*NOT PROVED*)
+
+text "Problem 22"
+lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem ~~23"
+lemma "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))"
+ by (tactic {* IntPr.fast_tac 1 *})
+
+text "Problem 24"
+lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
+ (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))
+ --> ~~(EX x. P(x)&R(x))"
+(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
+ apply (tactic "IntPr.safe_tac")
+ apply (erule impE)
+ apply (tactic "IntPr.fast_tac 1")
+ apply (tactic "IntPr.fast_tac 1")
+ done
+
+text "Problem 25"
+lemma "?p : (EX x. P(x)) &
+ (ALL x. L(x) --> ~ (M(x) & R(x))) &
+ (ALL x. P(x) --> (M(x) & L(x))) &
+ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
+ --> (EX x. Q(x)&P(x))"
+ by (tactic "IntPr.best_tac 1")
+
+text "Problem 29. Essentially the same as Principia Mathematica *11.71"
+lemma "?p : (EX x. P(x)) & (EX y. Q(y))
+ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <->
+ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
+ by (tactic "IntPr.fast_tac 1")
+
+text "Problem ~~30"
+lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &
+ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
+ --> (ALL x. ~~S(x))"
+ by (tactic "IntPr.fast_tac 1")
+
+text "Problem 31"
+lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &
+ (EX x. L(x) & P(x)) &
+ (ALL x. ~ R(x) --> M(x))
+ --> (EX x. L(x) & M(x))"
+ by (tactic "IntPr.fast_tac 1")
+
+text "Problem 32"
+lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
+ (ALL x. S(x) & R(x) --> L(x)) &
+ (ALL x. M(x) --> R(x))
+ --> (ALL x. P(x) & M(x) --> L(x))"
+ by (tactic "IntPr.best_tac 1") -- slow
+
+text "Problem 39"
+lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
+ by (tactic "IntPr.best_tac 1")
+
+text "Problem 40. AMENDED"
+lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->
+ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
+ by (tactic "IntPr.best_tac 1") -- slow
+
+text "Problem 44"
+lemma "?p : (ALL x. f(x) -->
+ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
+ (EX x. j(x) & (ALL y. g(y) --> h(x,y)))
+ --> (EX x. j(x) & ~f(x))"
+ by (tactic "IntPr.best_tac 1")
+
+text "Problem 48"
+lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+ by (tactic "IntPr.best_tac 1")
+
+text "Problem 51"
+lemma
+ "?p : (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
+ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
+ by (tactic "IntPr.best_tac 1") -- {*60 seconds*}
+
+text "Problem 56"
+lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
+ by (tactic "IntPr.best_tac 1")
+
+text "Problem 57"
+lemma
+ "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
+ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
+ by (tactic "IntPr.best_tac 1")
+
+text "Problem 60"
+lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+ by (tactic "IntPr.best_tac 1")
+
+end
--- a/src/FOLP/ex/ROOT.ML Tue Mar 18 21:57:36 2008 +0100
+++ b/src/FOLP/ex/ROOT.ML Tue Mar 18 22:19:18 2008 +0100
@@ -10,19 +10,15 @@
"Intro",
"Nat",
"Foundation",
- "If"
+ "If",
+ "Intuitionistic",
+ "Classical"
];
-writeln"\n** Intuitionistic examples **\n";
-time_use "int.ML";
-
val thy = theory "IFOLP" and tac = IntPr.fast_tac 1;
time_use "prop.ML";
time_use "quant.ML";
-writeln"\n** Classical examples **\n";
-time_use "cla.ML";
-
val thy = theory "FOLP" and tac = Cla.fast_tac FOLP_cs 1;
time_use "prop.ML";
time_use "quant.ML";
--- a/src/FOLP/ex/cla.ML Tue Mar 18 21:57:36 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,354 +0,0 @@
-(* Title: FOLP/ex/cla
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Classical First-Order Logic.
-*)
-
-goal (theory "FOLP") "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*If and only if*)
-
-goal (theory "FOLP") "?p : (P<->Q) <-> (Q<->P)";
-by (fast_tac FOLP_cs 1);
-result();
-
-goal (theory "FOLP") "?p : ~ (P <-> ~P)";
-by (fast_tac FOLP_cs 1);
-result();
-
-
-(*Sample problems from
- F. J. Pelletier,
- Seventy-Five Problems for Testing Automatic Theorem Provers,
- J. Automated Reasoning 2 (1986), 191-216.
- Errata, JAR 4 (1988), 236-236.
-
-The hardest problems -- judging by experience with several theorem provers,
-including matrix ones -- are 34 and 43.
-*)
-
-writeln"Pelletier's examples";
-(*1*)
-goal (theory "FOLP") "?p : (P-->Q) <-> (~Q --> ~P)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*2*)
-goal (theory "FOLP") "?p : ~ ~ P <-> P";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*3*)
-goal (theory "FOLP") "?p : ~(P-->Q) --> (Q-->P)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*4*)
-goal (theory "FOLP") "?p : (~P-->Q) <-> (~Q --> P)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*5*)
-goal (theory "FOLP") "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*6*)
-goal (theory "FOLP") "?p : P | ~ P";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*7*)
-goal (theory "FOLP") "?p : P | ~ ~ ~ P";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*8. Peirce's law*)
-goal (theory "FOLP") "?p : ((P-->Q) --> P) --> P";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*9*)
-goal (theory "FOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*10*)
-goal (theory "FOLP") "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
-goal (theory "FOLP") "?p : P<->P";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*12. "Dijkstra's law"*)
-goal (theory "FOLP") "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*13. Distributive law*)
-goal (theory "FOLP") "?p : P | (Q & R) <-> (P | Q) & (P | R)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*14*)
-goal (theory "FOLP") "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*15*)
-goal (theory "FOLP") "?p : (P --> Q) <-> (~P | Q)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*16*)
-goal (theory "FOLP") "?p : (P-->Q) | (Q-->P)";
-by (fast_tac FOLP_cs 1);
-result();
-
-(*17*)
-goal (theory "FOLP") "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Classical Logic: examples with quantifiers";
-
-goal (theory "FOLP") "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
-by (fast_tac FOLP_cs 1);
-result();
-
-goal (theory "FOLP") "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
-by (fast_tac FOLP_cs 1);
-result();
-
-goal (theory "FOLP") "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
-by (fast_tac FOLP_cs 1);
-result();
-
-goal (theory "FOLP") "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problems requiring quantifier duplication";
-
-(*Needs multiple instantiation of ALL.*)
-(*
-goal (theory "FOLP") "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))";
-by (best_tac FOLP_dup_cs 1);
-result();
-*)
-(*Needs double instantiation of the quantifier*)
-goal (theory "FOLP") "?p : EX x. P(x) --> P(a) & P(b)";
-by (best_tac FOLP_dup_cs 1);
-result();
-
-goal (theory "FOLP") "?p : EX z. P(z) --> (ALL x. P(x))";
-by (best_tac FOLP_dup_cs 1);
-result();
-
-
-writeln"Hard examples with quantifiers";
-
-writeln"Problem 18";
-goal (theory "FOLP") "?p : EX y. ALL x. P(y)-->P(x)";
-by (best_tac FOLP_dup_cs 1);
-result();
-
-writeln"Problem 19";
-goal (theory "FOLP") "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (best_tac FOLP_dup_cs 1);
-result();
-
-writeln"Problem 20";
-goal (theory "FOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \
-\ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
-by (fast_tac FOLP_cs 1);
-result();
-(*
-writeln"Problem 21";
-goal (theory "FOLP") "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
-by (best_tac FOLP_dup_cs 1);
-result();
-*)
-writeln"Problem 22";
-goal (theory "FOLP") "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 23";
-goal (theory "FOLP") "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))";
-by (best_tac FOLP_cs 1);
-result();
-
-writeln"Problem 24";
-goal (theory "FOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \
-\ (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \
-\ --> (EX x. P(x)&R(x))";
-by (fast_tac FOLP_cs 1);
-result();
-(*
-writeln"Problem 25";
-goal (theory "FOLP") "?p : (EX x. P(x)) & \
-\ (ALL x. L(x) --> ~ (M(x) & R(x))) & \
-\ (ALL x. P(x) --> (M(x) & L(x))) & \
-\ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \
-\ --> (EX x. Q(x)&P(x))";
-by (best_tac FOLP_cs 1);
-result();
-
-writeln"Problem 26";
-goal (theory "FOLP") "?u : ((EX x. p(x)) <-> (EX x. q(x))) & \
-\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
-\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
-by (fast_tac FOLP_cs 1);
-result();
-*)
-writeln"Problem 27";
-goal (theory "FOLP") "?p : (EX x. P(x) & ~Q(x)) & \
-\ (ALL x. P(x) --> R(x)) & \
-\ (ALL x. M(x) & L(x) --> P(x)) & \
-\ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \
-\ --> (ALL x. M(x) --> ~L(x))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 28. AMENDED";
-goal (theory "FOLP") "?p : (ALL x. P(x) --> (ALL x. Q(x))) & \
-\ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \
-\ ((EX x. S(x)) --> (ALL x. L(x) --> M(x))) \
-\ --> (ALL x. P(x) & L(x) --> M(x))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
-goal (theory "FOLP") "?p : (EX x. P(x)) & (EX y. Q(y)) \
-\ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \
-\ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 30";
-goal (theory "FOLP") "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & \
-\ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \
-\ --> (ALL x. S(x))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 31";
-goal (theory "FOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
-\ (EX x. L(x) & P(x)) & \
-\ (ALL x. ~ R(x) --> M(x)) \
-\ --> (EX x. L(x) & M(x))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 32";
-goal (theory "FOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
-\ (ALL x. S(x) & R(x) --> L(x)) & \
-\ (ALL x. M(x) --> R(x)) \
-\ --> (ALL x. P(x) & M(x) --> L(x))";
-by (best_tac FOLP_cs 1);
-result();
-
-writeln"Problem 33";
-goal (theory "FOLP") "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \
-\ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (best_tac FOLP_cs 1);
-result();
-
-writeln"Problem 35";
-goal (theory "FOLP") "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))";
-by (best_tac FOLP_dup_cs 1);
-result();
-
-writeln"Problem 36";
-goal (theory "FOLP")
-"?p : (ALL x. EX y. J(x,y)) & \
-\ (ALL x. EX y. G(x,y)) & \
-\ (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z))) \
-\ --> (ALL x. EX y. H(x,y))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 37";
-goal (theory "FOLP") "?p : (ALL z. EX w. ALL x. EX y. \
-\ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
-\ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
-\ ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) \
-\ --> (ALL x. EX y. R(x,y))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 39";
-goal (theory "FOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 40. AMENDED";
-goal (theory "FOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> \
-\ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 41";
-goal (theory "FOLP") "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \
-\ --> ~ (EX z. ALL x. f(x,z))";
-by (best_tac FOLP_cs 1);
-result();
-
-writeln"Problem 44";
-goal (theory "FOLP") "?p : (ALL x. f(x) --> \
-\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
-\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
-\ --> (EX x. j(x) & ~f(x))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problems (mainly) involving equality or functions";
-
-writeln"Problem 48";
-goal (theory "FOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 50";
-(*What has this to do with equality?*)
-goal (theory "FOLP") "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
-by (best_tac FOLP_dup_cs 1);
-result();
-
-writeln"Problem 56";
-goal (theory "FOLP")
- "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 57";
-goal (theory "FOLP")
-"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
-\ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))";
-by (fast_tac FOLP_cs 1);
-result();
-
-writeln"Problem 58 NOT PROVED AUTOMATICALLY";
-goal (theory "FOLP") "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
-val f_cong = read_instantiate [("t","f")] subst_context;
-by (fast_tac (FOLP_cs addIs [f_cong]) 1);
-result();
-
-writeln"Problem 59";
-goal (theory "FOLP") "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
-by (best_tac FOLP_dup_cs 1);
-result();
-
-writeln"Problem 60";
-goal (theory "FOLP")
-"?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
-by (fast_tac FOLP_cs 1);
-result();
--- a/src/FOLP/ex/int.ML Tue Mar 18 21:57:36 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,361 +0,0 @@
-(* Title: FOLP/ex/int.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Intuitionistic First-Order Logic
-
-Single-step commands:
-by (IntPr.step_tac 1);
-by (biresolve_tac safe_brls 1);
-by (biresolve_tac haz_brls 1);
-by (assume_tac 1);
-by (IntPr.safe_tac 1);
-by (IntPr.mp_tac 1);
-by (IntPr.fast_tac 1);
-*)
-
-(*Note: for PROPOSITIONAL formulae...
- ~A is classically provable iff it is intuitionistically provable.
- Therefore A is classically provable iff ~~A is intuitionistically provable.
-
-Let Q be the conjuction of the propositions A|~A, one for each atom A in
-P. If P is provable classically, then clearly P&Q is provable
-intuitionistically, so ~~(P&Q) is also provable intuitionistically.
-The latter is intuitionistically equivalent to ~~P&~~Q, hence to ~~P,
-since ~~Q is intuitionistically provable. Finally, if P is a negation then
-~~P is intuitionstically equivalent to P. [Andy Pitts]
-*)
-
-goal (theory "IFOLP") "?p : ~~(P&Q) <-> ~~P & ~~Q";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : ~~~P <-> ~P";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : (P<->Q) <-> (Q<->P)";
-by (IntPr.fast_tac 1);
-result();
-
-
-writeln"Lemmas for the propositional double-negation translation";
-
-goal (theory "IFOLP") "?p : P --> ~~P";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : ~~(~~P --> P)";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : ~~P & ~~(P --> Q) --> ~~Q";
-by (IntPr.fast_tac 1);
-result();
-
-
-writeln"The following are classically but not constructively valid.";
-
-(*The attempt to prove them terminates quickly!*)
-goal (theory "IFOLP") "?p : ((P-->Q) --> P) --> P";
-by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
-(*Check that subgoals remain: proof failed.*)
-getgoal 1;
-
-goal (theory "IFOLP") "?p : (P&Q-->R) --> (P-->R) | (Q-->R)";
-by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
-getgoal 1;
-
-
-writeln"Intuitionistic FOL: propositional problems based on Pelletier.";
-
-writeln"Problem ~~1";
-goal (theory "IFOLP") "?p : ~~((P-->Q) <-> (~Q --> ~P))";
-by (IntPr.fast_tac 1);
-result();
-(*5 secs*)
-
-
-writeln"Problem ~~2";
-goal (theory "IFOLP") "?p : ~~(~~P <-> P)";
-by (IntPr.fast_tac 1);
-result();
-(*1 secs*)
-
-
-writeln"Problem 3";
-goal (theory "IFOLP") "?p : ~(P-->Q) --> (Q-->P)";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~4";
-goal (theory "IFOLP") "?p : ~~((~P-->Q) <-> (~Q --> P))";
-by (IntPr.fast_tac 1);
-result();
-(*9 secs*)
-
-writeln"Problem ~~5";
-goal (theory "IFOLP") "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
-by (IntPr.fast_tac 1);
-result();
-(*10 secs*)
-
-
-writeln"Problem ~~6";
-goal (theory "IFOLP") "?p : ~~(P | ~P)";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~7";
-goal (theory "IFOLP") "?p : ~~(P | ~~~P)";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~8. Peirce's law";
-goal (theory "IFOLP") "?p : ~~(((P-->Q) --> P) --> P)";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 9";
-goal (theory "IFOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (IntPr.fast_tac 1);
-result();
-(*9 secs*)
-
-
-writeln"Problem 10";
-goal (theory "IFOLP") "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"11. Proved in each direction (incorrectly, says Pelletier!!) ";
-goal (theory "IFOLP") "?p : P<->P";
-by (IntPr.fast_tac 1);
-
-writeln"Problem ~~12. Dijkstra's law ";
-goal (theory "IFOLP") "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 13. Distributive law";
-goal (theory "IFOLP") "?p : P | (Q & R) <-> (P | Q) & (P | R)";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~14";
-goal (theory "IFOLP") "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~15";
-goal (theory "IFOLP") "?p : ~~((P --> Q) <-> (~P | Q))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~16";
-goal (theory "IFOLP") "?p : ~~((P-->Q) | (Q-->P))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~17";
-goal (theory "IFOLP")
- "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))";
-by (IntPr.fast_tac 1);
-(*over 5 minutes?? -- printing the proof term takes 40 secs!!*)
-result();
-
-
-writeln"** Examples with quantifiers **";
-
-writeln"The converse is classical in the following implications...";
-
-goal (theory "IFOLP") "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)";
-by (IntPr.fast_tac 1);
-result();
-
-goal (theory "IFOLP") "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
-by (IntPr.fast_tac 1);
-result();
-
-
-
-
-writeln"The following are not constructively valid!";
-(*The attempt to prove them terminates quickly!*)
-
-goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
-by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
-getgoal 1;
-
-goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
-by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
-getgoal 1;
-
-goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
-by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
-getgoal 1;
-
-goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
-by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
-getgoal 1;
-
-(*Classically but not intuitionistically valid. Proved by a bug in 1986!*)
-goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))";
-by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";
-getgoal 1;
-
-
-writeln"Hard examples with quantifiers";
-
-(*The ones that have not been proved are not known to be valid!
- Some will require quantifier duplication -- not currently available*)
-
-writeln"Problem ~~18";
-goal (theory "IFOLP") "?p : ~~(EX y. ALL x. P(y)-->P(x))";
-(*NOT PROVED*)
-
-writeln"Problem ~~19";
-goal (theory "IFOLP") "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
-(*NOT PROVED*)
-
-writeln"Problem 20";
-goal (theory "IFOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \
-\ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 21";
-goal (theory "IFOLP")
- "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))";
-(*NOT PROVED*)
-
-writeln"Problem 22";
-goal (theory "IFOLP") "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~23";
-goal (theory "IFOLP") "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))";
-by (IntPr.best_tac 1);
-result();
-
-writeln"Problem 24";
-goal (theory "IFOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \
-\ (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \
-\ --> ~~(EX x. P(x)&R(x))";
-(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
-by IntPr.safe_tac;
-by (etac impE 1);
-by (IntPr.fast_tac 1);
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 25";
-goal (theory "IFOLP") "?p : (EX x. P(x)) & \
-\ (ALL x. L(x) --> ~ (M(x) & R(x))) & \
-\ (ALL x. P(x) --> (M(x) & L(x))) & \
-\ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \
-\ --> (EX x. Q(x)&P(x))";
-by (IntPr.best_tac 1);
-result();
-
-writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
-goal (theory "IFOLP") "?p : (EX x. P(x)) & (EX y. Q(y)) \
-\ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \
-\ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem ~~30";
-goal (theory "IFOLP") "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
-\ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \
-\ --> (ALL x. ~~S(x))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 31";
-goal (theory "IFOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
-\ (EX x. L(x) & P(x)) & \
-\ (ALL x. ~ R(x) --> M(x)) \
-\ --> (EX x. L(x) & M(x))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 32";
-goal (theory "IFOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
-\ (ALL x. S(x) & R(x) --> L(x)) & \
-\ (ALL x. M(x) --> R(x)) \
-\ --> (ALL x. P(x) & M(x) --> L(x))";
-by (IntPr.best_tac 1); (*SLOW*)
-result();
-
-writeln"Problem 39";
-goal (theory "IFOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 40. AMENDED";
-goal (theory "IFOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> \
-\ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 44";
-goal (theory "IFOLP") "?p : (ALL x. f(x) --> \
-\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
-\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
-\ --> (EX x. j(x) & ~f(x))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 48";
-goal (theory "IFOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 51";
-goal (theory "IFOLP")
- "?p : (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \
-\ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
-by (IntPr.best_tac 1); (*60 seconds*)
-result();
-
-writeln"Problem 56";
-goal (theory "IFOLP")
- "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 57";
-goal (theory "IFOLP")
- "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
-\ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))";
-by (IntPr.fast_tac 1);
-result();
-
-writeln"Problem 60";
-goal (theory "IFOLP")
- "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
-by (IntPr.fast_tac 1);
-result();
--- a/src/FOLP/intprover.ML Tue Mar 18 21:57:36 2008 +0100
+++ b/src/FOLP/intprover.ML Tue Mar 18 22:19:18 2008 +0100
@@ -36,17 +36,17 @@
step of an intuitionistic proof.
*)
val safe_brls = sort (make_ord lessb)
- [ (true,FalseE), (false,TrueI), (false,refl),
- (false,impI), (false,notI), (false,allI),
- (true,conjE), (true,exE),
- (false,conjI), (true,conj_impE),
- (true,disj_impE), (true,disjE),
- (false,iffI), (true,iffE), (true,not_to_imp) ];
+ [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}),
+ (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
+ (true, @{thm conjE}), (true, @{thm exE}),
+ (false, @{thm conjI}), (true, @{thm conj_impE}),
+ (true, @{thm disj_impE}), (true, @{thm disjE}),
+ (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
val haz_brls =
- [ (false,disjI1), (false,disjI2), (false,exI),
- (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
- (true,all_impE), (true,ex_impE), (true,impE) ];
+ [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
+ (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
+ (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
(*0 subgoals vs 1 or more: the p in safep is for positive*)
val (safe0_brls, safep_brls) =
@@ -76,4 +76,3 @@
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
end;
-
--- a/src/FOLP/simpdata.ML Tue Mar 18 21:57:36 2008 +0100
+++ b/src/FOLP/simpdata.ML Tue Mar 18 22:19:18 2008 +0100
@@ -6,86 +6,39 @@
Simplification data for FOLP.
*)
-(*** Rewrite rules ***)
-fun int_prove_fun_raw s =
- (writeln s; prove_goal (the_context ()) s
- (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
-
-fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
-
-val conj_rews = map int_prove_fun
- ["P & True <-> P", "True & P <-> P",
- "P & False <-> False", "False & P <-> False",
- "P & P <-> P",
- "P & ~P <-> False", "~P & P <-> False",
- "(P & Q) & R <-> P & (Q & R)"];
-
-val disj_rews = map int_prove_fun
- ["P | True <-> True", "True | P <-> True",
- "P | False <-> P", "False | P <-> P",
- "P | P <-> P",
- "(P | Q) | R <-> P | (Q | R)"];
-
-val not_rews = map int_prove_fun
- ["~ False <-> True", "~ True <-> False"];
+fun make_iff_T th = th RS @{thm P_Imp_P_iff_T};
-val imp_rews = map int_prove_fun
- ["(P --> False) <-> ~P", "(P --> True) <-> True",
- "(False --> P) <-> True", "(True --> P) <-> P",
- "(P --> P) <-> True", "(P --> ~P) <-> ~P"];
-
-val iff_rews = map int_prove_fun
- ["(True <-> P) <-> P", "(P <-> True) <-> P",
- "(P <-> P) <-> True",
- "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
-
-val quant_rews = map int_prove_fun
- ["(ALL x. P) <-> P", "(EX x. P) <-> P"];
+val refl_iff_T = make_iff_T @{thm refl};
-(*These are NOT supplied by default!*)
-val distrib_rews = map int_prove_fun
- ["~(P|Q) <-> ~P & ~Q",
- "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
- "(P | Q --> R) <-> (P --> R) & (Q --> R)",
- "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
- "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
- "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
- "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
-
-val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
-
-fun make_iff_T th = th RS P_Imp_P_iff_T;
-
-val refl_iff_T = make_iff_T refl;
-
-val norm_thms = [(norm_eq RS sym, norm_eq),
- (NORM_iff RS iff_sym, NORM_iff)];
+val norm_thms = [(@{thm norm_eq} RS @{thm sym}, @{thm norm_eq}),
+ (@{thm NORM_iff} RS @{thm iff_sym}, @{thm NORM_iff})];
(* Conversion into rewrite rules *)
-val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
-
fun mk_eq th = case concl_of th of
- _ $ (Const("op <->",_)$_$_) $ _ => th
- | _ $ (Const("op =",_)$_$_) $ _ => th
- | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
+ _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
+ | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
+ | _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
| _ => make_iff_T th;
val mksimps_pairs =
- [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
- ("All", [spec]), ("True", []), ("False", [])];
+ [(@{const_name "op -->"}, [@{thm mp}]),
+ (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ (@{const_name "All"}, [@{thm spec}]),
+ (@{const_name True}, []),
+ (@{const_name False}, [])];
fun mk_atomize pairs =
let fun atoms th =
(case concl_of th of
- Const("Trueprop",_) $ p =>
+ Const ("Trueprop", _) $ p =>
(case head_of p of
Const(a,_) =>
(case AList.lookup (op =) pairs a of
- SOME(rls) => List.concat (map atoms ([th] RL rls))
+ SOME(rls) => maps atoms ([th] RL rls)
| NONE => [th])
| _ => [th])
| _ => [th])
@@ -95,47 +48,40 @@
(*destruct function for analysing equations*)
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
- | dest_red t = raise TERM("FOL/dest_red", [t]);
+ | dest_red t = raise TERM("dest_red", [t]);
structure FOLP_SimpData : SIMP_DATA =
- struct
- val refl_thms = [refl, iff_refl]
- val trans_thms = [trans, iff_trans]
- val red1 = iffD1
- val red2 = iffD2
+struct
+ val refl_thms = [@{thm refl}, @{thm iff_refl}]
+ val trans_thms = [@{thm trans}, @{thm iff_trans}]
+ val red1 = @{thm iffD1}
+ val red2 = @{thm iffD2}
val mk_rew_rules = mk_rew_rules
val case_splits = [] (*NO IF'S!*)
val norm_thms = norm_thms
- val subst_thms = [subst];
+ val subst_thms = [@{thm subst}];
val dest_red = dest_red
- end;
+end;
structure FOLP_Simp = SimpFun(FOLP_SimpData);
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
val FOLP_congs =
- [all_cong,ex_cong,eq_cong,
- conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
+ [@{thm all_cong}, @{thm ex_cong}, @{thm eq_cong},
+ @{thm conj_cong}, @{thm disj_cong}, @{thm imp_cong},
+ @{thm iff_cong}, @{thm not_cong}] @ @{thms pred_congs};
val IFOLP_rews =
- [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
- imp_rews @ iff_rews @ quant_rews;
+ [refl_iff_T] @ @{thms conj_rews} @ @{thms disj_rews} @ @{thms not_rews} @
+ @{thms imp_rews} @ @{thms iff_rews} @ @{thms quant_rews};
open FOLP_Simp;
-val auto_ss = empty_ss setauto ares_tac [TrueI];
+val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
-(*Classical version...*)
-fun prove_fun s =
- (writeln s; prove_goal (the_context ()) s
- (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
-val cla_rews = map prove_fun
- ["?p:P | ~P", "?p:~P | P",
- "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"];
-
-val FOLP_rews = IFOLP_rews@cla_rews;
+val FOLP_rews = IFOLP_rews @ @{thms cla_rews};
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;