src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 52788 da1fdbfebd39
child 54895 515630483010
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
     1 (*  Title:      HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
     2     Author:     Brian Huffman
     3 
     4 Defines new types satisfying the given domain equations.
     5 *)
     6 
     7 signature DOMAIN_ISOMORPHISM =
     8 sig
     9   val domain_isomorphism :
    10       (string list * binding * mixfix * typ
    11        * (binding * binding) option) list ->
    12       theory ->
    13       (Domain_Take_Proofs.iso_info list
    14        * Domain_Take_Proofs.take_induct_info) * theory
    15 
    16   val define_map_functions :
    17       (binding * Domain_Take_Proofs.iso_info) list ->
    18       theory ->
    19       {
    20         map_consts : term list,
    21         map_apply_thms : thm list,
    22         map_unfold_thms : thm list,
    23         map_cont_thm : thm,
    24         deflation_map_thms : thm list
    25       }
    26       * theory
    27 
    28   val domain_isomorphism_cmd :
    29     (string list * binding * mixfix * string * (binding * binding) option) list
    30       -> theory -> theory
    31 
    32   val setup : theory -> theory
    33 end
    34 
    35 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
    36 struct
    37 
    38 val beta_ss =
    39   simpset_of (put_simpset HOL_basic_ss @{context}
    40     addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}])
    41 
    42 fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
    43 
    44 (******************************************************************************)
    45 (******************************** theory data *********************************)
    46 (******************************************************************************)
    47 
    48 structure RepData = Named_Thms
    49 (
    50   val name = @{binding domain_defl_simps}
    51   val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
    52 )
    53 
    54 structure IsodeflData = Named_Thms
    55 (
    56   val name = @{binding domain_isodefl}
    57   val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
    58 )
    59 
    60 val setup = RepData.setup #> IsodeflData.setup
    61 
    62 
    63 (******************************************************************************)
    64 (************************** building types and terms **************************)
    65 (******************************************************************************)
    66 
    67 open HOLCF_Library
    68 
    69 infixr 6 ->>
    70 infixr -->>
    71 
    72 val udomT = @{typ udom}
    73 val deflT = @{typ "udom defl"}
    74 val udeflT = @{typ "udom u defl"}
    75 
    76 fun mk_DEFL T =
    77   Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T
    78 
    79 fun dest_DEFL (Const (@{const_name defl}, _) $ t) = Logic.dest_type t
    80   | dest_DEFL t = raise TERM ("dest_DEFL", [t])
    81 
    82 fun mk_LIFTDEFL T =
    83   Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) $ Logic.mk_type T
    84 
    85 fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t
    86   | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t])
    87 
    88 fun mk_u_defl t = mk_capply (@{const "u_defl"}, t)
    89 
    90 fun emb_const T = Const (@{const_name emb}, T ->> udomT)
    91 fun prj_const T = Const (@{const_name prj}, udomT ->> T)
    92 fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)
    93 
    94 fun isodefl_const T =
    95   Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT)
    96 
    97 fun isodefl'_const T =
    98   Const (@{const_name isodefl'}, (T ->> T) --> udeflT --> HOLogic.boolT)
    99 
   100 fun mk_deflation t =
   101   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
   102 
   103 (* splits a cterm into the right and lefthand sides of equality *)
   104 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
   105 
   106 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
   107 
   108 (******************************************************************************)
   109 (****************************** isomorphism info ******************************)
   110 (******************************************************************************)
   111 
   112 fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm =
   113   let
   114     val abs_iso = #abs_inverse info
   115     val rep_iso = #rep_inverse info
   116     val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]
   117   in
   118     Drule.zero_var_indexes thm
   119   end
   120 
   121 (******************************************************************************)
   122 (*************** fixed-point definitions and unfolding theorems ***************)
   123 (******************************************************************************)
   124 
   125 fun mk_projs []      _ = []
   126   | mk_projs (x::[]) t = [(x, t)]
   127   | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
   128 
   129 fun add_fixdefs
   130     (spec : (binding * term) list)
   131     (thy : theory) : (thm list * thm list * thm) * theory =
   132   let
   133     val binds = map fst spec
   134     val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec)
   135     val functional = lambda_tuple lhss (mk_tuple rhss)
   136     val fixpoint = mk_fix (mk_cabs functional)
   137 
   138     (* project components of fixpoint *)
   139     val projs = mk_projs lhss fixpoint
   140 
   141     (* convert parameters to lambda abstractions *)
   142     fun mk_eqn (lhs, rhs) =
   143         case lhs of
   144           Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) =>
   145             mk_eqn (f, big_lambda x rhs)
   146         | f $ Const (@{const_name TYPE}, T) =>
   147             mk_eqn (f, Abs ("t", T, rhs))
   148         | Const _ => Logic.mk_equals (lhs, rhs)
   149         | _ => raise TERM ("lhs not of correct form", [lhs, rhs])
   150     val eqns = map mk_eqn projs
   151 
   152     (* register constant definitions *)
   153     val (fixdef_thms, thy) =
   154       (Global_Theory.add_defs false o map Thm.no_attributes)
   155         (map Thm.def_binding binds ~~ eqns) thy
   156 
   157     (* prove applied version of definitions *)
   158     fun prove_proj (lhs, rhs) =
   159       let
   160         fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
   161           (simp_tac (Simplifier.global_context thy beta_ss)) 1
   162         val goal = Logic.mk_equals (lhs, rhs)
   163       in Goal.prove_global thy [] [] goal (tac o #context) end
   164     val proj_thms = map prove_proj projs
   165 
   166     (* mk_tuple lhss == fixpoint *)
   167     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]
   168     val tuple_fixdef_thm = foldr1 pair_equalI proj_thms
   169 
   170     val cont_thm =
   171       let
   172         val prop = mk_trp (mk_cont functional)
   173         val rules = Cont2ContData.get (Proof_Context.init_global thy)
   174         val tac = REPEAT_ALL_NEW (match_tac rules) 1
   175       in
   176         Goal.prove_global thy [] [] prop (K tac)
   177       end
   178 
   179     val tuple_unfold_thm =
   180       (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
   181       |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv}
   182 
   183     fun mk_unfold_thms [] _ = []
   184       | mk_unfold_thms (n::[]) thm = [(n, thm)]
   185       | mk_unfold_thms (n::ns) thm = let
   186           val thmL = thm RS @{thm Pair_eqD1}
   187           val thmR = thm RS @{thm Pair_eqD2}
   188         in (n, thmL) :: mk_unfold_thms ns thmR end
   189     val unfold_binds = map (Binding.suffix_name "_unfold") binds
   190 
   191     (* register unfold theorems *)
   192     val (unfold_thms, thy) =
   193       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   194         (mk_unfold_thms unfold_binds tuple_unfold_thm) thy
   195   in
   196     ((proj_thms, unfold_thms, cont_thm), thy)
   197   end
   198 
   199 
   200 (******************************************************************************)
   201 (****************** deflation combinators and map functions *******************)
   202 (******************************************************************************)
   203 
   204 fun defl_of_typ
   205     (thy : theory)
   206     (tab1 : (typ * term) list)
   207     (tab2 : (typ * term) list)
   208     (T : typ) : term =
   209   let
   210     val defl_simps = RepData.get (Proof_Context.init_global thy)
   211     val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
   212     val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
   213     fun proc1 t =
   214       (case dest_DEFL t of
   215         TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT))
   216       | _ => NONE) handle TERM _ => NONE
   217     fun proc2 t =
   218       (case dest_LIFTDEFL t of
   219         TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, udeflT))
   220       | _ => NONE) handle TERM _ => NONE
   221   in
   222     Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T)
   223   end
   224 
   225 (******************************************************************************)
   226 (********************* declaring definitions and theorems *********************)
   227 (******************************************************************************)
   228 
   229 fun define_const
   230     (bind : binding, rhs : term)
   231     (thy : theory)
   232     : (term * thm) * theory =
   233   let
   234     val typ = Term.fastype_of rhs
   235     val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy
   236     val eqn = Logic.mk_equals (const, rhs)
   237     val def = Thm.no_attributes (Thm.def_binding bind, eqn)
   238     val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy
   239   in
   240     ((const, def_thm), thy)
   241   end
   242 
   243 fun add_qualified_thm name (dbind, thm) =
   244     yield_singleton Global_Theory.add_thms
   245       ((Binding.qualified true name dbind, thm), [])
   246 
   247 (******************************************************************************)
   248 (*************************** defining map functions ***************************)
   249 (******************************************************************************)
   250 
   251 fun define_map_functions
   252     (spec : (binding * Domain_Take_Proofs.iso_info) list)
   253     (thy : theory) =
   254   let
   255 
   256     (* retrieve components of spec *)
   257     val dbinds = map fst spec
   258     val iso_infos = map snd spec
   259     val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos
   260     val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos
   261 
   262     fun mapT (T as Type (_, Ts)) =
   263         (map (fn T => T ->> T) (filter (is_cpo thy) Ts)) -->> (T ->> T)
   264       | mapT T = T ->> T
   265 
   266     (* declare map functions *)
   267     fun declare_map_const (tbind, (lhsT, _)) thy =
   268       let
   269         val map_type = mapT lhsT
   270         val map_bind = Binding.suffix_name "_map" tbind
   271       in
   272         Sign.declare_const_global ((map_bind, map_type), NoSyn) thy
   273       end
   274     val (map_consts, thy) = thy |>
   275       fold_map declare_map_const (dbinds ~~ dom_eqns)
   276 
   277     (* defining equations for map functions *)
   278     local
   279       fun unprime a = Library.unprefix "'" a
   280       fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T)
   281       fun map_lhs (map_const, lhsT) =
   282           (lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (snd (dest_Type lhsT)))))
   283       val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns)
   284       val Ts = (snd o dest_Type o fst o hd) dom_eqns
   285       val tab = (Ts ~~ map mapvar Ts) @ tab1
   286       fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) =
   287         let
   288           val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT
   289           val body = Domain_Take_Proofs.map_of_typ thy tab rhsT
   290           val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const))
   291         in mk_eqs (lhs, rhs) end
   292     in
   293       val map_specs =
   294           map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns)
   295     end
   296 
   297     (* register recursive definition of map functions *)
   298     val map_binds = map (Binding.suffix_name "_map") dbinds
   299     val ((map_apply_thms, map_unfold_thms, map_cont_thm), thy) =
   300       add_fixdefs (map_binds ~~ map_specs) thy
   301 
   302     (* prove deflation theorems for map functions *)
   303     val deflation_abs_rep_thms = map deflation_abs_rep iso_infos
   304     val deflation_map_thm =
   305       let
   306         fun unprime a = Library.unprefix "'" a
   307         fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T)
   308         fun mk_assm T = mk_trp (mk_deflation (mk_f T))
   309         fun mk_goal (map_const, (lhsT, _)) =
   310           let
   311             val (_, Ts) = dest_Type lhsT
   312             val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
   313           in mk_deflation map_term end
   314         val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns
   315         val goals = map mk_goal (map_consts ~~ dom_eqns)
   316         val goal = mk_trp (foldr1 HOLogic.mk_conj goals)
   317         val adm_rules =
   318           @{thms adm_conj adm_subst [OF _ adm_deflation]
   319                  cont2cont_fst cont2cont_snd cont_id}
   320         val bottom_rules =
   321           @{thms fst_strict snd_strict deflation_bottom simp_thms}
   322         val tuple_rules =
   323           @{thms split_def fst_conv snd_conv}
   324         val deflation_rules =
   325           @{thms conjI deflation_ID}
   326           @ deflation_abs_rep_thms
   327           @ Domain_Take_Proofs.get_deflation_thms thy
   328       in
   329         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
   330          EVERY
   331           [rewrite_goals_tac ctxt map_apply_thms,
   332            rtac (map_cont_thm RS @{thm cont_fix_ind}) 1,
   333            REPEAT (resolve_tac adm_rules 1),
   334            simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
   335            simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
   336            REPEAT (etac @{thm conjE} 1),
   337            REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)])
   338       end
   339     fun conjuncts [] _ = []
   340       | conjuncts (n::[]) thm = [(n, thm)]
   341       | conjuncts (n::ns) thm = let
   342           val thmL = thm RS @{thm conjunct1}
   343           val thmR = thm RS @{thm conjunct2}
   344         in (n, thmL):: conjuncts ns thmR end
   345     val deflation_map_binds = dbinds |>
   346         map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map")
   347     val (deflation_map_thms, thy) = thy |>
   348       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   349         (conjuncts deflation_map_binds deflation_map_thm)
   350 
   351     (* register indirect recursion in theory data *)
   352     local
   353       fun register_map (dname, args) =
   354         Domain_Take_Proofs.add_rec_type (dname, args)
   355       val dnames = map (fst o dest_Type o fst) dom_eqns
   356       fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []
   357       val argss = map args dom_eqns
   358     in
   359       val thy =
   360           fold register_map (dnames ~~ argss) thy
   361     end
   362 
   363     (* register deflation theorems *)
   364     val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy
   365 
   366     val result =
   367       {
   368         map_consts = map_consts,
   369         map_apply_thms = map_apply_thms,
   370         map_unfold_thms = map_unfold_thms,
   371         map_cont_thm = map_cont_thm,
   372         deflation_map_thms = deflation_map_thms
   373       }
   374   in
   375     (result, thy)
   376   end
   377 
   378 (******************************************************************************)
   379 (******************************* main function ********************************)
   380 (******************************************************************************)
   381 
   382 fun read_typ thy str sorts =
   383   let
   384     val ctxt = Proof_Context.init_global thy
   385       |> fold (Variable.declare_typ o TFree) sorts
   386     val T = Syntax.read_typ ctxt str
   387   in (T, Term.add_tfreesT T sorts) end
   388 
   389 fun cert_typ sign raw_T sorts =
   390   let
   391     val T = Type.no_tvars (Sign.certify_typ sign raw_T)
   392       handle TYPE (msg, _, _) => error msg
   393     val sorts' = Term.add_tfreesT T sorts
   394     val _ =
   395       case duplicates (op =) (map fst sorts') of
   396         [] => ()
   397       | dups => error ("Inconsistent sort constraints for " ^ commas dups)
   398   in (T, sorts') end
   399 
   400 fun gen_domain_isomorphism
   401     (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
   402     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
   403     (thy: theory)
   404     : (Domain_Take_Proofs.iso_info list
   405        * Domain_Take_Proofs.take_induct_info) * theory =
   406   let
   407     val _ = Theory.requires thy "Domain" "domain isomorphisms"
   408 
   409     (* this theory is used just for parsing *)
   410     val tmp_thy = thy |>
   411       Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>
   412         (tbind, length tvs, mx)) doms_raw)
   413 
   414     fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
   415       let val (typ, sorts') = prep_typ thy typ_raw sorts
   416       in ((vs, t, mx, typ, morphs), sorts') end
   417 
   418     val (doms : (string list * binding * mixfix * typ * (binding * binding) option) list,
   419          sorts : (string * sort) list) =
   420       fold_map (prep_dom tmp_thy) doms_raw []
   421 
   422     (* lookup function for sorts of type variables *)
   423     fun the_sort v = the (AList.lookup (op =) sorts v)
   424 
   425     (* declare arities in temporary theory *)
   426     val tmp_thy =
   427       let
   428         fun arity (vs, tbind, _, _, _) =
   429           (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
   430       in
   431         fold Axclass.axiomatize_arity (map arity doms) tmp_thy
   432       end
   433 
   434     (* check bifiniteness of right-hand sides *)
   435     fun check_rhs (_, _, _, rhs, _) =
   436       if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()
   437       else error ("Type not of sort domain: " ^
   438         quote (Syntax.string_of_typ_global tmp_thy rhs))
   439     val _ = map check_rhs doms
   440 
   441     (* domain equations *)
   442     fun mk_dom_eqn (vs, tbind, _, rhs, _) =
   443       let fun arg v = TFree (v, the_sort v)
   444       in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end
   445     val dom_eqns = map mk_dom_eqn doms
   446 
   447     (* check for valid type parameters *)
   448     val (tyvars, _, _, _, _) = hd doms
   449     val _ = map (fn (tvs, tname, _, _, _) =>
   450       let val full_tname = Sign.full_name tmp_thy tname
   451       in
   452         (case duplicates (op =) tvs of
   453           [] =>
   454             if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)
   455             else error ("Mutually recursive domains must have same type parameters")
   456         | dups => error ("Duplicate parameter(s) for domain " ^ Binding.print tname ^
   457             " : " ^ commas dups))
   458       end) doms
   459     val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms
   460     val morphs = map (fn (_, _, _, _, morphs) => morphs) doms
   461 
   462     (* determine deflation combinator arguments *)
   463     val lhsTs : typ list = map fst dom_eqns
   464     val defl_rec = Free ("t", mk_tupleT (map (K deflT) lhsTs))
   465     val defl_recs = mk_projs lhsTs defl_rec
   466     val defl_recs' = map (apsnd mk_u_defl) defl_recs
   467     fun defl_body (_, _, _, rhsT, _) =
   468       defl_of_typ tmp_thy defl_recs defl_recs' rhsT
   469     val functional = Term.lambda defl_rec (mk_tuple (map defl_body doms))
   470 
   471     val tfrees = map fst (Term.add_tfrees functional [])
   472     val frees = map fst (Term.add_frees functional [])
   473     fun get_defl_flags (vs, _, _, _, _) =
   474       let
   475         fun argT v = TFree (v, the_sort v)
   476         fun mk_d v = "d" ^ Library.unprefix "'" v
   477         fun mk_p v = "p" ^ Library.unprefix "'" v
   478         val args = maps (fn v => [(mk_d v, mk_DEFL (argT v)), (mk_p v, mk_LIFTDEFL (argT v))]) vs
   479         val typeTs = map argT (filter (member (op =) tfrees) vs)
   480         val defl_args = map snd (filter (member (op =) frees o fst) args)
   481       in
   482         (typeTs, defl_args)
   483       end
   484     val defl_flagss = map get_defl_flags doms
   485 
   486     (* declare deflation combinator constants *)
   487     fun declare_defl_const ((typeTs, defl_args), (_, tbind, _, _, _)) thy =
   488       let
   489         val defl_bind = Binding.suffix_name "_defl" tbind
   490         val defl_type =
   491           map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT
   492       in
   493         Sign.declare_const_global ((defl_bind, defl_type), NoSyn) thy
   494       end
   495     val (defl_consts, thy) =
   496       fold_map declare_defl_const (defl_flagss ~~ doms) thy
   497 
   498     (* defining equations for type combinators *)
   499     fun mk_defl_term (defl_const, (typeTs, defl_args)) =
   500       let
   501         val type_args = map Logic.mk_type typeTs
   502       in
   503         list_ccomb (list_comb (defl_const, type_args), defl_args)
   504       end
   505     val defl_terms = map mk_defl_term (defl_consts ~~ defl_flagss)
   506     val defl_tab = map fst dom_eqns ~~ defl_terms
   507     val defl_tab' = map fst dom_eqns ~~ map mk_u_defl defl_terms
   508     fun mk_defl_spec (lhsT, rhsT) =
   509       mk_eqs (defl_of_typ tmp_thy defl_tab defl_tab' lhsT,
   510               defl_of_typ tmp_thy defl_tab defl_tab' rhsT)
   511     val defl_specs = map mk_defl_spec dom_eqns
   512 
   513     (* register recursive definition of deflation combinators *)
   514     val defl_binds = map (Binding.suffix_name "_defl") dbinds
   515     val ((defl_apply_thms, defl_unfold_thms, defl_cont_thm), thy) =
   516       add_fixdefs (defl_binds ~~ defl_specs) thy
   517 
   518     (* define types using deflation combinators *)
   519     fun make_repdef ((vs, tbind, mx, _, _), defl) thy =
   520       let
   521         val spec = (tbind, map (rpair dummyS) vs, mx)
   522         val ((_, _, _, {DEFL, ...}), thy) =
   523           Domaindef.add_domaindef spec defl NONE thy
   524         (* declare domain_defl_simps rules *)
   525         val thy = Context.theory_map (RepData.add_thm DEFL) thy
   526       in
   527         (DEFL, thy)
   528       end
   529     val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy
   530 
   531     (* prove DEFL equations *)
   532     fun mk_DEFL_eq_thm (lhsT, rhsT) =
   533       let
   534         val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
   535         val DEFL_simps = RepData.get (Proof_Context.init_global thy)
   536         fun tac ctxt =
   537           rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
   538           THEN TRY (resolve_tac defl_unfold_thms 1)
   539       in
   540         Goal.prove_global thy [] [] goal (tac o #context)
   541       end
   542     val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns
   543 
   544     (* register DEFL equations *)
   545     val DEFL_eq_binds = map (Binding.prefix_name "DEFL_eq_") dbinds
   546     val (_, thy) = thy |>
   547       (Global_Theory.add_thms o map Thm.no_attributes)
   548         (DEFL_eq_binds ~~ DEFL_eq_thms)
   549 
   550     (* define rep/abs functions *)
   551     fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy =
   552       let
   553         val rep_bind = Binding.suffix_name "_rep" tbind
   554         val abs_bind = Binding.suffix_name "_abs" tbind
   555         val ((rep_const, rep_def), thy) =
   556             define_const (rep_bind, coerce_const (lhsT, rhsT)) thy
   557         val ((abs_const, abs_def), thy) =
   558             define_const (abs_bind, coerce_const (rhsT, lhsT)) thy
   559       in
   560         (((rep_const, abs_const), (rep_def, abs_def)), thy)
   561       end
   562     val ((rep_abs_consts, rep_abs_defs), thy) = thy
   563       |> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns)
   564       |>> ListPair.unzip
   565 
   566     (* prove isomorphism and isodefl rules *)
   567     fun mk_iso_thms ((tbind, DEFL_eq), (rep_def, abs_def)) thy =
   568       let
   569         fun make thm =
   570             Drule.zero_var_indexes (thm OF [DEFL_eq, abs_def, rep_def])
   571         val rep_iso_thm = make @{thm domain_rep_iso}
   572         val abs_iso_thm = make @{thm domain_abs_iso}
   573         val isodefl_thm = make @{thm isodefl_abs_rep}
   574         val thy = thy
   575           |> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm)
   576           |> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm)
   577           |> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm)
   578       in
   579         (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
   580       end
   581     val ((iso_thms, isodefl_abs_rep_thms), thy) =
   582       thy
   583       |> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs)
   584       |>> ListPair.unzip
   585 
   586     (* collect info about rep/abs *)
   587     val iso_infos : Domain_Take_Proofs.iso_info list =
   588       let
   589         fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
   590           {
   591             repT = rhsT,
   592             absT = lhsT,
   593             rep_const = repC,
   594             abs_const = absC,
   595             rep_inverse = rep_iso,
   596             abs_inverse = abs_iso
   597           }
   598       in
   599         map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms)
   600       end
   601 
   602     (* definitions and proofs related to map functions *)
   603     val (map_info, thy) =
   604         define_map_functions (dbinds ~~ iso_infos) thy
   605     val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info
   606 
   607     (* prove isodefl rules for map functions *)
   608     val isodefl_thm =
   609       let
   610         fun unprime a = Library.unprefix "'" a
   611         fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT)
   612         fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), udeflT)
   613         fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T)
   614         fun mk_assm t =
   615           case try dest_LIFTDEFL t of
   616             SOME T => mk_trp (isodefl'_const T $ mk_f T $ mk_p T)
   617           | NONE =>
   618             let val T = dest_DEFL t
   619             in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end
   620         fun mk_goal (map_const, (T, _)) =
   621           let
   622             val (_, Ts) = dest_Type T
   623             val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
   624             val defl_term = defl_of_typ thy (Ts ~~ map mk_d Ts) (Ts ~~ map mk_p Ts) T
   625           in isodefl_const T $ map_term $ defl_term end
   626         val assms = (map mk_assm o snd o hd) defl_flagss
   627         val goals = map mk_goal (map_consts ~~ dom_eqns)
   628         val goal = mk_trp (foldr1 HOLogic.mk_conj goals)
   629         val adm_rules =
   630           @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}
   631         val bottom_rules =
   632           @{thms fst_strict snd_strict isodefl_bottom simp_thms}
   633         val tuple_rules =
   634           @{thms split_def fst_conv snd_conv}
   635         val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy
   636         val map_ID_simps = map (fn th => th RS sym) map_ID_thms
   637         val isodefl_rules =
   638           @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
   639           @ isodefl_abs_rep_thms
   640           @ IsodeflData.get (Proof_Context.init_global thy)
   641       in
   642         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
   643          EVERY
   644           [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),
   645            rtac (@{thm cont_parallel_fix_ind}
   646              OF [defl_cont_thm, map_cont_thm]) 1,
   647            REPEAT (resolve_tac adm_rules 1),
   648            simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
   649            simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
   650            simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1,
   651            REPEAT (etac @{thm conjE} 1),
   652            REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
   653       end
   654     val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
   655     fun conjuncts [] _ = []
   656       | conjuncts (n::[]) thm = [(n, thm)]
   657       | conjuncts (n::ns) thm = let
   658           val thmL = thm RS @{thm conjunct1}
   659           val thmR = thm RS @{thm conjunct2}
   660         in (n, thmL):: conjuncts ns thmR end
   661     val (isodefl_thms, thy) = thy |>
   662       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   663         (conjuncts isodefl_binds isodefl_thm)
   664     val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy
   665 
   666     (* prove map_ID theorems *)
   667     fun prove_map_ID_thm
   668         (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) =
   669       let
   670         val Ts = snd (dest_Type lhsT)
   671         fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})
   672         val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts))
   673         val goal = mk_eqs (lhs, mk_ID lhsT)
   674         val tac = EVERY
   675           [rtac @{thm isodefl_DEFL_imp_ID} 1,
   676            stac DEFL_thm 1,
   677            rtac isodefl_thm 1,
   678            REPEAT (resolve_tac @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)]
   679       in
   680         Goal.prove_global thy [] [] goal (K tac)
   681       end
   682     val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds
   683     val map_ID_thms =
   684       map prove_map_ID_thm
   685         (map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms)
   686     val (_, thy) = thy |>
   687       (Global_Theory.add_thms o map (rpair [Domain_Take_Proofs.map_ID_add]))
   688         (map_ID_binds ~~ map_ID_thms)
   689 
   690     (* definitions and proofs related to take functions *)
   691     val (take_info, thy) =
   692         Domain_Take_Proofs.define_take_functions
   693           (dbinds ~~ iso_infos) thy
   694     val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} =
   695         take_info
   696 
   697     (* least-upper-bound lemma for take functions *)
   698     val lub_take_lemma =
   699       let
   700         val lhs = mk_tuple (map mk_lub take_consts)
   701         fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})
   702         fun mk_map_ID (map_const, (lhsT, _)) =
   703           list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))))
   704         val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns))
   705         val goal = mk_trp (mk_eq (lhs, rhs))
   706         val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy
   707         val start_rules =
   708             @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
   709             @ @{thms pair_collapse split_def}
   710             @ map_apply_thms @ map_ID_thms
   711         val rules0 =
   712             @{thms iterate_0 Pair_strict} @ take_0_thms
   713         val rules1 =
   714             @{thms iterate_Suc prod_eq_iff fst_conv snd_conv}
   715             @ take_Suc_thms
   716         fun tac ctxt =
   717             EVERY
   718             [simp_tac (put_simpset HOL_basic_ss ctxt addsimps start_rules) 1,
   719              simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms fix_def2}) 1,
   720              rtac @{thm lub_eq} 1,
   721              rtac @{thm nat.induct} 1,
   722              simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules0) 1,
   723              asm_full_simp_tac (put_simpset beta_ss ctxt addsimps rules1) 1]
   724       in
   725         Goal.prove_global thy [] [] goal (tac o #context)
   726       end
   727 
   728     (* prove lub of take equals ID *)
   729     fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =
   730       let
   731         val n = Free ("n", natT)
   732         val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
   733         val tac =
   734             EVERY
   735             [rtac @{thm trans} 1, rtac map_ID_thm 2,
   736              cut_tac lub_take_lemma 1,
   737              REPEAT (etac @{thm Pair_inject} 1), atac 1]
   738         val lub_take_thm = Goal.prove_global thy [] [] goal (K tac)
   739       in
   740         add_qualified_thm "lub_take" (dbind, lub_take_thm) thy
   741       end
   742     val (lub_take_thms, thy) =
   743         fold_map prove_lub_take
   744           (dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy
   745 
   746     (* prove additional take theorems *)
   747     val (take_info2, thy) =
   748         Domain_Take_Proofs.add_lub_take_theorems
   749           (dbinds ~~ iso_infos) take_info lub_take_thms thy
   750   in
   751     ((iso_infos, take_info2), thy)
   752   end
   753 
   754 val domain_isomorphism = gen_domain_isomorphism cert_typ
   755 val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ
   756 
   757 (******************************************************************************)
   758 (******************************** outer syntax ********************************)
   759 (******************************************************************************)
   760 
   761 local
   762 
   763 val parse_domain_iso :
   764     (string list * binding * mixfix * string * (binding * binding) option)
   765       parser =
   766   (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
   767     Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
   768     >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs))
   769 
   770 val parse_domain_isos = Parse.and_list1 parse_domain_iso
   771 
   772 in
   773 
   774 val _ =
   775   Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
   776     (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
   777 
   778 end
   779 
   780 end