src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
author wenzelm
Sun Apr 03 21:59:33 2011 +0200 (2011-04-03)
changeset 42204 b3277168c1e7
parent 42151 4da4fc77664b
child 42224 578a51fae383
permissions -rw-r--r--
added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Tools/Domain/domain_constructors.ML
huffman@35444
     2
    Author:     Brian Huffman
huffman@35444
     3
huffman@35444
     4
Defines constructor functions for a given domain isomorphism
huffman@35444
     5
and proves related theorems.
huffman@35444
     6
*)
huffman@35444
     7
huffman@35444
     8
signature DOMAIN_CONSTRUCTORS =
huffman@35444
     9
sig
huffman@40014
    10
  type constr_info =
huffman@40014
    11
    {
huffman@40017
    12
      iso_info : Domain_Take_Proofs.iso_info,
huffman@40019
    13
      con_specs : (term * (bool * typ) list) list,
huffman@40014
    14
      con_betas : thm list,
huffman@40014
    15
      nchotomy : thm,
huffman@40014
    16
      exhaust : thm,
huffman@40014
    17
      compacts : thm list,
huffman@40014
    18
      con_rews : thm list,
huffman@40014
    19
      inverts : thm list,
huffman@40014
    20
      injects : thm list,
huffman@40014
    21
      dist_les : thm list,
huffman@40014
    22
      dist_eqs : thm list,
huffman@40014
    23
      cases : thm list,
huffman@40014
    24
      sel_rews : thm list,
huffman@40014
    25
      dis_rews : thm list,
huffman@40014
    26
      match_rews : thm list
huffman@40014
    27
    }
huffman@35444
    28
  val add_domain_constructors :
huffman@35777
    29
      binding
huffman@35481
    30
      -> (binding * (bool * binding option * typ) list * mixfix) list
huffman@35514
    31
      -> Domain_Take_Proofs.iso_info
huffman@35444
    32
      -> theory
huffman@40832
    33
      -> constr_info * theory
huffman@40832
    34
end
huffman@35444
    35
huffman@35444
    36
huffman@41296
    37
structure Domain_Constructors : DOMAIN_CONSTRUCTORS =
huffman@35444
    38
struct
huffman@35444
    39
huffman@40832
    40
open HOLCF_Library
huffman@35561
    41
huffman@40832
    42
infixr 6 ->>
huffman@40832
    43
infix -->>
huffman@40832
    44
infix 9 `
huffman@35444
    45
huffman@40014
    46
type constr_info =
huffman@40014
    47
  {
huffman@40017
    48
    iso_info : Domain_Take_Proofs.iso_info,
huffman@40019
    49
    con_specs : (term * (bool * typ) list) list,
huffman@40014
    50
    con_betas : thm list,
huffman@40014
    51
    nchotomy : thm,
huffman@40014
    52
    exhaust : thm,
huffman@40014
    53
    compacts : thm list,
huffman@40014
    54
    con_rews : thm list,
huffman@40014
    55
    inverts : thm list,
huffman@40014
    56
    injects : thm list,
huffman@40014
    57
    dist_les : thm list,
huffman@40014
    58
    dist_eqs : thm list,
huffman@40014
    59
    cases : thm list,
huffman@40014
    60
    sel_rews : thm list,
huffman@40014
    61
    dis_rews : thm list,
huffman@40014
    62
    match_rews : thm list
huffman@40014
    63
  }
huffman@40014
    64
huffman@35446
    65
(************************** miscellaneous functions ***************************)
huffman@35446
    66
huffman@40832
    67
val simple_ss = HOL_basic_ss addsimps simp_thms
huffman@35456
    68
huffman@37078
    69
val beta_rules =
huffman@40326
    70
  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
huffman@40832
    71
  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}
huffman@37078
    72
huffman@40832
    73
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
huffman@35459
    74
huffman@35444
    75
fun define_consts
huffman@35444
    76
    (specs : (binding * term * mixfix) list)
huffman@35444
    77
    (thy : theory)
huffman@35444
    78
    : (term list * thm list) * theory =
huffman@35444
    79
  let
huffman@40832
    80
    fun mk_decl (b, t, mx) = (b, fastype_of t, mx)
huffman@40832
    81
    val decls = map mk_decl specs
huffman@40832
    82
    val thy = Cont_Consts.add_consts decls thy
huffman@40832
    83
    fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T)
huffman@40832
    84
    val consts = map mk_const decls
huffman@35444
    85
    fun mk_def c (b, t, mx) =
huffman@40832
    86
      (Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
huffman@40832
    87
    val defs = map2 mk_def consts specs
huffman@35444
    88
    val (def_thms, thy) =
huffman@40832
    89
      Global_Theory.add_defs false (map Thm.no_attributes defs) thy
huffman@35444
    90
  in
huffman@35444
    91
    ((consts, def_thms), thy)
huffman@40832
    92
  end
huffman@35444
    93
huffman@35449
    94
fun prove
huffman@35446
    95
    (thy : theory)
huffman@35449
    96
    (defs : thm list)
huffman@35447
    97
    (goal : term)
huffman@35449
    98
    (tacs : {prems: thm list, context: Proof.context} -> tactic list)
huffman@35447
    99
    : thm =
huffman@35449
   100
  let
huffman@35449
   101
    fun tac {prems, context} =
huffman@35449
   102
      rewrite_goals_tac defs THEN
huffman@35449
   103
      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
huffman@35449
   104
  in
huffman@35449
   105
    Goal.prove_global thy [] [] goal tac
huffman@40832
   106
  end
huffman@35445
   107
huffman@35483
   108
fun get_vars_avoiding
huffman@35483
   109
    (taken : string list)
huffman@35483
   110
    (args : (bool * typ) list)
huffman@35483
   111
    : (term list * term list) =
huffman@35483
   112
  let
huffman@40832
   113
    val Ts = map snd args
huffman@40832
   114
    val ns = Name.variant_list taken (Datatype_Prop.make_tnames Ts)
huffman@40832
   115
    val vs = map Free (ns ~~ Ts)
huffman@40832
   116
    val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
huffman@35483
   117
  in
huffman@35483
   118
    (vs, nonlazy)
huffman@40832
   119
  end
huffman@35483
   120
huffman@40832
   121
fun get_vars args = get_vars_avoiding [] args
huffman@35483
   122
huffman@35445
   123
(************** generating beta reduction rules from definitions **************)
huffman@35444
   124
huffman@35445
   125
local
huffman@35445
   126
  fun arglist (Const _ $ Abs (s, T, t)) =
huffman@35445
   127
      let
huffman@40832
   128
        val arg = Free (s, T)
huffman@40832
   129
        val (args, body) = arglist (subst_bound (arg, t))
huffman@35445
   130
      in (arg :: args, body) end
huffman@40832
   131
    | arglist t = ([], t)
huffman@35445
   132
in
huffman@35445
   133
  fun beta_of_def thy def_thm =
huffman@35445
   134
      let
huffman@40832
   135
        val (con, lam) = Logic.dest_equals (concl_of def_thm)
huffman@40832
   136
        val (args, rhs) = arglist lam
huffman@40832
   137
        val lhs = list_ccomb (con, args)
huffman@40832
   138
        val goal = mk_equals (lhs, rhs)
huffman@40832
   139
        val cs = ContProc.cont_thms lam
huffman@40832
   140
        val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs
huffman@35445
   141
      in
huffman@35449
   142
        prove thy (def_thm::betas) goal (K [rtac reflexive_thm 1])
huffman@40832
   143
      end
huffman@40832
   144
end
huffman@35444
   145
huffman@35446
   146
(******************************************************************************)
huffman@35453
   147
(************* definitions and theorems for constructor functions *************)
huffman@35453
   148
(******************************************************************************)
huffman@35453
   149
huffman@35453
   150
fun add_constructors
huffman@35454
   151
    (spec : (binding * (bool * typ) list * mixfix) list)
huffman@35453
   152
    (abs_const : term)
huffman@35453
   153
    (iso_locale : thm)
huffman@35453
   154
    (thy : theory)
huffman@35453
   155
    =
huffman@35453
   156
  let
huffman@35453
   157
huffman@35453
   158
    (* get theorems about rep and abs *)
huffman@40832
   159
    val abs_strict = iso_locale RS @{thm iso.abs_strict}
huffman@35453
   160
huffman@35457
   161
    (* get types of type isomorphism *)
huffman@40832
   162
    val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const)
huffman@35457
   163
huffman@35455
   164
    fun vars_of args =
huffman@35455
   165
      let
huffman@40832
   166
        val Ts = map snd args
huffman@40832
   167
        val ns = Datatype_Prop.make_tnames Ts
huffman@35455
   168
      in
huffman@35455
   169
        map Free (ns ~~ Ts)
huffman@40832
   170
      end
huffman@35455
   171
huffman@35453
   172
    (* define constructor functions *)
huffman@35453
   173
    val ((con_consts, con_defs), thy) =
huffman@35453
   174
      let
huffman@40832
   175
        fun one_arg (lazy, T) var = if lazy then mk_up var else var
huffman@40832
   176
        fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args))
huffman@40832
   177
        fun mk_abs t = abs_const ` t
