Theory Relators

header {* \isaheader{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 @{text "('c×'a) set"}.
  For each composed type, say @{text "'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, 
  @{text "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
  @{text "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 }"
  by (simp add: relAPP_def fun_rel_def_internal)

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 }"
  by (simp add: prod_rel_def_internal relAPP_def)

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)

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)}"
  by (simp add: option_rel_def_internal relAPP_def)

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 }"
  by (simp add: sum_rel_def_internal relAPP_def)

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: 
  "(a,a')∈Rl ==> (Inl a, Inl a') ∈ ⟨Rl,Rr⟩sum_rel"
  "(a,a')∈Rr ==> (Inr a, Inr a') ∈ ⟨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'}"
  by (simp add: list_rel_def_internal relAPP_def)

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)
proof safe
  case goal1 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 goal2 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)

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 ≡ {(S,S'). S'=R``S ∧ S⊆Domain R}"

lemma set_rel_def[refine_rel_defs]: 
  "⟨R⟩set_rel ≡ {(S,S'). S'=R``S ∧ S⊆Domain R}"
  by (simp add: set_rel_def_internal relAPP_def)

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

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}
    "Additional relator properties solver"
    (fn ctxt => (REPEAT_ALL_NEW (CHANGED o (
      match_tac (solve_relator_props.get ctxt) ORELSE'
      match_tac (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 (solve_relator_props.get ctxt) ORELSE'
      match_tac (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 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 mk_fun_rel: term -> term -> term

    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

    structure natural_relators = Generic_Data (
      type T = string Symtab.table
      val empty = Symtab.empty
      val extend = I
      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 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
  
    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 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
  |> cterm_of @{theory}
;
  Relators.mk_fun_rel @{term "⟨Id⟩option_rel"} @{term "⟨Id⟩list_rel"}
  |> cterm_of @{theory}
*}

subsubsection "Additional Properties"
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 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)" 
  by (simp add: list_rel_sv_iff)

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

text {* Pointwise refinement for set types: *}
lemma set_rel_sv[relator_props]: 
  "single_valued (⟨R⟩set_rel)"
  by (auto intro: single_valuedI dest: single_valuedD simp: set_rel_def) []

lemma set_rel_id[relator_props]: "R=Id ==> ⟨R⟩set_rel = Id"
  by (auto simp add: set_rel_def)

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)¯)"
  apply (rule single_valuedI)
  apply (simp only: converse_iff)

  apply (simp add: single_valued_def Image_def set_rel_def)
  apply (intro allI impI equalityI)
    apply (clarsimp, blast) []
    apply (clarsimp, drule (1) set_mp, blast) []
  done

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 brI[intro?]: "[| a=α c; I c |] ==> (c,a)∈br α I"
  by (simp add: br_def)

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 (αoβ) (λ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 }"
  by (auto simp add: br_def)

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)

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



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

end