1 (* Title: FOL/ex/Propositional_Cla.thy |
1 (* Title: FOL/ex/Propositional_Cla.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* First-Order Logic: propositional examples (classical version) *} |
6 section \<open>First-Order Logic: propositional examples (classical version)\<close> |
7 |
7 |
8 theory Propositional_Cla |
8 theory Propositional_Cla |
9 imports FOL |
9 imports FOL |
10 begin |
10 begin |
11 |
11 |
12 text {* commutative laws of @{text "&"} and @{text "|"} *} |
12 text \<open>commutative laws of @{text "&"} and @{text "|"}\<close> |
13 |
13 |
14 lemma "P & Q --> Q & P" |
14 lemma "P & Q --> Q & P" |
15 by (tactic "IntPr.fast_tac @{context} 1") |
15 by (tactic "IntPr.fast_tac @{context} 1") |
16 |
16 |
17 lemma "P | Q --> Q | P" |
17 lemma "P | Q --> Q | P" |
18 by fast |
18 by fast |
19 |
19 |
20 |
20 |
21 text {* associative laws of @{text "&"} and @{text "|"} *} |
21 text \<open>associative laws of @{text "&"} and @{text "|"}\<close> |
22 lemma "(P & Q) & R --> P & (Q & R)" |
22 lemma "(P & Q) & R --> P & (Q & R)" |
23 by fast |
23 by fast |
24 |
24 |
25 lemma "(P | Q) | R --> P | (Q | R)" |
25 lemma "(P | Q) | R --> P | (Q | R)" |
26 by fast |
26 by fast |
27 |
27 |
28 |
28 |
29 text {* distributive laws of @{text "&"} and @{text "|"} *} |
29 text \<open>distributive laws of @{text "&"} and @{text "|"}\<close> |
30 lemma "(P & Q) | R --> (P | R) & (Q | R)" |
30 lemma "(P & Q) | R --> (P | R) & (Q | R)" |
31 by fast |
31 by fast |
32 |
32 |
33 lemma "(P | R) & (Q | R) --> (P & Q) | R" |
33 lemma "(P | R) & (Q | R) --> (P & Q) | R" |
34 by fast |
34 by fast |
56 |
56 |
57 lemma "(P --> Q & R) <-> (P-->Q) & (P-->R)" |
57 lemma "(P --> Q & R) <-> (P-->Q) & (P-->R)" |
58 by fast |
58 by fast |
59 |
59 |
60 |
60 |
61 text {* Propositions-as-types *} |
61 text \<open>Propositions-as-types\<close> |
62 |
62 |
63 -- {* The combinator K *} |
63 -- \<open>The combinator K\<close> |
64 lemma "P --> (Q --> P)" |
64 lemma "P --> (Q --> P)" |
65 by fast |
65 by fast |
66 |
66 |
67 -- {* The combinator S *} |
67 -- \<open>The combinator S\<close> |
68 lemma "(P-->Q-->R) --> (P-->Q) --> (P-->R)" |
68 lemma "(P-->Q-->R) --> (P-->Q) --> (P-->R)" |
69 by fast |
69 by fast |
70 |
70 |
71 |
71 |
72 -- {* Converse is classical *} |
72 -- \<open>Converse is classical\<close> |
73 lemma "(P-->Q) | (P-->R) --> (P --> Q | R)" |
73 lemma "(P-->Q) | (P-->R) --> (P --> Q | R)" |
74 by fast |
74 by fast |
75 |
75 |
76 lemma "(P-->Q) --> (~Q --> ~P)" |
76 lemma "(P-->Q) --> (~Q --> ~P)" |
77 by fast |
77 by fast |
78 |
78 |
79 |
79 |
80 text {* Schwichtenberg's examples (via T. Nipkow) *} |
80 text \<open>Schwichtenberg's examples (via T. Nipkow)\<close> |
81 |
81 |
82 lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q" |
82 lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q" |
83 by fast |
83 by fast |
84 |
84 |
85 lemma stab_to_peirce: |
85 lemma stab_to_peirce: |