huffman@40832
   178
        val rhss = map mk_abs (mk_sinjects (map one_con spec))
huffman@35453
   179
        fun mk_def (bind, args, mx) rhs =
huffman@40832
   180
          (bind, big_lambdas (vars_of args) rhs, mx)
huffman@35453
   181
      in
huffman@35453
   182
        define_consts (map2 mk_def spec rhss) thy
huffman@40832
   183
      end
huffman@35453
   184
huffman@35453
   185
    (* prove beta reduction rules for constructors *)
huffman@40832
   186
    val con_betas = map (beta_of_def thy) con_defs
huffman@35453
   187
huffman@35453
   188
    (* replace bindings with terms in constructor spec *)
huffman@35453
   189
    val spec' : (term * (bool * typ) list) list =
huffman@40832
   190
      let fun one_con con (b, args, mx) = (con, args)
huffman@40832
   191
      in map2 one_con con_consts spec end
huffman@35453
   192
huffman@35457
   193
    (* prove exhaustiveness of constructors *)
huffman@35457
   194
    local
huffman@35457
   195
      fun arg2typ n (true,  T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
huffman@40832
   196
        | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo}))
huffman@35457
   197
      fun args2typ n [] = (n, oneT)
huffman@35457
   198
        | args2typ n [arg] = arg2typ n arg
huffman@35457
   199
        | args2typ n (arg::args) =
huffman@35457
   200
          let
huffman@40832
   201
            val (n1, t1) = arg2typ n arg
huffman@35457
   202
            val (n2, t2) = args2typ n1 args
huffman@40832
   203
          in (n2, mk_sprodT (t1, t2)) end
huffman@35457
   204
      fun cons2typ n [] = (n, oneT)
huffman@35457
   205
        | cons2typ n [con] = args2typ n (snd con)
huffman@35457
   206
        | cons2typ n (con::cons) =
huffman@35457
   207
          let
huffman@40832
   208
            val (n1, t1) = args2typ n (snd con)
huffman@35457
   209
            val (n2, t2) = cons2typ n1 cons
huffman@40832
   210
          in (n2, mk_ssumT (t1, t2)) end
