1.1 --- a/src/FOL/IsaMakefile Sun Jul 22 21:20:58 2007 +0200
1.2 +++ b/src/FOL/IsaMakefile Sun Jul 22 22:01:30 2007 +0200
1.3 @@ -50,7 +50,9 @@
1.4 ex/If.thy ex/IffOracle.thy ex/LocaleTest.thy \
1.5 ex/Nat.thy ex/Natural_Numbers.thy ex/Miniscope.thy \
1.6 ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex \
1.7 - ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy ex/prop.ML ex/quant.ML
1.8 + ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy \
1.9 + ex/Propositional_Int.thy ex/Propositional_Cla.thy \
1.10 + ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
1.11 @$(ISATOOL) usedir $(OUT)/FOL ex
1.12
1.13
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/FOL/ex/Propositional_Cla.thy Sun Jul 22 22:01:30 2007 +0200
2.3 @@ -0,0 +1,118 @@
2.4 +(* Title: FOL/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 (classical version) *}
2.11 +
2.12 +theory Propositional_Cla
2.13 +imports FOL
2.14 +begin
2.15 +
2.16 +text {* commutative laws of @{text "&"} and @{text "|"} *}
2.17 +
2.18 +lemma "P & Q --> Q & P"
2.19 + by (tactic "IntPr.fast_tac 1")
2.20 +
2.21 +lemma "P | Q --> Q | P"
2.22 + by fast
2.23 +
2.24 +
2.25 +text {* associative laws of @{text "&"} and @{text "|"} *}
2.26 +lemma "(P & Q) & R --> P & (Q & R)"
2.27 + by fast
2.28 +
2.29 +lemma "(P | Q) | R --> P | (Q | R)"
2.30 + by fast
2.31 +
2.32 +
2.33 +text {* distributive laws of @{text "&"} and @{text "|"} *}
2.34 +lemma "(P & Q) | R --> (P | R) & (Q | R)"
2.35 + by fast
2.36 +
2.37 +lemma "(P | R) & (Q | R) --> (P & Q) | R"
2.38 + by fast
2.39 +
2.40 +lemma "(P | Q) & R --> (P & R) | (Q & R)"
2.41 + by fast
2.42 +
2.43 +lemma "(P & R) | (Q & R) --> (P | Q) & R"
2.44 + by fast
2.45 +
2.46 +
2.47 +text {* Laws involving implication *}
2.48 +
2.49 +lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
2.50 + by fast
2.51 +
2.52 +lemma "(P & Q --> R) <-> (P--> (Q-->R))"
2.53 + by fast
2.54 +
2.55 +lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
2.56 + by fast
2.57 +
2.58 +lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
2.59 + by fast
2.60 +
2.61 +lemma "(P --> Q & R) <-> (P-->Q) & (P-->R)"
2.62 + by fast
2.63 +
2.64 +
2.65 +text {* Propositions-as-types *}
2.66 +
2.67 +-- {* The combinator K *}
2.68 +lemma "P --> (Q --> P)"
2.69 + by fast
2.70 +
2.71 +-- {* The combinator S *}
2.72 +lemma "(P-->Q-->R) --> (P-->Q) --> (P-->R)"
2.73 + by fast
2.74 +
2.75 +
2.76 +-- {* Converse is classical *}
2.77 +lemma "(P-->Q) | (P-->R) --> (P --> Q | R)"
2.78 + by fast
2.79 +
2.80 +lemma "(P-->Q) --> (~Q --> ~P)"
2.81 + by fast
2.82 +
2.83 +
2.84 +text {* Schwichtenberg's examples (via T. Nipkow) *}
2.85 +
2.86 +lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
2.87 + by fast
2.88 +
2.89 +lemma stab_to_peirce:
2.90 + "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
2.91 + --> ((P --> Q) --> P) --> P"
2.92 + by fast
2.93 +
2.94 +lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)
2.95 + --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
2.96 + by fast
2.97 +
2.98 +lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
2.99 + by fast
2.100 +
2.101 +lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
2.102 + by fast
2.103 +
2.104 +lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
2.105 + by fast
2.106 +
2.107 +lemma tatsuta: "(((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 fast
2.113 +
2.114 +lemma tatsuta1: "(((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 fast
2.120 +
2.121 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/FOL/ex/Propositional_Int.thy Sun Jul 22 22:01:30 2007 +0200
3.3 @@ -0,0 +1,118 @@
3.4 +(* Title: FOL/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 (intuitionistic version) *}
3.11 +
3.12 +theory Propositional_Int
3.13 +imports IFOL
3.14 +begin
3.15 +
3.16 +text {* commutative laws of @{text "&"} and @{text "|"} *}
3.17 +
3.18 +lemma "P & Q --> Q & P"
3.19 + by (tactic "IntPr.fast_tac 1")
3.20 +
3.21 +lemma "P | Q --> Q | P"
3.22 + by (tactic "IntPr.fast_tac 1")
3.23 +
3.24 +
3.25 +text {* associative laws of @{text "&"} and @{text "|"} *}
3.26 +lemma "(P & Q) & R --> P & (Q & R)"
3.27 + by (tactic "IntPr.fast_tac 1")
3.28 +
3.29 +lemma "(P | Q) | R --> P | (Q | R)"
3.30 + by (tactic "IntPr.fast_tac 1")
3.31 +
3.32 +
3.33 +text {* distributive laws of @{text "&"} and @{text "|"} *}
3.34 +lemma "(P & Q) | R --> (P | R) & (Q | R)"
3.35 + by (tactic "IntPr.fast_tac 1")
3.36 +
3.37 +lemma "(P | R) & (Q | R) --> (P & Q) | R"
3.38 + by (tactic "IntPr.fast_tac 1")
3.39 +
3.40 +lemma "(P | Q) & R --> (P & R) | (Q & R)"
3.41 + by (tactic "IntPr.fast_tac 1")
3.42 +
3.43 +lemma "(P & R) | (Q & R) --> (P | Q) & R"
3.44 + by (tactic "IntPr.fast_tac 1")
3.45 +
3.46 +
3.47 +text {* Laws involving implication *}
3.48 +
3.49 +lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
3.50 + by (tactic "IntPr.fast_tac 1")
3.51 +
3.52 +lemma "(P & Q --> R) <-> (P--> (Q-->R))"
3.53 + by (tactic "IntPr.fast_tac 1")
3.54 +
3.55 +lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
3.56 + by (tactic "IntPr.fast_tac 1")
3.57 +
3.58 +lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
3.59 + by (tactic "IntPr.fast_tac 1")
3.60 +
3.61 +lemma "(P --> Q & R) <-> (P-->Q) & (P-->R)"
3.62 + by (tactic "IntPr.fast_tac 1")
3.63 +
3.64 +
3.65 +text {* Propositions-as-types *}
3.66 +
3.67 +-- {* The combinator K *}
3.68 +lemma "P --> (Q --> P)"
3.69 + by (tactic "IntPr.fast_tac 1")
3.70 +
3.71 +-- {* The combinator S *}
3.72 +lemma "(P-->Q-->R) --> (P-->Q) --> (P-->R)"
3.73 + by (tactic "IntPr.fast_tac 1")
3.74 +
3.75 +
3.76 +-- {* Converse is classical *}
3.77 +lemma "(P-->Q) | (P-->R) --> (P --> Q | R)"
3.78 + by (tactic "IntPr.fast_tac 1")
3.79 +
3.80 +lemma "(P-->Q) --> (~Q --> ~P)"
3.81 + by (tactic "IntPr.fast_tac 1")
3.82 +
3.83 +
3.84 +text {* Schwichtenberg's examples (via T. Nipkow) *}
3.85 +
3.86 +lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
3.87 + by (tactic "IntPr.fast_tac 1")
3.88 +
3.89 +lemma stab_to_peirce:
3.90 + "(((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: "(((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 --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
3.99 + by (tactic "IntPr.fast_tac 1")
3.100 +
3.101 +lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
3.102 + by (tactic "IntPr.fast_tac 1")
3.103 +
3.104 +lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
3.105 + by (tactic "IntPr.fast_tac 1")
3.106 +
3.107 +lemma tatsuta: "(((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: "(((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/FOL/ex/Quantifiers_Cla.thy Sun Jul 22 22:01:30 2007 +0200
4.3 @@ -0,0 +1,101 @@
4.4 +(* Title: FOL/ex/Quantifiers_Int.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 +
4.10 +header {* First-Order Logic: quantifier examples (classical version) *}
4.11 +
4.12 +theory Quantifiers_Cla
4.13 +imports FOL
4.14 +begin
4.15 +
4.16 +lemma "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
4.17 + by fast
4.18 +
4.19 +lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
4.20 + by fast
4.21 +
4.22 +
4.23 +-- {* Converse is false *}
4.24 +lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
4.25 + by fast
4.26 +
4.27 +lemma "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
4.28 + by fast
4.29 +
4.30 +
4.31 +lemma "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
4.32 + by fast
4.33 +
4.34 +
4.35 +text {* Some harder ones *}
4.36 +
4.37 +lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
4.38 + by fast
4.39 +
4.40 +-- {* Converse is false *}
4.41 +lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
4.42 + by fast
4.43 +
4.44 +
4.45 +text {* Basic test of quantifier reasoning *}
4.46 +
4.47 +-- {* TRUE *}
4.48 +lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
4.49 + by fast
4.50 +
4.51 +lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
4.52 + by fast
4.53 +
4.54 +
4.55 +text {* The following should fail, as they are false! *}
4.56 +
4.57 +lemma "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
4.58 + apply fast?
4.59 + oops
4.60 +
4.61 +lemma "(EX x. Q(x)) --> (ALL x. Q(x))"
4.62 + apply fast?
4.63 + oops
4.64 +
4.65 +lemma "P(?a) --> (ALL x. P(x))"
4.66 + apply fast?
4.67 + oops
4.68 +
4.69 +lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
4.70 + apply fast?
4.71 + oops
4.72 +
4.73 +
4.74 +text {* Back to things that are provable \dots *}
4.75 +
4.76 +lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
4.77 + by fast
4.78 +
4.79 +-- {* An example of why exI should be delayed as long as possible *}
4.80 +lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
4.81 + by fast
4.82 +
4.83 +lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
4.84 + by fast
4.85 +
4.86 +lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
4.87 + by fast
4.88 +
4.89 +
4.90 +text {* Some slow ones *}
4.91 +
4.92 +-- {* Principia Mathematica *11.53 *}
4.93 +lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
4.94 + by fast
4.95 +
4.96 +(*Principia Mathematica *11.55 *)
4.97 +lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
4.98 + by fast
4.99 +
4.100 +(*Principia Mathematica *11.61 *)
4.101 +lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
4.102 + by fast
4.103 +
4.104 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/FOL/ex/Quantifiers_Int.thy Sun Jul 22 22:01:30 2007 +0200
5.3 @@ -0,0 +1,101 @@
5.4 +(* Title: FOL/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 +
5.10 +header {* First-Order Logic: quantifier examples (intuitionistic version) *}
5.11 +
5.12 +theory Quantifiers_Int
5.13 +imports IFOL
5.14 +begin
5.15 +
5.16 +lemma "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
5.17 + by (tactic "IntPr.fast_tac 1")
5.18 +
5.19 +lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
5.20 + by (tactic "IntPr.fast_tac 1")
5.21 +
5.22 +
5.23 +-- {* Converse is false *}
5.24 +lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
5.25 + by (tactic "IntPr.fast_tac 1")
5.26 +
5.27 +lemma "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
5.28 + by (tactic "IntPr.fast_tac 1")
5.29 +
5.30 +
5.31 +lemma "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
5.32 + by (tactic "IntPr.fast_tac 1")
5.33 +
5.34 +
5.35 +text {* Some harder ones *}
5.36 +
5.37 +lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
5.38 + by (tactic "IntPr.fast_tac 1")
5.39 +
5.40 +-- {* Converse is false *}
5.41 +lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
5.42 + by (tactic "IntPr.fast_tac 1")
5.43 +
5.44 +
5.45 +text {* Basic test of quantifier reasoning *}
5.46 +
5.47 +-- {* TRUE *}
5.48 +lemma "(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 "(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 "(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 "(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(?a) --> (ALL x. P(x))"
5.66 + apply (tactic "IntPr.fast_tac 1")?
5.67 + oops
5.68 +
5.69 +lemma "(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 \dots *}
5.75 +
5.76 +lemma "(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 +-- {* An example of why exI should be delayed as long as possible *}
5.80 +lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
5.81 + by (tactic "IntPr.fast_tac 1")
5.82 +
5.83 +lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
5.84 + by (tactic "IntPr.fast_tac 1")
5.85 +
5.86 +lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
5.87 + by (tactic "IntPr.fast_tac 1")
5.88 +
5.89 +
5.90 +text {* Some slow ones *}
5.91 +
5.92 +-- {* Principia Mathematica *11.53 *}
5.93 +lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
5.94 + by (tactic "IntPr.fast_tac 1")
5.95 +
5.96 +(*Principia Mathematica *11.55 *)
5.97 +lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
5.98 + by (tactic "IntPr.fast_tac 1")
5.99 +
5.100 +(*Principia Mathematica *11.61 *)
5.101 +lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
5.102 + by (tactic "IntPr.fast_tac 1")
5.103 +
5.104 +end
6.1 --- a/src/FOL/ex/ROOT.ML Sun Jul 22 21:20:58 2007 +0200
6.2 +++ b/src/FOL/ex/ROOT.ML Sun Jul 22 22:01:30 2007 +0200
6.3 @@ -6,31 +6,27 @@
6.4 Examples for First-Order Logic.
6.5 *)
6.6
6.7 -time_use_thy "First_Order_Logic";
6.8 -time_use_thy "Natural_Numbers";
6.9 -time_use_thy "Intro";
6.10 -time_use_thy "Nat";
6.11 -time_use_thy "Foundation";
6.12 -time_use_thy "Prolog";
6.13 +use_thys [
6.14 + "First_Order_Logic",
6.15 + "Natural_Numbers",
6.16 + "Intro",
6.17 + "Nat",
6.18 + "Foundation",
6.19 + "Prolog",
6.20
6.21 -time_use_thy "Intuitionistic";
6.22 + "Intuitionistic",
6.23 + "Propositional_Int",
6.24 + "Quantifiers_Int",
6.25
6.26 -val thy = theory "IFOL" and tac = IntPr.fast_tac 1;
6.27 -time_use "prop.ML";
6.28 -time_use "quant.ML";
6.29 + "Classical",
6.30 + "Propositional_Cla",
6.31 + "Quantifiers_Cla",
6.32 + "Miniscope",
6.33 + "If",
6.34
6.35 -writeln"\n** Classical examples **\n";
6.36 -time_use_thy "Miniscope";
6.37 -time_use_thy "Classical";
6.38 -time_use_thy "If";
6.39 -
6.40 -val thy = theory "FOL" and tac = Cla.fast_tac FOL_cs 1;
6.41 -time_use "prop.ML";
6.42 -time_use "quant.ML";
6.43 -
6.44 -time_use_thy "NatClass";
6.45 -
6.46 -time_use_thy "IffOracle";
6.47 + "NatClass",
6.48 + "IffOracle"
6.49 +];
6.50
6.51 (*regression test for locales -- sets several global flags!*)
6.52 -time_use_thy "LocaleTest";
6.53 +no_document use_thy "LocaleTest";
7.1 --- a/src/FOL/ex/prop.ML Sun Jul 22 21:20:58 2007 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,153 +0,0 @@
7.4 -(* Title: FOL/ex/prop
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 -writeln"File FOL/ex/prop.";
7.14 -
7.15 -
7.16 -writeln"commutative laws of & and | ";
7.17 -Goal "P & Q --> Q & P";
7.18 -by tac;
7.19 -result();
7.20 -
7.21 -Goal "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 & Q) & R --> P & (Q & R)";
7.28 -by tac;
7.29 -result();
7.30 -
7.31 -Goal "(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 & Q) | R --> (P | R) & (Q | R)";
7.39 -by tac;
7.40 -result();
7.41 -
7.42 -Goal "(P | R) & (Q | R) --> (P & Q) | R";
7.43 -by tac;
7.44 -result();
7.45 -
7.46 -Goal "(P | Q) & R --> (P & R) | (Q & R)";
7.47 -by tac;
7.48 -result();
7.49 -
7.50 -
7.51 -Goal "(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-->R) & (Q-->R) <-> (P|Q --> R)";
7.59 -by tac;
7.60 -result();
7.61 -
7.62 -
7.63 -Goal "(P & Q --> R) <-> (P--> (Q-->R))";
7.64 -by tac;
7.65 -result();
7.66 -
7.67 -
7.68 -Goal "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
7.69 -by tac;
7.70 -result();
7.71 -
7.72 -Goal "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
7.73 -by tac;
7.74 -result();
7.75 -
7.76 -Goal "(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 --> (Q --> P)";
7.85 -by tac;
7.86 -result();
7.87 -
7.88 -(*The combinator S*)
7.89 -Goal "(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-->Q) | (P-->R) --> (P --> Q | R)";
7.96 -by tac;
7.97 -result();
7.98 -
7.99 -Goal "(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 "(((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 --> 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 "(((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 --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
7.125 -by tac;
7.126 -result();
7.127 -
7.128 -(* mints *)
7.129 -Goal "((((P --> Q) --> P) --> P) --> Q) --> Q";
7.130 -by tac;
7.131 -result();
7.132 -
7.133 -(* mints-solovev *)
7.134 -Goal "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
7.135 -by tac;
7.136 -result();
7.137 -
7.138 -(* tatsuta *)
7.139 -Goal "(((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 "(((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();
7.155 -
7.156 -writeln"Reached end of file.";
8.1 --- a/src/FOL/ex/quant.ML Sun Jul 22 21:20:58 2007 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,129 +0,0 @@
8.4 -(* Title: FOL/ex/quant
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 -writeln"File FOL/ex/quant.";
8.14 -
8.15 -Goal "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
8.16 -by tac;
8.17 -result();
8.18 -
8.19 -
8.20 -Goal "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
8.21 -by tac;
8.22 -result();
8.23 -
8.24 -
8.25 -(*Converse is false*)
8.26 -Goal "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
8.27 -by tac;
8.28 -result();
8.29 -
8.30 -Goal "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
8.31 -by tac;
8.32 -result();
8.33 -
8.34 -
8.35 -Goal "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
8.36 -by tac;
8.37 -result();
8.38 -
8.39 -
8.40 -writeln"Some harder ones";
8.41 -
8.42 -Goal "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
8.43 -by tac;
8.44 -result();
8.45 -(*6 secs*)
8.46 -
8.47 -(*Converse is false*)
8.48 -Goal "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
8.49 -by tac;
8.50 -result();
8.51 -
8.52 -
8.53 -writeln"Basic test of quantifier reasoning";
8.54 -(*TRUE*)
8.55 -Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
8.56 -by tac;
8.57 -result();
8.58 -
8.59 -
8.60 -Goal "(ALL x. Q(x)) --> (EX x. Q(x))";
8.61 -by tac;
8.62 -result();
8.63 -
8.64 -
8.65 -writeln"The following should fail, as they are false!";
8.66 -
8.67 -Goal "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
8.68 -by tac handle ERROR _ => writeln"Failed, as expected";
8.69 -(*Check that subgoals remain: proof failed.*)
8.70 -getgoal 1;
8.71 -
8.72 -Goal "(EX x. Q(x)) --> (ALL x. Q(x))";
8.73 -by tac handle ERROR _ => writeln"Failed, as expected";
8.74 -getgoal 1;
8.75 -
8.76 -Goal "P(?a) --> (ALL x. P(x))";
8.77 -by tac handle ERROR _ => writeln"Failed, as expected";
8.78 -(*Check that subgoals remain: proof failed.*)
8.79 -getgoal 1;
8.80 -
8.81 -Goal
8.82 - "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
8.83 -by tac handle ERROR _ => writeln"Failed, as expected";
8.84 -getgoal 1;
8.85 -
8.86 -
8.87 -writeln"Back to things that are provable...";
8.88 -
8.89 -Goal "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
8.90 -by tac;
8.91 -result();
8.92 -
8.93 -
8.94 -(*An example of why exI should be delayed as long as possible*)
8.95 -Goal "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
8.96 -by tac;
8.97 -result();
8.98 -
8.99 -Goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
8.100 -by tac;
8.101 -(*Verify that no subgoals remain.*)
8.102 -uresult();
8.103 -
8.104 -
8.105 -Goal "(ALL x. Q(x)) --> (EX x. Q(x))";
8.106 -by tac;
8.107 -result();
8.108 -
8.109 -
8.110 -writeln"Some slow ones";
8.111 -
8.112 -
8.113 -(*Principia Mathematica *11.53 *)
8.114 -Goal "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
8.115 -by tac;
8.116 -result();
8.117 -(*6 secs*)
8.118 -
8.119 -(*Principia Mathematica *11.55 *)
8.120 -Goal "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
8.121 -by tac;
8.122 -result();
8.123 -(*9 secs*)
8.124 -
8.125 -(*Principia Mathematica *11.61 *)
8.126 -Goal "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
8.127 -by tac;
8.128 -result();
8.129 -(*3 secs*)
8.130 -
8.131 -writeln"Reached end of file.";
8.132 -