src/HOLCF/Tools/Domain/domain_isomorphism.ML
author wenzelm
Mon May 17 23:54:15 2010 +0200 (2010-05-17)
changeset 36960 01594f816e3a
parent 36610 bafd82950e24
child 37078 a1656804fcad
permissions -rw-r--r--
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
     1 (*  Title:      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         deflation_map_thms : thm list
    24       }
    25       * theory
    26 
    27   val domain_isomorphism_cmd :
    28     (string list * binding * mixfix * string * (binding * binding) option) list
    29       -> theory -> theory
    30   val add_type_constructor :
    31     (string * term * string * thm  * thm * thm * thm) -> theory -> theory
    32 end;
    33 
    34 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
    35 struct
    36 
    37 val beta_ss =
    38   HOL_basic_ss
    39     addsimps simp_thms
    40     addsimps [@{thm beta_cfun}]
    41     addsimprocs [@{simproc cont_proc}];
    42 
    43 val beta_tac = simp_tac beta_ss;
    44 
    45 (******************************************************************************)
    46 (******************************** theory data *********************************)
    47 (******************************************************************************)
    48 
    49 structure DeflData = Theory_Data
    50 (
    51   (* terms like "foo_defl" *)
    52   type T = term Symtab.table;
    53   val empty = Symtab.empty;
    54   val extend = I;
    55   fun merge data = Symtab.merge (K true) data;
    56 );
    57 
    58 structure RepData = Theory_Data
    59 (
    60   (* theorems like "REP('a foo) = foo_defl$REP('a)" *)
    61   type T = thm list;
    62   val empty = [];
    63   val extend = I;
    64   val merge = Thm.merge_thms;
    65 );
    66 
    67 structure MapIdData = Theory_Data
    68 (
    69   (* theorems like "foo_map$ID = ID" *)
    70   type T = thm list;
    71   val empty = [];
    72   val extend = I;
    73   val merge = Thm.merge_thms;
    74 );
    75 
    76 structure IsodeflData = Theory_Data
    77 (
    78   (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *)
    79   type T = thm list;
    80   val empty = [];
    81   val extend = I;
    82   val merge = Thm.merge_thms;
    83 );
    84 
    85 fun add_type_constructor
    86   (tname, defl_const, map_name, REP_thm,
    87    isodefl_thm, map_ID_thm, defl_map_thm) =
    88     DeflData.map (Symtab.insert (K true) (tname, defl_const))
    89     #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
    90     #> RepData.map (Thm.add_thm REP_thm)
    91     #> IsodeflData.map (Thm.add_thm isodefl_thm)
    92     #> MapIdData.map (Thm.add_thm map_ID_thm);
    93 
    94 
    95 (* val get_map_tab = MapData.get; *)
    96 
    97 
    98 (******************************************************************************)
    99 (************************** building types and terms **************************)
   100 (******************************************************************************)
   101 
   102 open HOLCF_Library;
   103 
   104 infixr 6 ->>;
   105 infix -->>;
   106 
   107 val deflT = @{typ "udom alg_defl"};
   108 
   109 fun mapT (T as Type (_, Ts)) =
   110     (map (fn T => T ->> T) Ts) -->> (T ->> T)
   111   | mapT T = T ->> T;
   112 
   113 fun mk_Rep_of T =
   114   Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
   115 
   116 fun coerce_const T = Const (@{const_name coerce}, T);
   117 
   118 fun isodefl_const T =
   119   Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
   120 
   121 fun mk_deflation t =
   122   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
   123 
   124 (* splits a cterm into the right and lefthand sides of equality *)
   125 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
   126 
   127 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
   128 
   129 (******************************************************************************)
   130 (****************************** isomorphism info ******************************)
   131 (******************************************************************************)
   132 
   133 fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm =
   134   let
   135     val abs_iso = #abs_inverse info;
   136     val rep_iso = #rep_inverse info;
   137     val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
   138   in
   139     Drule.zero_var_indexes thm
   140   end
   141 
   142 (******************************************************************************)
   143 (*************** fixed-point definitions and unfolding theorems ***************)
   144 (******************************************************************************)
   145 
   146 fun add_fixdefs
   147     (spec : (binding * term) list)
   148     (thy : theory) : (thm list * thm list) * theory =
   149   let
   150     val binds = map fst spec;
   151     val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
   152     val functional = lambda_tuple lhss (mk_tuple rhss);
   153     val fixpoint = mk_fix (mk_cabs functional);
   154 
   155     (* project components of fixpoint *)
   156     fun mk_projs []      t = []
   157       | mk_projs (x::[]) t = [(x, t)]
   158       | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
   159     val projs = mk_projs lhss fixpoint;
   160 
   161     (* convert parameters to lambda abstractions *)
   162     fun mk_eqn (lhs, rhs) =
   163         case lhs of
   164           Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
   165             mk_eqn (f, big_lambda x rhs)
   166         | Const _ => Logic.mk_equals (lhs, rhs)
   167         | _ => raise TERM ("lhs not of correct form", [lhs, rhs]);
   168     val eqns = map mk_eqn projs;
   169 
   170     (* register constant definitions *)
   171     val (fixdef_thms, thy) =
   172       (PureThy.add_defs false o map Thm.no_attributes)
   173         (map (Binding.suffix_name "_def") binds ~~ eqns) thy;
   174 
   175     (* prove applied version of definitions *)
   176     fun prove_proj (lhs, rhs) =
   177       let
   178         val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1;
   179         val goal = Logic.mk_equals (lhs, rhs);
   180       in Goal.prove_global thy [] [] goal (K tac) end;
   181     val proj_thms = map prove_proj projs;
   182 
   183     (* mk_tuple lhss == fixpoint *)
   184     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
   185     val tuple_fixdef_thm = foldr1 pair_equalI proj_thms;
   186 
   187     val cont_thm =
   188       Goal.prove_global thy [] [] (mk_trp (mk_cont functional))
   189         (K (beta_tac 1));
   190     val tuple_unfold_thm =
   191       (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
   192       |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv};
   193 
   194     fun mk_unfold_thms [] thm = []
   195       | mk_unfold_thms (n::[]) thm = [(n, thm)]
   196       | mk_unfold_thms (n::ns) thm = let
   197           val thmL = thm RS @{thm Pair_eqD1};
   198           val thmR = thm RS @{thm Pair_eqD2};
   199         in (n, thmL) :: mk_unfold_thms ns thmR end;
   200     val unfold_binds = map (Binding.suffix_name "_unfold") binds;
   201 
   202     (* register unfold theorems *)
   203     val (unfold_thms, thy) =
   204       (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   205         (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
   206   in
   207     ((proj_thms, unfold_thms), thy)
   208   end;
   209 
   210 
   211 (******************************************************************************)
   212 (****************** deflation combinators and map functions *******************)
   213 (******************************************************************************)
   214 
   215 fun defl_of_typ
   216     (tab : term Symtab.table)
   217     (T : typ) : term =
   218   let
   219     fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
   220       | is_closed_typ _ = false;
   221     fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
   222       | defl_of (TVar _) = error ("defl_of_typ: TVar")
   223       | defl_of (T as Type (c, Ts)) =
   224         case Symtab.lookup tab c of
   225           SOME t => list_ccomb (t, map defl_of Ts)
   226         | NONE => if is_closed_typ T
   227                   then mk_Rep_of T
   228                   else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
   229   in defl_of T end;
   230 
   231 
   232 (******************************************************************************)
   233 (********************* declaring definitions and theorems *********************)
   234 (******************************************************************************)
   235 
   236 fun define_const
   237     (bind : binding, rhs : term)
   238     (thy : theory)
   239     : (term * thm) * theory =
   240   let
   241     val typ = Term.fastype_of rhs;
   242     val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
   243     val eqn = Logic.mk_equals (const, rhs);
   244     val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
   245     val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
   246   in
   247     ((const, def_thm), thy)
   248   end;
   249 
   250 fun add_qualified_thm name (dbind, thm) =
   251     yield_singleton PureThy.add_thms
   252       ((Binding.qualified true name dbind, thm), []);
   253 
   254 (******************************************************************************)
   255 (*************************** defining map functions ***************************)
   256 (******************************************************************************)
   257 
   258 fun define_map_functions
   259     (spec : (binding * Domain_Take_Proofs.iso_info) list)
   260     (thy : theory) =
   261   let
   262 
   263     (* retrieve components of spec *)
   264     val dbinds = map fst spec;
   265     val iso_infos = map snd spec;
   266     val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
   267     val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
   268 
   269     (* declare map functions *)
   270     fun declare_map_const (tbind, (lhsT, rhsT)) thy =
   271       let
   272         val map_type = mapT lhsT;
   273         val map_bind = Binding.suffix_name "_map" tbind;
   274       in
   275         Sign.declare_const ((map_bind, map_type), NoSyn) thy
   276       end;
   277     val (map_consts, thy) = thy |>
   278       fold_map declare_map_const (dbinds ~~ dom_eqns);
   279 
   280     (* defining equations for map functions *)
   281     local
   282       fun unprime a = Library.unprefix "'" a;
   283       fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T);
   284       fun map_lhs (map_const, lhsT) =
   285           (lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT))));
   286       val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns);
   287       val Ts = (snd o dest_Type o fst o hd) dom_eqns;
   288       val tab = (Ts ~~ map mapvar Ts) @ tab1;
   289       fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
   290         let
   291           val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT;
   292           val body = Domain_Take_Proofs.map_of_typ thy tab rhsT;
   293           val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
   294         in mk_eqs (lhs, rhs) end;
   295     in
   296       val map_specs =
   297           map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns);
   298     end;
   299 
   300     (* register recursive definition of map functions *)
   301     val map_binds = map (Binding.suffix_name "_map") dbinds;
   302     val ((map_apply_thms, map_unfold_thms), thy) =
   303       add_fixdefs (map_binds ~~ map_specs) thy;
   304 
   305     (* prove deflation theorems for map functions *)
   306     val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
   307     val deflation_map_thm =
   308       let
   309         fun unprime a = Library.unprefix "'" a;
   310         fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T);
   311         fun mk_assm T = mk_trp (mk_deflation (mk_f T));
   312         fun mk_goal (map_const, (lhsT, rhsT)) =
   313           let
   314             val (_, Ts) = dest_Type lhsT;
   315             val map_term = list_ccomb (map_const, map mk_f Ts);
   316           in mk_deflation map_term end;
   317         val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns;
   318         val goals = map mk_goal (map_consts ~~ dom_eqns);
   319         val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
   320         val start_thms =
   321           @{thm split_def} :: map_apply_thms;
   322         val adm_rules =
   323           @{thms adm_conj adm_subst [OF _ adm_deflation]
   324                  cont2cont_fst cont2cont_snd cont_id};
   325         val bottom_rules =
   326           @{thms fst_strict snd_strict deflation_UU simp_thms};
   327         val deflation_rules =
   328           @{thms conjI deflation_ID}
   329           @ deflation_abs_rep_thms
   330           @ Domain_Take_Proofs.get_deflation_thms thy;
   331       in
   332         Goal.prove_global thy [] assms goal (fn {prems, ...} =>
   333          EVERY
   334           [simp_tac (HOL_basic_ss addsimps start_thms) 1,
   335            rtac @{thm fix_ind} 1,
   336            REPEAT (resolve_tac adm_rules 1),
   337            simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
   338            simp_tac beta_ss 1,
   339            simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
   340            REPEAT (etac @{thm conjE} 1),
   341            REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)])
   342       end;
   343     fun conjuncts [] thm = []
   344       | conjuncts (n::[]) thm = [(n, thm)]
   345       | conjuncts (n::ns) thm = let
   346           val thmL = thm RS @{thm conjunct1};
   347           val thmR = thm RS @{thm conjunct2};
   348         in (n, thmL):: conjuncts ns thmR end;
   349     val deflation_map_binds = dbinds |>
   350         map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map");
   351     val (deflation_map_thms, thy) = thy |>
   352       (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   353         (conjuncts deflation_map_binds deflation_map_thm);
   354 
   355     (* register map functions in theory data *)
   356     local
   357       fun register_map ((dname, map_name), defl_thm) =
   358           Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm);
   359       val dnames = map (fst o dest_Type o fst) dom_eqns;
   360       val map_names = map (fst o dest_Const) map_consts;
   361     in
   362       val thy =
   363           fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy;
   364     end;
   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         deflation_map_thms = deflation_map_thms
   372       }
   373   in
   374     (result, thy)
   375   end;
   376 
   377 (******************************************************************************)
   378 (******************************* main function ********************************)
   379 (******************************************************************************)
   380 
   381 fun read_typ thy str sorts =
   382   let
   383     val ctxt = ProofContext.init_global thy
   384       |> fold (Variable.declare_typ o TFree) sorts;
   385     val T = Syntax.read_typ ctxt str;
   386   in (T, Term.add_tfreesT T sorts) end;
   387 
   388 fun cert_typ sign raw_T sorts =
   389   let
   390     val T = Type.no_tvars (Sign.certify_typ sign raw_T)
   391       handle TYPE (msg, _, _) => error msg;
   392     val sorts' = Term.add_tfreesT T sorts;
   393     val _ =
   394       case duplicates (op =) (map fst sorts') of
   395         [] => ()
   396       | dups => error ("Inconsistent sort constraints for " ^ commas dups)
   397   in (T, sorts') end;
   398 
   399 fun gen_domain_isomorphism
   400     (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
   401     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
   402     (thy: theory)
   403     : (Domain_Take_Proofs.iso_info list
   404        * Domain_Take_Proofs.take_induct_info) * theory =
   405   let
   406     val _ = Theory.requires thy "Representable" "domain isomorphisms";
   407 
   408     (* this theory is used just for parsing *)
   409     val tmp_thy = thy |>
   410       Theory.copy |>
   411       Sign.add_types (map (fn (tvs, tname, mx, _, morphs) =>
   412         (tname, 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     (* domain equations *)
   423     fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
   424       let fun arg v = TFree (v, the (AList.lookup (op =) sorts v));
   425       in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end;
   426     val dom_eqns = map mk_dom_eqn doms;
   427 
   428     (* check for valid type parameters *)
   429     val (tyvars, _, _, _, _) = hd doms;
   430     val new_doms = map (fn (tvs, tname, mx, _, _) =>
   431       let val full_tname = Sign.full_name tmp_thy tname
   432       in
   433         (case duplicates (op =) tvs of
   434           [] =>
   435             if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)
   436             else error ("Mutually recursive domains must have same type parameters")
   437         | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^
   438             " : " ^ commas dups))
   439       end) doms;
   440     val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms;
   441     val morphs = map (fn (_, _, _, _, morphs) => morphs) doms;
   442 
   443     (* declare deflation combinator constants *)
   444     fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
   445       let
   446         val defl_type = map (K deflT) vs -->> deflT;
   447         val defl_bind = Binding.suffix_name "_defl" tbind;
   448       in
   449         Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
   450       end;
   451     val (defl_consts, thy) = fold_map declare_defl_const doms thy;
   452 
   453     (* defining equations for type combinators *)
   454     val defl_tab1 = DeflData.get thy;
   455     val defl_tab2 =
   456       Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts);
   457     val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
   458     val thy = DeflData.put defl_tab' thy;
   459     fun mk_defl_spec (lhsT, rhsT) =
   460       mk_eqs (defl_of_typ defl_tab' lhsT,
   461               defl_of_typ defl_tab' rhsT);
   462     val defl_specs = map mk_defl_spec dom_eqns;
   463 
   464     (* register recursive definition of deflation combinators *)
   465     val defl_binds = map (Binding.suffix_name "_defl") dbinds;
   466     val ((defl_apply_thms, defl_unfold_thms), thy) =
   467       add_fixdefs (defl_binds ~~ defl_specs) thy;
   468 
   469     (* define types using deflation combinators *)
   470     fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
   471       let
   472         fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
   473         val reps = map (mk_Rep_of o tfree) vs;
   474         val defl = list_ccomb (defl_const, reps);
   475         val ((_, _, _, {REP, ...}), thy) =
   476           Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
   477       in
   478         (REP, thy)
   479       end;
   480     val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
   481     val thy = RepData.map (fold Thm.add_thm REP_thms) thy;
   482 
   483     (* prove REP equations *)
   484     fun mk_REP_eq_thm (lhsT, rhsT) =
   485       let
   486         val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
   487         val REP_simps = RepData.get thy;
   488         val tac =
   489           rewrite_goals_tac (map mk_meta_eq REP_simps)
   490           THEN resolve_tac defl_unfold_thms 1;
   491       in
   492         Goal.prove_global thy [] [] goal (K tac)
   493       end;
   494     val REP_eq_thms = map mk_REP_eq_thm dom_eqns;
   495 
   496     (* register REP equations *)
   497     val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds;
   498     val (_, thy) = thy |>
   499       (PureThy.add_thms o map Thm.no_attributes)
   500         (REP_eq_binds ~~ REP_eq_thms);
   501 
   502     (* define rep/abs functions *)
   503     fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
   504       let
   505         val rep_bind = Binding.suffix_name "_rep" tbind;
   506         val abs_bind = Binding.suffix_name "_abs" tbind;
   507         val ((rep_const, rep_def), thy) =
   508             define_const (rep_bind, coerce_const (lhsT ->> rhsT)) thy;
   509         val ((abs_const, abs_def), thy) =
   510             define_const (abs_bind, coerce_const (rhsT ->> lhsT)) thy;
   511       in
   512         (((rep_const, abs_const), (rep_def, abs_def)), thy)
   513       end;
   514     val ((rep_abs_consts, rep_abs_defs), thy) = thy
   515       |> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns)
   516       |>> ListPair.unzip;
   517 
   518     (* prove isomorphism and isodefl rules *)
   519     fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
   520       let
   521         fun make thm =
   522             Drule.zero_var_indexes (thm OF [REP_eq, abs_def, rep_def]);
   523         val rep_iso_thm = make @{thm domain_rep_iso};
   524         val abs_iso_thm = make @{thm domain_abs_iso};
   525         val isodefl_thm = make @{thm isodefl_abs_rep};
   526         val thy = thy
   527           |> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm)
   528           |> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm)
   529           |> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm);
   530       in
   531         (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
   532       end;
   533     val ((iso_thms, isodefl_abs_rep_thms), thy) =
   534       thy
   535       |> fold_map mk_iso_thms (dbinds ~~ REP_eq_thms ~~ rep_abs_defs)
   536       |>> ListPair.unzip;
   537 
   538     (* collect info about rep/abs *)
   539     val iso_infos : Domain_Take_Proofs.iso_info list =
   540       let
   541         fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
   542           {
   543             repT = rhsT,
   544             absT = lhsT,
   545             rep_const = repC,
   546             abs_const = absC,
   547             rep_inverse = rep_iso,
   548             abs_inverse = abs_iso
   549           };
   550       in
   551         map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms)
   552       end
   553 
   554     (* definitions and proofs related to map functions *)
   555     val (map_info, thy) =
   556         define_map_functions (dbinds ~~ iso_infos) thy;
   557     val { map_consts, map_apply_thms, map_unfold_thms,
   558           deflation_map_thms } = map_info;
   559 
   560     (* prove isodefl rules for map functions *)
   561     val isodefl_thm =
   562       let
   563         fun unprime a = Library.unprefix "'" a;
   564         fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT);
   565         fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T);
   566         fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
   567         fun mk_goal ((map_const, defl_const), (T, rhsT)) =
   568           let
   569             val (_, Ts) = dest_Type T;
   570             val map_term = list_ccomb (map_const, map mk_f Ts);
   571             val defl_term = list_ccomb (defl_const, map mk_d Ts);
   572           in isodefl_const T $ map_term $ defl_term end;
   573         val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns;
   574         val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns);
   575         val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
   576         val start_thms =
   577           @{thm split_def} :: defl_apply_thms @ map_apply_thms;
   578         val adm_rules =
   579           @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
   580         val bottom_rules =
   581           @{thms fst_strict snd_strict isodefl_bottom simp_thms};
   582         val REP_simps = map (fn th => th RS sym) (RepData.get thy);
   583         val isodefl_rules =
   584           @{thms conjI isodefl_ID_REP}
   585           @ isodefl_abs_rep_thms
   586           @ IsodeflData.get thy;
   587       in
   588         Goal.prove_global thy [] assms goal (fn {prems, ...} =>
   589          EVERY
   590           [simp_tac (HOL_basic_ss addsimps start_thms) 1,
   591            (* FIXME: how reliable is unification here? *)
   592            (* Maybe I should instantiate the rule. *)
   593            rtac @{thm parallel_fix_ind} 1,
   594            REPEAT (resolve_tac adm_rules 1),
   595            simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
   596            simp_tac beta_ss 1,
   597            simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
   598            simp_tac (HOL_basic_ss addsimps REP_simps) 1,
   599            REPEAT (etac @{thm conjE} 1),
   600            REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
   601       end;
   602     val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds;
   603     fun conjuncts [] thm = []
   604       | conjuncts (n::[]) thm = [(n, thm)]
   605       | conjuncts (n::ns) thm = let
   606           val thmL = thm RS @{thm conjunct1};
   607           val thmR = thm RS @{thm conjunct2};
   608         in (n, thmL):: conjuncts ns thmR end;
   609     val (isodefl_thms, thy) = thy |>
   610       (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
   611         (conjuncts isodefl_binds isodefl_thm);
   612     val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
   613 
   614     (* prove map_ID theorems *)
   615     fun prove_map_ID_thm
   616         (((map_const, (lhsT, _)), REP_thm), isodefl_thm) =
   617       let
   618         val Ts = snd (dest_Type lhsT);
   619         val lhs = list_ccomb (map_const, map mk_ID Ts);
   620         val goal = mk_eqs (lhs, mk_ID lhsT);
   621         val tac = EVERY
   622           [rtac @{thm isodefl_REP_imp_ID} 1,
   623            stac REP_thm 1,
   624            rtac isodefl_thm 1,
   625            REPEAT (rtac @{thm isodefl_ID_REP} 1)];
   626       in
   627         Goal.prove_global thy [] [] goal (K tac)
   628       end;
   629     val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds;
   630     val map_ID_thms =
   631       map prove_map_ID_thm
   632         (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms);
   633     val (_, thy) = thy |>
   634       (PureThy.add_thms o map Thm.no_attributes)
   635         (map_ID_binds ~~ map_ID_thms);
   636     val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
   637 
   638     (* definitions and proofs related to take functions *)
   639     val (take_info, thy) =
   640         Domain_Take_Proofs.define_take_functions
   641           (dbinds ~~ iso_infos) thy;
   642     val { take_consts, take_defs, chain_take_thms, take_0_thms,
   643           take_Suc_thms, deflation_take_thms,
   644           finite_consts, finite_defs } = take_info;
   645 
   646     (* least-upper-bound lemma for take functions *)
   647     val lub_take_lemma =
   648       let
   649         val lhs = mk_tuple (map mk_lub take_consts);
   650         fun mk_map_ID (map_const, (lhsT, rhsT)) =
   651           list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT)));
   652         val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
   653         val goal = mk_trp (mk_eq (lhs, rhs));
   654         val start_rules =
   655             @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
   656             @ @{thms pair_collapse split_def}
   657             @ map_apply_thms @ MapIdData.get thy;
   658         val rules0 =
   659             @{thms iterate_0 Pair_strict} @ take_0_thms;
   660         val rules1 =
   661             @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv}
   662             @ take_Suc_thms;
   663         val tac =
   664             EVERY
   665             [simp_tac (HOL_basic_ss addsimps start_rules) 1,
   666              simp_tac (HOL_basic_ss addsimps @{thms fix_def2}) 1,
   667              rtac @{thm lub_eq} 1,
   668              rtac @{thm nat.induct} 1,
   669              simp_tac (HOL_basic_ss addsimps rules0) 1,
   670              asm_full_simp_tac (beta_ss addsimps rules1) 1];
   671       in
   672         Goal.prove_global thy [] [] goal (K tac)
   673       end;
   674 
   675     (* prove lub of take equals ID *)
   676     fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
   677       let
   678         val n = Free ("n", natT);
   679         val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT);
   680         val tac =
   681             EVERY
   682             [rtac @{thm trans} 1, rtac map_ID_thm 2,
   683              cut_facts_tac [lub_take_lemma] 1,
   684              REPEAT (etac @{thm Pair_inject} 1), atac 1];
   685         val lub_take_thm = Goal.prove_global thy [] [] goal (K tac);
   686       in
   687         add_qualified_thm "lub_take" (dbind, lub_take_thm) thy
   688       end;
   689     val (lub_take_thms, thy) =
   690         fold_map prove_lub_take
   691           (dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy;
   692 
   693     (* prove additional take theorems *)
   694     val (take_info2, thy) =
   695         Domain_Take_Proofs.add_lub_take_theorems
   696           (dbinds ~~ iso_infos) take_info lub_take_thms thy;
   697   in
   698     ((iso_infos, take_info2), thy)
   699   end;
   700 
   701 val domain_isomorphism = gen_domain_isomorphism cert_typ;
   702 val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ;
   703 
   704 (******************************************************************************)
   705 (******************************** outer syntax ********************************)
   706 (******************************************************************************)
   707 
   708 local
   709 
   710 val parse_domain_iso :
   711     (string list * binding * mixfix * string * (binding * binding) option)
   712       parser =
   713   (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   714     Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
   715     >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
   716 
   717 val parse_domain_isos = Parse.and_list1 parse_domain_iso;
   718 
   719 in
   720 
   721 val _ =
   722   Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
   723     Keyword.thy_decl
   724     (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
   725 
   726 end;
   727 
   728 end;