huffman@40832
   211
      val ct = ctyp_of thy (snd (cons2typ 1 spec'))
huffman@40832
   212
      val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
huffman@40832
   213
      val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
huffman@40832
   214
      val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2
huffman@35457
   215
huffman@40832
   216
      val y = Free ("y", lhsT)
huffman@35457
   217
      fun one_con (con, args) =
huffman@35457
   218
        let
huffman@40832
   219
          val (vs, nonlazy) = get_vars_avoiding ["y"] args
huffman@40832
   220
          val eqn = mk_eq (y, list_ccomb (con, vs))
huffman@40832
   221
          val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy)
huffman@40832
   222
        in Library.foldr mk_ex (vs, conj) end
huffman@40832
   223
      val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
huffman@41429
   224
      (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
huffman@35457
   225
      val tacs = [
huffman@35457
   226
          rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
huffman@35457
   227
          rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
huffman@40832
   228
          rtac thm3 1]
huffman@35457
   229
    in
huffman@40832
   230
      val nchotomy = prove thy con_betas goal (K tacs)
huffman@35781
   231
      val exhaust =
huffman@35781
   232
          (nchotomy RS @{thm exh_casedist0})
huffman@35457
   233
          |> rewrite_rule @{thms exh_casedists}
huffman@40832
   234
          |> Drule.zero_var_indexes
huffman@40832
   235
    end
huffman@35457
   236
huffman@35453
   237
    (* prove compactness rules for constructors *)
huffman@35781
   238
    val compacts =
huffman@35453
   239
      let
huffman@35453
   240
        val rules = @{thms compact_sinl compact_sinr compact_spair
huffman@40832
   241
                           compact_up compact_ONE}
huffman@35453
   242
        val tacs =
huffman@35453
   243
          [rtac (iso_locale RS @{thm iso.compact_abs}) 1,
huffman@40832
   244
           REPEAT (resolve_tac rules 1 ORELSE atac 1)]
huffman@35453
   245
        fun con_compact (con, args) =
huffman@35453
   246
          let
huffman@40832
   247
            val vs = vars_of args
huffman@40832
   248
            val con_app = list_ccomb (con, vs)
huffman@40832
   249
            val concl = mk_trp (mk_compact con_app)
huffman@40832
   250
            val assms = map (mk_trp o mk_compact) vs
huffman@40832
   251
            val goal = Logic.list_implies (assms, concl)
huffman@35453
   252
          in
huffman@35453
   253
            prove thy con_betas goal (K tacs)
huffman@40832
   254
          end
huffman@35453
   255
      in
huffman@35453
   256
        map con_compact spec'
huffman@40832
   257
      end
huffman@35453
   258
huffman@35453
   259
    (* prove strictness rules for constructors *)
huffman@35453
   260
    local
huffman@35453
   261
      fun con_strict (con, args) = 
huffman@35453
   262
        let
huffman@40832
   263
          val rules = abs_strict :: @{thms con_strict_rules}
huffman@40832
   264
          val (vs, nonlazy) = get_vars args
huffman@35453
   265
          fun one_strict v' =
huffman@35453
   266
            let
huffman@41429
   267
              val bottom = mk_bottom (fastype_of v')
huffman@41429
   268
              val vs' = map (fn v => if v = v' then bottom else v) vs
huffman@40832
   269
              val goal = mk_trp (mk_undef (list_ccomb (con, vs')))
huffman@40832
   270
              val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]
huffman@40832
   271
            in prove thy con_betas goal (K tacs) end
huffman@40832
   272
        in map one_strict nonlazy end
huffman@35453
   273
huffman@35453
   274
      fun con_defin (con, args) =
huffman@35453
   275
        let
huffman@35453
   276
          fun iff_disj (t, []) = HOLogic.mk_not t
huffman@40832
   277
            | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts)
huffman@40832
   278
          val (vs, nonlazy) = get_vars args
huffman@40832
   279
          val lhs = mk_undef (list_ccomb (con, vs))
huffman@40832
   280
          val rhss = map mk_undef nonlazy
huffman@40832
   281
          val goal = mk_trp (iff_disj (lhs, rhss))
huffman@40832
   282
          val rule1 = iso_locale RS @{thm iso.abs_bottom_iff}
huffman@40832
   283
          val rules = rule1 :: @{thms con_bottom_iff_rules}
huffman@40832
   284
          val tacs = [simp_tac (HOL_ss addsimps rules) 1]
huffman@40832
   285
        in prove thy con_betas goal (K tacs) end
huffman@35453
   286
    in
huffman@40832
   287
      val con_stricts = maps con_strict spec'
huffman@40832
   288
      val con_defins = map con_defin spec'
huffman@40832
   289
      val con_rews = con_stricts @ con_defins
huffman@40832
   290
    end
huffman@35453
   291
huffman@35456
   292
    (* prove injectiveness of constructors *)
huffman@35456
   293
    local
huffman@35456
   294
      fun pgterm rel (con, args) =
huffman@35456
   295
        let
huffman@35456
   296
          fun prime (Free (n, T)) = Free (n^"'", T)
huffman@40832
   297
            | prime t             = t
huffman@40832
   298
          val (xs, nonlazy) = get_vars args
huffman@40832
   299
          val ys = map prime xs
huffman@40832
   300
          val lhs = rel (list_ccomb (con, xs), list_ccomb (con, ys))
huffman@40832
   301
          val rhs = foldr1 mk_conj (ListPair.map rel (xs, ys))
huffman@40832
   302
          val concl = mk_trp (mk_eq (lhs, rhs))
huffman@40832
   303
          val zs = case args of [_] => [] | _ => nonlazy
huffman@40832
   304
          val assms = map (mk_trp o mk_defined) zs
huffman@40832
   305
          val goal = Logic.list_implies (assms, concl)
huffman@40832
   306
        in prove thy con_betas goal end
huffman@40832
   307
      val cons' = filter (fn (_, args) => not (null args)) spec'
huffman@35456
   308
    in
huffman@35456
   309
      val inverts =
huffman@35456
   310
        let
huffman@40832
   311
          val abs_below = iso_locale RS @{thm iso.abs_below}
huffman@40832
   312
          val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}
huffman@35456
   313
          val rules2 = @{thms up_defined spair_defined ONE_defined}
huffman@40832
   314
          val rules = rules1 @ rules2
huffman@40832
   315
          val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]
huffman@40832
   316
        in map (fn c => pgterm mk_below c (K tacs)) cons' end
huffman@35456
   317
      val injects =
huffman@35456
   318
        let
huffman@40832
   319
          val abs_eq = iso_locale RS @{thm iso.abs_eq}
huffman@40832
   320
          val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}
huffman@35456
   321
          val rules2 = @{thms up_defined spair_defined ONE_defined}
huffman@40832
   322
          val rules = rules1 @ rules2
huffman@40832
   323
          val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]
huffman@40832
   324
        in map (fn c => pgterm mk_eq c (K tacs)) cons' end
huffman@40832
   325
    end
huffman@35456
   326
huffman@35458
   327
    (* prove distinctness of constructors *)
huffman@35458
   328
    local
huffman@35458
   329
      fun map_dist (f : 'a -> 'a -> 'b) (xs : 'a list) : 'b list =
huffman@40832
   330
        flat (map_index (fn (i, x) => map (f x) (nth_drop i xs)) xs)
huffman@35458
   331
      fun prime (Free (n, T)) = Free (n^"'", T)
huffman@40832
   332
        | prime t             = t
huffman@35458
   333
      fun iff_disj (t, []) = mk_not t
huffman@40832
   334
        | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts)
huffman@35458
   335
      fun iff_disj2 (t, [], us) = mk_not t
huffman@35458
   336
        | iff_disj2 (t, ts, []) = mk_not t
huffman@35458
   337
        | iff_disj2 (t, ts, us) =
huffman@40832
   338
          mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us))
huffman@35458
   339
      fun dist_le (con1, args1) (con2, args2) =
huffman@35458
   340
        let
huffman@40832
   341
          val (vs1, zs1) = get_vars args1
huffman@40832
   342
          val (vs2, zs2) = get_vars args2 |> pairself (map prime)
huffman@40832
   343
          val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
huffman@40832
   344
          val rhss = map mk_undef zs1
huffman@40832
   345
          val goal = mk_trp (iff_disj (lhs, rhss))
huffman@40832
   346
          val rule1 = iso_locale RS @{thm iso.abs_below}
huffman@40832
   347
          val rules = rule1 :: @{thms con_below_iff_rules}
huffman@40832
   348
          val tacs = [simp_tac (HOL_ss addsimps rules) 1]
huffman@40832
   349
        in prove thy con_betas goal (K tacs) end
huffman@35458
   350
      fun dist_eq (con1, args1) (con2, args2) =
huffman@35458
   351
        let
huffman@40832
   352
          val (vs1, zs1) = get_vars args1
huffman@40832
   353
          val (vs2, zs2) = get_vars args2 |> pairself (map prime)
huffman@40832
   354
          val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
huffman@40832
   355
          val rhss1 = map mk_undef zs1
huffman@40832
   356
          val rhss2 = map mk_undef zs2
huffman@40832
   357
          val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2))
huffman@40832
   358
          val rule1 = iso_locale RS @{thm iso.abs_eq}
huffman@40832
   359
          val rules = rule1 :: @{thms con_eq_iff_rules}
huffman@40832
   360
          val tacs = [simp_tac (HOL_ss addsimps rules) 1]
huffman@40832
   361
        in prove thy con_betas goal (K tacs) end
huffman@35458
   362
    in
huffman@40832
   363
      val dist_les = map_dist dist_le spec'
huffman@40832
   364
      val dist_eqs = map_dist dist_eq spec'
huffman@40832
   365
    end
huffman@35456
   366
