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