Quelle Executable_Relation.thy Sprache: Isabelle

theory Executable_Relation
imports Main
begin

subsection \<open>A dedicated type for relations\<close>

subsubsection \<open>Definition of the dedicated type for relations\<close>

typedef 'a rel = "UNIV :: (('a * 'a) set) set"
morphisms set_of_rel rel_of_set by simp

setup_lifting type_definition_rel

lift_definition Rel :: "'a set => ('a * 'a) set => 'a rel" is "\ X R. Id_on X Un R" .

subsubsection \<open>Constant definitions on relations\<close>

hide_const (open) converse relcomp rtrancl Image

lift_definition member :: "'a * 'a => 'a rel => bool" is "Set.member" .

lift_definition converse :: "'a rel => 'a rel" is "Relation.converse" .

lift_definition union :: "'a rel => 'a rel => 'a rel" is "Set.union" .

lift_definition relcomp :: "'a rel => 'a rel => 'a rel" is "Relation.relcomp" .

lift_definition rtrancl :: "'a rel => 'a rel" is "Transitive_Closure.rtrancl" .

lift_definition Image :: "'a rel => 'a set => 'a set" is "Relation.Image" .

subsubsection \<open>Code generation\<close>

code_datatype Rel

lemma [code]:
  "member (x, y) (Rel X R) = ((x = y \ x \ X) \ (x, y) \ R)"
by transfer auto

lemma [code]:
  "converse (Rel X R) = Rel X (R\)"
by transfer auto

lemma [code]:
  "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)"
by transfer auto

lemma [code]:
   "relcomp (Rel X R) (Rel Y S) = Rel (X \ Y) (Set.filter (\(x, y). y \ Y) R \ (Set.filter (\(x, y). x \ X) S \ R O S))"
by transfer (auto simp add: Id_on_eqI relcomp.simps)

lemma [code]:
  "rtrancl (Rel X R) = Rel UNIV (R\<^sup>+)"
apply transfer
apply auto
apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
by (metis in_rtrancl_UnI trancl_into_rtrancl)

lemma [code]:
  "Image (Rel X R) S = (X Int S) Un (R `` S)"
by transfer auto

quickcheck_generator rel constructors: Rel

lemma
  "member (x, (y :: nat)) (rtrancl (union R S)) \ member (x, y) (union (rtrancl R) (rtrancl S))"
quickcheck[exhaustive, expect = counterexample]
oops

end

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.