huffman@35453
   367
    val result =
huffman@35453
   368
      {
huffman@35453
   369
        con_consts = con_consts,
huffman@35453
   370
        con_betas = con_betas,
huffman@35781
   371
        nchotomy = nchotomy,
huffman@35457
   372
        exhaust = exhaust,
huffman@35781
   373
        compacts = compacts,
huffman@35456
   374
        con_rews = con_rews,
huffman@35456
   375
        inverts = inverts,
huffman@35458
   376
        injects = injects,
huffman@35458
   377
        dist_les = dist_les,
huffman@35458
   378
        dist_eqs = dist_eqs
huffman@40832
   379
      }
huffman@35453
   380
  in
huffman@35453
   381
    (result, thy)
huffman@40832
   382
  end
huffman@35453
   383
huffman@35453
   384
(******************************************************************************)
huffman@35459
   385
(**************** definition and theorems for case combinator *****************)
huffman@35459
   386
(******************************************************************************)
huffman@35459
   387
huffman@35459
   388
fun add_case_combinator
huffman@35459
   389
    (spec : (term * (bool * typ) list) list)
huffman@35459
   390
    (lhsT : typ)
huffman@35777
   391
    (dbind : binding)
huffman@35459
   392
    (con_betas : thm list)
huffman@35781
   393
    (exhaust : thm)
huffman@35459
   394
    (iso_locale : thm)
huffman@35486
   395
    (rep_const : term)
huffman@35460
   396
    (thy : theory)
huffman@35460
   397
    : ((typ -> term) * thm list) * theory =
huffman@35459
   398
  let
huffman@35459
   399
huffman@35459
   400
    (* prove rep/abs rules *)
huffman@40832
   401
    val rep_strict = iso_locale RS @{thm iso.rep_strict}
huffman@40832
   402
    val abs_inverse = iso_locale RS @{thm iso.abs_iso}
huffman@35459
   403
huffman@35459
   404
    (* calculate function arguments of case combinator *)
huffman@40832
   405
    val tns = map fst (Term.add_tfreesT lhsT [])
huffman@40832
   406
    val resultT = TFree (Name.variant tns "'t", @{sort pcpo})
huffman@40832
   407
    fun fTs T = map (fn (_, args) => map snd args -->> T) spec
huffman@40832
   408
    val fns = Datatype_Prop.indexify_names (map (K "f") spec)
huffman@40832
   409
    val fs = map Free (fns ~~ fTs resultT)
huffman@40832
   410
    fun caseT T = fTs T -->> (lhsT ->> T)
huffman@35459
   411
huffman@35486
   412
    (* definition of case combinator *)
huffman@35486
   413
    local
huffman@40832
   414
      val case_bind = Binding.suffix_name "_case" dbind
huffman@35784
   415
      fun lambda_arg (lazy, v) t =
huffman@40832
   416
          (if lazy then mk_fup else I) (big_lambda v t)
huffman@40212
   417
      fun lambda_args []      t = mk_one_case t
huffman@35784
   418
        | lambda_args (x::[]) t = lambda_arg x t
huffman@40832
   419
        | lambda_args (x::xs) t = mk_ssplit (lambda_arg x (lambda_args xs t))
huffman@35486
   420
      fun one_con f (_, args) =
huffman@35486
   421
        let
huffman@40832
   422
          val Ts = map snd args
huffman@40832
   423
          val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts)
huffman@40832
   424
          val vs = map Free (ns ~~ Ts)
huffman@35486
   425
        in
huffman@35784
   426
          lambda_args (map fst args ~~ vs) (list_ccomb (f, vs))
huffman@40832
   427
        end
huffman@35785
   428
      fun mk_sscases [t] = mk_strictify t
huffman@40832
   429
        | mk_sscases ts = foldr1 mk_sscase ts
huffman@40832
   430
      val body = mk_sscases (map2 one_con fs spec)
huffman@40832
   431
      val rhs = big_lambdas fs (mk_cfcomp (body, rep_const))
huffman@35486
   432
      val ((case_consts, case_defs), thy) =
huffman@40832
   433
          define_consts [(case_bind, rhs, NoSyn)] thy
huffman@40832
   434
      val case_name = Sign.full_name thy case_bind
huffman@35486
   435
    in
huffman@40832
   436
      val case_def = hd case_defs
huffman@40832
   437
      fun case_const T = Const (case_name, caseT T)
huffman@40832
   438
      val case_app = list_ccomb (case_const resultT, fs)
huffman@40832
   439
      val thy = thy
huffman@40832
   440
    end
huffman@35459
   441
huffman@35472
   442
    (* define syntax for case combinator *)
huffman@35472
   443
    (* TODO: re-implement case syntax using a parse translation *)
huffman@35472
   444
    local
huffman@35472
   445
      open Syntax
huffman@40832
   446
      fun syntax c = Syntax.mark_const (fst (dest_Const c))
huffman@40832
   447
      fun xconst c = Long_Name.base_name (fst (dest_Const c))
huffman@35472
   448
      fun c_ast authentic con =
huffman@40832
   449
          Constant (if authentic then syntax con else xconst con)
huffman@40832
   450
      fun showint n = string_of_int (n+1)
huffman@40832
   451
      fun expvar n = Variable ("e" ^ showint n)
huffman@40832
   452
      fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m)
huffman@40832
   453
      fun argvars n args = map_index (argvar n) args
huffman@40832
   454
      fun app s (l, r) = mk_appl (Constant s) [l, r]
huffman@40832
   455
      val cabs = app "_cabs"
huffman@40832
   456
      val capp = app @{const_syntax Rep_cfun}
huffman@35472
   457
      val capps = Library.foldl capp
huffman@35472
   458
      fun con1 authentic n (con,args) =
huffman@40832
   459
          Library.foldl capp (c_ast authentic con, argvars n args)
huffman@35485
   460
      fun case1 authentic (n, c) =
wenzelm@42057
   461
          app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
huffman@40832
   462
      fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
huffman@35485
   463
      fun when1 n (m, c) =
huffman@41429
   464
          if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
huffman@40832
   465
      val case_constant = Constant (syntax (case_const dummyT))
huffman@35472
   466
      fun case_trans authentic =
wenzelm@42204
   467
          (if authentic then Parse_Print_Rule else Parse_Rule)
huffman@35472
   468
            (app "_case_syntax"
huffman@35472
   469
              (Variable "x",
huffman@35485
   470
               foldr1 (app "_case2") (map_index (case1 authentic) spec)),
huffman@40832
   471
             capp (capps (case_constant, map_index arg1 spec), Variable "x"))
huffman@35485
   472
      fun one_abscon_trans authentic (n, c) =
wenzelm@42204
   473
          (if authentic then Parse_Print_Rule else Parse_Rule)
huffman@35472
   474
            (cabs (con1 authentic n c, expvar n),
huffman@40832
   475
             capps (case_constant, map_index (when1 n) spec))
huffman@35472
   476
      fun abscon_trans authentic =
huffman@40832
   477
          map_index (one_abscon_trans authentic) spec
