Quellcode-Bibliothek 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%

¤ 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.0.16Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders