section "Playing with HOL"
theory Tutorial5
imports Main
begin
(*<*)
text "Ignore this"
no_notation
subset ("op \") and
subset ("(_/ \ _)" [51, 51] 50) and
subset_eq ("op \") and
subset_eq ("(_/ \ _)" [51, 51] 50)
no_notation
union (infixl "\" 65) and
inter (infixl "\" 70)
no_notation
Set.member ("op \") and
Set.member ("(_/ \ _)" [51, 51] 50)
text "Ignore this END"
(*>*)
subsection "Sets"
text \In the context of HOL, a set @{term "A"} can be defined using
its characteristic function @{term "\\<^sub>A"}:
For a set @{term "A"} of objects of type @{text "'a"},
an object @{term "x :: 'a"} is an element of @{term "A"}
if and only if @{term "\\<^sub>A x"} holds
(i.e. @{term "\\<^sub>A"} represents
the extension of the set @{term "A"} when interpreted as a predicate).
Speaking in HOL terms, the
char. function @{term "\\<^sub>A"} is a term of type @{text "'a \ bool"}.\
type_synonym 'a Set = "'a \ bool"
paragraph "Constructing sets"
term "\x. P x" -- "set of objects for which P holds"
paragraph "Membership"
text \Membership of a set can easily defined as application to the characteristic
function.\
definition member :: "'a \ 'a Set \ bool" (infix "\" 42) where
"x \ A \ A x"
paragraph "Other operators on sets"
text "Define intersection by"
abbreviation intersect :: "'a Set \ 'a Set \ 'a Set" (infix "\" 41) where
"A \ B \ \"
text "Define union by"
abbreviation union :: "'a Set \ 'a Set \ 'a Set" (infix "\" 41) where
"A \ B \ \e"
text "Define difference by"
abbreviation diff :: "'a Set \ 'a Set \ 'a Set" (infix "\" 41) where
"A \ B \ \"
text "Define subset by"
abbreviation subset :: "'a Set \ 'a Set \ bool" (infix "\" 41) where
"A \ B \ \"
text "Define intersection by"
abbreviation setequiv :: "'a Set \ 'a Set \ bool" (infix "\" 41) where
"A \ B \ \"
subsection "Relations"
text \As for sets, we can define relations in HOL.
A relation @{term "R"} can be modeled by a term @{term "R"}
of type @{text "'a \ 'a \ bool"}.
Then, for two objects @{term "x :: 'a"}, @{term "y :: 'a"}
@{term "x"} is in relation to @{term "y"}, infix-ly written @{term "xRy"},
if and only if @{term "R x y"} holds.\
text \
\<^enum> Formulate a predicate that is true iff a given relation
@{term "R :: 'a \ 'a \ bool"} is reflexive.
\<^enum> Formulate a predicate that is true iff a given relation
@{term "R :: 'a \ 'a \ bool"} is transitive.
\<^enum> Formulate a predicate that is true iff a given relation
@{term "R :: 'a \ 'a \ bool"} is symmetric.
\<^enum> Formulate a predicate that is true iff a given relation
@{term "R :: 'a \ 'a \ bool"} is an equivalence relation.
\<^enum> Formulate a predicate that is true iff a given relation.
@{term "R :: 'a \ 'a \ bool"} is a total order.
\
text \
Bonus-task (harder):
\<^enum> Formulate a function that returns the reflexive closure
of a relation @{term "R :: 'a \ 'a \ bool"}.
\<^enum> Formulate a function that returns the transitive closure
of a relation @{term "R :: 'a \ 'a \ bool"}.
\
text "You can verify your definitions using by proving:"
lemma "\R. trans (transclosure R)" oops
lemma "\R. \x. \y. R x y \ (transclosure R) x y" oops
end