huffman@35472
   478
      val trans_rules : ast Syntax.trrule list =
huffman@35472
   479
          case_trans false :: case_trans true ::
huffman@40832
   480
          abscon_trans false @ abscon_trans true
huffman@35472
   481
    in
wenzelm@42204
   482
      val thy = Sign.add_trrules trans_rules thy
huffman@40832
   483
    end
huffman@35472
   484
huffman@35459
   485
    (* prove beta reduction rule for case combinator *)
huffman@40832
   486
    val case_beta = beta_of_def thy case_def
huffman@35459
   487
huffman@35459
   488
    (* prove strictness of case combinator *)
huffman@35459
   489
    val case_strict =
huffman@35459
   490
      let
huffman@40832
   491
        val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}]
huffman@40832
   492
        val goal = mk_trp (mk_strict case_app)
huffman@40832
   493
        val rules = @{thms sscase1 ssplit1 strictify1 one_case1}
huffman@40832
   494
        val tacs = [resolve_tac rules 1]
huffman@40832
   495
      in prove thy defs goal (K tacs) end
huffman@35459
   496
        
huffman@35459
   497
    (* prove rewrites for case combinator *)
huffman@35459
   498
    local
huffman@35459
   499
      fun one_case (con, args) f =
huffman@35459
   500
        let
huffman@40832
   501
          val (vs, nonlazy) = get_vars args
huffman@40832
   502
          val assms = map (mk_trp o mk_defined) nonlazy
huffman@40832
   503
          val lhs = case_app ` list_ccomb (con, vs)
huffman@40832
   504
          val rhs = list_ccomb (f, vs)
huffman@40832
   505
          val concl = mk_trp (mk_eq (lhs, rhs))
huffman@40832
   506
          val goal = Logic.list_implies (assms, concl)
huffman@40832
   507
          val defs = case_beta :: con_betas
huffman@40832
   508
          val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1}
huffman@40832
   509
          val rules2 = @{thms con_bottom_iff_rules}
huffman@40832
   510
          val rules3 = @{thms cfcomp2 one_case2}
huffman@40832
   511
          val rules = abs_inverse :: rules1 @ rules2 @ rules3
huffman@40832
   512
          val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]
huffman@40832
   513
        in prove thy defs goal (K tacs) end
huffman@35459
   514
    in
huffman@40832
   515
      val case_apps = map2 one_case spec fs
huffman@35459
   516
    end
huffman@35459
   517
huffman@35459
   518
  in
huffman@35460
   519
    ((case_const, case_strict :: case_apps), thy)
huffman@35459
   520
  end
huffman@35459
   521
huffman@35459
   522
(******************************************************************************)
huffman@35446
   523
(************** definitions and theorems for selector functions ***************)
huffman@35446
   524
(******************************************************************************)
huffman@35446
   525
huffman@35446
   526
fun add_selectors
huffman@35446
   527
    (spec : (term * (bool * binding option * typ) list) list)
huffman@35446
   528
    (rep_const : term)
huffman@35446
   529
    (abs_inv : thm)
huffman@35446
   530
    (rep_strict : thm)
huffman@40321
   531
    (rep_bottom_iff : thm)
huffman@35446
   532
    (con_betas : thm list)
huffman@35446
   533
    (thy : theory)
huffman@35446
   534
    : thm list * theory =
huffman@35446
   535
  let
huffman@35446
   536
huffman@35446
   537
    (* define selector functions *)
huffman@35446
   538
    val ((sel_consts, sel_defs), thy) =
huffman@35446
   539
      let
huffman@40832
   540
        fun rangeT s = snd (dest_cfunT (fastype_of s))
huffman@40832
   541
        fun mk_outl s = mk_cfcomp (from_sinl (dest_ssumT (rangeT s)), s)
huffman@40832
   542
        fun mk_outr s = mk_cfcomp (from_sinr (dest_ssumT (rangeT s)), s)
huffman@40832
   543
        fun mk_sfst s = mk_cfcomp (sfst_const (dest_sprodT (rangeT s)), s)
huffman@40832
   544
        fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s)
huffman@40832
   545
        fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s)
huffman@35446
   546
huffman@35446
   547
        fun sels_of_arg s (lazy, NONE,   T) = []
huffman@35446
   548
          | sels_of_arg s (lazy, SOME b, T) =
huffman@40832
   549
            [(b, if lazy then mk_down s else s, NoSyn)]
huffman@35446
   550
        fun sels_of_args s [] = []
huffman@35446
   551
          | sels_of_args s (v :: []) = sels_of_arg s v
huffman@35446
   552
          | sels_of_args s (v :: vs) =
huffman@40832
   553
            sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs
huffman@35446
   554
        fun sels_of_cons s [] = []
huffman@35446
   555
          | sels_of_cons s ((con, args) :: []) = sels_of_args s args
huffman@35446
   556
          | sels_of_cons s ((con, args) :: cs) =
huffman@40832
   557
            sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs
huffman@35446
   558
        val sel_eqns : (binding * term * mixfix) list =
huffman@40832
   559
            sels_of_cons rep_const spec
huffman@35446
   560
      in
huffman@35446
   561
        define_consts sel_eqns thy
huffman@35446
   562
      end
huffman@35446
   563
huffman@35446
   564
    (* replace bindings with terms in constructor spec *)
huffman@35446
   565
    val spec2 : (term * (bool * term option * typ) list) list =
huffman@35446
   566
      let
huffman@35446
   567
        fun prep_arg (lazy, NONE, T) sels = ((lazy, NONE, T), sels)
huffman@35446
   568
          | prep_arg (lazy, SOME _, T) sels =
huffman@40832
   569
            ((lazy, SOME (hd sels), T), tl sels)
huffman@35446
   570
        fun prep_con (con, args) sels =
huffman@40832
   571
            apfst (pair con) (fold_map prep_arg args sels)
huffman@35446
   572
      in
huffman@35446
   573
        fst (fold_map prep_con spec sel_consts)
huffman@40832
   574
      end
huffman@35446
   575
huffman@35446
   576
    (* prove selector strictness rules *)
huffman@35446
   577
    val sel_stricts : thm list =
huffman@35446
   578
      let
huffman@40832
   579
        val rules = rep_strict :: @{thms sel_strict_rules}
huffman@40832
   580
        val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]
huffman@35446
   581
        fun sel_strict sel =
huffman@35446
   582
          let
huffman@40832
   583
            val goal = mk_trp (mk_strict sel)
huffman@35446
   584
          in
huffman@35449
   585
            prove thy sel_defs goal (K tacs)
huffman@35446
   586
          end
huffman@35446
   587
      in
huffman@35446
   588
        map sel_strict sel_consts
huffman@35446
   589
      end
huffman@35446
   590
huffman@35446
   591
    (* prove selector application rules *)
huffman@35446
   592
    val sel_apps : thm list =
huffman@35446
   593
      let
huffman@40832
   594
        val defs = con_betas @ sel_defs
huffman@40832
   595
        val rules = abs_inv :: @{thms sel_app_rules}
huffman@40832
   596
        val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]
wenzelm@37165
   597
        fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
huffman@35446
   598
          let
huffman@40832
   599
            val Ts : typ list = map #3 args
huffman@40832
   600
            val ns : string list = Datatype_Prop.make_tnames Ts
huffman@40832
   601
            val vs : term list = map Free (ns ~~ Ts)
huffman@40832
   602
            val con_app : term = list_ccomb (con, vs)
huffman@40832
   603
            val vs' : (bool * term) list = map #1 args ~~ vs
huffman@35446
   604
            fun one_same (n, sel, T) =
huffman@35446
   605
              let
huffman@40832
   606
                val xs = map snd (filter_out fst (nth_drop n vs'))
huffman@40832
   607
                val assms = map (mk_trp o mk_defined) xs
huffman@40832
   608
                val concl = mk_trp (mk_eq (sel ` con_app, nth vs n))
huffman@40832
   609
                val goal = Logic.list_implies (assms, concl)
huffman@35446
   610
              in
huffman@35449
   611
                prove thy defs goal (K tacs)
huffman@40832
   612
              end
huffman@35446
   613
            fun one_diff (n, sel, T) =
huffman@35446
   614
              let
huffman@40832
   615
                val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
huffman@35446
   616
              in
huffman@35449
   617
                prove thy defs goal (K tacs)
huffman@40832
   618
              end
huffman@35446
   619
            fun one_con (j, (_, args')) : thm list =
huffman@35446
   620
              let
huffman@35446
   621
                fun prep (i, (lazy, NONE, T)) = NONE
huffman@40832
   622
                  | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T)
huffman@35446
   623
                val sels : (int * term * typ) list =
huffman@40832
   624
                  map_filter prep (map_index I args')
huffman@35446
   625
              in
huffman@35446
   626
                if i = j
huffman@35446
   627
                then map one_same sels
huffman@35446
   628
                else map one_diff sels
huffman@35446
   629
              end
huffman@35446
   630
          in
huffman@35446
   631
            flat (map_index one_con spec2)
huffman@35446
   632
          end
huffman@35446
   633
      in
huffman@35446
   634
        flat (map_index sel_apps_of spec2)
huffman@35446
   635
      end
huffman@35446
   636
huffman@35446
   637
  (* prove selector definedness rules *)
huffman@35446
   638
    val sel_defins : thm list =
huffman@35446
   639
      let
huffman@40832
   640
        val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules}
huffman@40832
   641
        val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]
huffman@35446
   642
        fun sel_defin sel =
huffman@35446
   643
          let
huffman@40832
   644
            val (T, U) = dest_cfunT (fastype_of sel)
huffman@40832
   645
            val x = Free ("x", T)
huffman@40832
   646
            val lhs = mk_eq (sel ` x, mk_bottom U)
huffman@40832
   647
            val rhs = mk_eq (x, mk_bottom T)
huffman@40832
   648
            val goal = mk_trp (mk_eq (lhs, rhs))
huffman@35446
   649
          in
huffman@35449
   650
            prove thy sel_defs goal (K tacs)
huffman@35446
   651
          end
huffman@35446
   652
        fun one_arg (false, SOME sel, T) = SOME (sel_defin sel)
huffman@40832
   653
          | one_arg _                    = NONE
huffman@35446
   654
      in
huffman@35446
   655
        case spec2 of
huffman@35446
   656
          [(con, args)] => map_filter one_arg args
huffman@35446
   657
        | _             => []
huffman@40832
   658
      end
huffman@35446
   659
huffman@35446
   660
  in
huffman@35446
   661
    (sel_stricts @ sel_defins @ sel_apps, thy)
huffman@35446
   662
  end
huffman@35446
   663
huffman@35446
   664
(******************************************************************************)
huffman@35460
   665
(************ definitions and theorems for discriminator functions ************)
huffman@35460
   666
(******************************************************************************)
huffman@35460
   667
huffman@35460
   668
fun add_discriminators
huffman@35460
   669
    (bindings : binding list)
huffman@35460
   670
    (spec : (term * (bool * typ) list) list)
huffman@35461
   671
    (lhsT : typ)
huffman@35781
   672
    (exhaust : thm)
huffman@35460
   673
    (case_const : typ -> term)
huffman@35461
   674
    (case_rews : thm list)
huffman@35460
   675
    (thy : theory) =
huffman@35460
   676
  let
huffman@35460
   677
huffman@35460
   678
    fun vars_of args =
huffman@35460
   679
      let
huffman@40832
   680
        val Ts = map snd args
huffman@40832
   681
        val ns = Datatype_Prop.make_tnames Ts
huffman@35460
   682
      in
huffman@35460
   683
        map Free (ns ~~ Ts)
huffman@40832
   684
      end
huffman@35460
   685
huffman@35460
   686
    (* define discriminator functions *)
huffman@35460
   687
    local
huffman@35460
   688
      fun dis_fun i (j, (con, args)) =
huffman@35460
   689
        let
huffman@40832
   690
          val (vs, nonlazy) = get_vars args
huffman@40832
   691
          val tr = if i = j then @{term TT} else @{term FF}
huffman@35460
   692
        in
huffman@35460
   693
          big_lambdas vs tr
huffman@40832
   694
        end
huffman@35460
   695
      fun dis_eqn (i, bind) : binding * term * mixfix =
huffman@35460
   696
        let
huffman@40832
   697
          val dis_bind = Binding.prefix_name "is_" bind
huffman@40832
   698
          val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec)
huffman@35460
   699
        in
huffman@35460
   700
          (dis_bind, rhs, NoSyn)
huffman@40832
   701
        end
huffman@35460
   702
    in
huffman@35460
   703
      val ((dis_consts, dis_defs), thy) =
huffman@35460
   704
          define_consts (map_index dis_eqn bindings) thy
huffman@40832
   705
    end
huffman@35460
   706
huffman@35461
   707
    (* prove discriminator strictness rules *)
huffman@35461
   708
    local
huffman@35461
   709
      fun dis_strict dis =
huffman@40832
   710
        let val goal = mk_trp (mk_strict dis)
huffman@40832
   711
        in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end
huffman@35461
   712
    in
huffman@40832
   713
      val dis_stricts = map dis_strict dis_consts
huffman@40832
   714
    end
huffman@35461
   715
huffman@35461
   716
    (* prove discriminator/constructor rules *)
huffman@35461
   717
    local
huffman@35461
   718
      fun dis_app (i, dis) (j, (con, args)) =
huffman@35461
   719
        let
huffman@40832
   720
          val (vs, nonlazy) = get_vars args
huffman@40832
   721
          val lhs = dis ` list_ccomb (con, vs)
huffman@40832
   722
          val rhs = if i = j then @{term TT} else @{term FF}
huffman@40832
   723
          val assms = map (mk_trp o mk_defined) nonlazy
huffman@40832
   724
          val concl = mk_trp (mk_eq (lhs, rhs))
huffman@40832
   725
          val goal = Logic.list_implies (assms, concl)
huffman@40832
   726
          val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]
