src/HOL/ex/Executable_Relation.thy

renewing Executable_Relation

theory Executable_Relation
imports Main
begin

subsection {* Preliminaries on the raw type of relations *}

definition rel_raw :: "'a set => ('a * 'a) set => ('a * 'a) set"
where
  "rel_raw X R = Id_on X Un R"

lemma member_raw:
  "(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
unfolding rel_raw_def by auto

lemma Id_raw:
  "Id = rel_raw UNIV {}"
unfolding rel_raw_def by auto

lemma converse_raw:
  "converse (rel_raw X R) = rel_raw X (converse R)"
unfolding rel_raw_def by auto

lemma union_raw:
  "(rel_raw X R) Un (rel_raw Y S) = rel_raw (X Un Y) (R Un S)"
unfolding rel_raw_def by auto

lemma comp_Id_on:
  "Id_on X O R = Set.project (%(x, y). x : X) R"
by (auto intro!: rel_compI)

lemma comp_Id_on':
  "R O Id_on X = Set.project (%(x, y). y : X) R"
by auto

lemma project_Id_on:
  "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
by auto

lemma rel_comp_raw:
  "(rel_raw X R) O (rel_raw Y S) = rel_raw (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
unfolding rel_raw_def
apply simp
apply (simp add: comp_Id_on)
apply (simp add: project_Id_on)
apply (simp add: comp_Id_on')
apply auto
done

lemma rtrancl_raw:
  "(rel_raw X R)^* = rel_raw UNIV (R^+)"
unfolding rel_raw_def
apply auto
apply (metis Id_on_iff Un_commute iso_tuple_UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
by (metis in_rtrancl_UnI trancl_into_rtrancl)

lemma Image_raw:
  "(rel_raw X R) `` S = (X Int S) Un (R `` S)"
unfolding rel_raw_def by auto

subsection {* A dedicated type for relations *}

subsubsection {* Definition of the dedicated type for relations *}

quotient_type 'a rel = "('a * 'a) set" / "(op =)"
morphisms set_of_rel rel_of_set by (metis identity_equivp)

lemma [simp]:
  "rel_of_set (set_of_rel S) = S"
by (rule Quotient_abs_rep[OF Quotient_rel])

lemma [simp]:
  "set_of_rel (rel_of_set R) = R"
by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)

lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]

definition rel :: "'a set => ('a * 'a) set => 'a rel"
where
  "rel X R = rel_of_set (rel_raw X R)"

subsubsection {* Constant definitions on relations *}

hide_const (open) converse rel_comp rtrancl Image

quotient_definition member :: "'a * 'a => 'a rel => bool" where
  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"

quotient_definition converse :: "'a rel => 'a rel"
where
  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set"

quotient_definition union :: "'a rel => 'a rel => 'a rel"
where
  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"

quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
where
  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"

quotient_definition rtrancl :: "'a rel => 'a rel"
where
  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set"

quotient_definition Image :: "'a rel => 'a set => 'a set"
where
  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set"

subsubsection {* Code generation *}

code_datatype rel

lemma [code]:
  "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
unfolding rel_def member_def
by (simp add: member_raw)

lemma [code]:
  "converse (rel X R) = rel X (R^-1)"
unfolding rel_def converse_def
by (simp add: converse_raw)

lemma [code]:
  "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
unfolding rel_def union_def
by (simp add: union_raw)

lemma [code]:
   "rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
unfolding rel_def rel_comp_def
by (simp add: rel_comp_raw)

lemma [code]:
  "rtrancl (rel X R) = rel UNIV (R^+)"
unfolding rel_def rtrancl_def
by (simp add: rtrancl_raw)

lemma [code]:
  "Image (rel X R) S = (X Int S) Un (R `` S)"
unfolding rel_def Image_def
by (simp add: Image_raw)

quickcheck_generator rel constructors: rel

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

end