# Theory Relators

section ‹Relators›
theory Relators
imports "../Lib/Refine_Lib"
begin

text ‹
We define the concept of relators. The relation between a concrete type and
an abstract type is expressed by a relation of type ‹('c×'a) set›.
For each composed type, say ‹'a list›, we can define a {\em relator},
that takes as argument a relation for the element type, and returns a relation
for the list type. For most datatypes, there exists a {\em natural relator}.
For algebraic datatypes, this is the relator that preserves the structure
of the datatype, and changes the components. For example,
‹list_rel::('c×'a) set ⇒ ('c list×'a list) set› is the natural
relator for lists.

However, relators can also be used to change the representation, and thus
relate an implementation with an abstract type. For example, the relator
‹list_set_rel::('c×'a) set ⇒ ('c list×'a set) set› relates lists
with the set of their elements.

In this theory, we define some basic notions for relators, and
then define natural relators for all HOL-types, including the function type.
For each relator, we also show a single-valuedness property, and initialize a
solver for single-valued properties.
›

subsection ‹Basic Definitions›

text ‹
For smoother handling of relator unification, we require relator arguments to
be applied by a special operator, such that we avoid higher-order
unification problems. We try to set up some syntax to make this more
transparent, and give relators a type-like prefix-syntax.
›

definition relAPP
:: "(('c1×'a1) set ⇒ _) ⇒ ('c1×'a1) set ⇒ _"
where "relAPP f x ≡ f x"

syntax "_rel_APP" :: "args ⇒ 'a ⇒ 'b" ("⟨_⟩_" [0,900] 900)

translations
"⟨x,xs⟩R" == "⟨xs⟩(CONST relAPP R x)"
"⟨x⟩R" == "CONST relAPP R x"

ML ‹
structure Refine_Relators_Thms = struct
structure rel_comb_def_rules = Named_Thms (
val name = @{binding refine_rel_defs}
val description = "Refinement Framework: " ^
"Relator definitions"
);
end
›

setup Refine_Relators_Thms.rel_comb_def_rules.setup

subsection ‹Basic HOL Relators›
subsubsection ‹Function›
definition fun_rel where
fun_rel_def_internal: "fun_rel A B ≡ { (f,f'). ∀(a,a')∈A. (f a, f' a')∈B }"
abbreviation fun_rel_syn (infixr "→" 60) where "A→B ≡ ⟨A,B⟩fun_rel"

lemma fun_rel_def[refine_rel_defs]:
"A→B ≡ { (f,f'). ∀(a,a')∈A. (f a, f' a')∈B }"

lemma fun_relI[intro!]: "⟦⋀a a'. (a,a')∈A ⟹ (f a,f' a')∈B⟧ ⟹ (f,f')∈A→B"
by (auto simp: fun_rel_def)

lemma fun_relD:
shows " ((f,f')∈(A→B)) ⟹
(⋀x x'. ⟦ (x,x')∈A ⟧ ⟹ (f x, f' x')∈B)"
apply rule
by (auto simp: fun_rel_def)

lemma fun_relD1:
assumes "(f,f')∈Ra→Rr"
assumes "f x = r"
shows "∀x'. (x,x')∈Ra ⟶ (r,f' x')∈Rr"
using assms by (auto simp: fun_rel_def)

lemma fun_relD2:
assumes "(f,f')∈Ra→Rr"
assumes "f' x' = r'"
shows "∀x. (x,x')∈Ra ⟶ (f x,r')∈Rr"
using assms by (auto simp: fun_rel_def)

lemma fun_relE1:
assumes "(f,f')∈Id → Rv"
assumes "t' = f' x"
shows "(f x,t')∈Rv" using assms
by (auto elim: fun_relD)

lemma fun_relE2:
assumes "(f,f')∈Id → Rv"
assumes "t = f x"
shows "(t,f' x)∈Rv" using assms
by (auto elim: fun_relD)

subsubsection ‹Terminal Types›
abbreviation unit_rel :: "(unit×unit) set" where "unit_rel == Id"

abbreviation "nat_rel ≡ Id::(nat×_) set"
abbreviation "int_rel ≡ Id::(int×_) set"
abbreviation "bool_rel ≡ Id::(bool×_) set"

subsubsection ‹Product›
definition prod_rel where
prod_rel_def_internal: "prod_rel R1 R2
≡ { ((a,b),(a',b')) . (a,a')∈R1 ∧ (b,b')∈R2 }"

abbreviation prod_rel_syn (infixr "×⇩r" 70) where "a×⇩rb ≡ ⟨a,b⟩prod_rel"

lemma prod_rel_def[refine_rel_defs]:
"(⟨R1,R2⟩prod_rel) ≡ { ((a,b),(a',b')) . (a,a')∈R1 ∧ (b,b')∈R2 }"

lemma prod_relI: "⟦(a,a')∈R1; (b,b')∈R2⟧ ⟹ ((a,b),(a',b'))∈⟨R1,R2⟩prod_rel"
by (auto simp: prod_rel_def)
lemma prod_relE:
assumes "(p,p')∈⟨R1,R2⟩prod_rel"
obtains a b a' b' where "p=(a,b)" and "p'=(a',b')"
and "(a,a')∈R1" and "(b,b')∈R2"
using assms
by (auto simp: prod_rel_def)

lemma prod_rel_simp[simp]:
"((a,b),(a',b'))∈⟨R1,R2⟩prod_rel ⟷ (a,a')∈R1 ∧ (b,b')∈R2"
by (auto intro: prod_relI elim: prod_relE)

lemma in_Domain_prod_rel_iff[iff]: "(a,b)∈Domain (A×⇩rB) ⟷ a∈Domain A ∧ b∈Domain B"
by (auto simp: prod_rel_def)

lemma prod_rel_comp: "(A ×⇩r B) O (C ×⇩r D) = (A O C) ×⇩r (B O D)"
unfolding prod_rel_def
by auto

subsubsection ‹Option›
definition option_rel where
option_rel_def_internal:
"option_rel R ≡ { (Some a,Some a') | a a'. (a,a')∈R } ∪ {(None,None)}"

lemma option_rel_def[refine_rel_defs]:
"⟨R⟩option_rel ≡ { (Some a,Some a') | a a'. (a,a')∈R } ∪ {(None,None)}"

lemma option_relI:
"(None,None)∈⟨R⟩ option_rel"
"⟦ (a,a')∈R ⟧ ⟹ (Some a, Some a')∈⟨R⟩option_rel"
by (auto simp: option_rel_def)

lemma option_relE:
assumes "(x,x')∈⟨R⟩option_rel"
obtains "x=None" and "x'=None"
| a a' where "x=Some a" and "x'=Some a'" and "(a,a')∈R"
using assms by (auto simp: option_rel_def)

lemma option_rel_simp[simp]:
"(None,a)∈⟨R⟩option_rel ⟷ a=None"
"(c,None)∈⟨R⟩option_rel ⟷ c=None"
"(Some x,Some y)∈⟨R⟩option_rel ⟷ (x,y)∈R"
by (auto intro: option_relI elim: option_relE)