huffman@40832
   727
        in prove thy dis_defs goal (K tacs) end
huffman@35461
   728
      fun one_dis (i, dis) =
huffman@40832
   729
          map_index (dis_app (i, dis)) spec
huffman@35461
   730
    in
huffman@40832
   731
      val dis_apps = flat (map_index one_dis dis_consts)
huffman@40832
   732
    end
huffman@35461
   733
huffman@35461
   734
    (* prove discriminator definedness rules *)
huffman@35461
   735
    local
huffman@35461
   736
      fun dis_defin dis =
huffman@35461
   737
        let
huffman@40832
   738
          val x = Free ("x", lhsT)
huffman@40832
   739
          val simps = dis_apps @ @{thms dist_eq_tr}
huffman@35461
   740
          val tacs =
huffman@35461
   741
            [rtac @{thm iffI} 1,
huffman@35461
   742
             asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2,
huffman@35781
   743
             rtac exhaust 1, atac 1,
huffman@35461
   744
             DETERM_UNTIL_SOLVED (CHANGED
huffman@40832
   745
               (asm_full_simp_tac (simple_ss addsimps simps) 1))]
huffman@40832
   746
          val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x))
huffman@40832
   747
        in prove thy [] goal (K tacs) end
huffman@35461
   748
    in
huffman@40832
   749
      val dis_defins = map dis_defin dis_consts
huffman@40832
   750
    end
huffman@35461
   751
huffman@35460
   752
  in
huffman@35461
   753
    (dis_stricts @ dis_defins @ dis_apps, thy)
huffman@40832
   754
  end
huffman@35460
   755
huffman@35460
   756
(******************************************************************************)
huffman@35462
   757
(*************** definitions and theorems for match combinators ***************)
huffman@35462
   758
(******************************************************************************)
huffman@35462
   759
huffman@35462
   760
fun add_match_combinators
huffman@35462
   761
    (bindings : binding list)
huffman@35462
   762
    (spec : (term * (bool * typ) list) list)
huffman@35462
   763
    (lhsT : typ)
huffman@35781
   764
    (exhaust : thm)
huffman@35462
   765
    (case_const : typ -> term)
huffman@35462
   766
    (case_rews : thm list)
huffman@35462
   767
    (thy : theory) =
huffman@35462
   768
  let
huffman@35462
   769
huffman@35462
   770
    (* get a fresh type variable for the result type *)
huffman@35462
   771
    val resultT : typ =
huffman@35462
   772
      let
huffman@40832
   773
        val ts : string list = map fst (Term.add_tfreesT lhsT [])
huffman@40832
   774
        val t : string = Name.variant ts "'t"
huffman@40832
   775
      in TFree (t, @{sort pcpo}) end
huffman@35462
   776
huffman@35462
   777
    (* define match combinators *)
huffman@35462
   778
    local
huffman@40832
   779
      val x = Free ("x", lhsT)
huffman@40832
   780
      fun k args = Free ("k", map snd args -->> mk_matchT resultT)
huffman@40832
   781
      val fail = mk_fail resultT
huffman@35462
   782
      fun mat_fun i (j, (con, args)) =
huffman@35462
   783
        let
huffman@40832
   784
          val (vs, nonlazy) = get_vars_avoiding ["x","k"] args
huffman@35462
   785
        in
huffman@35462
   786
          if i = j then k args else big_lambdas vs fail
huffman@40832
   787
        end
huffman@35462
   788
      fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
huffman@35462
   789
        let
huffman@40832
   790
          val mat_bind = Binding.prefix_name "match_" bind
huffman@35462
   791
          val funs = map_index (mat_fun i) spec
huffman@40832
   792
          val body = list_ccomb (case_const (mk_matchT resultT), funs)
