7 |
7 |
8 theory Foundation |
8 theory Foundation |
9 imports IFOL |
9 imports IFOL |
10 begin |
10 begin |
11 |
11 |
12 lemma "A \<and> B \<longrightarrow> (C \<longrightarrow> A \<and> C)" |
12 lemma \<open>A \<and> B \<longrightarrow> (C \<longrightarrow> A \<and> C)\<close> |
13 apply (rule impI) |
13 apply (rule impI) |
14 apply (rule impI) |
14 apply (rule impI) |
15 apply (rule conjI) |
15 apply (rule conjI) |
16 prefer 2 apply assumption |
16 prefer 2 apply assumption |
17 apply (rule conjunct1) |
17 apply (rule conjunct1) |
18 apply assumption |
18 apply assumption |
19 done |
19 done |
20 |
20 |
21 text \<open>A form of conj-elimination\<close> |
21 text \<open>A form of conj-elimination\<close> |
22 lemma |
22 lemma |
23 assumes "A \<and> B" |
23 assumes \<open>A \<and> B\<close> |
24 and "A \<Longrightarrow> B \<Longrightarrow> C" |
24 and \<open>A \<Longrightarrow> B \<Longrightarrow> C\<close> |
25 shows C |
25 shows \<open>C\<close> |
26 apply (rule assms) |
26 apply (rule assms) |
27 apply (rule conjunct1) |
27 apply (rule conjunct1) |
28 apply (rule assms) |
28 apply (rule assms) |
29 apply (rule conjunct2) |
29 apply (rule conjunct2) |
30 apply (rule assms) |
30 apply (rule assms) |
31 done |
31 done |
32 |
32 |
33 lemma |
33 lemma |
34 assumes "\<And>A. \<not> \<not> A \<Longrightarrow> A" |
34 assumes \<open>\<And>A. \<not> \<not> A \<Longrightarrow> A\<close> |
35 shows "B \<or> \<not> B" |
35 shows \<open>B \<or> \<not> B\<close> |
36 apply (rule assms) |
36 apply (rule assms) |
37 apply (rule notI) |
37 apply (rule notI) |
38 apply (rule_tac P = "\<not> B" in notE) |
38 apply (rule_tac P = \<open>\<not> B\<close> in notE) |
39 apply (rule_tac [2] notI) |
39 apply (rule_tac [2] notI) |
40 apply (rule_tac [2] P = "B \<or> \<not> B" in notE) |
40 apply (rule_tac [2] P = \<open>B \<or> \<not> B\<close> in notE) |
41 prefer 2 apply assumption |
41 prefer 2 apply assumption |
42 apply (rule_tac [2] disjI1) |
42 apply (rule_tac [2] disjI1) |
43 prefer 2 apply assumption |
43 prefer 2 apply assumption |
44 apply (rule notI) |
44 apply (rule notI) |
45 apply (rule_tac P = "B \<or> \<not> B" in notE) |
45 apply (rule_tac P = \<open>B \<or> \<not> B\<close> in notE) |
46 apply assumption |
46 apply assumption |
47 apply (rule disjI2) |
47 apply (rule disjI2) |
48 apply assumption |
48 apply assumption |
49 done |
49 done |
50 |
50 |
51 lemma |
51 lemma |
52 assumes "\<And>A. \<not> \<not> A \<Longrightarrow> A" |
52 assumes \<open>\<And>A. \<not> \<not> A \<Longrightarrow> A\<close> |
53 shows "B \<or> \<not> B" |
53 shows \<open>B \<or> \<not> B\<close> |
54 apply (rule assms) |
54 apply (rule assms) |
55 apply (rule notI) |
55 apply (rule notI) |
56 apply (rule notE) |
56 apply (rule notE) |
57 apply (rule_tac [2] notI) |
57 apply (rule_tac [2] notI) |
58 apply (erule_tac [2] notE) |
58 apply (erule_tac [2] notE) |
62 apply (erule disjI2) |
62 apply (erule disjI2) |
63 done |
63 done |
64 |
64 |
65 |
65 |
66 lemma |
66 lemma |
67 assumes "A \<or> \<not> A" |
67 assumes \<open>A \<or> \<not> A\<close> |
68 and "\<not> \<not> A" |
68 and \<open>\<not> \<not> A\<close> |
69 shows A |
69 shows \<open>A\<close> |
70 apply (rule disjE) |
70 apply (rule disjE) |
71 apply (rule assms) |
71 apply (rule assms) |
72 apply assumption |
72 apply assumption |
73 apply (rule FalseE) |
73 apply (rule FalseE) |
74 apply (rule_tac P = "\<not> A" in notE) |
74 apply (rule_tac P = \<open>\<not> A\<close> in notE) |
75 apply (rule assms) |
75 apply (rule assms) |
76 apply assumption |
76 apply assumption |
77 done |
77 done |
78 |
78 |
79 |
79 |
80 subsection "Examples with quantifiers" |
80 subsection "Examples with quantifiers" |
81 |
81 |
82 lemma |
82 lemma |
83 assumes "\<forall>z. G(z)" |
83 assumes \<open>\<forall>z. G(z)\<close> |
84 shows "\<forall>z. G(z) \<or> H(z)" |
84 shows \<open>\<forall>z. G(z) \<or> H(z)\<close> |
85 apply (rule allI) |
85 apply (rule allI) |
86 apply (rule disjI1) |
86 apply (rule disjI1) |
87 apply (rule assms [THEN spec]) |
87 apply (rule assms [THEN spec]) |
88 done |
88 done |
89 |
89 |
90 lemma "\<forall>x. \<exists>y. x = y" |
90 lemma \<open>\<forall>x. \<exists>y. x = y\<close> |
91 apply (rule allI) |
91 apply (rule allI) |
92 apply (rule exI) |
92 apply (rule exI) |
93 apply (rule refl) |
93 apply (rule refl) |
94 done |
94 done |
95 |
95 |
96 lemma "\<exists>y. \<forall>x. x = y" |
96 lemma \<open>\<exists>y. \<forall>x. x = y\<close> |
97 apply (rule exI) |
97 apply (rule exI) |
98 apply (rule allI) |
98 apply (rule allI) |
99 apply (rule refl)? |
99 apply (rule refl)? |
100 oops |
100 oops |
101 |
101 |
102 text \<open>Parallel lifting example.\<close> |
102 text \<open>Parallel lifting example.\<close> |
103 lemma "\<exists>u. \<forall>x. \<exists>v. \<forall>y. \<exists>w. P(u,x,v,y,w)" |
103 lemma \<open>\<exists>u. \<forall>x. \<exists>v. \<forall>y. \<exists>w. P(u,x,v,y,w)\<close> |
104 apply (rule exI allI) |
104 apply (rule exI allI) |
105 apply (rule exI allI) |
105 apply (rule exI allI) |
106 apply (rule exI allI) |
106 apply (rule exI allI) |
107 apply (rule exI allI) |
107 apply (rule exI allI) |
108 apply (rule exI allI) |
108 apply (rule exI allI) |
109 oops |
109 oops |
110 |
110 |
111 lemma |
111 lemma |
112 assumes "(\<exists>z. F(z)) \<and> B" |
112 assumes \<open>(\<exists>z. F(z)) \<and> B\<close> |
113 shows "\<exists>z. F(z) \<and> B" |
113 shows \<open>\<exists>z. F(z) \<and> B\<close> |
114 apply (rule conjE) |
114 apply (rule conjE) |
115 apply (rule assms) |
115 apply (rule assms) |
116 apply (rule exE) |
116 apply (rule exE) |
117 apply assumption |
117 apply assumption |
118 apply (rule exI) |
118 apply (rule exI) |
120 apply assumption |
120 apply assumption |
121 apply assumption |
121 apply assumption |
122 done |
122 done |
123 |
123 |
124 text \<open>A bigger demonstration of quantifiers -- not in the paper.\<close> |
124 text \<open>A bigger demonstration of quantifiers -- not in the paper.\<close> |
125 lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))" |
125 lemma \<open>(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))\<close> |
126 apply (rule impI) |
126 apply (rule impI) |
127 apply (rule allI) |
127 apply (rule allI) |
128 apply (rule exE, assumption) |
128 apply (rule exE, assumption) |
129 apply (rule exI) |
129 apply (rule exI) |
130 apply (rule allE, assumption) |
130 apply (rule allE, assumption) |