section \Example theory file for getting acquainted with Isabelle\
(*<*)
theory Example
imports Main
begin
(*>*)
subsection \Terms\
text \
We can write logical formulae and terms in the usual notation.
Connectives such as @{text "\"},@{text "\"}, @{text "\"} etc. can be typed using the backslash
@{text "\\"} followed by the name of the sign. I.e. @{text "\\not"} for @{text "\"}.
Note that during typing @{text "\\not"} at some point there will be a pop-up menu
offering you certain auto completion suggestions that you can accept by
pressing the tab key.
\
subsection \Types\
text \
All terms (and also constant symbols, variables etc.) are associated
a type. The type @{type "bool"} is the type of all Boolean-values objects
(e.g. truth values).
New types can be inserted at will.
\
typedecl "i" -- "Create a new type i for the type of individuals"
subsection \Constants\
text \
New constants can be defined using the @{text "consts"} keyword.
You need to specify the type of the constant explicitly.
\
subsection \Terms and Formulas\
text \
In higher-order logic (HOL), terms are all well-formed expressions
that can be expressed within the logic. A term has a unique type, such
as in @{term "f(A) :: i"} where the term @{term "f(A)"} has type
@{type "i"}. Terms of type @{type "bool"} are called "formulas".
\
subsubsection \Example formula 1\
text \If it's raining the street will get wet\
consts raining :: "bool" -- "constant symbol for raining"
consts wet :: "i \ bool" -- "predicate symbol for wet"
consts street :: "i" -- "constant symbol for the street"
prop "raining \ wet(street)" -- "raining implies street-is-wet"
subsubsection \Example formula 2\
consts good :: "i \ bool" -- "predicate symbol for being good"
prop "good(A)" -- "A is good"
text \A is a free variable of the above term, hence it is not closed\
subsubsection \Example formula 3\
prop "\A. good(A)" -- "everything is good"
text \A is a a bound variable of the above term, which is universally qualified.\
subsection \Proofs\
text \We will learn how to formalize proofs in Isabelle throughout this course.\
subsubsection \Proofs with handy keywords\
theorem MyFirstTheorem:
assumes "A"
shows "B \ A"
proof -
{
assume "B"
from assms have "A" by - -- "Iterate the fact that A holds by assumptions using the - sign"
}
then have "B \ A" by (rule impI)
thus ?thesis .
qed
subsubsection \Proofs with labels\
theorem MyFirstTheorem2:
assumes 1: "A"
shows "B \ A"
proof -
{
assume "B"
from 1 have "A" by -
} note 2 = this
from 2 have "B \ A" by (rule impI)
thus ?thesis .
qed
subsubsection \Using the proofs\
text \
We can now derive simple facts of the above theorem.
\
corollary ThatFollowsDirectly:
assumes "A"
shows "P(A) \ A"
using assms by (rule MyFirstTheorem[where B = "P(A)"])
(*<*)
end
(*>*)