huffman@40832
   793
          val rhs = big_lambda x (big_lambda (k args) (body ` x))
huffman@35462
   794
        in
huffman@35462
   795
          (mat_bind, rhs, NoSyn)
huffman@40832
   796
        end
huffman@35462
   797
    in
huffman@35462
   798
      val ((match_consts, match_defs), thy) =
huffman@35462
   799
          define_consts (map_index mat_eqn (bindings ~~ spec)) thy
huffman@40832
   800
    end
huffman@35462
   801
huffman@35463
   802
    (* register match combinators with fixrec package *)
huffman@35463
   803
    local
huffman@40832
   804
      val con_names = map (fst o dest_Const o fst) spec
huffman@40832
   805
      val mat_names = map (fst o dest_Const) match_consts
huffman@35463
   806
    in
huffman@40832
   807
      val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy
huffman@40832
   808
    end
huffman@35463
   809
huffman@35466
   810
    (* prove strictness of match combinators *)
huffman@35466
   811
    local
huffman@35466
   812
      fun match_strict mat =
huffman@35466
   813
        let
huffman@40832
   814
          val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat))
huffman@40832
   815
          val k = Free ("k", U)
huffman@40832
   816
          val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V))
huffman@40832
   817
          val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]
huffman@40832
   818
        in prove thy match_defs goal (K tacs) end
huffman@35466
   819
    in
huffman@40832
   820
      val match_stricts = map match_strict match_consts
huffman@40832
   821
    end
huffman@35466
   822
huffman@35466
   823
    (* prove match/constructor rules *)
huffman@35466
   824
    local
huffman@40832
   825
      val fail = mk_fail resultT
huffman@35466
   826
      fun match_app (i, mat) (j, (con, args)) =
huffman@35466
   827
        let
huffman@40832
   828
          val (vs, nonlazy) = get_vars_avoiding ["k"] args
huffman@40832
   829
          val (_, (kT, _)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat))
huffman@40832
   830
          val k = Free ("k", kT)
huffman@40832
   831
          val lhs = mat ` list_ccomb (con, vs) ` k
huffman@40832
   832
          val rhs = if i = j then list_ccomb (k, vs) else fail
huffman@40832
   833
          val assms = map (mk_trp o mk_defined) nonlazy
huffman@40832
   834
          val concl = mk_trp (mk_eq (lhs, rhs))
huffman@40832
   835
          val goal = Logic.list_implies (assms, concl)
huffman@40832
   836
          val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]
huffman@40832
   837
        in prove thy match_defs goal (K tacs) end
huffman@35466
   838
      fun one_match (i, mat) =
huffman@40832
   839
          map_index (match_app (i, mat)) spec
huffman@35466
   840
    in
huffman@40832
   841
      val match_apps = flat (map_index one_match match_consts)
huffman@40832
   842
    end
huffman@35466
   843
huffman@35462
   844
  in
huffman@35462
   845
    (match_stricts @ match_apps, thy)
huffman@40832
   846
  end
huffman@35462
   847
huffman@35462
   848
(******************************************************************************)
huffman@35450
   849
(******************************* main function ********************************)
huffman@35450
   850
(******************************************************************************)
huffman@35450
   851
huffman@35450
   852
fun add_domain_constructors
huffman@35777
   853
    (dbind : binding)
huffman@35481
   854
    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
huffman@35514
   855
    (iso_info : Domain_Take_Proofs.iso_info)
huffman@35450
   856
    (thy : theory) =
huffman@35450
   857
  let
huffman@40832
   858
    val dname = Binding.name_of dbind
huffman@40832
   859
    val _ = writeln ("Proving isomorphism properties of domain "^dname^" ...")
huffman@35450
   860
huffman@40832
   861
    val bindings = map #1 spec
huffman@40019
   862
huffman@35481
   863
    (* retrieve facts about rep/abs *)
huffman@40832
   864
    val lhsT = #absT iso_info
huffman@40832
   865
    val {rep_const, abs_const, ...} = iso_info
huffman@40832
   866
    val abs_iso_thm = #abs_inverse iso_info
huffman@40832
   867
    val rep_iso_thm = #rep_inverse iso_info
huffman@40832
   868
    val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm]
huffman@40832
   869
    val rep_strict = iso_locale RS @{thm iso.rep_strict}
huffman@40832
   870
    val abs_strict = iso_locale RS @{thm iso.abs_strict}
huffman@40832
   871
    val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff}
huffman@40832
   872
    val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff}
huffman@40832
   873
    val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict]
huffman@35450
   874
huffman@35487
   875
    (* qualify constants and theorems with domain name *)
huffman@40832
   876
    val thy = Sign.add_path dname thy
huffman@35487
   877
huffman@35450
   878
    (* define constructor functions *)
huffman@35457
   879
    val (con_result, thy) =
huffman@35454
   880
      let
huffman@40832
   881
        fun prep_arg (lazy, sel, T) = (lazy, T)
huffman@40832
   882
        fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
huffman@40832
   883
        val con_spec = map prep_con spec
huffman@35454
   884
      in
huffman@35454
   885
        add_constructors con_spec abs_const iso_locale thy
huffman@40832
   886
      end
huffman@40016
   887
    val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews,
huffman@40832
   888
          inverts, injects, dist_les, dist_eqs} = con_result
huffman@35459
   889
huffman@40019
   890
    (* prepare constructor spec *)
huffman@40019
   891
    val con_specs : (term * (bool * typ) list) list =
huffman@35459
   892
      let
huffman@40832
   893
        fun prep_arg (lazy, sel, T) = (lazy, T)
huffman@40832
   894
        fun prep_con c (b, args, mx) = (c, map prep_arg args)
huffman@35459
   895
      in
huffman@40019
   896
        map2 prep_con con_consts spec
huffman@40832
   897
      end
huffman@40019
   898
huffman@40019
   899
    (* define case combinator *)
huffman@40019
   900
    val ((case_const : typ -> term, cases : thm list), thy) =
huffman@40019
   901
        add_case_combinator con_specs lhsT dbind
huffman@35781
   902
          con_betas exhaust iso_locale rep_const thy
huffman@35450
   903
huffman@35446
   904
    (* define and prove theorems for selector functions *)
huffman@35446
   905
    val (sel_thms : thm list, thy : theory) =
huffman@35460
   906
      let
huffman@35460
   907
        val sel_spec : (term * (bool * binding option * typ) list) list =
huffman@40832
   908
          map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec
huffman@35460
   909
      in
huffman@35460
   910
        add_selectors sel_spec rep_const
huffman@40321
   911
          abs_iso_thm rep_strict rep_bottom_iff con_betas thy
huffman@40832
   912
      end
huffman@35460
   913
huffman@35460
   914
    (* define and prove theorems for discriminator functions *)
huffman@35460
   915
    val (dis_thms : thm list, thy : theory) =
huffman@40019
   916
        add_discriminators bindings con_specs lhsT
huffman@40832
   917
          exhaust case_const cases thy
huffman@35446
   918
huffman@35462
   919
    (* define and prove theorems for match combinators *)
huffman@35462
   920
    val (match_thms : thm list, thy : theory) =
huffman@40019
   921
        add_match_combinators bindings con_specs lhsT
huffman@40832
   922
          exhaust case_const cases thy
huffman@35462
   923
huffman@35446
   924
    (* restore original signature path *)
huffman@40832
   925
    val thy = Sign.parent_path thy
huffman@35444
   926
huffman@40016
   927
    (* bind theorem names in global theory *)
huffman@40016
   928
    val (_, thy) =
huffman@40016
   929
      let
huffman@40832
   930
        fun qualified name = Binding.qualified true name dbind
huffman@40832
   931
        val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec
huffman@40832
   932
        val dname = fst (dest_Type lhsT)
huffman@40832
   933
        val simp = Simplifier.simp_add
huffman@40832
   934
        val case_names = Rule_Cases.case_names names
huffman@40832
   935
        val cases_type = Induct.cases_type dname
huffman@40016
   936
      in
huffman@40016
   937
        Global_Theory.add_thmss [
huffman@40016
   938
          ((qualified "iso_rews"  , iso_rews    ), [simp]),
huffman@40016
   939
          ((qualified "nchotomy"  , [nchotomy]  ), []),
huffman@40016
   940
          ((qualified "exhaust"   , [exhaust]   ), [case_names, cases_type]),
huffman@40213
   941
          ((qualified "case_rews" , cases       ), [simp]),
huffman@40016
   942
          ((qualified "compacts"  , compacts    ), [simp]),
huffman@40016
   943
          ((qualified "con_rews"  , con_rews    ), [simp]),
huffman@40016
   944
          ((qualified "sel_rews"  , sel_thms    ), [simp]),
huffman@40016
   945
          ((qualified "dis_rews"  , dis_thms    ), [simp]),
huffman@40016
   946
          ((qualified "dist_les"  , dist_les    ), [simp]),
huffman@40016
   947
          ((qualified "dist_eqs"  , dist_eqs    ), [simp]),
huffman@40016
   948
          ((qualified "inverts"   , inverts     ), [simp]),
huffman@40016
   949
          ((qualified "injects"   , injects     ), [simp]),
huffman@40016
   950
          ((qualified "match_rews", match_thms  ), [simp])] thy
huffman@40832
   951
      end
huffman@40016
   952
huffman@35444
   953
    val result =
huffman@40017
   954
      {
huffman@40017
   955
        iso_info = iso_info,
huffman@40019
   956
        con_specs = con_specs,
huffman@35451
   957
        con_betas = con_betas,
huffman@40016
   958
        nchotomy = nchotomy,
huffman@35781
   959
        exhaust = exhaust,
huffman@40016
   960
        compacts = compacts,
huffman@40016
   961
        con_rews = con_rews,
huffman@40016
   962
        inverts = inverts,
huffman@40016
   963
        injects = injects,
huffman@40016
   964
        dist_les = dist_les,
huffman@40016
   965
        dist_eqs = dist_eqs,
huffman@35459
   966
        cases = cases,
huffman@35460
   967
        sel_rews = sel_thms,
huffman@35462
   968
        dis_rews = dis_thms,
huffman@40017
   969
        match_rews = match_thms
huffman@40832
   970
      }
huffman@35444
   971
  in
huffman@35444
   972
    (result, thy)
huffman@40832
   973
  end
huffman@35444
   974
huffman@40832
   975
end