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