7 |
7 |
8 theory Propositional_Int |
8 theory Propositional_Int |
9 imports IFOL |
9 imports IFOL |
10 begin |
10 begin |
11 |
11 |
12 text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close> |
12 text \<open>commutative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close> |
13 |
13 |
14 lemma "P \<and> Q \<longrightarrow> Q \<and> P" |
14 lemma "P \<and> Q \<longrightarrow> Q \<and> P" |
15 by (tactic "IntPr.fast_tac @{context} 1") |
15 by (tactic "IntPr.fast_tac @{context} 1") |
16 |
16 |
17 lemma "P \<or> Q \<longrightarrow> Q \<or> P" |
17 lemma "P \<or> Q \<longrightarrow> Q \<or> P" |
18 by (tactic "IntPr.fast_tac @{context} 1") |
18 by (tactic "IntPr.fast_tac @{context} 1") |
19 |
19 |
20 |
20 |
21 text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close> |
21 text \<open>associative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close> |
22 lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)" |
22 lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)" |
23 by (tactic "IntPr.fast_tac @{context} 1") |
23 by (tactic "IntPr.fast_tac @{context} 1") |
24 |
24 |
25 lemma "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)" |
25 lemma "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)" |
26 by (tactic "IntPr.fast_tac @{context} 1") |
26 by (tactic "IntPr.fast_tac @{context} 1") |
27 |
27 |
28 |
28 |
29 text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close> |
29 text \<open>distributive laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close> |
30 lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)" |
30 lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)" |
31 by (tactic "IntPr.fast_tac @{context} 1") |
31 by (tactic "IntPr.fast_tac @{context} 1") |
32 |
32 |
33 lemma "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R" |
33 lemma "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R" |
34 by (tactic "IntPr.fast_tac @{context} 1") |
34 by (tactic "IntPr.fast_tac @{context} 1") |
58 by (tactic "IntPr.fast_tac @{context} 1") |
58 by (tactic "IntPr.fast_tac @{context} 1") |
59 |
59 |
60 |
60 |
61 text \<open>Propositions-as-types\<close> |
61 text \<open>Propositions-as-types\<close> |
62 |
62 |
63 -- \<open>The combinator K\<close> |
63 \<comment> \<open>The combinator K\<close> |
64 lemma "P \<longrightarrow> (Q \<longrightarrow> P)" |
64 lemma "P \<longrightarrow> (Q \<longrightarrow> P)" |
65 by (tactic "IntPr.fast_tac @{context} 1") |
65 by (tactic "IntPr.fast_tac @{context} 1") |
66 |
66 |
67 -- \<open>The combinator S\<close> |
67 \<comment> \<open>The combinator S\<close> |
68 lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)" |
68 lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)" |
69 by (tactic "IntPr.fast_tac @{context} 1") |
69 by (tactic "IntPr.fast_tac @{context} 1") |
70 |
70 |
71 |
71 |
72 -- \<open>Converse is classical\<close> |
72 \<comment> \<open>Converse is classical\<close> |
73 lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)" |
73 lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)" |
74 by (tactic "IntPr.fast_tac @{context} 1") |
74 by (tactic "IntPr.fast_tac @{context} 1") |
75 |
75 |
76 lemma "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)" |
76 lemma "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)" |
77 by (tactic "IntPr.fast_tac @{context} 1") |
77 by (tactic "IntPr.fast_tac @{context} 1") |