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