subsubsection ‹Sum›
definition sum_rel where sum_rel_def_internal:
"sum_rel Rl Rr
≡ { (Inl a, Inl a') | a a'. (a,a')∈Rl } ∪
{ (Inr a, Inr a') | a a'. (a,a')∈Rr }"

lemma sum_rel_def[refine_rel_defs]:
"⟨Rl,Rr⟩sum_rel ≡
{ (Inl a, Inl a') | a a'. (a,a')∈Rl } ∪
{ (Inr a, Inr a') | a a'. (a,a')∈Rr }"

lemma sum_rel_simp[simp]:
"⋀a a'. (Inl a, Inl a') ∈ ⟨Rl,Rr⟩sum_rel ⟷ (a,a')∈Rl"
"⋀a a'. (Inr a, Inr a') ∈ ⟨Rl,Rr⟩sum_rel ⟷ (a,a')∈Rr"
"⋀a a'. (Inl a, Inr a') ∉ ⟨Rl,Rr⟩sum_rel"
"⋀a a'. (Inr a, Inl a') ∉ ⟨Rl,Rr⟩sum_rel"
unfolding sum_rel_def by auto

lemma sum_relI:
"(l,l')∈Rl ⟹ (Inl l, Inl l') ∈ ⟨Rl,Rr⟩sum_rel"
"(r,r')∈Rr ⟹ (Inr r, Inr r') ∈ ⟨Rl,Rr⟩sum_rel"
by simp_all

lemma sum_relE:
assumes "(x,x')∈⟨Rl,Rr⟩sum_rel"
obtains
l l' where "x=Inl l" and "x'=Inl l'" and "(l,l')∈Rl"
| r r' where "x=Inr r" and "x'=Inr r'" and "(r,r')∈Rr"
using assms by (auto simp: sum_rel_def)

subsubsection ‹Lists›
definition list_rel where list_rel_def_internal:
"list_rel R ≡ {(l,l'). list_all2 (λx x'. (x,x')∈R) l l'}"

lemma list_rel_def[refine_rel_defs]:
"⟨R⟩list_rel ≡ {(l,l'). list_all2 (λx x'. (x,x')∈R) l l'}"

lemma list_rel_induct[induct set,consumes 1, case_names Nil Cons]:
assumes "(l,l')∈⟨R⟩ list_rel"
assumes "P [] []"
assumes "⋀x x' l l'. ⟦ (x,x')∈R; (l,l')∈⟨R⟩list_rel; P l l' ⟧
⟹ P (x#l) (x'#l')"
shows "P l l'"
using assms unfolding list_rel_def
apply simp
by (rule list_all2_induct)

lemma list_rel_eq_listrel: "list_rel = listrel"
apply (rule ext)
apply safe
proof goal_cases
case (1 x a b) thus ?case
unfolding list_rel_def_internal
apply simp
apply (induct a b rule: list_all2_induct)
apply (auto intro: listrel.intros)
done
next
case 2 thus ?case
apply (induct)
apply (auto simp: list_rel_def_internal)
done
qed

lemma list_relI:
"([],[])∈⟨R⟩list_rel"
"⟦ (x,x')∈R; (l,l')∈⟨R⟩list_rel ⟧ ⟹ (x#l,x'#l')∈⟨R⟩list_rel"
by (auto simp: list_rel_def)

lemma list_rel_simp[simp]:
"([],l')∈⟨R⟩list_rel ⟷ l'=[]"
"(l,[])∈⟨R⟩list_rel ⟷ l=[]"
"([],[])∈⟨R⟩list_rel"
"(x#l,x'#l')∈⟨R⟩list_rel ⟷ (x,x')∈R ∧ (l,l')∈⟨R⟩list_rel"
by (auto simp: list_rel_def)

lemma list_relE1:
assumes "(l,[])∈⟨R⟩list_rel" obtains "l=[]" using assms by auto

lemma list_relE2:
assumes "([],l)∈⟨R⟩list_rel" obtains "l=[]" using assms by auto

lemma list_relE3:
assumes "(x#xs,l')∈⟨R⟩list_rel" obtains x' xs' where
"l'=x'#xs'" and "(x,x')∈R" and "(xs,xs')∈⟨R⟩list_rel"
using assms
apply (cases l')
apply auto
done

lemma list_relE4:
assumes "(l,x'#xs')∈⟨R⟩list_rel" obtains x xs where
"l=x#xs" and "(x,x')∈R" and "(xs,xs')∈⟨R⟩list_rel"
using assms
apply (cases l)
apply auto
done

lemmas list_relE = list_relE1 list_relE2 list_relE3 list_relE4

lemma list_rel_imp_same_length:
"(l, l') ∈ ⟨R⟩list_rel ⟹ length l = length l'"
unfolding list_rel_eq_listrel relAPP_def
by (rule listrel_eq_len)

lemma list_rel_split_right_iff:
"(x#xs,l)∈⟨R⟩list_rel ⟷ (∃y ys. l=y#ys ∧ (x,y)∈R ∧ (xs,ys)∈⟨R⟩list_rel)"
by (cases l) auto
lemma list_rel_split_left_iff:
"(l,y#ys)∈⟨R⟩list_rel ⟷ (∃x xs. l=x#xs ∧ (x,y)∈R ∧ (xs,ys)∈⟨R⟩list_rel)"
by (cases l) auto

subsubsection ‹Sets›
text ‹Pointwise refinement: The abstract set is the image of
the concrete set, and the concrete set only contains elements that
have an abstract counterpart›

definition set_rel where
set_rel_def_internal:
"set_rel R ≡ {(A,B). (∀x∈A. ∃y∈B. (x,y)∈R) ∧ (∀y∈B. ∃x∈A. (x,y)∈R)}"

term set_rel

lemma set_rel_def[refine_rel_defs]:
"⟨R⟩set_rel ≡ {(A,B). (∀x∈A. ∃y∈B. (x,y)∈R) ∧ (∀y∈B. ∃x∈A. (x,y)∈R)}"

lemma set_rel_alt: "⟨R⟩set_rel = {(A,B). A ⊆ R¯B ∧ B ⊆ RA}"
unfolding set_rel_def by auto

lemma set_relI[intro?]:
assumes "⋀x. x∈A ⟹ ∃y∈B. (x,y)∈R"
assumes "⋀y. y∈B ⟹ ∃x∈A. (x,y)∈R"
shows "(A,B)∈⟨R⟩set_rel"
using assms unfolding set_rel_def by blast

text ‹Original definition of ‹set_rel› in refinement framework.
Abandoned in favour of more symmetric definition above: ›
definition old_set_rel where old_set_rel_def_internal:
"old_set_rel R ≡ {(S,S'). S'=RS ∧ S⊆Domain R}"

lemma old_set_rel_def[refine_rel_defs]:
"⟨R⟩old_set_rel ≡ {(S,S'). S'=RS ∧ S⊆Domain R}"

text ‹Old definition coincides with new definition for single-valued
element relations. This is probably the reason why the old definition worked
for most applications.›
lemma old_set_rel_sv_eq: "single_valued R ⟹ ⟨R⟩old_set_rel = ⟨R⟩set_rel"
unfolding set_rel_def old_set_rel_def single_valued_def
by blast

lemma set_rel_simp[simp]:
"({},{})∈⟨R⟩set_rel"
by (auto simp: set_rel_def)

lemma set_rel_empty_iff[simp]:
"({},y)∈⟨A⟩set_rel ⟷ y={}"
"(x,{})∈⟨A⟩set_rel ⟷ x={}"
by (auto simp: set_rel_def; fastforce)+

lemma set_relD1: "(s,s')∈⟨R⟩set_rel ⟹ x∈s ⟹ ∃x'∈s'. (x,x')∈R"
unfolding set_rel_def by blast

lemma set_relD2: "(s,s')∈⟨R⟩set_rel ⟹ x'∈s' ⟹ ∃x∈s. (x,x')∈R"
unfolding set_rel_def by blast

lemma set_relE1[consumes 2]:
assumes "(s,s')∈⟨R⟩set_rel" "x∈s"
obtains x' where "x'∈s'" "(x,x')∈R"
using set_relD1[OF assms] ..

lemma set_relE2[consumes 2]:
assumes "(s,s')∈⟨R⟩set_rel" "x'∈s'"
obtains x where "x∈s" "(x,x')∈R"
using set_relD2[OF assms] ..

subsection ‹Automation›
subsubsection ‹A solver for relator properties›
lemma relprop_triggers:
"⋀R. single_valued R ⟹ single_valued R"
"⋀R. R=Id ⟹ R=Id"
"⋀R. R=Id ⟹ Id=R"
"⋀R. Range R = UNIV ⟹ Range R = UNIV"
"⋀R. Range R = UNIV ⟹ UNIV = Range R"
"⋀R R'. R⊆R' ⟹ R⊆R'"
by auto

ML ‹
structure relator_props = Named_Thms (
val name = @{binding relator_props}
val description = "Additional relator properties"
)

structure solve_relator_props = Named_Thms (
val name = @{binding solve_relator_props}
val description = "Relator properties that solve goal"
)

›
setup relator_props.setup
setup solve_relator_props.setup

declaration ‹
Tagged_Solver.declare_solver
@{thms relprop_triggers}
@{binding relator_props_solver}
(fn ctxt => (REPEAT_ALL_NEW (CHANGED o (
match_tac ctxt (solve_relator_props.get ctxt) ORELSE'
match_tac ctxt (relator_props.get ctxt)
))))
›

declaration ‹
Tagged_Solver.declare_solver
[]
@{binding force_relator_props_solver}
"Additional relator properties solver (instantiate schematics)"
(fn ctxt => (REPEAT_ALL_NEW (CHANGED o (
resolve_tac ctxt (solve_relator_props.get ctxt) ORELSE'
match_tac ctxt (relator_props.get ctxt)
))))
›

lemma
relprop_id_orient[relator_props]: "R=Id ⟹ Id=R" and
relprop_eq_refl[solve_relator_props]: "t = t"
by auto

lemma
relprop_UNIV_orient[relator_props]: "R=UNIV ⟹ UNIV=R"
by auto

subsubsection ‹ML-Level utilities›

ML ‹
signature RELATORS = sig
val mk_relT: typ * typ -> typ
val dest_relT: typ -> typ * typ

val mk_relAPP: term -> term -> term
val list_relAPP: term list -> term -> term
val strip_relAPP: term -> term list * term
val mk_fun_rel: term -> term -> term

val list_rel: term list -> term -> term

val rel_absT: term -> typ
val rel_concT: term -> typ

val mk_prodrel: term * term -> term
val is_prodrel: term -> bool
val dest_prodrel: term -> term * term

val strip_prodrel_left: term -> term list
val list_prodrel_left: term list -> term

val declare_natural_relator:
(string*string) -> Context.generic -> Context.generic
val remove_natural_relator: string -> Context.generic -> Context.generic
val natural_relator_of: Proof.context -> string -> string option

val mk_natural_relator: Proof.context -> term list -> string -> term option

val setup: theory -> theory
end

structure Relators :RELATORS = struct
val mk_relT = HOLogic.mk_prodT #> HOLogic.mk_setT

fun dest_relT (Type (@{type_name set},[Type (@{type_name prod},[cT,aT])]))
= (cT,aT)
| dest_relT ty = raise TYPE ("dest_relT",[ty],[])

fun mk_relAPP x f = let
val xT = fastype_of x
val fT = fastype_of f
val rT = range_type fT
in
Const (@{const_name relAPP},fT-->xT-->rT)$f$x
end

val list_relAPP = fold mk_relAPP

fun strip_relAPP R = let
fun aux @{mpat "⟨?R⟩?S"} l = aux S (R::l)
| aux R l = (l,R)
in aux R [] end

val rel_absT = fastype_of #> HOLogic.dest_setT #> HOLogic.dest_prodT #> snd
val rel_concT = fastype_of #> HOLogic.dest_setT #> HOLogic.dest_prodT #> fst

fun mk_fun_rel r1 r2 = let
val (r1T,r2T) = (fastype_of r1,fastype_of r2)
val (c1T,a1T) = dest_relT r1T
val (c2T,a2T) = dest_relT r2T
val (cT,aT) = (c1T --> c2T, a1T --> a2T)
val rT = mk_relT (cT,aT)
in
list_relAPP [r1,r2] (Const (@{const_name fun_rel},r1T-->r2T-->rT))
end

val list_rel = fold_rev mk_fun_rel

fun mk_prodrel (A,B) = @{mk_term "?A ×⇩r ?B"}
fun is_prodrel @{mpat "_ ×⇩r _"} = true | is_prodrel _ = false
fun dest_prodrel @{mpat "?A ×⇩r ?B"} = (A,B) | dest_prodrel t = raise TERM("dest_prodrel",[t])

fun strip_prodrel_left @{mpat "?A ×⇩r ?B"} = strip_prodrel_left A @ [B]
| strip_prodrel_left @{mpat (typs) "unit_rel"} = []
| strip_prodrel_left R = [R]

val list_prodrel_left = Refine_Util.list_binop_left @{term unit_rel} mk_prodrel

structure natural_relators = Generic_Data (
type T = string Symtab.table
val empty = Symtab.empty
val merge = Symtab.join (fn _ => fn (_,cn) => cn)
)

fun declare_natural_relator tcp =
natural_relators.map (Symtab.update tcp)

fun remove_natural_relator tname =
natural_relators.map (Symtab.delete_safe tname)

fun natural_relator_of ctxt =
Symtab.lookup (natural_relators.get (Context.Proof ctxt))

(* [R1,…,Rn] T is mapped to ⟨R1,…,Rn⟩ Trel *)
fun mk_natural_relator ctxt args Tname =
case natural_relator_of ctxt Tname of
NONE => NONE
| SOME Cname => SOME let
val argsT = map fastype_of args
val (cTs, aTs) = map dest_relT argsT |> split_list
val aT = Type (Tname,aTs)
val cT = Type (Tname,cTs)
val rT = mk_relT (cT,aT)
in
list_relAPP args (Const (Cname,argsT--->rT))
end

fun
natural_relator_from_term (t as Const (name,T)) = let
fun err msg = raise TERM (msg,[t])

val (argTs,bodyT) = strip_type T
val (conTs,absTs) = argTs |> map (HOLogic.dest_setT #> HOLogic.dest_prodT) |> split_list
val (bconT,babsT) = bodyT |> HOLogic.dest_setT |> HOLogic.dest_prodT
val (Tcon,bconTs) = dest_Type bconT
val (Tcon',babsTs) = dest_Type babsT

val _ = Tcon = Tcon' orelse err "Type constructors do not match"
val _ = conTs = bconTs orelse err "Concrete types do not match"
val _ = absTs = babsTs orelse err "Abstract types do not match"

in
(Tcon,name)
end
| natural_relator_from_term t =
raise TERM ("Expected constant",[t]) (* TODO: Localize this! *)

local
fun decl_natrel_aux t context = let
fun warn msg = let
val tP =
Context.cases Syntax.pretty_term_global Syntax.pretty_term
context t
val m = Pretty.block [
Pretty.str "Ignoring invalid natural_relator declaration:",
Pretty.brk 1,
Pretty.str msg,
Pretty.brk 1,
tP
] |> Pretty.string_of
val _ = warning m
in context end
in
declare_natural_relator (natural_relator_from_term t) context
handle
TERM (msg,_) => warn msg
| exn => if Exn.is_interrupt exn then Exn.reraise exn else warn ""
end
in
val natural_relator_attr = Scan.repeat1 Args.term >> (fn ts =>
Thm.declaration_attribute ( fn _ => fold decl_natrel_aux ts)
)
end

val setup = I
#> Attrib.setup
@{binding natural_relator} natural_relator_attr "Declare natural relator"

end
›

setup Relators.setup

subsection ‹Setup›
subsubsection "Natural Relators"

declare [[natural_relator
unit_rel int_rel nat_rel bool_rel
fun_rel prod_rel option_rel sum_rel list_rel
]]

(*declaration {* let open Relators in
fn _ =>
declare_natural_relator (@{type_name unit},@{const_name unit_rel})
#> declare_natural_relator (@{type_name fun},@{const_name fun_rel})
#> declare_natural_relator (@{type_name prod},@{const_name prod_rel})
#> declare_natural_relator (@{type_name option},@{const_name option_rel})
#> declare_natural_relator (@{type_name sum},@{const_name sum_rel})
#> declare_natural_relator (@{type_name list},@{const_name list_rel})

end
*}*)

ML_val ‹
Relators.mk_natural_relator
@{context}
[@{term "Ra::('c×'a) set"},@{term "⟨Rb⟩option_rel"}]
@{type_name prod}
|> the
|> Thm.cterm_of @{context}
;
Relators.mk_fun_rel @{term "⟨Id⟩option_rel"} @{term "⟨Id⟩list_rel"}
|> Thm.cterm_of @{context}
›

lemmas [relator_props] =
single_valued_Id
subset_refl
refl

(* TODO: Move *)
lemma eq_UNIV_iff: "S=UNIV ⟷ (∀x. x∈S)" by auto

lemma fun_rel_sv[relator_props]:
assumes RAN: "Range Ra = UNIV"
assumes SV: "single_valued Rv"
shows "single_valued (Ra → Rv)"
proof (intro single_valuedI ext impI allI)
fix f g h x'
assume R1: "(f,g)∈Ra→Rv"
and R2: "(f,h)∈Ra→Rv"

from RAN obtain x where AR: "(x,x')∈Ra" by auto
from fun_relD[OF R1 AR] have "(f x,g x') ∈ Rv" .
moreover from fun_relD[OF R2 AR] have "(f x,h x') ∈ Rv" .
ultimately show "g x' = h x'" using SV by (auto dest: single_valuedD)
qed

lemmas [relator_props] = Range_Id

lemma fun_rel_id[relator_props]: "⟦R1=Id; R2=Id⟧ ⟹ R1 → R2 = Id"
by (auto simp: fun_rel_def)

lemma fun_rel_id_simp[simp]: "Id→Id = Id" by tagged_solver

lemma fun_rel_comp_dist[relator_props]:
"(R1→R2) O (R3→R4) ⊆ ((R1 O R3) → (R2 O R4))"
by (auto simp: fun_rel_def)

lemma fun_rel_mono[relator_props]: "⟦ R1⊆R2; R3⊆R4 ⟧ ⟹ R2→R3 ⊆ R1→R4"
by (force simp: fun_rel_def)

lemma prod_rel_sv[relator_props]:
"⟦single_valued R1; single_valued R2⟧ ⟹ single_valued (⟨R1,R2⟩prod_rel)"
by (auto intro: single_valuedI dest: single_valuedD simp: prod_rel_def)

lemma prod_rel_id[relator_props]: "⟦R1=Id; R2=Id⟧ ⟹ ⟨R1,R2⟩prod_rel = Id"
by (auto simp: prod_rel_def)

lemma prod_rel_id_simp[simp]: "⟨Id,Id⟩prod_rel = Id" by tagged_solver

lemma prod_rel_mono[relator_props]:
"⟦ R2⊆R1; R3⊆R4 ⟧ ⟹ ⟨R2,R3⟩prod_rel ⊆ ⟨R1,R4⟩prod_rel"
by (auto simp: prod_rel_def)

lemma prod_rel_range[relator_props]: "⟦Range Ra=UNIV; Range Rb=UNIV⟧
⟹ Range (⟨Ra,Rb⟩prod_rel) = UNIV"
apply (auto simp: prod_rel_def)
by (metis Range_iff UNIV_I)+

lemma option_rel_sv[relator_props]:
"⟦single_valued R⟧ ⟹ single_valued (⟨R⟩option_rel)"
by (auto intro: single_valuedI dest: single_valuedD simp: option_rel_def)

lemma option_rel_id[relator_props]:
"R=Id ⟹ ⟨R⟩option_rel = Id" by (auto simp: option_rel_def)

lemma option_rel_id_simp[simp]: "⟨Id⟩option_rel = Id" by tagged_solver

lemma option_rel_mono[relator_props]: "R⊆R' ⟹ ⟨R⟩option_rel ⊆ ⟨R'⟩option_rel"
by (auto simp: option_rel_def)

lemma option_rel_range: "Range R = UNIV ⟹ Range (⟨R⟩option_rel) = UNIV"
apply (auto simp: option_rel_def Range_iff)
by (metis Range_iff UNIV_I option.exhaust)

lemma option_rel_inter[simp]: "⟨R1 ∩ R2⟩option_rel = ⟨R1⟩option_rel ∩ ⟨R2⟩option_rel"
by (auto simp: option_rel_def)

lemma option_rel_constraint[simp]:
"(x,x)∈⟨UNIV×C⟩option_rel ⟷ (∀v. x=Some v ⟶ v∈C)"
by (auto simp: option_rel_def)

lemma sum_rel_sv[relator_props]:
"⟦single_valued Rl; single_valued Rr⟧ ⟹ single_valued (⟨Rl,Rr⟩sum_rel)"
by (auto intro: single_valuedI dest: single_valuedD simp: sum_rel_def)

lemma sum_rel_id[relator_props]: "⟦Rl=Id; Rr=Id⟧ ⟹ ⟨Rl,Rr⟩sum_rel = Id"
apply (auto elim: sum_relE)
apply (case_tac b)
apply simp_all
done

lemma sum_rel_id_simp[simp]: "⟨Id,Id⟩sum_rel = Id" by tagged_solver

lemma sum_rel_mono[relator_props]:
"⟦ Rl⊆Rl'; Rr⊆Rr' ⟧ ⟹ ⟨Rl,Rr⟩sum_rel ⊆ ⟨Rl',Rr'⟩sum_rel"
by (auto simp: sum_rel_def)

lemma sum_rel_range[relator_props]:
"⟦ Range Rl=UNIV; Range Rr=UNIV ⟧ ⟹ Range (⟨Rl,Rr⟩sum_rel) = UNIV"
apply (auto simp: sum_rel_def Range_iff)
by (metis Range_iff UNIV_I sumE)

lemma list_rel_sv_iff:
"single_valued (⟨R⟩list_rel) ⟷ single_valued R"
apply (intro iffI[rotated] single_valuedI allI impI)
apply (clarsimp simp: list_rel_def)
proof -
fix x y z
assume SV: "single_valued R"
assume "list_all2 (λx x'. (x, x') ∈ R) x y" and
"list_all2 (λx x'. (x, x') ∈ R) x z"
thus "y=z"
apply (induct arbitrary: z rule: list_all2_induct)
apply simp
apply (case_tac z)
apply force
apply (force intro: single_valuedD[OF SV])
done
next
fix x y z
assume SV: "single_valued (⟨R⟩list_rel)"
assume "(x,y)∈R" "(x,z)∈R"
hence "([x],[y])∈⟨R⟩list_rel" and "([x],[z])∈⟨R⟩list_rel"
by (auto simp: list_rel_def)
with single_valuedD[OF SV] show "y=z" by blast
qed

lemma list_rel_sv[relator_props]:
"single_valued R ⟹ single_valued (⟨R⟩list_rel)"

lemma list_rel_id[relator_props]: "⟦R=Id⟧ ⟹ ⟨R⟩list_rel = Id"
by (auto simp add: list_rel_def list_all2_eq[symmetric])

lemma list_rel_id_simp[simp]: "⟨Id⟩list_rel = Id" by tagged_solver

lemma list_rel_mono[relator_props]:
assumes A: "R⊆R'"
shows "⟨R⟩list_rel ⊆ ⟨R'⟩list_rel"
proof clarsimp
fix l l'
assume "(l,l')∈⟨R⟩list_rel"
thus "(l,l')∈⟨R'⟩list_rel"
apply induct
using A
by auto
qed

lemma list_rel_range[relator_props]:
assumes A: "Range R = UNIV"
shows "Range (⟨R⟩list_rel) = UNIV"
proof (clarsimp simp: eq_UNIV_iff)
fix l
show "l∈Range (⟨R⟩list_rel)"
apply (induct l)
using A[unfolded eq_UNIV_iff]
by (auto simp: Range_iff intro: list_relI)
qed

lemma bijective_imp_sv:
"bijective R ⟹ single_valued R"
"bijective R ⟹ single_valued (R¯)"

(* TODO: Move *)
declare bijective_Id[relator_props]
declare bijective_Empty[relator_props]

text ‹Pointwise refinement for set types:›

lemma set_rel_sv[relator_props]:
"single_valued R ⟹ single_valued (⟨R⟩set_rel)"
unfolding single_valued_def set_rel_def by blast

lemma set_rel_id[relator_props]: "R=Id ⟹ ⟨R⟩set_rel = Id"

lemma set_rel_id_simp[simp]: "⟨Id⟩set_rel = Id" by tagged_solver

lemma set_rel_csv[relator_props]:
"⟦ single_valued (R¯) ⟧
⟹ single_valued ((⟨R⟩set_rel)¯)"
unfolding single_valued_def set_rel_def converse_iff
by fast

subsection ‹Invariant and Abstraction›

text ‹
Quite often, a relation can be described as combination of an
abstraction function and an invariant, such that the invariant describes valid
values on the concrete domain, and the abstraction function maps valid
concrete values to its corresponding abstract value.
›
definition build_rel where
"build_rel α I ≡ {(c,a) . a=α c ∧ I c}"
abbreviation "br≡build_rel"
lemmas br_def[refine_rel_defs] = build_rel_def

lemma in_br_conv: "(c,a)∈br α I ⟷ a=α c ∧ I c"
by (auto simp: br_def)

lemma brI[intro?]: "⟦ a=α c; I c ⟧ ⟹ (c,a)∈br α I"

lemma br_id[simp]: "br id (λ_. True) = Id"
unfolding build_rel_def by auto

lemma br_chain:
"(build_rel β J) O (build_rel α I) = build_rel (α∘β) (λs. J s ∧ I (β s))"
unfolding build_rel_def by auto

lemma br_sv[simp, intro!,relator_props]: "single_valued (br α I)"
unfolding build_rel_def
apply (rule single_valuedI)
apply auto
done

lemma converse_br_sv_iff[simp]:
"single_valued (converse (br α I)) ⟷ inj_on α (Collect I)"
by (auto intro!: inj_onI single_valuedI dest: single_valuedD inj_onD
simp: br_def) []

lemmas [relator_props] = single_valued_relcomp

lemma br_comp_alt: "br α I O R = { (c,a) . I c ∧ (α c,a)∈R }"

lemma br_comp_alt':
"{(c,a) . a=α c ∧ I c} O R = { (c,a) . I c ∧ (α c,a)∈R }"
by auto

lemma single_valued_as_brE:
assumes "single_valued R"
obtains α invar where "R=br α invar"
apply (rule that[of "λx. THE y. (x,y)∈R" "λx. x∈Domain R"])
using assms unfolding br_def
by (auto dest: single_valuedD
intro: the_equality[symmetric] theI)

"single_valued R ⟹ single_valued {(c, a). (c, a) ∈ R ∧ I c}"
by (auto dest: single_valuedD intro: single_valuedI)

lemma br_Image_conv[simp]: "br α I  S = {α x | x. x∈S ∧ I x}"
by (auto simp: br_def)

subsection ‹Miscellanneous›
lemma rel_cong: "(f,g)∈Id ⟹ (x,y)∈Id ⟹ (f x, g y)∈Id" by simp
lemma rel_fun_cong: "(f,g)∈Id ⟹ (f x, g x)∈Id" by simp
lemma rel_arg_cong: "(x,y)∈Id ⟹ (f x, f y)∈Id" by simp

subsection ‹Conversion between Predicate and Set Based Relators›
text ‹
Autoref uses set-based relators of type @{typ ‹('a×'b) set›}, while the
transfer and lifting package of Isabelle/HOL uses predicate based relators
of type @{typ ‹'a ⇒ 'b ⇒ bool›}. This section defines some utilities
to convert between the two.
›

definition "rel2p R x y ≡ (x,y)∈R"
definition "p2rel P ≡ {(x,y). P x y}"

lemma rel2pD: "⟦rel2p R a b⟧ ⟹ (a,b)∈R" by (auto simp: rel2p_def)
lemma p2relD: "⟦(a,b) ∈ p2rel R⟧ ⟹ R a b" by (auto simp: p2rel_def)

lemma rel2p_inv[simp]:
"rel2p (p2rel P) = P"
"p2rel (rel2p R) = R"
by (auto simp: rel2p_def[abs_def] p2rel_def)

named_theorems rel2p
named_theorems p2rel

lemma rel2p_dflt[rel2p]:
"rel2p Id = (=)"
"rel2p (A→B) = rel_fun (rel2p A) (rel2p B)"
"rel2p (A×⇩rB) = rel_prod (rel2p A) (rel2p B)"
"rel2p (⟨A,B⟩sum_rel) = rel_sum (rel2p A) (rel2p B)"
"rel2p (⟨A⟩option_rel) = rel_option (rel2p A)"
"rel2p (⟨A⟩list_rel) = list_all2 (rel2p A)"
by (auto
simp: rel2p_def[abs_def]
intro!: ext
simp: fun_rel_def rel_fun_def
simp: sum_rel_def elim: rel_sum.cases
simp: option_rel_def elim: option.rel_cases
simp: list_rel_def
simp: set_rel_def rel_set_def Image_def
)

lemma p2rel_dflt[p2rel]:
"p2rel (=) = Id"
"p2rel (rel_fun A B) = p2rel A → p2rel B"
"p2rel (rel_prod A B) = p2rel A ×⇩r p2rel B"
"p2rel (rel_sum A B) = ⟨p2rel A, p2rel B⟩sum_rel"
"p2rel (rel_option A) = ⟨p2rel A⟩option_rel"
"p2rel (list_all2 A) = ⟨p2rel A⟩list_rel"
by (auto
simp: p2rel_def[abs_def]
simp: fun_rel_def rel_fun_def
simp: sum_rel_def elim: rel_sum.cases
simp: option_rel_def elim: option.rel_cases
simp: list_rel_def
)

lemma [rel2p]: "rel2p (⟨A⟩set_rel) = rel_set (rel2p A)"
unfolding set_rel_def rel_set_def rel2p_def[abs_def]
by blast

lemma [p2rel]: "left_unique A ⟹ p2rel (rel_set A) = (⟨p2rel A⟩set_rel)"
unfolding set_rel_def rel_set_def p2rel_def[abs_def]
by blast

lemma rel2p_comp: "rel2p A OO rel2p B = rel2p (A O B)"
by (auto simp: rel2p_def[abs_def] intro!: ext)

lemma rel2p_inj[simp]: "rel2p A = rel2p B ⟷ A=B"
by (auto simp: rel2p_def[abs_def]; meson)

lemma rel2p_left_unique: "left_unique (rel2p A) = single_valued (A¯)"
unfolding left_unique_def rel2p_def single_valued_def by blast

lemma rel2p_right_unique: "right_unique (rel2p A) = single_valued A"
unfolding right_unique_def rel2p_def single_valued_def by blast

lemma rel2p_bi_unique: "bi_unique (rel2p A) ⟷ single_valued A ∧ single_valued (A¯)"
unfolding bi_unique_alt_def by (auto simp: rel2p_left_unique rel2p_right_unique)

lemma p2rel_left_unique: "single_valued ((p2rel A)¯) = left_unique A"
unfolding left_unique_def p2rel_def single_valued_def by blast

lemma p2rel_right_unique: "single_valued (p2rel A) = right_unique A"
unfolding right_unique_def p2rel_def single_valued_def by blast

subsection ‹More Properties›
(* TODO: Do compp-lemmas for other standard relations *)
lemma list_rel_compp: "⟨A O B⟩list_rel = ⟨A⟩list_rel O ⟨B⟩list_rel"
using list.rel_compp[of "rel2p A" "rel2p B"]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *)

lemma option_rel_compp: "⟨A O B⟩option_rel = ⟨A⟩option_rel O ⟨B⟩option_rel"
using option.rel_compp[of "rel2p A" "rel2p B"]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *)

lemma prod_rel_compp: "⟨A O B, C O D⟩prod_rel = ⟨A,C⟩prod_rel O ⟨B,D⟩prod_rel"
using prod.rel_compp[of "rel2p A" "rel2p B" "rel2p C" "rel2p D"]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *)

lemma sum_rel_compp: "⟨A O B, C O D⟩sum_rel = ⟨A,C⟩sum_rel O ⟨B,D⟩sum_rel"
using sum.rel_compp[of "rel2p A" "rel2p B" "rel2p C" "rel2p D"]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *)

lemma set_rel_compp: "⟨A O B⟩set_rel = ⟨A⟩set_rel O ⟨B⟩set_rel"
using rel_set_OO[of "rel2p A" "rel2p B"]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *)

lemma map_in_list_rel_conv:
shows "(l, map α l) ∈ ⟨br α I⟩list_rel ⟷ (∀x∈set l. I x)"
by (induction l) (auto simp: in_br_conv)

lemma br_set_rel_alt: "(s',s)∈⟨br α I⟩set_rel ⟷ (s=αs' ∧ (∀x∈s'. I x))"
by (auto simp: set_rel_def br_def)

(* TODO: Find proof that does not depend on br, and move to Misc *)
lemma finite_Image_sv: "single_valued R ⟹ finite s ⟹ finite (Rs)"
by (erule single_valued_as_brE) simp

lemma finite_set_rel_transfer: "⟦(s,s')∈⟨R⟩set_rel; single_valued R; finite s⟧ ⟹ finite s'"
unfolding set_rel_alt
by (blast intro: finite_subset[OF _ finite_Image_sv])

lemma finite_set_rel_transfer_back: "⟦(s,s')∈⟨R⟩set_rel; single_valued (R¯); finite s'⟧ ⟹ finite s"
unfolding set_rel_alt
by (blast intro: finite_subset[OF _ finite_Image_sv])

end
`