Theory Automatic_Refinement.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)

syntax_consts "_rel_APP" == relAPP

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)

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)}"
  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: 
  "(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'}"
  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)
  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)}"
  by (simp add: set_rel_def_internal relAPP_def)
    
lemma set_rel_alt: "⟨R⟩set_rel = {(A,B). A ⊆ R¯``B ∧ B ⊆ R``A}"
  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'=R``S ∧ S⊆Domain R}"

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

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}
    "Additional relator properties 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
        \<^try>‹declare_natural_relator (natural_relator_from_term t) context
          catch TERM (msg,_) => warn msg
            | exn => 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}
›

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 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)" 
  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

lemma bijective_imp_sv:  
  "bijective R ⟹ single_valued R"
  "bijective R ⟹ single_valued (R¯)"
  by (simp_all add: bijective_alt)

(* 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"
  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)¯)"
  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"
  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 (α∘β) (λ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)

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 (R``s)" 
  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