# HG changeset patch # User wenzelm # Date 1205875158 -3600 # Node ID eaf634e975faba8ce0dff7dde81afef7e417bf32 # Parent d875e70a94de1ef726bbc21e1c6403ade2f65472 converted legacy ML scripts; diff -r d875e70a94de -r eaf634e975fa src/FOLP/FOLP.thy --- 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" diff -r d875e70a94de -r eaf634e975fa src/FOLP/FOLP_lemmas.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"; diff -r d875e70a94de -r eaf634e975fa src/FOLP/IFOLP.ML --- 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"; diff -r d875e70a94de -r eaf634e975fa src/FOLP/IFOLP.thy --- 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 \ q:P \ ?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 - - diff -r d875e70a94de -r eaf634e975fa src/FOLP/IsaMakefile --- 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 diff -r d875e70a94de -r eaf634e975fa src/FOLP/ex/Classical.thy --- /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 diff -r d875e70a94de -r eaf634e975fa src/FOLP/ex/Intuitionistic.thy --- /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 diff -r d875e70a94de -r eaf634e975fa src/FOLP/ex/ROOT.ML --- 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"; diff -r d875e70a94de -r eaf634e975fa src/FOLP/ex/cla.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(); diff -r d875e70a94de -r eaf634e975fa src/FOLP/ex/int.ML --- 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(); diff -r d875e70a94de -r eaf634e975fa src/FOLP/intprover.ML --- 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; - diff -r d875e70a94de -r eaf634e975fa src/FOLP/simpdata.ML --- 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;