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