author | wenzelm |
Thu, 13 Nov 2014 23:45:15 +0100 | |
changeset 58999 | ed09ae4ea2d8 |
parent 58889 | 5b7a9633cfa8 |
child 61420 | ee42cba50933 |
permissions | -rw-r--r-- |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
1 |
|
58889 | 2 |
section \<open>Example: First-Order Logic\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
3 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
4 |
theory %visible First_Order_Logic |
42651 | 5 |
imports Base (* FIXME Pure!? *) |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
6 |
begin |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
7 |
|
58618 | 8 |
text \<open> |
29732 | 9 |
\noindent In order to commence a new object-logic within |
10 |
Isabelle/Pure we introduce abstract syntactic categories @{text "i"} |
|
11 |
for individuals and @{text "o"} for object-propositions. The latter |
|
12 |
is embedded into the language of Pure propositions by means of a |
|
13 |
separate judgment. |
|
58618 | 14 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
15 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
16 |
typedecl i |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
17 |
typedecl o |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
18 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
19 |
judgment |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
20 |
Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
21 |
|
58618 | 22 |
text \<open> |
56594 | 23 |
\noindent Note that the object-logic judgment is implicit in the |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
24 |
syntax: writing @{prop A} produces @{term "Trueprop A"} internally. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
25 |
From the Pure perspective this means ``@{prop A} is derivable in the |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
26 |
object-logic''. |
58618 | 27 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
28 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
29 |
|
58618 | 30 |
subsection \<open>Equational reasoning \label{sec:framework-ex-equal}\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
31 |
|
58618 | 32 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
33 |
Equality is axiomatized as a binary predicate on individuals, with |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
34 |
reflexivity as introduction, and substitution as elimination |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
35 |
principle. Note that the latter is particularly convenient in a |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
36 |
framework like Isabelle, because syntactic congruences are |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
37 |
implicitly produced by unification of @{term "B x"} against |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
38 |
expressions containing occurrences of @{term x}. |
58618 | 39 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
40 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
41 |
axiomatization |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
42 |
equal :: "i \<Rightarrow> i \<Rightarrow> o" (infix "=" 50) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
43 |
where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
44 |
refl [intro]: "x = x" and |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
45 |
subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
46 |
|
58618 | 47 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
48 |
\noindent Substitution is very powerful, but also hard to control in |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
49 |
full generality. We derive some common symmetry~/ transitivity |
45103 | 50 |
schemes of @{term equal} as particular consequences. |
58618 | 51 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
52 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
53 |
theorem sym [sym]: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
54 |
assumes "x = y" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
55 |
shows "y = x" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
56 |
proof - |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
57 |
have "x = x" .. |
58618 | 58 |
with \<open>x = y\<close> show "y = x" .. |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
59 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
60 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
61 |
theorem forw_subst [trans]: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
62 |
assumes "y = x" and "B x" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
63 |
shows "B y" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
64 |
proof - |
58618 | 65 |
from \<open>y = x\<close> have "x = y" .. |
66 |
from this and \<open>B x\<close> show "B y" .. |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
67 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
68 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
69 |
theorem back_subst [trans]: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
70 |
assumes "B x" and "x = y" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
71 |
shows "B y" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
72 |
proof - |
58618 | 73 |
from \<open>x = y\<close> and \<open>B x\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
74 |
show "B y" .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
75 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
76 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
77 |
theorem trans [trans]: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
78 |
assumes "x = y" and "y = z" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
79 |
shows "x = z" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
80 |
proof - |
58618 | 81 |
from \<open>y = z\<close> and \<open>x = y\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
82 |
show "x = z" .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
83 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
84 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
85 |
|
58618 | 86 |
subsection \<open>Basic group theory\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
87 |
|
58618 | 88 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
89 |
As an example for equational reasoning we consider some bits of |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
90 |
group theory. The subsequent locale definition postulates group |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
91 |
operations and axioms; we also derive some consequences of this |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
92 |
specification. |
58618 | 93 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
94 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
95 |
locale group = |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
96 |
fixes prod :: "i \<Rightarrow> i \<Rightarrow> i" (infix "\<circ>" 70) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
97 |
and inv :: "i \<Rightarrow> i" ("(_\<inverse>)" [1000] 999) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
98 |
and unit :: i ("1") |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
99 |
assumes assoc: "(x \<circ> y) \<circ> z = x \<circ> (y \<circ> z)" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
100 |
and left_unit: "1 \<circ> x = x" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
101 |
and left_inv: "x\<inverse> \<circ> x = 1" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
102 |
begin |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
103 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
104 |
theorem right_inv: "x \<circ> x\<inverse> = 1" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
105 |
proof - |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
106 |
have "x \<circ> x\<inverse> = 1 \<circ> (x \<circ> x\<inverse>)" by (rule left_unit [symmetric]) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
107 |
also have "\<dots> = (1 \<circ> x) \<circ> x\<inverse>" by (rule assoc [symmetric]) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
108 |
also have "1 = (x\<inverse>)\<inverse> \<circ> x\<inverse>" by (rule left_inv [symmetric]) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
109 |
also have "\<dots> \<circ> x = (x\<inverse>)\<inverse> \<circ> (x\<inverse> \<circ> x)" by (rule assoc) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
110 |
also have "x\<inverse> \<circ> x = 1" by (rule left_inv) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
111 |
also have "((x\<inverse>)\<inverse> \<circ> \<dots>) \<circ> x\<inverse> = (x\<inverse>)\<inverse> \<circ> (1 \<circ> x\<inverse>)" by (rule assoc) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
112 |
also have "1 \<circ> x\<inverse> = x\<inverse>" by (rule left_unit) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
113 |
also have "(x\<inverse>)\<inverse> \<circ> \<dots> = 1" by (rule left_inv) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
114 |
finally show "x \<circ> x\<inverse> = 1" . |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
115 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
116 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
117 |
theorem right_unit: "x \<circ> 1 = x" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
118 |
proof - |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
119 |
have "1 = x\<inverse> \<circ> x" by (rule left_inv [symmetric]) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
120 |
also have "x \<circ> \<dots> = (x \<circ> x\<inverse>) \<circ> x" by (rule assoc [symmetric]) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
121 |
also have "x \<circ> x\<inverse> = 1" by (rule right_inv) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
122 |
also have "\<dots> \<circ> x = x" by (rule left_unit) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
123 |
finally show "x \<circ> 1 = x" . |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
124 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
125 |
|
58618 | 126 |
text \<open> |
29732 | 127 |
\noindent Reasoning from basic axioms is often tedious. Our proofs |
128 |
work by producing various instances of the given rules (potentially |
|
129 |
the symmetric form) using the pattern ``@{command have}~@{text |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
130 |
eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
131 |
results via @{command also}/@{command finally}. These steps may |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
132 |
involve any of the transitivity rules declared in |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
133 |
\secref{sec:framework-ex-equal}, namely @{thm trans} in combining |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
134 |
the first two results in @{thm right_inv} and in the final steps of |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
135 |
both proofs, @{thm forw_subst} in the first combination of @{thm |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
136 |
right_unit}, and @{thm back_subst} in all other calculational steps. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
137 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
138 |
Occasional substitutions in calculations are adequate, but should |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
139 |
not be over-emphasized. The other extreme is to compose a chain by |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
140 |
plain transitivity only, with replacements occurring always in |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
141 |
topmost position. For example: |
58618 | 142 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
143 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
144 |
(*<*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
145 |
theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
146 |
proof - |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
147 |
assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)" |
56594 | 148 |
fix x |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
149 |
(*>*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
150 |
have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
151 |
also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
152 |
also have "\<dots> = 1 \<circ> x" unfolding right_inv .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
153 |
also have "\<dots> = x" unfolding left_unit .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
154 |
finally have "x \<circ> 1 = x" . |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
155 |
(*<*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
156 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
157 |
(*>*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
158 |
|
58618 | 159 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
160 |
\noindent Here we have re-used the built-in mechanism for unfolding |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
161 |
definitions in order to normalize each equational problem. A more |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
162 |
realistic object-logic would include proper setup for the Simplifier |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
163 |
(\secref{sec:simplifier}), the main automated tool for equational |
29732 | 164 |
reasoning in Isabelle. Then ``@{command unfolding}~@{thm |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
165 |
left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text |
29735 | 166 |
"(simp only: left_inv)"}'' etc. |
58618 | 167 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
168 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
169 |
end |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
170 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
171 |
|
58618 | 172 |
subsection \<open>Propositional logic \label{sec:framework-ex-prop}\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
173 |
|
58618 | 174 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
175 |
We axiomatize basic connectives of propositional logic: implication, |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
176 |
disjunction, and conjunction. The associated rules are modeled |
58552 | 177 |
after Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}. |
58618 | 178 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
179 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
180 |
axiomatization |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
181 |
imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
182 |
impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
183 |
impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
184 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
185 |
axiomatization |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
186 |
disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset
|
187 |
disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B" and |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset
|
188 |
disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B" and |
29734 | 189 |
disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
190 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
191 |
axiomatization |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
192 |
conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
193 |
conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset
|
194 |
conjD\<^sub>1: "A \<and> B \<Longrightarrow> A" and |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset
|
195 |
conjD\<^sub>2: "A \<and> B \<Longrightarrow> B" |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
196 |
|
58618 | 197 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
198 |
\noindent The conjunctive destructions have the disadvantage that |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
199 |
decomposing @{prop "A \<and> B"} involves an immediate decision which |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
200 |
component should be projected. The more convenient simultaneous |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
201 |
elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
202 |
follows: |
58618 | 203 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
204 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
205 |
theorem conjE [elim]: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
206 |
assumes "A \<and> B" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
207 |
obtains A and B |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
208 |
proof |
58618 | 209 |
from \<open>A \<and> B\<close> show A by (rule conjD\<^sub>1) |
210 |
from \<open>A \<and> B\<close> show B by (rule conjD\<^sub>2) |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
211 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
212 |
|
58618 | 213 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
214 |
\noindent Here is an example of swapping conjuncts with a single |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
215 |
intermediate elimination step: |
58618 | 216 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
217 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
218 |
(*<*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
219 |
lemma "\<And>A. PROP A \<Longrightarrow> PROP A" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
220 |
proof - |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
221 |
(*>*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
222 |
assume "A \<and> B" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
223 |
then obtain B and A .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
224 |
then have "B \<and> A" .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
225 |
(*<*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
226 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
227 |
(*>*) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
228 |
|
58618 | 229 |
text \<open> |
29732 | 230 |
\noindent Note that the analogous elimination rule for disjunction |
231 |
``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with |
|
232 |
the original axiomatization of @{thm disjE}. |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
233 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
234 |
\medskip We continue propositional logic by introducing absurdity |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
235 |
with its characteristic elimination. Plain truth may then be |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
236 |
defined as a proposition that is trivially true. |
58618 | 237 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
238 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
239 |
axiomatization |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
240 |
false :: o ("\<bottom>") where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
241 |
falseE [elim]: "\<bottom> \<Longrightarrow> A" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
242 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
243 |
definition |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
244 |
true :: o ("\<top>") where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
245 |
"\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
246 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
247 |
theorem trueI [intro]: \<top> |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
248 |
unfolding true_def .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
249 |
|
58618 | 250 |
text \<open> |
29732 | 251 |
\medskip\noindent Now negation represents an implication towards |
252 |
absurdity: |
|
58618 | 253 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
254 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
255 |
definition |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
256 |
not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
257 |
"\<not> A \<equiv> A \<longrightarrow> \<bottom>" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
258 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
259 |
theorem notI [intro]: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
260 |
assumes "A \<Longrightarrow> \<bottom>" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
261 |
shows "\<not> A" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
262 |
unfolding not_def |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
263 |
proof |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
264 |
assume A |
58618 | 265 |
then show \<bottom> by (rule \<open>A \<Longrightarrow> \<bottom>\<close>) |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
266 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
267 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
268 |
theorem notE [elim]: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
269 |
assumes "\<not> A" and A |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
270 |
shows B |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
271 |
proof - |
58618 | 272 |
from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def . |
273 |
from \<open>A \<longrightarrow> \<bottom>\<close> and \<open>A\<close> have \<bottom> .. |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
274 |
then show B .. |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
275 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
276 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
277 |
|
58618 | 278 |
subsection \<open>Classical logic\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
279 |
|
58618 | 280 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
281 |
Subsequently we state the principle of classical contradiction as a |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
282 |
local assumption. Thus we refrain from forcing the object-logic |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
283 |
into the classical perspective. Within that context, we may derive |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
284 |
well-known consequences of the classical principle. |
58618 | 285 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
286 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
287 |
locale classical = |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
288 |
assumes classical: "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
289 |
begin |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
290 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
291 |
theorem double_negation: |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
292 |
assumes "\<not> \<not> C" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
293 |
shows C |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
294 |
proof (rule classical) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
295 |
assume "\<not> C" |
58618 | 296 |
with \<open>\<not> \<not> C\<close> show C .. |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
297 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
298 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
299 |
theorem tertium_non_datur: "C \<or> \<not> C" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
300 |
proof (rule double_negation) |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
301 |
show "\<not> \<not> (C \<or> \<not> C)" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
302 |
proof |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
303 |
assume "\<not> (C \<or> \<not> C)" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
304 |
have "\<not> C" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
305 |
proof |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
306 |
assume C then have "C \<or> \<not> C" .. |
58618 | 307 |
with \<open>\<not> (C \<or> \<not> C)\<close> show \<bottom> .. |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
308 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
309 |
then have "C \<or> \<not> C" .. |
58618 | 310 |
with \<open>\<not> (C \<or> \<not> C)\<close> show \<bottom> .. |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
311 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
312 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
313 |
|
58618 | 314 |
text \<open> |
29735 | 315 |
\noindent These examples illustrate both classical reasoning and |
316 |
non-trivial propositional proofs in general. All three rules |
|
317 |
characterize classical logic independently, but the original rule is |
|
318 |
already the most convenient to use, because it leaves the conclusion |
|
319 |
unchanged. Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our |
|
320 |
format for eliminations, despite the additional twist that the |
|
321 |
context refers to the main conclusion. So we may write @{thm |
|
322 |
classical} as the Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''. |
|
323 |
This also explains nicely how classical reasoning really works: |
|
324 |
whatever the main @{text thesis} might be, we may always assume its |
|
325 |
negation! |
|
58618 | 326 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
327 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
328 |
end |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
329 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
330 |
|
58618 | 331 |
subsection \<open>Quantifiers \label{sec:framework-ex-quant}\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
332 |
|
58618 | 333 |
text \<open> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
334 |
Representing quantifiers is easy, thanks to the higher-order nature |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
335 |
of the underlying framework. According to the well-known technique |
58552 | 336 |
introduced by Church @{cite "church40"}, quantifiers are operators on |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
337 |
predicates, which are syntactically represented as @{text "\<lambda>"}-terms |
29732 | 338 |
of type @{typ "i \<Rightarrow> o"}. Binder notation turns @{text "All (\<lambda>x. B |
339 |
x)"} into @{text "\<forall>x. B x"} etc. |
|
58618 | 340 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
341 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
342 |
axiomatization |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
343 |
All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
344 |
allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x" and |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
345 |
allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
346 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
347 |
axiomatization |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
348 |
Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
349 |
exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)" and |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
350 |
exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
351 |
|
58618 | 352 |
text \<open> |
29735 | 353 |
\noindent The statement of @{thm exE} corresponds to ``@{text |
354 |
"\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}'' in Isar. In the |
|
355 |
subsequent example we illustrate quantifier reasoning involving all |
|
356 |
four rules: |
|
58618 | 357 |
\<close> |
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
358 |
|
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
359 |
theorem |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
360 |
assumes "\<exists>x. \<forall>y. R x y" |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
361 |
shows "\<forall>y. \<exists>x. R x y" |
58618 | 362 |
proof -- \<open>@{text "\<forall>"} introduction\<close> |
363 |
obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> .. -- \<open>@{text "\<exists>"} elimination\<close> |
|
364 |
fix y have "R x y" using \<open>\<forall>y. R x y\<close> .. -- \<open>@{text "\<forall>"} destruction\<close> |
|
365 |
then show "\<exists>x. R x y" .. -- \<open>@{text "\<exists>"} introduction\<close> |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
366 |
qed |
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
367 |
|
29734 | 368 |
|
58618 | 369 |
subsection \<open>Canonical reasoning patterns\<close> |
29734 | 370 |
|
58618 | 371 |
text \<open> |
29734 | 372 |
The main rules of first-order predicate logic from |
373 |
\secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant} |
|
374 |
can now be summarized as follows, using the native Isar statement |
|
375 |
format of \secref{sec:framework-stmt}. |
|
376 |
||
377 |
\medskip |
|
378 |
\begin{tabular}{l} |
|
379 |
@{text "impI: \<ASSUMES> A \<Longrightarrow> B \<SHOWS> A \<longrightarrow> B"} \\ |
|
380 |
@{text "impD: \<ASSUMES> A \<longrightarrow> B \<AND> A \<SHOWS> B"} \\[1ex] |
|
381 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset
|
382 |
@{text "disjI\<^sub>1: \<ASSUMES> A \<SHOWS> A \<or> B"} \\ |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset
|
383 |
@{text "disjI\<^sub>2: \<ASSUMES> B \<SHOWS> A \<or> B"} \\ |
29734 | 384 |
@{text "disjE: \<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"} \\[1ex] |
385 |
||
386 |
@{text "conjI: \<ASSUMES> A \<AND> B \<SHOWS> A \<and> B"} \\ |
|
387 |
@{text "conjE: \<ASSUMES> A \<and> B \<OBTAINS> A \<AND> B"} \\[1ex] |
|
388 |
||
389 |
@{text "falseE: \<ASSUMES> \<bottom> \<SHOWS> A"} \\ |
|
390 |
@{text "trueI: \<SHOWS> \<top>"} \\[1ex] |
|
391 |
||
392 |
@{text "notI: \<ASSUMES> A \<Longrightarrow> \<bottom> \<SHOWS> \<not> A"} \\ |
|
393 |
@{text "notE: \<ASSUMES> \<not> A \<AND> A \<SHOWS> B"} \\[1ex] |
|
394 |
||
395 |
@{text "allI: \<ASSUMES> \<And>x. B x \<SHOWS> \<forall>x. B x"} \\ |
|
396 |
@{text "allE: \<ASSUMES> \<forall>x. B x \<SHOWS> B a"} \\[1ex] |
|
397 |
||
398 |
@{text "exI: \<ASSUMES> B a \<SHOWS> \<exists>x. B x"} \\ |
|
399 |
@{text "exE: \<ASSUMES> \<exists>x. B x \<OBTAINS> a \<WHERE> B a"} |
|
400 |
\end{tabular} |
|
401 |
\medskip |
|
402 |
||
403 |
\noindent This essentially provides a declarative reading of Pure |
|
404 |
rules as Isar reasoning patterns: the rule statements tells how a |
|
405 |
canonical proof outline shall look like. Since the above rules have |
|
29735 | 406 |
already been declared as @{attribute (Pure) intro}, @{attribute |
407 |
(Pure) elim}, @{attribute (Pure) dest} --- each according to its |
|
408 |
particular shape --- we can immediately write Isar proof texts as |
|
409 |
follows: |
|
58618 | 410 |
\<close> |
29734 | 411 |
|
412 |
(*<*) |
|
413 |
theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
|
414 |
proof - |
|
415 |
(*>*) |
|
416 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
417 |
text_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 418 |
|
419 |
have "A \<longrightarrow> B" |
|
420 |
proof |
|
421 |
assume A |
|
422 |
show B sorry %noproof |
|
423 |
qed |
|
424 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
425 |
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 426 |
|
427 |
have "A \<longrightarrow> B" and A sorry %noproof |
|
428 |
then have B .. |
|
429 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
430 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 431 |
|
432 |
have A sorry %noproof |
|
433 |
then have "A \<or> B" .. |
|
434 |
||
435 |
have B sorry %noproof |
|
436 |
then have "A \<or> B" .. |
|
437 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
438 |
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 439 |
|
440 |
have "A \<or> B" sorry %noproof |
|
441 |
then have C |
|
442 |
proof |
|
443 |
assume A |
|
444 |
then show C sorry %noproof |
|
445 |
next |
|
446 |
assume B |
|
447 |
then show C sorry %noproof |
|
448 |
qed |
|
449 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
450 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 451 |
|
452 |
have A and B sorry %noproof |
|
453 |
then have "A \<and> B" .. |
|
454 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
455 |
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 456 |
|
457 |
have "A \<and> B" sorry %noproof |
|
458 |
then obtain A and B .. |
|
459 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
460 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 461 |
|
462 |
have "\<bottom>" sorry %noproof |
|
463 |
then have A .. |
|
464 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
465 |
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 466 |
|
467 |
have "\<top>" .. |
|
468 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
469 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 470 |
|
471 |
have "\<not> A" |
|
472 |
proof |
|
473 |
assume A |
|
474 |
then show "\<bottom>" sorry %noproof |
|
475 |
qed |
|
476 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
477 |
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 478 |
|
479 |
have "\<not> A" and A sorry %noproof |
|
480 |
then have B .. |
|
481 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
482 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 483 |
|
484 |
have "\<forall>x. B x" |
|
485 |
proof |
|
486 |
fix x |
|
487 |
show "B x" sorry %noproof |
|
488 |
qed |
|
489 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
490 |
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 491 |
|
492 |
have "\<forall>x. B x" sorry %noproof |
|
493 |
then have "B a" .. |
|
494 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
495 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 496 |
|
497 |
have "\<exists>x. B x" |
|
498 |
proof |
|
499 |
show "B a" sorry %noproof |
|
500 |
qed |
|
501 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
502 |
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
29734 | 503 |
|
504 |
have "\<exists>x. B x" sorry %noproof |
|
505 |
then obtain a where "B a" .. |
|
506 |
||
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset
|
507 |
text_raw \<open>\end{minipage}\<close> |
29734 | 508 |
|
509 |
(*<*) |
|
510 |
qed |
|
511 |
(*>*) |
|
512 |
||
58618 | 513 |
text \<open> |
29734 | 514 |
\bigskip\noindent Of course, these proofs are merely examples. As |
515 |
sketched in \secref{sec:framework-subproof}, there is a fair amount |
|
516 |
of flexibility in expressing Pure deductions in Isar. Here the user |
|
517 |
is asked to express himself adequately, aiming at proof texts of |
|
518 |
literary quality. |
|
58618 | 519 |
\<close> |
29734 | 520 |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
diff
changeset
|
521 |
end %visible |