converted legacy ML scripts;
authorwenzelm
Wed Mar 26 22:38:55 2008 +0100 (2008-03-26 ago)
changeset 264086964c4799f47
parent 26407 562a1d615336
child 26409 1ceabad5a2c8
converted legacy ML scripts;
src/FOLP/IsaMakefile
src/FOLP/ex/Propositional_Cla.thy
src/FOLP/ex/Propositional_Int.thy
src/FOLP/ex/Quantifiers_Cla.thy
src/FOLP/ex/Quantifiers_Int.thy
src/FOLP/ex/ROOT.ML
src/FOLP/ex/prop.ML
src/FOLP/ex/quant.ML
     1.1 --- a/src/FOLP/IsaMakefile	Wed Mar 26 22:38:17 2008 +0100
     1.2 +++ b/src/FOLP/IsaMakefile	Wed Mar 26 22:38:55 2008 +0100
     1.3 @@ -26,8 +26,8 @@
     1.4  Pure:
     1.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.6  
     1.7 -$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML \
     1.8 -  classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
     1.9 +$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML	\
    1.10 +  hypsubst.ML intprover.ML simp.ML simpdata.ML
    1.11  	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
    1.12  
    1.13  
    1.14 @@ -35,10 +35,11 @@
    1.15  
    1.16  FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
    1.17  
    1.18 -$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy \
    1.19 -  ex/If.thy ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy   \
    1.20 -  ex/Classical.thy					    \
    1.21 -  ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
    1.22 +$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy ex/If.thy	\
    1.23 +  ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy ex/Classical.thy	\
    1.24 +  ex/Prolog.ML ex/Prolog.thy ex/Propositional_Int.thy			\
    1.25 +  ex/Propositional_Cla.thy ex/Quantifiers_Int.thy			\
    1.26 +  ex/Quantifiers_Cla.thy
    1.27  	@$(ISATOOL) usedir $(OUT)/FOLP ex
    1.28  
    1.29  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/FOLP/ex/Propositional_Cla.thy	Wed Mar 26 22:38:55 2008 +0100
     2.3 @@ -0,0 +1,118 @@
     2.4 +(*  Title:      FOLP/ex/Propositional_Cla.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1991  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +header {* First-Order Logic: propositional examples *}
    2.11 +
    2.12 +theory Propositional_Cla
    2.13 +imports FOLP
    2.14 +begin
    2.15 +
    2.16 +
    2.17 +text "commutative laws of & and | "
    2.18 +lemma "?p : P & Q  -->  Q & P"
    2.19 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.20 +
    2.21 +lemma "?p : P | Q  -->  Q | P"
    2.22 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.23 +
    2.24 +
    2.25 +text "associative laws of & and | "
    2.26 +lemma "?p : (P & Q) & R  -->  P & (Q & R)"
    2.27 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.28 +
    2.29 +lemma "?p : (P | Q) | R  -->  P | (Q | R)"
    2.30 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.31 +
    2.32 +
    2.33 +text "distributive laws of & and | "
    2.34 +lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
    2.35 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.36 +
    2.37 +lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
    2.38 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.39 +
    2.40 +lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
    2.41 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.42 +
    2.43 +
    2.44 +lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
    2.45 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.46 +
    2.47 +
    2.48 +text "Laws involving implication"
    2.49 +
    2.50 +lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
    2.51 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.52 +
    2.53 +lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
    2.54 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.55 +
    2.56 +lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
    2.57 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.58 +
    2.59 +lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
    2.60 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.61 +
    2.62 +lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
    2.63 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.64 +
    2.65 +
    2.66 +text "Propositions-as-types"
    2.67 +
    2.68 +(*The combinator K*)
    2.69 +lemma "?p : P --> (Q --> P)"
    2.70 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.71 +
    2.72 +(*The combinator S*)
    2.73 +lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
    2.74 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.75 +
    2.76 +
    2.77 +(*Converse is classical*)
    2.78 +lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
    2.79 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.80 +
    2.81 +lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
    2.82 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.83 +
    2.84 +
    2.85 +text "Schwichtenberg's examples (via T. Nipkow)"
    2.86 +
    2.87 +lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
    2.88 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.89 +
    2.90 +lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
    2.91 +              --> ((P --> Q) --> P) --> P"
    2.92 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.93 +
    2.94 +lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
    2.95 +               --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
    2.96 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    2.97 +  
    2.98 +lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
    2.99 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   2.100 +
   2.101 +lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
   2.102 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   2.103 +
   2.104 +lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
   2.105 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   2.106 +
   2.107 +lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
   2.108 +          --> (((P8 --> P2) --> P9) --> P3 --> P10)  
   2.109 +          --> (P1 --> P8) --> P6 --> P7  
   2.110 +          --> (((P3 --> P2) --> P9) --> P4)  
   2.111 +          --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
   2.112 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   2.113 +
   2.114 +lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
   2.115 +     --> (((P3 --> P2) --> P9) --> P4)  
   2.116 +     --> (((P6 --> P1) --> P2) --> P9)  
   2.117 +     --> (((P7 --> P1) --> P10) --> P4 --> P5)  
   2.118 +     --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
   2.119 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   2.120 +
   2.121 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/FOLP/ex/Propositional_Int.thy	Wed Mar 26 22:38:55 2008 +0100
     3.3 @@ -0,0 +1,118 @@
     3.4 +(*  Title:      FOLP/ex/Propositional_Int.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1991  University of Cambridge
     3.8 +*)
     3.9 +
    3.10 +header {* First-Order Logic: propositional examples *}
    3.11 +
    3.12 +theory Propositional_Int
    3.13 +imports IFOLP
    3.14 +begin
    3.15 +
    3.16 +
    3.17 +text "commutative laws of & and | "
    3.18 +lemma "?p : P & Q  -->  Q & P"
    3.19 +  by (tactic {* IntPr.fast_tac 1 *})
    3.20 +
    3.21 +lemma "?p : P | Q  -->  Q | P"
    3.22 +  by (tactic {* IntPr.fast_tac 1 *})
    3.23 +
    3.24 +
    3.25 +text "associative laws of & and | "
    3.26 +lemma "?p : (P & Q) & R  -->  P & (Q & R)"
    3.27 +  by (tactic {* IntPr.fast_tac 1 *})
    3.28 +
    3.29 +lemma "?p : (P | Q) | R  -->  P | (Q | R)"
    3.30 +  by (tactic {* IntPr.fast_tac 1 *})
    3.31 +
    3.32 +
    3.33 +text "distributive laws of & and | "
    3.34 +lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
    3.35 +  by (tactic {* IntPr.fast_tac 1 *})
    3.36 +
    3.37 +lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
    3.38 +  by (tactic {* IntPr.fast_tac 1 *})
    3.39 +
    3.40 +lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
    3.41 +  by (tactic {* IntPr.fast_tac 1 *})
    3.42 +
    3.43 +
    3.44 +lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
    3.45 +  by (tactic {* IntPr.fast_tac 1 *})
    3.46 +
    3.47 +
    3.48 +text "Laws involving implication"
    3.49 +
    3.50 +lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
    3.51 +  by (tactic {* IntPr.fast_tac 1 *})
    3.52 +
    3.53 +lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
    3.54 +  by (tactic {* IntPr.fast_tac 1 *})
    3.55 +
    3.56 +lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
    3.57 +  by (tactic {* IntPr.fast_tac 1 *})
    3.58 +
    3.59 +lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
    3.60 +  by (tactic {* IntPr.fast_tac 1 *})
    3.61 +
    3.62 +lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
    3.63 +  by (tactic {* IntPr.fast_tac 1 *})
    3.64 +
    3.65 +
    3.66 +text "Propositions-as-types"
    3.67 +
    3.68 +(*The combinator K*)
    3.69 +lemma "?p : P --> (Q --> P)"
    3.70 +  by (tactic {* IntPr.fast_tac 1 *})
    3.71 +
    3.72 +(*The combinator S*)
    3.73 +lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
    3.74 +  by (tactic {* IntPr.fast_tac 1 *})
    3.75 +
    3.76 +
    3.77 +(*Converse is classical*)
    3.78 +lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
    3.79 +  by (tactic {* IntPr.fast_tac 1 *})
    3.80 +
    3.81 +lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
    3.82 +  by (tactic {* IntPr.fast_tac 1 *})
    3.83 +
    3.84 +
    3.85 +text "Schwichtenberg's examples (via T. Nipkow)"
    3.86 +
    3.87 +lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
    3.88 +  by (tactic {* IntPr.fast_tac 1 *})
    3.89 +
    3.90 +lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
    3.91 +              --> ((P --> Q) --> P) --> P"
    3.92 +  by (tactic {* IntPr.fast_tac 1 *})
    3.93 +
    3.94 +lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
    3.95 +               --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
    3.96 +  by (tactic {* IntPr.fast_tac 1 *})
    3.97 +  
    3.98 +lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
    3.99 +  by (tactic {* IntPr.fast_tac 1 *})
   3.100 +
   3.101 +lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
   3.102 +  by (tactic {* IntPr.fast_tac 1 *})
   3.103 +
   3.104 +lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
   3.105 +  by (tactic {* IntPr.fast_tac 1 *})
   3.106 +
   3.107 +lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
   3.108 +          --> (((P8 --> P2) --> P9) --> P3 --> P10)  
   3.109 +          --> (P1 --> P8) --> P6 --> P7  
   3.110 +          --> (((P3 --> P2) --> P9) --> P4)  
   3.111 +          --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
   3.112 +  by (tactic {* IntPr.fast_tac 1 *})
   3.113 +
   3.114 +lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
   3.115 +     --> (((P3 --> P2) --> P9) --> P4)  
   3.116 +     --> (((P6 --> P1) --> P2) --> P9)  
   3.117 +     --> (((P7 --> P1) --> P10) --> P4 --> P5)  
   3.118 +     --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
   3.119 +  by (tactic {* IntPr.fast_tac 1 *})
   3.120 +
   3.121 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/FOLP/ex/Quantifiers_Cla.thy	Wed Mar 26 22:38:55 2008 +0100
     4.3 @@ -0,0 +1,102 @@
     4.4 +(*  Title:      FOLP/ex/Quantifiers_Cla.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1991  University of Cambridge
     4.8 +
     4.9 +First-Order Logic: quantifier examples (intuitionistic and classical)
    4.10 +Needs declarations of the theory "thy" and the tactic "tac"
    4.11 +*)
    4.12 +
    4.13 +theory Quantifiers_Cla
    4.14 +imports FOLP
    4.15 +begin
    4.16 +
    4.17 +lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    4.18 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.19 +
    4.20 +lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
    4.21 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.22 +
    4.23 +
    4.24 +(*Converse is false*)
    4.25 +lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
    4.26 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.27 +
    4.28 +lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
    4.29 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.30 +
    4.31 +
    4.32 +lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
    4.33 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.34 +
    4.35 +
    4.36 +text "Some harder ones"
    4.37 +
    4.38 +lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
    4.39 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.40 +
    4.41 +(*Converse is false*)
    4.42 +lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
    4.43 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.44 +
    4.45 +
    4.46 +text "Basic test of quantifier reasoning"
    4.47 +(*TRUE*)
    4.48 +lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    4.49 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.50 +
    4.51 +lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
    4.52 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.53 +
    4.54 +
    4.55 +text "The following should fail, as they are false!"
    4.56 +
    4.57 +lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
    4.58 +  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    4.59 +  oops
    4.60 +
    4.61 +lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
    4.62 +  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    4.63 +  oops
    4.64 +
    4.65 +lemma "?p : P(?a) --> (ALL x. P(x))"
    4.66 +  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    4.67 +  oops
    4.68 +
    4.69 +lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
    4.70 +  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    4.71 +  oops
    4.72 +
    4.73 +
    4.74 +text "Back to things that are provable..."
    4.75 +
    4.76 +lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
    4.77 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.78 +
    4.79 +
    4.80 +(*An example of why exI should be delayed as long as possible*)
    4.81 +lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
    4.82 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.83 +
    4.84 +lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
    4.85 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.86 +
    4.87 +lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
    4.88 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.89 +
    4.90 +
    4.91 +text "Some slow ones"
    4.92 +
    4.93 +(*Principia Mathematica *11.53  *)
    4.94 +lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
    4.95 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    4.96 +
    4.97 +(*Principia Mathematica *11.55  *)
    4.98 +lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
    4.99 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   4.100 +
   4.101 +(*Principia Mathematica *11.61  *)
   4.102 +lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
   4.103 +  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   4.104 +
   4.105 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/FOLP/ex/Quantifiers_Int.thy	Wed Mar 26 22:38:55 2008 +0100
     5.3 @@ -0,0 +1,102 @@
     5.4 +(*  Title:      FOLP/ex/Quantifiers_Int.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1991  University of Cambridge
     5.8 +
     5.9 +First-Order Logic: quantifier examples (intuitionistic and classical)
    5.10 +Needs declarations of the theory "thy" and the tactic "tac"
    5.11 +*)
    5.12 +
    5.13 +theory Quantifiers_Int
    5.14 +imports IFOLP
    5.15 +begin
    5.16 +
    5.17 +lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    5.18 +  by (tactic {* IntPr.fast_tac 1 *})
    5.19 +
    5.20 +lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
    5.21 +  by (tactic {* IntPr.fast_tac 1 *})
    5.22 +
    5.23 +
    5.24 +(*Converse is false*)
    5.25 +lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
    5.26 +  by (tactic {* IntPr.fast_tac 1 *})
    5.27 +
    5.28 +lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
    5.29 +  by (tactic {* IntPr.fast_tac 1 *})
    5.30 +
    5.31 +
    5.32 +lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
    5.33 +  by (tactic {* IntPr.fast_tac 1 *})
    5.34 +
    5.35 +
    5.36 +text "Some harder ones"
    5.37 +
    5.38 +lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
    5.39 +  by (tactic {* IntPr.fast_tac 1 *})
    5.40 +
    5.41 +(*Converse is false*)
    5.42 +lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
    5.43 +  by (tactic {* IntPr.fast_tac 1 *})
    5.44 +
    5.45 +
    5.46 +text "Basic test of quantifier reasoning"
    5.47 +(*TRUE*)
    5.48 +lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    5.49 +  by (tactic {* IntPr.fast_tac 1 *})
    5.50 +
    5.51 +lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
    5.52 +  by (tactic {* IntPr.fast_tac 1 *})
    5.53 +
    5.54 +
    5.55 +text "The following should fail, as they are false!"
    5.56 +
    5.57 +lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
    5.58 +  apply (tactic {* IntPr.fast_tac 1 *})?
    5.59 +  oops
    5.60 +
    5.61 +lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
    5.62 +  apply (tactic {* IntPr.fast_tac 1 *})?
    5.63 +  oops
    5.64 +
    5.65 +lemma "?p : P(?a) --> (ALL x. P(x))"
    5.66 +  apply (tactic {* IntPr.fast_tac 1 *})?
    5.67 +  oops
    5.68 +
    5.69 +lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
    5.70 +  apply (tactic {* IntPr.fast_tac 1 *})?
    5.71 +  oops
    5.72 +
    5.73 +
    5.74 +text "Back to things that are provable..."
    5.75 +
    5.76 +lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
    5.77 +  by (tactic {* IntPr.fast_tac 1 *})
    5.78 +
    5.79 +
    5.80 +(*An example of why exI should be delayed as long as possible*)
    5.81 +lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
    5.82 +  by (tactic {* IntPr.fast_tac 1 *})
    5.83 +
    5.84 +lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
    5.85 +  by (tactic {* IntPr.fast_tac 1 *})
    5.86 +
    5.87 +lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
    5.88 +  by (tactic {* IntPr.fast_tac 1 *})
    5.89 +
    5.90 +
    5.91 +text "Some slow ones"
    5.92 +
    5.93 +(*Principia Mathematica *11.53  *)
    5.94 +lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
    5.95 +  by (tactic {* IntPr.fast_tac 1 *})
    5.96 +
    5.97 +(*Principia Mathematica *11.55  *)
    5.98 +lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
    5.99 +  by (tactic {* IntPr.fast_tac 1 *})
   5.100 +
   5.101 +(*Principia Mathematica *11.61  *)
   5.102 +lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
   5.103 +  by (tactic {* IntPr.fast_tac 1 *})
   5.104 +
   5.105 +end
     6.1 --- a/src/FOLP/ex/ROOT.ML	Wed Mar 26 22:38:17 2008 +0100
     6.2 +++ b/src/FOLP/ex/ROOT.ML	Wed Mar 26 22:38:55 2008 +0100
     6.3 @@ -12,13 +12,9 @@
     6.4    "Foundation",
     6.5    "If",
     6.6    "Intuitionistic",
     6.7 -  "Classical"
     6.8 +  "Classical",
     6.9 +  "Propositional_Int",
    6.10 +  "Quantifiers_Int",
    6.11 +  "Propositional_Cla",
    6.12 +  "Quantifiers_Cla"
    6.13  ];
    6.14 -
    6.15 -val thy = theory "IFOLP"  and  tac = IntPr.fast_tac 1;
    6.16 -time_use     "prop.ML";
    6.17 -time_use     "quant.ML";
    6.18 -
    6.19 -val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
    6.20 -time_use     "prop.ML";
    6.21 -time_use     "quant.ML";
     7.1 --- a/src/FOLP/ex/prop.ML	Wed Mar 26 22:38:17 2008 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,151 +0,0 @@
     7.4 -(*  Title:      FOLP/ex/prop.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 -    Copyright   1991  University of Cambridge
     7.8 -
     7.9 -First-Order Logic: propositional examples (intuitionistic and classical)
    7.10 -Needs declarations of the theory "thy" and the tactic "tac"
    7.11 -*)
    7.12 -
    7.13 -ML_Context.set_context (SOME (Context.Theory thy));
    7.14 -
    7.15 -
    7.16 -writeln"commutative laws of & and | ";
    7.17 -Goal "?p : P & Q  -->  Q & P";
    7.18 -by tac;
    7.19 -result();
    7.20 -
    7.21 -Goal "?p : P | Q  -->  Q | P";
    7.22 -by tac;
    7.23 -result();
    7.24 -
    7.25 -
    7.26 -writeln"associative laws of & and | ";
    7.27 -Goal "?p : (P & Q) & R  -->  P & (Q & R)";
    7.28 -by tac;
    7.29 -result();
    7.30 -
    7.31 -Goal "?p : (P | Q) | R  -->  P | (Q | R)";
    7.32 -by tac;
    7.33 -result();
    7.34 -
    7.35 -
    7.36 -
    7.37 -writeln"distributive laws of & and | ";
    7.38 -Goal "?p : (P & Q) | R  --> (P | R) & (Q | R)";
    7.39 -by tac;
    7.40 -result();
    7.41 -
    7.42 -Goal "?p : (P | R) & (Q | R)  --> (P & Q) | R";
    7.43 -by tac;
    7.44 -result();
    7.45 -
    7.46 -Goal "?p : (P | Q) & R  --> (P & R) | (Q & R)";
    7.47 -by tac;
    7.48 -result();
    7.49 -
    7.50 -
    7.51 -Goal "?p : (P & R) | (Q & R)  --> (P | Q) & R";
    7.52 -by tac;
    7.53 -result();
    7.54 -
    7.55 -
    7.56 -writeln"Laws involving implication";
    7.57 -
    7.58 -Goal "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)";
    7.59 -by tac;
    7.60 -result();
    7.61 -
    7.62 -
    7.63 -Goal "?p : (P & Q --> R) <-> (P--> (Q-->R))";
    7.64 -by tac;
    7.65 -result();
    7.66 -
    7.67 -
    7.68 -Goal "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
    7.69 -by tac;
    7.70 -result();
    7.71 -
    7.72 -Goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
    7.73 -by tac;
    7.74 -result();
    7.75 -
    7.76 -Goal "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
    7.77 -by tac;
    7.78 -result();
    7.79 -
    7.80 -
    7.81 -writeln"Propositions-as-types";
    7.82 -
    7.83 -(*The combinator K*)
    7.84 -Goal "?p : P --> (Q --> P)";
    7.85 -by tac;
    7.86 -result();
    7.87 -
    7.88 -(*The combinator S*)
    7.89 -Goal "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)";
    7.90 -by tac;
    7.91 -result();
    7.92 -
    7.93 -
    7.94 -(*Converse is classical*)
    7.95 -Goal "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)";
    7.96 -by tac;
    7.97 -result();
    7.98 -
    7.99 -Goal "?p : (P-->Q)  -->  (~Q --> ~P)";
   7.100 -by tac;
   7.101 -result();
   7.102 -
   7.103 -
   7.104 -writeln"Schwichtenberg's examples (via T. Nipkow)";
   7.105 -
   7.106 -(* stab-imp *)
   7.107 -Goal "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
   7.108 -by tac;
   7.109 -result();
   7.110 -
   7.111 -(* stab-to-peirce *)
   7.112 -Goal "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
   7.113 -\             --> ((P --> Q) --> P) --> P";
   7.114 -by tac;
   7.115 -result();
   7.116 -
   7.117 -(* peirce-imp1 *)
   7.118 -Goal "?p : (((Q --> R) --> Q) --> Q) \
   7.119 -\              --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
   7.120 -by tac;
   7.121 -result();
   7.122 -  
   7.123 -(* peirce-imp2 *)
   7.124 -Goal "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
   7.125 -by tac;
   7.126 -result();
   7.127 -
   7.128 -(* mints  *)
   7.129 -Goal "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q";
   7.130 -by tac;
   7.131 -result();
   7.132 -
   7.133 -(* mints-solovev *)
   7.134 -Goal "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
   7.135 -by tac;
   7.136 -result();
   7.137 -
   7.138 -(* tatsuta *)
   7.139 -Goal "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \
   7.140 -\         --> (((P8 --> P2) --> P9) --> P3 --> P10) \
   7.141 -\         --> (P1 --> P8) --> P6 --> P7 \
   7.142 -\         --> (((P3 --> P2) --> P9) --> P4) \
   7.143 -\         --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
   7.144 -by tac;
   7.145 -result();
   7.146 -
   7.147 -(* tatsuta1 *)
   7.148 -Goal "?p : (((P8 --> P2) --> P9) --> P3 --> P10) \
   7.149 -\    --> (((P3 --> P2) --> P9) --> P4) \
   7.150 -\    --> (((P6 --> P1) --> P2) --> P9) \
   7.151 -\    --> (((P7 --> P1) --> P10) --> P4 --> P5) \
   7.152 -\    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
   7.153 -by tac;
   7.154 -result();
     8.1 --- a/src/FOLP/ex/quant.ML	Wed Mar 26 22:38:17 2008 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,124 +0,0 @@
     8.4 -(*  Title:      FOLP/ex/quant.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1991  University of Cambridge
     8.8 -
     8.9 -First-Order Logic: quantifier examples (intuitionistic and classical)
    8.10 -Needs declarations of the theory "thy" and the tactic "tac"
    8.11 -*)
    8.12 -
    8.13 -Goal "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
    8.14 -by tac;
    8.15 -result();
    8.16 -
    8.17 -
    8.18 -Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
    8.19 -by tac;
    8.20 -result();
    8.21 -
    8.22 -
    8.23 -(*Converse is false*)
    8.24 -Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
    8.25 -by tac;
    8.26 -result();
    8.27 -
    8.28 -Goal "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
    8.29 -by tac;
    8.30 -result();
    8.31 -
    8.32 -
    8.33 -Goal "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
    8.34 -by tac;
    8.35 -result();
    8.36 -
    8.37 -
    8.38 -writeln"Some harder ones";
    8.39 -
    8.40 -Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
    8.41 -by tac;
    8.42 -result();
    8.43 -(*6 secs*)
    8.44 -
    8.45 -(*Converse is false*)
    8.46 -Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
    8.47 -by tac;
    8.48 -result();
    8.49 -
    8.50 -
    8.51 -writeln"Basic test of quantifier reasoning";
    8.52 -(*TRUE*)
    8.53 -Goal "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
    8.54 -by tac;
    8.55 -result();
    8.56 -
    8.57 -
    8.58 -Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
    8.59 -by tac;
    8.60 -result();
    8.61 -
    8.62 -
    8.63 -writeln"The following should fail, as they are false!";
    8.64 -
    8.65 -Goal "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
    8.66 -by tac handle ERROR _ => writeln"Failed, as expected";
    8.67 -(*Check that subgoals remain: proof failed.*)
    8.68 -getgoal 1;
    8.69 -
    8.70 -Goal "?p : (EX x. Q(x))  -->  (ALL x. Q(x))";
    8.71 -by tac handle ERROR _ => writeln"Failed, as expected";
    8.72 -getgoal 1;
    8.73 -
    8.74 -Goal "?p : P(?a) --> (ALL x. P(x))";
    8.75 -by tac handle ERROR _ => writeln"Failed, as expected";
    8.76 -(*Check that subgoals remain: proof failed.*)
    8.77 -getgoal 1;
    8.78 -
    8.79 -Goal
    8.80 -    "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
    8.81 -by tac handle ERROR _ => writeln"Failed, as expected";
    8.82 -getgoal 1;
    8.83 -
    8.84 -
    8.85 -writeln"Back to things that are provable...";
    8.86 -
    8.87 -Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
    8.88 -by tac;
    8.89 -result();
    8.90 -
    8.91 -
    8.92 -(*An example of why exI should be delayed as long as possible*)
    8.93 -Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
    8.94 -by tac;
    8.95 -result();
    8.96 -
    8.97 -Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
    8.98 -by tac;
    8.99 -(*Verify that no subgoals remain.*)
   8.100 -uresult();
   8.101 -
   8.102 -
   8.103 -Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
   8.104 -by tac;
   8.105 -result();
   8.106 -
   8.107 -
   8.108 -writeln"Some slow ones";
   8.109 -
   8.110 -
   8.111 -(*Principia Mathematica *11.53  *)
   8.112 -Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
   8.113 -by tac;
   8.114 -result();
   8.115 -(*6 secs*)
   8.116 -
   8.117 -(*Principia Mathematica *11.55  *)
   8.118 -Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
   8.119 -by tac;
   8.120 -result();
   8.121 -(*9 secs*)
   8.122 -
   8.123 -(*Principia Mathematica *11.61  *)
   8.124 -Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
   8.125 -by tac;
   8.126 -result();
   8.127 -(*3 secs*)