--- a/src/FOLP/FOLP.ML Sat Sep 17 20:49:14 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(* Title: FOLP/FOLP.ML
- ID: $Id$
- Author: Martin D Coen, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
-*)
-
-(*** Classical introduction rules for | and EX ***)
-
-val prems= goal FOLP.thy
- "(!!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 FOLP.thy
- "( !!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 FOLP.thy
- "(!!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 FOLP.thy "?p : ~P | P"
- (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
-
-
-(*** Special elimination rules *)
-
-
-(*Classical implies (-->) elimination. *)
-val major::prems= goal FOLP.thy
- "[| 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 FOLP.thy [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 FOLP.thy
- "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/FOLP.thy Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/FOLP.thy Sun Sep 18 14:25:48 2005 +0200
@@ -2,13 +2,88 @@
ID: $Id$
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-Classical First-Order Logic with Proofs
*)
-FOLP = IFOLP +
+header {* Classical First-Order Logic with Proofs *}
+
+theory FOLP
+imports IFOLP
+uses
+ ("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")
+ ("simp.ML") ("intprover.ML") ("simpdata.ML")
+begin
+
consts
cla :: "[p=>p]=>p"
-rules
- classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+axioms
+ classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+use "FOLP_lemmas.ML"
+
+use "hypsubst.ML"
+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 (the_context ())
+ "[| 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 (the_context ())
+ "!!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
+ val sizef = size_of_thm
+ val mp = mp
+ val not_elim = notE
+ val swap = swap
+ val hyp_subst_tacs=[hyp_subst_tac]
+ end;
+
+structure Cla = ClassicalFun(Classical_Data);
+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 [refl,TrueI,conjI,disjCI,impI,notI,iffI]
+ addSEs [conjE,disjE,impCE,FalseE,iffE];
+
+(*Quantifier rules*)
+val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
+ addSEs [exE,ex1E] addEs [allE];
+
+val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
+ addSEs [exE,ex1E] addEs [all_dupE];
+
+*}
+
+use "simpdata.ML"
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/FOLP_lemmas.ML Sun Sep 18 14:25:48 2005 +0200
@@ -0,0 +1,73 @@
+(* Title: FOLP/FOLP.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 Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IFOLP.ML Sun Sep 18 14:25:48 2005 +0200
@@ -2,29 +2,28 @@
ID: $Id$
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
+*)
-Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
-*)
(*** Sequent-style elimination rules for & --> and ALL ***)
-val prems= Goal
+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
+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
+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
+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)) ;
@@ -33,16 +32,16 @@
(*** Negation rules, which translate between ~P and P-->False ***)
-val notI = prove_goalw IFOLP.thy [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P"
+val notI = prove_goalw (the_context ()) [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P"
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
-val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P; q:P |] ==> ?p:R"
+val 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
+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";
@@ -65,7 +64,7 @@
(** Unique assumption tactic.
Ignores proof objects.
- Fails unless one assumption is equal and exactly one is unifiable
+ Fails unless one assumption is equal and exactly one is unifiable
**)
local
@@ -76,7 +75,7 @@
(fn (prem,i) =>
let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
and concl = discard_proof (Logic.strip_assums_concl prem)
- in
+ in
if exists (fn hyp => hyp aconv concl) hyps
then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
[_] => assume_tac i
@@ -97,22 +96,22 @@
(*** If-and-only-if ***)
-val iffI = prove_goalw IFOLP.thy [iff_def]
+val 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) *)
-val iffE = prove_goalw IFOLP.thy [iff_def]
+val 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 *)
-val iffD1 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q; q:P |] ==> ?p:Q"
+val 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)) ]);
-val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q; q:Q |] ==> ?p:P"
+val 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";
@@ -137,12 +136,12 @@
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
***)
-val prems = goalw IFOLP.thy [ex1_def]
+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 IFOLP.thy [ex1_def]
+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";
@@ -158,7 +157,7 @@
resolve_tac (prems RL [iffE]) i THEN
REPEAT1 (eresolve_tac [asm_rl,mp] i);
-val conj_cong = prove_goal IFOLP.thy
+val 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),
@@ -166,7 +165,7 @@
ORELSE eresolve_tac [iffE,conjE,mp] 1
ORELSE iff_tac prems 1)) ]);
-val disj_cong = prove_goal IFOLP.thy
+val disj_cong = prove_goal (the_context ())
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -174,7 +173,7 @@
ORELSE ares_tac [iffI] 1
ORELSE mp_tac 1)) ]);
-val imp_cong = prove_goal IFOLP.thy
+val 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),
@@ -182,7 +181,7 @@
ORELSE etac iffE 1
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]);
-val iff_cong = prove_goal IFOLP.thy
+val iff_cong = prove_goal (the_context ())
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -190,7 +189,7 @@
ORELSE ares_tac [iffI] 1
ORELSE mp_tac 1)) ]);
-val not_cong = prove_goal IFOLP.thy
+val not_cong = prove_goal (the_context ())
"p:P <-> P' ==> ?p:~P <-> ~P'"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -198,14 +197,14 @@
ORELSE mp_tac 1
ORELSE eresolve_tac [iffE,notE] 1)) ]);
-val all_cong = prove_goal IFOLP.thy
+val 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)) ]);
-val ex_cong = prove_goal IFOLP.thy
+val 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
@@ -213,7 +212,7 @@
ORELSE iff_tac prems 1)) ]);
(*NOT PROVED
-val ex1_cong = prove_goal IFOLP.thy
+val 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
@@ -225,8 +224,8 @@
val refl = ieqI;
-val subst = prove_goal IFOLP.thy "[| p:a=b; q:P(a) |] ==> ?p : P(b)"
- (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),
+val 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";
@@ -235,7 +234,7 @@
qed "sym";
Goal "[| p:a=b; q:b=c |] ==> ?d:a=c";
-by (etac subst 1 THEN assume_tac 1);
+by (etac subst 1 THEN assume_tac 1);
qed "trans";
(** ~ b=a ==> ~ a=b **)
@@ -263,12 +262,12 @@
qed "subst_context";
Goal "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)";
-by (REPEAT (etac ssubst 1));
+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 (REPEAT (etac ssubst 1));
by (rtac refl 1) ;
qed "subst_context3";
@@ -309,8 +308,8 @@
(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
-val pred_congs =
- List.concat (map (fn c =>
+val pred_congs =
+ List.concat (map (fn c =>
map (fn th => read_instantiate [("P",c)] th)
[pred1_cong,pred2_cong,pred3_cong])
(explode"PQRS"));
@@ -321,30 +320,30 @@
(*** 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
+ 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
+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
+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.
+(*Simplifies the implication. Classical version is stronger.
Still UNSAFE since Q must be provable -- backtracking needed. *)
-val major::prems= Goal
+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.
+(*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";
@@ -352,20 +351,20 @@
qed "not_impE";
(*Simplifies the implication. UNSAFE. *)
-val major::prems= Goal
+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
+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
+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 Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IFOLP.thy Sun Sep 18 14:25:48 2005 +0200
@@ -2,30 +2,32 @@
ID: $Id$
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-Intuitionistic First-Order Logic with Proofs
*)
-IFOLP = Pure +
+header {* Intuitionistic First-Order Logic with Proofs *}
+
+theory IFOLP
+imports Pure
+begin
global
-classes term
-default term
+classes "term"
+defaultsort "term"
-types
- p
- o
+typedecl p
+typedecl o
-consts
+consts
(*** Judgements ***)
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5)
Proof :: "[o,p]=>prop"
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)
-
+
(*** Logical Connectives -- Type Formers ***)
"=" :: "['a,'a] => o" (infixl 50)
- True,False :: "o"
+ True :: "o"
+ False :: "o"
Not :: "o => o" ("~ _" [40] 40)
"&" :: "[o,o] => o" (infixr 35)
"|" :: "[o,o] => o" (infixr 30)
@@ -42,10 +44,12 @@
(*** Proof Term Formers: precedence must exceed 50 ***)
tt :: "p"
contr :: "p=>p"
- fst,snd :: "p=>p"
+ fst :: "p=>p"
+ snd :: "p=>p"
pair :: "[p,p]=>p" ("(1<_,/_>)")
split :: "[p, [p,p]=>p] =>p"
- inl,inr :: "p=>p"
+ inl :: "p=>p"
+ inr :: "p=>p"
when :: "[p, p=>p, p=>p]=>p"
lambda :: "(p => p) => p" (binder "lam " 55)
"`" :: "[p,p]=>p" (infixl 60)
@@ -55,98 +59,103 @@
xsplit :: "[p,['a,p]=>p]=>p"
ideq :: "'a=>p"
idpeel :: "[p,'a=>p]=>p"
- nrm, NRM :: "p"
+ nrm :: p
+ NRM :: p
local
-rules
+ML {*
+
+(*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] =
+ if !show_proofs then Const("@Proof",dummyT) $ p $ P
+ else P (*this case discards the proof term*);
+*}
+
+parse_translation {* [("@Proof", proof_tr)] *}
+print_translation {* [("Proof", proof_tr')] *}
+
+axioms
(**** Propositional logic ****)
(*Equality*)
(* Like Intensional Equality in MLTT - but proofs distinct from terms *)
-ieqI "ideq(a) : a=a"
-ieqE "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
+ieqI: "ideq(a) : a=a"
+ieqE: "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
(* Truth and Falsity *)
-TrueI "tt : True"
-FalseE "a:False ==> contr(a):P"
+TrueI: "tt : True"
+FalseE: "a:False ==> contr(a):P"
(* Conjunction *)
-conjI "[| a:P; b:Q |] ==> <a,b> : P&Q"
-conjunct1 "p:P&Q ==> fst(p):P"
-conjunct2 "p:P&Q ==> snd(p):Q"
+conjI: "[| a:P; b:Q |] ==> <a,b> : P&Q"
+conjunct1: "p:P&Q ==> fst(p):P"
+conjunct2: "p:P&Q ==> snd(p):Q"
(* Disjunction *)
-disjI1 "a:P ==> inl(a):P|Q"
-disjI2 "b:Q ==> inr(b):P|Q"
-disjE "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R
- |] ==> when(a,f,g):R"
+disjI1: "a:P ==> inl(a):P|Q"
+disjI2: "b:Q ==> inr(b):P|Q"
+disjE: "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R
+ |] ==> when(a,f,g):R"
(* Implication *)
-impI "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
-mp "[| f:P-->Q; a:P |] ==> f`a:Q"
+impI: "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
+mp: "[| f:P-->Q; a:P |] ==> f`a:Q"
(*Quantifiers*)
-allI "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
-spec "(f:ALL x. P(x)) ==> f^x : P(x)"
+allI: "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
+spec: "(f:ALL x. P(x)) ==> f^x : P(x)"
-exI "p : P(x) ==> [x,p] : EX x. P(x)"
-exE "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
+exI: "p : P(x) ==> [x,p] : EX x. P(x)"
+exE: "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
(**** Equality between proofs ****)
-prefl "a : P ==> a = a : P"
-psym "a = b : P ==> b = a : P"
-ptrans "[| a = b : P; b = c : P |] ==> a = c : P"
+prefl: "a : P ==> a = a : P"
+psym: "a = b : P ==> b = a : P"
+ptrans: "[| a = b : P; b = c : P |] ==> a = c : P"
-idpeelB "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
+idpeelB: "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
-fstB "a:P ==> fst(<a,b>) = a : P"
-sndB "b:Q ==> snd(<a,b>) = b : Q"
-pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
+fstB: "a:P ==> fst(<a,b>) = a : P"
+sndB: "b:Q ==> snd(<a,b>) = b : Q"
+pairEC: "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
-whenBinl "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
-whenBinr "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
-plusEC "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
+whenBinl: "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
+whenBinr: "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
+plusEC: "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
-applyB "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
-funEC "f:P ==> f = lam x. f`x : P"
+applyB: "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
+funEC: "f:P ==> f = lam x. f`x : P"
-specB "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
+specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
(**** Definitions ****)
-not_def "~P == P-->False"
-iff_def "P<->Q == (P-->Q) & (Q-->P)"
+not_def: "~P == P-->False"
+iff_def: "P<->Q == (P-->Q) & (Q-->P)"
(*Unique existence*)
-ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
(*Rewriting -- special constants to flag normalized terms and formulae*)
-norm_eq "nrm : norm(x) = x"
-NORM_iff "NRM : NORM(P) <-> P"
+norm_eq: "nrm : norm(x) = x"
+NORM_iff: "NRM : NORM(P) <-> P"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
-ML
-(*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] =
- if !show_proofs then Const("@Proof",dummyT) $ p $ P
- else P (*this case discards the proof term*);
-
-val parse_translation = [("@Proof", proof_tr)];
-val print_translation = [("Proof", proof_tr')];
-
--- a/src/FOLP/IsaMakefile Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IsaMakefile Sun Sep 18 14:25:48 2005 +0200
@@ -26,7 +26,7 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
+$(OUT)/FOLP: $(OUT)/Pure FOLP_lemmas.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
--- a/src/FOLP/ROOT.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
@@ -1,4 +1,4 @@
-(* Title: FOLP/ROOT
+(* Title: FOLP/ROOT.ML
ID: $Id$
Author: martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -9,72 +9,6 @@
*)
val banner = "First-Order Logic with Natural Deduction with Proof Terms";
-
writeln banner;
-print_depth 1;
-
-use_thy "IFOLP";
use_thy "FOLP";
-
-use "hypsubst.ML";
-use "classical.ML"; (* Patched 'cos matching won't instantiate proof *)
-use "simp.ML"; (* Patched 'cos matching won't instantiate proof *)
-
-
-(*** 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 IFOLP.thy
- "[| 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 IFOLP.thy
- "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
- end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-open Hypsubst;
-
-use "intprover.ML";
-
-(*** Applying ClassicalFun to create a classical prover ***)
-structure Classical_Data =
- struct
- val sizef = size_of_thm
- val mp = mp
- val not_elim = notE
- val swap = swap
- val hyp_subst_tacs=[hyp_subst_tac]
- end;
-
-structure Cla = ClassicalFun(Classical_Data);
-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 [refl,TrueI,conjI,disjCI,impI,notI,iffI]
- addSEs [conjE,disjE,impCE,FalseE,iffE];
-
-(*Quantifier rules*)
-val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
- addSEs [exE,ex1E] addEs [allE];
-
-val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
- addSEs [exE,ex1E] addEs [all_dupE];
-
-use "simpdata.ML";
-
-
-print_depth 8;
--- a/src/FOLP/ex/If.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/If.ML Sun Sep 18 14:25:48 2005 +0200
@@ -1,20 +1,15 @@
-(* Title: FOLP/ex/if
+(* Title: FOLP/ex/If.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-
-For ex/if.thy. First-Order Logic: the 'if' example
*)
-open If;
-open Cla; (*in case structure Int is open!*)
-
-val prems = goalw If.thy [if_def]
+val prems = goalw (the_context ()) [if_def]
"[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
by (fast_tac (FOLP_cs addIs prems) 1);
val ifI = result();
-val major::prems = goalw If.thy [if_def]
+val major::prems = goalw (the_context ()) [if_def]
"[| p:if(P,Q,R); !!x y.[| x:P; y:Q |] ==> f(x,y):S; \
\ !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S";
by (cut_facts_tac [major] 1);
@@ -39,5 +34,3 @@
Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
by (fast_tac if_cs 1);
val nested_ifs = result();
-
-writeln"Reached end of file.";
--- a/src/FOLP/ex/If.thy Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/If.thy Sun Sep 18 14:25:48 2005 +0200
@@ -1,5 +1,13 @@
-If = FOLP +
-consts if :: "[o,o,o]=>o"
-rules
- if_def "if(P,Q,R) == P&Q | ~P&R"
+(* $Id$ *)
+
+theory If
+imports FOLP
+begin
+
+constdefs
+ if :: "[o,o,o]=>o"
+ "if(P,Q,R) == P&Q | ~P&R"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/FOLP/ex/Nat.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/Nat.ML Sun Sep 18 14:25:48 2005 +0200
@@ -2,17 +2,8 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-Examples for the manual "Introduction to Isabelle"
-
-Proofs about the natural numbers
-
-To generate similar output to manual, execute these commands:
- Pretty.setmargin 72; print_depth 0;
*)
-open Nat;
-
Goal "?p : ~ (Suc(k) = k)";
by (res_inst_tac [("n","k")] induct 1);
by (rtac notI 1);
@@ -42,23 +33,23 @@
val add_Suc = result();
(*
-val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
+val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];
prths nat_congs;
*)
-val prems = goal Nat.thy "p: x=y ==> ?p : Suc(x) = Suc(y)";
+val prems = goal (the_context ()) "p: x=y ==> ?p : Suc(x) = Suc(y)";
by (resolve_tac (prems RL [subst]) 1);
by (rtac refl 1);
val Suc_cong = result();
-val prems = goal Nat.thy "[| p : a=x; q: b=y |] ==> ?p : a+b=x+y";
-by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
+val prems = goal (the_context ()) "[| p : a=x; q: b=y |] ==> ?p : a+b=x+y";
+by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
rtac refl 1);
val Plus_cong = result();
val nat_congs = [Suc_cong,Plus_cong];
-val add_ss = FOLP_ss addcongs nat_congs
+val add_ss = FOLP_ss addcongs nat_congs
addrews [add_0, add_Suc];
Goal "?p : (k+m)+n = k+(m+n)";
@@ -79,4 +70,3 @@
val add_Suc_right = result();
(*mk_typed_congs appears not to work with FOLP's version of subst*)
-
--- a/src/FOLP/ex/Nat.thy Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/Nat.thy Sun Sep 18 14:25:48 2005 +0200
@@ -2,15 +2,16 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-Examples for the manual "Introduction to Isabelle"
-
-Theory of the natural numbers: Peano's axioms, primitive recursion
*)
-Nat = IFOLP +
-types nat
-arities nat :: term
+header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+
+theory Nat
+imports FOLP
+begin
+
+typedecl nat
+arities nat :: "term"
consts "0" :: "nat" ("0")
Suc :: "nat=>nat"
rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
@@ -18,19 +19,24 @@
(*Proof terms*)
nrec :: "[nat,p,[nat,p]=>p]=>p"
- ninj,nneq :: "p=>p"
- rec0, recSuc :: "p"
+ ninj :: "p=>p"
+ nneq :: "p=>p"
+ rec0 :: "p"
+ recSuc :: "p"
+
+axioms
+ induct: "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
+ |] ==> nrec(n,b,c):P(n)"
-rules
- induct "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
- |] ==> nrec(n,b,c):P(n)"
-
- Suc_inject "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
- Suc_neq_0 "p:Suc(m)=0 ==> nneq(p) : R"
- rec_0 "rec0 : rec(0,a,f) = a"
- rec_Suc "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
- add_def "m+n == rec(m, n, %x y. Suc(y))"
+ Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
+ Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R"
+ rec_0: "rec0 : rec(0,a,f) = a"
+ rec_Suc: "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
+ add_def: "m+n == rec(m, n, %x y. Suc(y))"
- nrecB0 "b: A ==> nrec(0,b,c) = b : A"
- nrecBSuc "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
+ nrecB0: "b: A ==> nrec(0,b,c) = b : A"
+ nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/FOLP/ex/ROOT.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
@@ -1,9 +1,9 @@
-(* Title: FOLP/ex/ROOT
+(* Title: FOLP/ex/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Executes all examples for First-Order Logic.
+Examples for First-Order Logic.
*)
time_use "intro.ML";
@@ -13,7 +13,7 @@
writeln"\n** Intuitionistic examples **\n";
time_use "int.ML";
-val thy = IFOLP.thy and tac = IntPr.fast_tac 1;
+val thy = theory "IFOLP" and tac = IntPr.fast_tac 1;
time_use "prop.ML";
time_use "quant.ML";
@@ -21,6 +21,6 @@
time_use "cla.ML";
time_use_thy "If";
-val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1;
+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 Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/cla.ML Sun Sep 18 14:25:48 2005 +0200
@@ -3,24 +3,20 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Classical First-Order Logic
+Classical First-Order Logic.
*)
-writeln"File FOLP/ex/cla.ML";
-
-open Cla; (*in case structure Int is open!*)
-
-goal FOLP.thy "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
+goal (theory "FOLP") "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
by (fast_tac FOLP_cs 1);
result();
(*If and only if*)
-goal FOLP.thy "?p : (P<->Q) <-> (Q<->P)";
+goal (theory "FOLP") "?p : (P<->Q) <-> (Q<->P)";
by (fast_tac FOLP_cs 1);
result();
-goal FOLP.thy "?p : ~ (P <-> ~P)";
+goal (theory "FOLP") "?p : ~ (P <-> ~P)";
by (fast_tac FOLP_cs 1);
result();
@@ -37,105 +33,105 @@
writeln"Pelletier's examples";
(*1*)
-goal FOLP.thy "?p : (P-->Q) <-> (~Q --> ~P)";
+goal (theory "FOLP") "?p : (P-->Q) <-> (~Q --> ~P)";
by (fast_tac FOLP_cs 1);
result();
(*2*)
-goal FOLP.thy "?p : ~ ~ P <-> P";
+goal (theory "FOLP") "?p : ~ ~ P <-> P";
by (fast_tac FOLP_cs 1);
result();
(*3*)
-goal FOLP.thy "?p : ~(P-->Q) --> (Q-->P)";
+goal (theory "FOLP") "?p : ~(P-->Q) --> (Q-->P)";
by (fast_tac FOLP_cs 1);
result();
(*4*)
-goal FOLP.thy "?p : (~P-->Q) <-> (~Q --> P)";
+goal (theory "FOLP") "?p : (~P-->Q) <-> (~Q --> P)";
by (fast_tac FOLP_cs 1);
result();
(*5*)
-goal FOLP.thy "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
+goal (theory "FOLP") "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
by (fast_tac FOLP_cs 1);
result();
(*6*)
-goal FOLP.thy "?p : P | ~ P";
+goal (theory "FOLP") "?p : P | ~ P";
by (fast_tac FOLP_cs 1);
result();
(*7*)
-goal FOLP.thy "?p : P | ~ ~ ~ P";
+goal (theory "FOLP") "?p : P | ~ ~ ~ P";
by (fast_tac FOLP_cs 1);
result();
(*8. Peirce's law*)
-goal FOLP.thy "?p : ((P-->Q) --> P) --> P";
+goal (theory "FOLP") "?p : ((P-->Q) --> P) --> P";
by (fast_tac FOLP_cs 1);
result();
(*9*)
-goal FOLP.thy "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+goal (theory "FOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
by (fast_tac FOLP_cs 1);
result();
(*10*)
-goal FOLP.thy "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
+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 FOLP.thy "?p : P<->P";
+goal (theory "FOLP") "?p : P<->P";
by (fast_tac FOLP_cs 1);
result();
(*12. "Dijkstra's law"*)
-goal FOLP.thy "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))";
+goal (theory "FOLP") "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))";
by (fast_tac FOLP_cs 1);
result();
(*13. Distributive law*)
-goal FOLP.thy "?p : P | (Q & R) <-> (P | Q) & (P | R)";
+goal (theory "FOLP") "?p : P | (Q & R) <-> (P | Q) & (P | R)";
by (fast_tac FOLP_cs 1);
result();
(*14*)
-goal FOLP.thy "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
+goal (theory "FOLP") "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
by (fast_tac FOLP_cs 1);
result();
(*15*)
-goal FOLP.thy "?p : (P --> Q) <-> (~P | Q)";
+goal (theory "FOLP") "?p : (P --> Q) <-> (~P | Q)";
by (fast_tac FOLP_cs 1);
result();
(*16*)
-goal FOLP.thy "?p : (P-->Q) | (Q-->P)";
+goal (theory "FOLP") "?p : (P-->Q) | (Q-->P)";
by (fast_tac FOLP_cs 1);
result();
(*17*)
-goal FOLP.thy "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
+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 FOLP.thy "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
+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 FOLP.thy "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
+goal (theory "FOLP") "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
by (fast_tac FOLP_cs 1);
result();
-goal FOLP.thy "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
+goal (theory "FOLP") "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
by (fast_tac FOLP_cs 1);
result();
-goal FOLP.thy "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
+goal (theory "FOLP") "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
by (fast_tac FOLP_cs 1);
result();
@@ -143,16 +139,16 @@
(*Needs multiple instantiation of ALL.*)
(*
-goal FOLP.thy "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))";
+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 FOLP.thy "?p : EX x. P(x) --> P(a) & P(b)";
+goal (theory "FOLP") "?p : EX x. P(x) --> P(a) & P(b)";
by (best_tac FOLP_dup_cs 1);
result();
-goal FOLP.thy "?p : EX z. P(z) --> (ALL x. P(x))";
+goal (theory "FOLP") "?p : EX z. P(z) --> (ALL x. P(x))";
by (best_tac FOLP_dup_cs 1);
result();
@@ -160,45 +156,45 @@
writeln"Hard examples with quantifiers";
writeln"Problem 18";
-goal FOLP.thy "?p : EX y. ALL x. P(y)-->P(x)";
+goal (theory "FOLP") "?p : EX y. ALL x. P(y)-->P(x)";
by (best_tac FOLP_dup_cs 1);
result();
writeln"Problem 19";
-goal FOLP.thy "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
+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 FOLP.thy "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \
+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 FOLP.thy "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
+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 FOLP.thy "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))";
+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 FOLP.thy "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))";
+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 FOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \
+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 FOLP.thy "?p : (EX x. P(x)) & \
+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))) \
@@ -207,14 +203,14 @@
result();
writeln"Problem 26";
-goal FOLP.thy "?u : ((EX x. p(x)) <-> (EX x. q(x))) & \
+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 FOLP.thy "?p : (EX x. P(x) & ~Q(x)) & \
+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))) \
@@ -223,7 +219,7 @@
result();
writeln"Problem 28. AMENDED";
-goal FOLP.thy "?p : (ALL x. P(x) --> (ALL x. Q(x))) & \
+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))";
@@ -231,21 +227,21 @@
result();
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
-goal FOLP.thy "?p : (EX x. P(x)) & (EX y. Q(y)) \
+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 FOLP.thy "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & \
+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 FOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
+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))";
@@ -253,7 +249,7 @@
result();
writeln"Problem 32";
-goal FOLP.thy "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
+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))";
@@ -261,18 +257,18 @@
result();
writeln"Problem 33";
-goal FOLP.thy "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \
+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 FOLP.thy "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))";
+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 FOLP.thy
+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))) \
@@ -281,7 +277,7 @@
result();
writeln"Problem 37";
-goal FOLP.thy "?p : (ALL z. EX w. ALL x. EX y. \
+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))) \
@@ -290,24 +286,24 @@
result();
writeln"Problem 39";
-goal FOLP.thy "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+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 FOLP.thy "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> \
+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 FOLP.thy "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \
+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 FOLP.thy "?p : (ALL x. f(x) --> \
+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))";
@@ -317,44 +313,42 @@
writeln"Problems (mainly) involving equality or functions";
writeln"Problem 48";
-goal FOLP.thy "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
+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 FOLP.thy "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
+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 FOLP.thy
+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 FOLP.thy
+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 FOLP.thy "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
+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 FOLP.thy "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
+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 FOLP.thy
+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();
-
-writeln"Reached end of file.";
--- a/src/FOLP/ex/foundn.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/foundn.ML Sun Sep 18 14:25:48 2005 +0200
@@ -6,9 +6,7 @@
Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
*)
-writeln"File FOLP/ex/foundn.ML";
-
-goal IFOLP.thy "?p : A&B --> (C-->A&C)";
+goal (theory "IFOLP") "?p : A&B --> (C-->A&C)";
by (rtac impI 1);
by (rtac impI 1);
by (rtac conjI 1);
@@ -19,7 +17,7 @@
(*A form of conj-elimination*)
val prems =
-goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A; y:B |] ==> f(x,y):C) ==> ?p:C";
+goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A; y:B |] ==> f(x,y):C) ==> ?p:C";
by (resolve_tac prems 1);
by (rtac conjunct1 1);
by (resolve_tac prems 1);
@@ -29,7 +27,7 @@
val prems =
-goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
+goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
by (rtac notI 1);
by (res_inst_tac [ ("P", "~B") ] notE 1);
@@ -47,7 +45,7 @@
val prems =
-goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
+goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
by (rtac notI 1);
by (rtac notE 1);
@@ -61,7 +59,7 @@
val prems =
-goal IFOLP.thy "[| p:A | ~A; q:~ ~A |] ==> ?p:A";
+goal (theory "IFOLP") "[| p:A | ~A; q:~ ~A |] ==> ?p:A";
by (rtac disjE 1);
by (resolve_tac prems 1);
by (assume_tac 1);
@@ -75,7 +73,7 @@
writeln"Examples with quantifiers";
val prems =
-goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
+goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
by (rtac allI 1);
by (rtac disjI1 1);
by (resolve_tac (prems RL [spec]) 1);
@@ -84,14 +82,14 @@
result();
-goal IFOLP.thy "?p : ALL x. EX y. x=y";
+goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
by (rtac allI 1);
by (rtac exI 1);
by (rtac refl 1);
result();
-goal IFOLP.thy "?p : EX y. ALL x. x=y";
+goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
by (rtac exI 1);
by (rtac allI 1);
by (rtac refl 1) handle ERROR => writeln"Failed, as expected";
@@ -99,7 +97,7 @@
(*Parallel lifting example. *)
-goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
+goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
@@ -108,7 +106,7 @@
val prems =
-goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
+goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
by (rtac conjE 1);
by (resolve_tac prems 1);
by (rtac exE 1);
@@ -121,7 +119,7 @@
(*A bigger demonstration of quantifiers -- not in the paper*)
-goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
+goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac exE 1 THEN assume_tac 1);
@@ -129,6 +127,3 @@
by (rtac allE 1 THEN assume_tac 1);
by (assume_tac 1);
result();
-
-
-writeln"Reached end of file.";
--- a/src/FOLP/ex/int.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/int.ML Sun Sep 18 14:25:48 2005 +0200
@@ -15,8 +15,6 @@
by (IntPr.fast_tac 1);
*)
-writeln"File FOLP/ex/int.ML";
-
(*Note: for PROPOSITIONAL formulae...
~A is classically provable iff it is intuitionistically provable.
Therefore A is classically provable iff ~~A is intuitionistically provable.
@@ -29,34 +27,34 @@
~~P is intuitionstically equivalent to P. [Andy Pitts]
*)
-goal IFOLP.thy "?p : ~~(P&Q) <-> ~~P & ~~Q";
+goal (theory "IFOLP") "?p : ~~(P&Q) <-> ~~P & ~~Q";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ~~~P <-> ~P";
+goal (theory "IFOLP") "?p : ~~~P <-> ~P";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))";
+goal (theory "IFOLP") "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : (P<->Q) <-> (Q<->P)";
+goal (theory "IFOLP") "?p : (P<->Q) <-> (Q<->P)";
by (IntPr.fast_tac 1);
result();
writeln"Lemmas for the propositional double-negation translation";
-goal IFOLP.thy "?p : P --> ~~P";
+goal (theory "IFOLP") "?p : P --> ~~P";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ~~(~~P --> P)";
+goal (theory "IFOLP") "?p : ~~(~~P --> P)";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ~~P & ~~(P --> Q) --> ~~Q";
+goal (theory "IFOLP") "?p : ~~P & ~~(P --> Q) --> ~~Q";
by (IntPr.fast_tac 1);
result();
@@ -64,12 +62,12 @@
writeln"The following are classically but not constructively valid.";
(*The attempt to prove them terminates quickly!*)
-goal IFOLP.thy "?p : ((P-->Q) --> P) --> P";
+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 IFOLP.thy "?p : (P&Q-->R) --> (P-->R) | (Q-->R)";
+goal (theory "IFOLP") "?p : (P&Q-->R) --> (P-->R) | (Q-->R)";
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
@@ -77,99 +75,99 @@
writeln"Intuitionistic FOL: propositional problems based on Pelletier.";
writeln"Problem ~~1";
-goal IFOLP.thy "?p : ~~((P-->Q) <-> (~Q --> ~P))";
+goal (theory "IFOLP") "?p : ~~((P-->Q) <-> (~Q --> ~P))";
by (IntPr.fast_tac 1);
result();
(*5 secs*)
writeln"Problem ~~2";
-goal IFOLP.thy "?p : ~~(~~P <-> P)";
+goal (theory "IFOLP") "?p : ~~(~~P <-> P)";
by (IntPr.fast_tac 1);
result();
(*1 secs*)
writeln"Problem 3";
-goal IFOLP.thy "?p : ~(P-->Q) --> (Q-->P)";
+goal (theory "IFOLP") "?p : ~(P-->Q) --> (Q-->P)";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~4";
-goal IFOLP.thy "?p : ~~((~P-->Q) <-> (~Q --> P))";
+goal (theory "IFOLP") "?p : ~~((~P-->Q) <-> (~Q --> P))";
by (IntPr.fast_tac 1);
result();
(*9 secs*)
writeln"Problem ~~5";
-goal IFOLP.thy "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
+goal (theory "IFOLP") "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
by (IntPr.fast_tac 1);
result();
(*10 secs*)
writeln"Problem ~~6";
-goal IFOLP.thy "?p : ~~(P | ~P)";
+goal (theory "IFOLP") "?p : ~~(P | ~P)";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~7";
-goal IFOLP.thy "?p : ~~(P | ~~~P)";
+goal (theory "IFOLP") "?p : ~~(P | ~~~P)";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~8. Peirce's law";
-goal IFOLP.thy "?p : ~~(((P-->Q) --> P) --> P)";
+goal (theory "IFOLP") "?p : ~~(((P-->Q) --> P) --> P)";
by (IntPr.fast_tac 1);
result();
writeln"Problem 9";
-goal IFOLP.thy "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+goal (theory "IFOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
by (IntPr.fast_tac 1);
result();
(*9 secs*)
writeln"Problem 10";
-goal IFOLP.thy "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
+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 IFOLP.thy "?p : P<->P";
+goal (theory "IFOLP") "?p : P<->P";
by (IntPr.fast_tac 1);
writeln"Problem ~~12. Dijkstra's law ";
-goal IFOLP.thy "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))";
+goal (theory "IFOLP") "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))";
+goal (theory "IFOLP") "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))";
by (IntPr.fast_tac 1);
result();
writeln"Problem 13. Distributive law";
-goal IFOLP.thy "?p : P | (Q & R) <-> (P | Q) & (P | R)";
+goal (theory "IFOLP") "?p : P | (Q & R) <-> (P | Q) & (P | R)";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~14";
-goal IFOLP.thy "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
+goal (theory "IFOLP") "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~15";
-goal IFOLP.thy "?p : ~~((P --> Q) <-> (~P | Q))";
+goal (theory "IFOLP") "?p : ~~((P --> Q) <-> (~P | Q))";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~16";
-goal IFOLP.thy "?p : ~~((P-->Q) | (Q-->P))";
+goal (theory "IFOLP") "?p : ~~((P-->Q) | (Q-->P))";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~17";
-goal IFOLP.thy
+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!!*)
@@ -180,23 +178,23 @@
writeln"The converse is classical in the following implications...";
-goal IFOLP.thy "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q";
+goal (theory "IFOLP") "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
+goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))";
+goal (theory "IFOLP") "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)";
+goal (theory "IFOLP") "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
+goal (theory "IFOLP") "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
by (IntPr.fast_tac 1);
result();
@@ -206,24 +204,24 @@
writeln"The following are not constructively valid!";
(*The attempt to prove them terminates quickly!*)
-goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
+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 IFOLP.thy "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
+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 IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
+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 IFOLP.thy "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
+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 IFOLP.thy "?p : EX x. Q(x) --> (ALL x. Q(x))";
+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;
@@ -234,36 +232,36 @@
Some will require quantifier duplication -- not currently available*)
writeln"Problem ~~18";
-goal IFOLP.thy "?p : ~~(EX y. ALL x. P(y)-->P(x))";
+goal (theory "IFOLP") "?p : ~~(EX y. ALL x. P(y)-->P(x))";
(*NOT PROVED*)
writeln"Problem ~~19";
-goal IFOLP.thy "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
+goal (theory "IFOLP") "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
(*NOT PROVED*)
writeln"Problem 20";
-goal IFOLP.thy "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \
+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 IFOLP.thy
+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 IFOLP.thy "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))";
+goal (theory "IFOLP") "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))";
by (IntPr.fast_tac 1);
result();
writeln"Problem ~~23";
-goal IFOLP.thy "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))";
+goal (theory "IFOLP") "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))";
by (IntPr.best_tac 1);
result();
writeln"Problem 24";
-goal IFOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \
+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*)
@@ -274,7 +272,7 @@
result();
writeln"Problem 25";
-goal IFOLP.thy "?p : (EX x. P(x)) & \
+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))) \
@@ -283,21 +281,21 @@
result();
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
-goal IFOLP.thy "?p : (EX x. P(x)) & (EX y. Q(y)) \
+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 IFOLP.thy "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
+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 IFOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
+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))";
@@ -305,7 +303,7 @@
result();
writeln"Problem 32";
-goal IFOLP.thy "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
+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))";
@@ -313,18 +311,18 @@
result();
writeln"Problem 39";
-goal IFOLP.thy "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+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 IFOLP.thy "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> \
+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 IFOLP.thy "?p : (ALL x. f(x) --> \
+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))";
@@ -332,34 +330,32 @@
result();
writeln"Problem 48";
-goal IFOLP.thy "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
+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 IFOLP.thy
+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 IFOLP.thy
+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 IFOLP.thy
+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 IFOLP.thy
+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();
-
-writeln"Reached end of file.";
--- a/src/FOLP/ex/intro.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/intro.ML Sun Sep 18 14:25:48 2005 +0200
@@ -14,7 +14,7 @@
(**** Some simple backward proofs ****)
-goal FOLP.thy "?p:P|P --> P";
+goal (theory "FOLP") "?p:P|P --> P";
by (rtac impI 1);
by (rtac disjE 1);
by (assume_tac 3);
@@ -22,7 +22,7 @@
by (assume_tac 1);
val mythm = result();
-goal FOLP.thy "?p:(P & Q) | R --> (P | R)";
+goal (theory "FOLP") "?p:(P & Q) | R --> (P | R)";
by (rtac impI 1);
by (etac disjE 1);
by (dtac conjunct1 1);
@@ -32,7 +32,7 @@
result();
(*Correct version, delaying use of "spec" until last*)
-goal FOLP.thy "?p:(ALL x y. P(x,y)) --> (ALL z w. P(w,z))";
+goal (theory "FOLP") "?p:(ALL x y. P(x,y)) --> (ALL z w. P(w,z))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac allI 1);
@@ -44,12 +44,12 @@
(**** Demonstration of fast_tac ****)
-goal FOLP.thy "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x)) \
+goal (theory "FOLP") "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x)) \
\ --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
by (fast_tac FOLP_cs 1);
result();
-goal FOLP.thy "?p:ALL x. P(x,f(x)) <-> \
+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();
@@ -57,7 +57,7 @@
(**** Derivation of conjunction elimination rule ****)
-val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
+val [major,minor] = goal (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
by (rtac minor 1);
by (resolve_tac [major RS conjunct1] 1);
by (resolve_tac [major RS conjunct2] 1);
@@ -69,14 +69,14 @@
(** Derivation of negation introduction **)
-val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
+val prems = goal (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
by (rewtac not_def);
by (rtac impI 1);
by (resolve_tac prems 1);
by (assume_tac 1);
result();
-val [major,minor] = goal FOLP.thy "[| p:~P; q:P |] ==> ?p:R";
+val [major,minor] = goal (theory "FOLP") "[| p:~P; q:P |] ==> ?p:R";
by (rtac FalseE 1);
by (rtac mp 1);
by (resolve_tac [rewrite_rule [not_def] major] 1);
@@ -84,9 +84,7 @@
result();
(*Alternative proof of above result*)
-val [major,minor] = goalw FOLP.thy [not_def]
+val [major,minor] = goalw (theory "FOLP") [not_def]
"[| p:~P; q:P |] ==> ?p:R";
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
result();
-
-writeln"Reached end of file.";
--- a/src/FOLP/ex/prop.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/prop.ML Sun Sep 18 14:25:48 2005 +0200
@@ -7,9 +7,6 @@
Needs declarations of the theory "thy" and the tactic "tac"
*)
-writeln"File FOLP/ex/prop.ML";
-
-
writeln"commutative laws of & and | ";
Goal "?p : P & Q --> Q & P";
by tac;
@@ -149,5 +146,3 @@
\ --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
by tac;
result();
-
-writeln"Reached end of file.";
--- a/src/FOLP/ex/quant.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/quant.ML Sun Sep 18 14:25:48 2005 +0200
@@ -7,101 +7,99 @@
Needs declarations of the theory "thy" and the tactic "tac"
*)
-writeln"File FOLP/ex/quant.ML";
-
Goal "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
by tac;
-result();
+result();
Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
by tac;
-result();
+result();
(*Converse is false*)
Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
by tac;
-result();
+result();
Goal "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
by tac;
-result();
+result();
Goal "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
by tac;
-result();
+result();
writeln"Some harder ones";
Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
by tac;
-result();
+result();
(*6 secs*)
(*Converse is false*)
Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
by tac;
-result();
+result();
writeln"Basic test of quantifier reasoning";
(*TRUE*)
Goal "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
-by tac;
-result();
+by tac;
+result();
Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))";
-by tac;
-result();
+by tac;
+result();
writeln"The following should fail, as they are false!";
Goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
-by tac handle ERROR => writeln"Failed, as expected";
+by tac handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
-getgoal 1;
+getgoal 1;
Goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))";
-by tac handle ERROR => writeln"Failed, as expected";
-getgoal 1;
+by tac handle ERROR => writeln"Failed, as expected";
+getgoal 1;
Goal "?p : P(?a) --> (ALL x. P(x))";
by tac handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
-getgoal 1;
+getgoal 1;
Goal
"?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
by tac handle ERROR => writeln"Failed, as expected";
-getgoal 1;
+getgoal 1;
writeln"Back to things that are provable...";
Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
-by tac;
-result();
+by tac;
+result();
(*An example of why exI should be delayed as long as possible*)
Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
-by tac;
-result();
+by tac;
+result();
Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
-by tac;
-(*Verify that no subgoals remain.*)
-uresult();
+by tac;
+(*Verify that no subgoals remain.*)
+uresult();
Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))";
by tac;
-result();
+result();
writeln"Some slow ones";
@@ -110,20 +108,17 @@
(*Principia Mathematica *11.53 *)
Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
by tac;
-result();
+result();
(*6 secs*)
(*Principia Mathematica *11.55 *)
Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
by tac;
-result();
+result();
(*9 secs*)
(*Principia Mathematica *11.61 *)
Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
by tac;
-result();
+result();
(*3 secs*)
-
-writeln"Reached end of file.";
-
--- a/src/FOLP/simpdata.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/simpdata.ML Sun Sep 18 14:25:48 2005 +0200
@@ -3,13 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Simplification data for FOLP
+Simplification data for FOLP.
*)
(*** Rewrite rules ***)
-fun int_prove_fun_raw s =
- (writeln s; prove_goal IFOLP.thy s
+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);
@@ -32,7 +32,7 @@
val imp_rews = map int_prove_fun
["(P --> False) <-> ~P", "(P --> True) <-> True",
- "(False --> P) <-> True", "(True --> P) <-> P",
+ "(False --> P) <-> True", "(True --> P) <-> P",
"(P --> P) <-> True", "(P --> ~P) <-> ~P"];
val iff_rews = map int_prove_fun
@@ -70,7 +70,7 @@
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("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
| _ => make_iff_T th;
@@ -113,12 +113,12 @@
structure FOLP_Simp = SimpFun(FOLP_SimpData);
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
-val FOLP_congs =
+val FOLP_congs =
[all_cong,ex_cong,eq_cong,
conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
val IFOLP_rews =
- [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
+ [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
imp_rews @ iff_rews @ quant_rews;
open FOLP_Simp;
@@ -128,8 +128,8 @@
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
(*Classical version...*)
-fun prove_fun s =
- (writeln s; prove_goal FOLP.thy s
+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
@@ -139,5 +139,3 @@
val FOLP_rews = IFOLP_rews@cla_rews;
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
-
-