(*  Title:      HOL/HOLCF/Tools/Domain/domain_isomorphism.ML

     Author:     Brian Huffman

 Defines new types satisfying the given domain equations.

 *)

 signature DOMAIN_ISOMORPHISM =

 sig

   val domain_isomorphism :

       (string list * binding * mixfix * typ

        * (binding * binding) option) list ->

       theory ->

       (Domain_Take_Proofs.iso_info list

        * Domain_Take_Proofs.take_induct_info) * theory

   val define_map_functions :

       (binding * Domain_Take_Proofs.iso_info) list ->

       theory ->

       {

         map_consts : term list,

         map_apply_thms : thm list,

         map_unfold_thms : thm list,

         map_cont_thm : thm,

         deflation_map_thms : thm list

       }

       * theory

   val domain_isomorphism_cmd :

     (string list * binding * mixfix * string * (binding * binding) option) list

       -> theory -> theory

 end

 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =

 struct

 val beta_ss =

   simpset_of (put_simpset HOL_basic_ss @{context}

     addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}])

 fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})

 (******************************************************************************)

 (************************** building types and terms **************************)

 (******************************************************************************)

 open HOLCF_Library

 infixr 6 ->>

 infixr -->>

 val udomT = @{typ udom}

 val deflT = @{typ "udom defl"}

 val udeflT = @{typ "udom u defl"}

 fun mk_DEFL T =

   Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T

 fun dest_DEFL (Const (@{const_name defl}, _) $ t) = Logic.dest_type t

   | dest_DEFL t = raise TERM ("dest_DEFL", [t])

 fun mk_LIFTDEFL T =

   Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) $ Logic.mk_type T

 fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t

   | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t])

 fun mk_u_defl t = mk_capply (@{const "u_defl"}, t)

 fun emb_const T = Const (@{const_name emb}, T ->> udomT)

 fun prj_const T = Const (@{const_name prj}, udomT ->> T)

 fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)

 fun isodefl_const T =

   Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT)

 fun isodefl'_const T =

   Const (@{const_name isodefl'}, (T ->> T) --> udeflT --> HOLogic.boolT)

 fun mk_deflation t =

   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t

 (* splits a cterm into the right and lefthand sides of equality *)

 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)

 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))

 (******************************************************************************)

 (****************************** isomorphism info ******************************)

 (******************************************************************************)

 fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm =

   let

     val abs_iso = #abs_inverse info

     val rep_iso = #rep_inverse info

     val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]

   in

     Drule.zero_var_indexes thm

   end

 (******************************************************************************)

 (*************** fixed-point definitions and unfolding theorems ***************)

 (******************************************************************************)

 fun mk_projs []      _ = []

   | mk_projs (x::[]) t = [(x, t)]

   | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)

 fun add_fixdefs

     (spec : (binding * term) list)

     (thy : theory) : (thm list * thm list * thm) * theory =

   let

     val binds = map fst spec

     val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec)

     val functional = lambda_tuple lhss (mk_tuple rhss)

     val fixpoint = mk_fix (mk_cabs functional)

     (* project components of fixpoint *)

     val projs = mk_projs lhss fixpoint

     (* convert parameters to lambda abstractions *)

     fun mk_eqn (lhs, rhs) =

         case lhs of

           Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) =>

             mk_eqn (f, big_lambda x rhs)

         | f $ Const (@{const_name Pure.type}, T) =>

             mk_eqn (f, Abs ("t", T, rhs))

         | Const _ => Logic.mk_equals (lhs, rhs)

         | _ => raise TERM ("lhs not of correct form", [lhs, rhs])

     val eqns = map mk_eqn projs

     (* register constant definitions *)

     val (fixdef_thms, thy) =

       (Global_Theory.add_defs false o map Thm.no_attributes)

         (map Thm.def_binding binds ~~ eqns) thy

     (* prove applied version of definitions *)

     fun prove_proj (lhs, rhs) =

       let

         fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN

           (simp_tac (put_simpset beta_ss ctxt)) 1

         val goal = Logic.mk_equals (lhs, rhs)

       in Goal.prove_global thy [] [] goal (tac o #context) end

     val proj_thms = map prove_proj projs

     (* mk_tuple lhss == fixpoint *)

     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]

     val tuple_fixdef_thm = foldr1 pair_equalI proj_thms

     val cont_thm =

       let

         val prop = mk_trp (mk_cont functional)

         val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}

         fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1

       in

         Goal.prove_global thy [] [] prop (tac o #context)

       end

     val tuple_unfold_thm =

       (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])

       |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv}

     fun mk_unfold_thms [] _ = []

       | mk_unfold_thms (n::[]) thm = [(n, thm)]

       | mk_unfold_thms (n::ns) thm = let

           val thmL = thm RS @{thm Pair_eqD1}

           val thmR = thm RS @{thm Pair_eqD2}

         in (n, thmL) :: mk_unfold_thms ns thmR end

     val unfold_binds = map (Binding.suffix_name "_unfold") binds

     (* register unfold theorems *)

     val (unfold_thms, thy) =

       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))

         (mk_unfold_thms unfold_binds tuple_unfold_thm) thy

   in

     ((proj_thms, unfold_thms, cont_thm), thy)

   end

 (******************************************************************************)

 (****************** deflation combinators and map functions *******************)

 (******************************************************************************)

 fun defl_of_typ

     (thy : theory)

     (tab1 : (typ * term) list)

     (tab2 : (typ * term) list)

     (T : typ) : term =

   let

     val defl_simps =

       Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}

     val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) (rev defl_simps)

     val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2

     fun proc1 t =

       (case dest_DEFL t of

         TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT))

       | _ => NONE) handle TERM _ => NONE

     fun proc2 t =

       (case dest_LIFTDEFL t of

         TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, udeflT))

       | _ => NONE) handle TERM _ => NONE

   in

     Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T)

   end

 (******************************************************************************)

 (********************* declaring definitions and theorems *********************)

 (******************************************************************************)

 fun define_const

     (bind : binding, rhs : term)

     (thy : theory)

     : (term * thm) * theory =

   let

     val typ = Term.fastype_of rhs

     val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy

     val eqn = Logic.mk_equals (const, rhs)

     val def = Thm.no_attributes (Thm.def_binding bind, eqn)

     val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy

   in

     ((const, def_thm), thy)

   end

 fun add_qualified_thm name (dbind, thm) =

     yield_singleton Global_Theory.add_thms

       ((Binding.qualified true name dbind, thm), [])

 (******************************************************************************)

 (*************************** defining map functions ***************************)

 (******************************************************************************)

 fun define_map_functions

     (spec : (binding * Domain_Take_Proofs.iso_info) list)

     (thy : theory) =

   let

     (* retrieve components of spec *)

     val dbinds = map fst spec

     val iso_infos = map snd spec

     val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos

     val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos

     fun mapT (T as Type (_, Ts)) =

         (map (fn T => T ->> T) (filter (is_cpo thy) Ts)) -->> (T ->> T)

       | mapT T = T ->> T

     (* declare map functions *)

     fun declare_map_const (tbind, (lhsT, _)) thy =

       let

         val map_type = mapT lhsT

         val map_bind = Binding.suffix_name "_map" tbind

       in

         Sign.declare_const_global ((map_bind, map_type), NoSyn) thy

       end

     val (map_consts, thy) = thy |>

       fold_map declare_map_const (dbinds ~~ dom_eqns)

     (* defining equations for map functions *)

     local

       fun unprime a = Library.unprefix "'" a

       fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T)

       fun map_lhs (map_const, lhsT) =

           (lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (snd (dest_Type lhsT)))))

       val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns)

       val Ts = (snd o dest_Type o fst o hd) dom_eqns

       val tab = (Ts ~~ map mapvar Ts) @ tab1

       fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) =

         let

           val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT

           val body = Domain_Take_Proofs.map_of_typ thy tab rhsT

           val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const))

         in mk_eqs (lhs, rhs) end

     in

       val map_specs =

           map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns)

     end

     (* register recursive definition of map functions *)

     val map_binds = map (Binding.suffix_name "_map") dbinds

     val ((map_apply_thms, map_unfold_thms, map_cont_thm), thy) =

       add_fixdefs (map_binds ~~ map_specs) thy

     (* prove deflation theorems for map functions *)

     val deflation_abs_rep_thms = map deflation_abs_rep iso_infos

     val deflation_map_thm =

       let

         fun unprime a = Library.unprefix "'" a

         fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T)

         fun mk_assm T = mk_trp (mk_deflation (mk_f T))

         fun mk_goal (map_const, (lhsT, _)) =

           let

             val (_, Ts) = dest_Type lhsT

             val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))

           in mk_deflation map_term end

         val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns

         val goals = map mk_goal (map_consts ~~ dom_eqns)

         val goal = mk_trp (foldr1 HOLogic.mk_conj goals)

         val adm_rules =

           @{thms adm_conj adm_subst [OF _ adm_deflation]

                  cont2cont_fst cont2cont_snd cont_id}

         val bottom_rules =

           @{thms fst_strict snd_strict deflation_bottom simp_thms}

         val tuple_rules =

           @{thms split_def fst_conv snd_conv}

         val deflation_rules =

           @{thms conjI deflation_ID}

           @ deflation_abs_rep_thms

           @ Domain_Take_Proofs.get_deflation_thms thy

       in

         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>

          EVERY

           [rewrite_goals_tac ctxt map_apply_thms,

            resolve_tac ctxt [map_cont_thm RS @{thm cont_fix_ind}] 1,

            REPEAT (resolve_tac ctxt adm_rules 1),

            simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,

            simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,

            REPEAT (eresolve_tac ctxt @{thms conjE} 1),

            REPEAT (resolve_tac ctxt (deflation_rules @ prems) 1 ORELSE assume_tac ctxt 1)])

       end

     fun conjuncts [] _ = []

       | conjuncts (n::[]) thm = [(n, thm)]

       | conjuncts (n::ns) thm = let

           val thmL = thm RS @{thm conjunct1}

           val thmR = thm RS @{thm conjunct2}

         in (n, thmL):: conjuncts ns thmR end

     val deflation_map_binds = dbinds |>

         map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map")

     val (deflation_map_thms, thy) = thy |>

       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))

         (conjuncts deflation_map_binds deflation_map_thm)

     (* register indirect recursion in theory data *)

     local

       fun register_map (dname, args) =

         Domain_Take_Proofs.add_rec_type (dname, args)

       val dnames = map (fst o dest_Type o fst) dom_eqns

       fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []

       val argss = map args dom_eqns

     in

       val thy =

           fold register_map (dnames ~~ argss) thy

     end

     (* register deflation theorems *)

     val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy

     val result =

       {

         map_consts = map_consts,

         map_apply_thms = map_apply_thms,

         map_unfold_thms = map_unfold_thms,

         map_cont_thm = map_cont_thm,

         deflation_map_thms = deflation_map_thms

       }

   in

     (result, thy)

   end

 (******************************************************************************)

 (******************************* main function ********************************)

 (******************************************************************************)

 fun read_typ thy str sorts =

   let

     val ctxt = Proof_Context.init_global thy

       |> fold (Variable.declare_typ o TFree) sorts

     val T = Syntax.read_typ ctxt str

   in (T, Term.add_tfreesT T sorts) end

 fun cert_typ sign raw_T sorts =

   let

     val T = Type.no_tvars (Sign.certify_typ sign raw_T)

       handle TYPE (msg, _, _) => error msg

     val sorts' = Term.add_tfreesT T sorts

     val _ =

       case duplicates (op =) (map fst sorts') of

         [] => ()

       | dups => error ("Inconsistent sort constraints for " ^ commas dups)

   in (T, sorts') end

 fun gen_domain_isomorphism

     (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)

     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)

     (thy: theory)

     : (Domain_Take_Proofs.iso_info list

        * Domain_Take_Proofs.take_induct_info) * theory =

   let

     (* this theory is used just for parsing *)

     val tmp_thy = thy |>

       Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>

         (tbind, length tvs, mx)) doms_raw)

     fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =

       let val (typ, sorts') = prep_typ thy typ_raw sorts

       in ((vs, t, mx, typ, morphs), sorts') end

     val (doms : (string list * binding * mixfix * typ * (binding * binding) option) list,

          sorts : (string * sort) list) =

       fold_map (prep_dom tmp_thy) doms_raw []

     (* lookup function for sorts of type variables *)

     fun the_sort v = the (AList.lookup (op =) sorts v)

     (* declare arities in temporary theory *)

     val tmp_thy =

       let

         fun arity (vs, tbind, _, _, _) =

           (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})

       in

         fold Axclass.arity_axiomatization (map arity doms) tmp_thy

       end

     (* check bifiniteness of right-hand sides *)

     fun check_rhs (_, _, _, rhs, _) =

       if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()

       else error ("Type not of sort domain: " ^

         quote (Syntax.string_of_typ_global tmp_thy rhs))

     val _ = map check_rhs doms

     (* domain equations *)

     fun mk_dom_eqn (vs, tbind, _, rhs, _) =

       let fun arg v = TFree (v, the_sort v)

       in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end

     val dom_eqns = map mk_dom_eqn doms

     (* check for valid type parameters *)

     val (tyvars, _, _, _, _) = hd doms

     val _ = map (fn (tvs, tname, _, _, _) =>

       let val full_tname = Sign.full_name tmp_thy tname

       in

         (case duplicates (op =) tvs of

           [] =>

             if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)

             else error ("Mutually recursive domains must have same type parameters")

         | dups => error ("Duplicate parameter(s) for domain " ^ Binding.print tname ^

             " : " ^ commas dups))

       end) doms

     val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms

     val morphs = map (fn (_, _, _, _, morphs) => morphs) doms

     (* determine deflation combinator arguments *)

     val lhsTs : typ list = map fst dom_eqns

     val defl_rec = Free ("t", mk_tupleT (map (K deflT) lhsTs))

     val defl_recs = mk_projs lhsTs defl_rec

     val defl_recs' = map (apsnd mk_u_defl) defl_recs

     fun defl_body (_, _, _, rhsT, _) =

       defl_of_typ tmp_thy defl_recs defl_recs' rhsT

     val functional = Term.lambda defl_rec (mk_tuple (map defl_body doms))

     val tfrees = map fst (Term.add_tfrees functional [])

     val frees = map fst (Term.add_frees functional [])

     fun get_defl_flags (vs, _, _, _, _) =

       let

         fun argT v = TFree (v, the_sort v)

         fun mk_d v = "d" ^ Library.unprefix "'" v

         fun mk_p v = "p" ^ Library.unprefix "'" v

         val args = maps (fn v => [(mk_d v, mk_DEFL (argT v)), (mk_p v, mk_LIFTDEFL (argT v))]) vs

         val typeTs = map argT (filter (member (op =) tfrees) vs)

         val defl_args = map snd (filter (member (op =) frees o fst) args)

       in

         (typeTs, defl_args)

       end

     val defl_flagss = map get_defl_flags doms

     (* declare deflation combinator constants *)

     fun declare_defl_const ((typeTs, defl_args), (_, tbind, _, _, _)) thy =

       let

         val defl_bind = Binding.suffix_name "_defl" tbind

         val defl_type =

           map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT

       in

         Sign.declare_const_global ((defl_bind, defl_type), NoSyn) thy

       end

     val (defl_consts, thy) =

       fold_map declare_defl_const (defl_flagss ~~ doms) thy

     (* defining equations for type combinators *)

     fun mk_defl_term (defl_const, (typeTs, defl_args)) =

       let

         val type_args = map Logic.mk_type typeTs

       in

         list_ccomb (list_comb (defl_const, type_args), defl_args)

       end

     val defl_terms = map mk_defl_term (defl_consts ~~ defl_flagss)

     val defl_tab = map fst dom_eqns ~~ defl_terms

     val defl_tab' = map fst dom_eqns ~~ map mk_u_defl defl_terms

     fun mk_defl_spec (lhsT, rhsT) =

       mk_eqs (defl_of_typ tmp_thy defl_tab defl_tab' lhsT,

               defl_of_typ tmp_thy defl_tab defl_tab' rhsT)

     val defl_specs = map mk_defl_spec dom_eqns

     (* register recursive definition of deflation combinators *)

     val defl_binds = map (Binding.suffix_name "_defl") dbinds

     val ((defl_apply_thms, defl_unfold_thms, defl_cont_thm), thy) =

       add_fixdefs (defl_binds ~~ defl_specs) thy

     (* define types using deflation combinators *)

     fun make_repdef ((vs, tbind, mx, _, _), defl) thy =

       let

         val spec = (tbind, map (rpair dummyS) vs, mx)

         val ((_, _, _, {DEFL, ...}), thy) =

           Domaindef.add_domaindef spec defl NONE thy

         (* declare domain_defl_simps rules *)

         val thy =

           Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_defl_simps} DEFL) thy

       in

         (DEFL, thy)

       end

     val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy

     (* prove DEFL equations *)

     fun mk_DEFL_eq_thm (lhsT, rhsT) =

       let

         val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)

         val DEFL_simps =

           Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}

         fun tac ctxt =

           rewrite_goals_tac ctxt (map mk_meta_eq (rev DEFL_simps))

           THEN TRY (resolve_tac ctxt defl_unfold_thms 1)

       in

         Goal.prove_global thy [] [] goal (tac o #context)

       end

     val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns

     (* register DEFL equations *)

     val DEFL_eq_binds = map (Binding.prefix_name "DEFL_eq_") dbinds

     val (_, thy) = thy |>

       (Global_Theory.add_thms o map Thm.no_attributes)

         (DEFL_eq_binds ~~ DEFL_eq_thms)

     (* define rep/abs functions *)

     fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy =

       let

         val rep_bind = Binding.suffix_name "_rep" tbind

         val abs_bind = Binding.suffix_name "_abs" tbind

         val ((rep_const, rep_def), thy) =

             define_const (rep_bind, coerce_const (lhsT, rhsT)) thy

         val ((abs_const, abs_def), thy) =

             define_const (abs_bind, coerce_const (rhsT, lhsT)) thy

       in

         (((rep_const, abs_const), (rep_def, abs_def)), thy)

       end

     val ((rep_abs_consts, rep_abs_defs), thy) = thy

       |> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns)

       |>> ListPair.unzip

     (* prove isomorphism and isodefl rules *)

     fun mk_iso_thms ((tbind, DEFL_eq), (rep_def, abs_def)) thy =

       let

         fun make thm =

             Drule.zero_var_indexes (thm OF [DEFL_eq, abs_def, rep_def])

         val rep_iso_thm = make @{thm domain_rep_iso}

         val abs_iso_thm = make @{thm domain_abs_iso}

         val isodefl_thm = make @{thm isodefl_abs_rep}

         val thy = thy

           |> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm)

           |> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm)

           |> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm)

       in

         (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)

       end

     val ((iso_thms, isodefl_abs_rep_thms), thy) =

       thy

       |> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs)

       |>> ListPair.unzip

     (* collect info about rep/abs *)

     val iso_infos : Domain_Take_Proofs.iso_info list =

       let

         fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =

           {

             repT = rhsT,

             absT = lhsT,

             rep_const = repC,

             abs_const = absC,

             rep_inverse = rep_iso,

             abs_inverse = abs_iso

           }

       in

         map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms)

       end

     (* definitions and proofs related to map functions *)

     val (map_info, thy) =

         define_map_functions (dbinds ~~ iso_infos) thy

     val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info

     (* prove isodefl rules for map functions *)

     val isodefl_thm =

       let

         fun unprime a = Library.unprefix "'" a

         fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT)

         fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), udeflT)

         fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T)

         fun mk_assm t =

           case try dest_LIFTDEFL t of

             SOME T => mk_trp (isodefl'_const T $ mk_f T $ mk_p T)

           | NONE =>

             let val T = dest_DEFL t

             in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end

         fun mk_goal (map_const, (T, _)) =

           let

             val (_, Ts) = dest_Type T

             val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))

             val defl_term = defl_of_typ thy (Ts ~~ map mk_d Ts) (Ts ~~ map mk_p Ts) T

           in isodefl_const T $ map_term $ defl_term end

         val assms = (map mk_assm o snd o hd) defl_flagss

         val goals = map mk_goal (map_consts ~~ dom_eqns)

         val goal = mk_trp (foldr1 HOLogic.mk_conj goals)

         val adm_rules =

           @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}

         val bottom_rules =

           @{thms fst_strict snd_strict isodefl_bottom simp_thms}

         val tuple_rules =

           @{thms split_def fst_conv snd_conv}

         val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy

         val map_ID_simps = map (fn th => th RS sym) map_ID_thms

         val isodefl_rules =

           @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}

           @ isodefl_abs_rep_thms

           @ rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl})

       in

         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>

          EVERY

           [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),

            resolve_tac ctxt [@{thm cont_parallel_fix_ind} OF [defl_cont_thm, map_cont_thm]] 1,

            REPEAT (resolve_tac ctxt adm_rules 1),

            simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,

            simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,

            simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1,

            REPEAT (eresolve_tac ctxt @{thms conjE} 1),

            REPEAT (resolve_tac ctxt (isodefl_rules @ prems) 1 ORELSE assume_tac ctxt 1)])

       end

     val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds

     fun conjuncts [] _ = []

       | conjuncts (n::[]) thm = [(n, thm)]

       | conjuncts (n::ns) thm = let

           val thmL = thm RS @{thm conjunct1}

           val thmR = thm RS @{thm conjunct2}

         in (n, thmL):: conjuncts ns thmR end

     val (isodefl_thms, thy) = thy |>

       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))

         (conjuncts isodefl_binds isodefl_thm)

     val thy =

       fold (Context.theory_map o Named_Theorems.add_thm @{named_theorems domain_isodefl})

         isodefl_thms thy

     (* prove map_ID theorems *)

     fun prove_map_ID_thm

         (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) =

       let

         val Ts = snd (dest_Type lhsT)

         fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})

         val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts))

         val goal = mk_eqs (lhs, mk_ID lhsT)

         fun tac ctxt = EVERY

           [resolve_tac ctxt @{thms isodefl_DEFL_imp_ID} 1,

            stac ctxt DEFL_thm 1,

            resolve_tac ctxt [isodefl_thm] 1,

            REPEAT (resolve_tac ctxt @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)]

       in

         Goal.prove_global thy [] [] goal (tac o #context)

       end

     val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds

     val map_ID_thms =

       map prove_map_ID_thm

         (map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms)

     val (_, thy) = thy |>

       (Global_Theory.add_thms o map (rpair [Domain_Take_Proofs.map_ID_add]))

         (map_ID_binds ~~ map_ID_thms)

     (* definitions and proofs related to take functions *)

     val (take_info, thy) =

         Domain_Take_Proofs.define_take_functions

           (dbinds ~~ iso_infos) thy

     val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} =

         take_info

     (* least-upper-bound lemma for take functions *)

     val lub_take_lemma =

       let

         val lhs = mk_tuple (map mk_lub take_consts)

         fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})

         fun mk_map_ID (map_const, (lhsT, _)) =

           list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))))

         val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns))

         val goal = mk_trp (mk_eq (lhs, rhs))

         val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy

         val start_rules =

             @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms

             @ @{thms prod.collapse split_def}

             @ map_apply_thms @ map_ID_thms

         val rules0 =

             @{thms iterate_0 Pair_strict} @ take_0_thms

         val rules1 =

             @{thms iterate_Suc prod_eq_iff fst_conv snd_conv}

             @ take_Suc_thms

         fun tac ctxt =

             EVERY

             [simp_tac (put_simpset HOL_basic_ss ctxt addsimps start_rules) 1,

              simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms fix_def2}) 1,

              resolve_tac ctxt @{thms lub_eq} 1,

              resolve_tac ctxt @{thms nat.induct} 1,

              simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules0) 1,

              asm_full_simp_tac (put_simpset beta_ss ctxt addsimps rules1) 1]

       in

         Goal.prove_global thy [] [] goal (tac o #context)

       end

     (* prove lub of take equals ID *)

     fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =

       let

         val n = Free ("n", natT)

         val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)

         fun tac ctxt =

             EVERY

             [resolve_tac ctxt @{thms trans} 1,

              resolve_tac ctxt [map_ID_thm] 2,

              cut_tac lub_take_lemma 1,

              REPEAT (eresolve_tac ctxt @{thms Pair_inject} 1), assume_tac ctxt 1]

         val lub_take_thm = Goal.prove_global thy [] [] goal (tac o #context)

       in

         add_qualified_thm "lub_take" (dbind, lub_take_thm) thy

       end

     val (lub_take_thms, thy) =

         fold_map prove_lub_take

           (dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy

     (* prove additional take theorems *)

     val (take_info2, thy) =

         Domain_Take_Proofs.add_lub_take_theorems

           (dbinds ~~ iso_infos) take_info lub_take_thms thy

   in

     ((iso_infos, take_info2), thy)

   end

 val domain_isomorphism = gen_domain_isomorphism cert_typ

 val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ

 (******************************************************************************)

 (******************************** outer syntax ********************************)

 (******************************************************************************)

 local

 val parse_domain_iso :

     (string list * binding * mixfix * string * (binding * binding) option)

       parser =

   (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --

     Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))

     >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs))

 val parse_domain_isos = Parse.and_list1 parse_domain_iso

 in

 val _ =

   Outer_Syntax.command @{command_keyword domain_isomorphism} "define domain isomorphisms (HOLCF)"

     (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))

 end

 end