src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
author wenzelm
Sat Aug 16 16:18:39 2014 +0200 (2014-08-16)
changeset 57954 c52223cd1003
parent 57945 cacb00a569e0
child 59498 50b60f501b05
permissions -rw-r--r--
clarified order of rules for match_tac/resolve_tac;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
huffman@35514
     2
    Author:     Brian Huffman
huffman@35514
     3
huffman@35514
     4
Defines take functions for the given domain equation
huffman@35514
     5
and proves related theorems.
huffman@35514
     6
*)
huffman@35514
     7
huffman@35514
     8
signature DOMAIN_TAKE_PROOFS =
huffman@35514
     9
sig
huffman@35514
    10
  type iso_info =
huffman@35514
    11
    {
huffman@35514
    12
      absT : typ,
huffman@35514
    13
      repT : typ,
huffman@35514
    14
      abs_const : term,
huffman@35514
    15
      rep_const : term,
huffman@35514
    16
      abs_inverse : thm,
huffman@35514
    17
      rep_inverse : thm
huffman@35514
    18
    }
huffman@35651
    19
  type take_info =
huffman@35659
    20
    {
huffman@35659
    21
      take_consts : term list,
huffman@35514
    22
      take_defs : thm list,
huffman@35514
    23
      chain_take_thms : thm list,
huffman@35514
    24
      take_0_thms : thm list,
huffman@35514
    25
      take_Suc_thms : thm list,
huffman@35515
    26
      deflation_take_thms : thm list,
huffman@40015
    27
      take_strict_thms : thm list,
huffman@35515
    28
      finite_consts : term list,
huffman@35515
    29
      finite_defs : thm list
huffman@35651
    30
    }
huffman@35656
    31
  type take_induct_info =
huffman@35656
    32
    {
huffman@35659
    33
      take_consts         : term list,
huffman@35659
    34
      take_defs           : thm list,
huffman@35659
    35
      chain_take_thms     : thm list,
huffman@35659
    36
      take_0_thms         : thm list,
huffman@35659
    37
      take_Suc_thms       : thm list,
huffman@35659
    38
      deflation_take_thms : thm list,
huffman@40015
    39
      take_strict_thms    : thm list,
huffman@35659
    40
      finite_consts       : term list,
huffman@35659
    41
      finite_defs         : thm list,
huffman@35659
    42
      lub_take_thms       : thm list,
huffman@35659
    43
      reach_thms          : thm list,
huffman@35659
    44
      take_lemma_thms     : thm list,
huffman@35659
    45
      is_finite           : bool,
huffman@35659
    46
      take_induct_thms    : thm list
huffman@35656
    47
    }
huffman@35651
    48
  val define_take_functions :
huffman@35651
    49
    (binding * iso_info) list -> theory -> take_info * theory
huffman@35514
    50
huffman@35654
    51
  val add_lub_take_theorems :
huffman@35654
    52
    (binding * iso_info) list -> take_info -> thm list ->
huffman@35656
    53
    theory -> take_induct_info * theory
huffman@35654
    54
huffman@35514
    55
  val map_of_typ :
huffman@35514
    56
    theory -> (typ * term) list -> typ -> term
huffman@35514
    57
huffman@40737
    58
  val add_rec_type : (string * bool list) -> theory -> theory
huffman@40737
    59
  val get_rec_tab : theory -> (bool list) Symtab.table
huffman@40216
    60
  val add_deflation_thm : thm -> theory -> theory
huffman@35514
    61
  val get_deflation_thms : theory -> thm list
huffman@40489
    62
  val map_ID_add : attribute
huffman@40489
    63
  val get_map_ID_thms : theory -> thm list
huffman@40832
    64
end
huffman@35514
    65
huffman@35514
    66
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
huffman@35514
    67
struct
huffman@35514
    68
huffman@35514
    69
type iso_info =
huffman@35514
    70
  {
huffman@35514
    71
    absT : typ,
huffman@35514
    72
    repT : typ,
huffman@35514
    73
    abs_const : term,
huffman@35514
    74
    rep_const : term,
huffman@35514
    75
    abs_inverse : thm,
huffman@35514
    76
    rep_inverse : thm
huffman@40832
    77
  }
huffman@35514
    78
huffman@35651
    79
type take_info =
huffman@35651
    80
  { take_consts : term list,
huffman@35651
    81
    take_defs : thm list,
huffman@35651
    82
    chain_take_thms : thm list,
huffman@35651
    83
    take_0_thms : thm list,
huffman@35651
    84
    take_Suc_thms : thm list,
huffman@35651
    85
    deflation_take_thms : thm list,
huffman@40015
    86
    take_strict_thms : thm list,
huffman@35651
    87
    finite_consts : term list,
huffman@35651
    88
    finite_defs : thm list
huffman@40832
    89
  }
huffman@35651
    90
huffman@35656
    91
type take_induct_info =
huffman@35656
    92
  {
huffman@35659
    93
    take_consts         : term list,
huffman@35659
    94
    take_defs           : thm list,
huffman@35659
    95
    chain_take_thms     : thm list,
huffman@35659
    96
    take_0_thms         : thm list,
huffman@35659
    97
    take_Suc_thms       : thm list,
huffman@35659
    98
    deflation_take_thms : thm list,
huffman@40015
    99
    take_strict_thms    : thm list,
huffman@35659
   100
    finite_consts       : term list,
huffman@35659
   101
    finite_defs         : thm list,
huffman@35659
   102
    lub_take_thms       : thm list,
huffman@35659
   103
    reach_thms          : thm list,
huffman@35659
   104
    take_lemma_thms     : thm list,
huffman@35659
   105
    is_finite           : bool,
huffman@35659
   106
    take_induct_thms    : thm list
huffman@40832
   107
  }
huffman@35656
   108
huffman@40833
   109
val beta_ss =
wenzelm@51717
   110
  simpset_of (put_simpset HOL_basic_ss @{context}
wenzelm@51717
   111
    addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}])
huffman@35514
   112
huffman@35514
   113
(******************************************************************************)
huffman@35514
   114
(******************************** theory data *********************************)
huffman@35514
   115
(******************************************************************************)
huffman@35514
   116
huffman@40737
   117
structure Rec_Data = Theory_Data
huffman@35514
   118
(
huffman@40737
   119
  (* list indicates which type arguments allow indirect recursion *)
huffman@40832
   120
  type T = (bool list) Symtab.table
huffman@40832
   121
  val empty = Symtab.empty
huffman@40832
   122
  val extend = I
huffman@40832
   123
  fun merge data = Symtab.merge (K true) data
huffman@40832
   124
)
huffman@35514
   125
huffman@40737
   126
fun add_rec_type (tname, bs) =
huffman@40832
   127
    Rec_Data.map (Symtab.insert (K true) (tname, bs))
huffman@40216
   128
huffman@40216
   129
fun add_deflation_thm thm =
wenzelm@57945
   130
    Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm)
huffman@35514
   131
huffman@40832
   132
val get_rec_tab = Rec_Data.get
wenzelm@57945
   133
fun get_deflation_thms thy =
wenzelm@57954
   134
  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation})
huffman@40216
   135
wenzelm@57945
   136
val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
wenzelm@57945
   137
fun get_map_ID_thms thy =
wenzelm@57954
   138
  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID})
huffman@40489
   139
huffman@35514
   140
huffman@35514
   141
(******************************************************************************)
huffman@35514
   142
(************************** building types and terms **************************)
huffman@35514
   143
(******************************************************************************)
huffman@35514
   144
huffman@40832
   145
open HOLCF_Library
huffman@35514
   146
huffman@40832
   147
infixr 6 ->>
huffman@40832
   148
infix -->>
huffman@40832
   149
infix 9 `
huffman@35514
   150
huffman@35514
   151
fun mk_deflation t =
huffman@40832
   152
  Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
huffman@35514
   153
huffman@40832
   154
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
huffman@35514
   155
huffman@35514
   156
(******************************************************************************)
huffman@35514
   157
(****************************** isomorphism info ******************************)
huffman@35514
   158
(******************************************************************************)
huffman@35514
   159
huffman@35514
   160
fun deflation_abs_rep (info : iso_info) : thm =
huffman@35514
   161
  let
huffman@40832
   162
    val abs_iso = #abs_inverse info
huffman@40832
   163
    val rep_iso = #rep_inverse info
huffman@40832
   164
    val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]
huffman@35514
   165
  in
huffman@36241
   166
    Drule.zero_var_indexes thm
huffman@35514
   167
  end
huffman@35514
   168
huffman@35514
   169
(******************************************************************************)
huffman@35514
   170
(********************* building map functions over types **********************)
huffman@35514
   171
(******************************************************************************)
huffman@35514
   172
huffman@35514
   173
fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
huffman@35514
   174
  let
huffman@40832
   175
    val thms = get_map_ID_thms thy
huffman@40832
   176
    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms
huffman@40832
   177
    val rules' = map (apfst mk_ID) sub @ map swap rules
huffman@35514
   178
  in
huffman@40489
   179
    mk_ID T
huffman@40489
   180
    |> Pattern.rewrite_term thy rules' []
huffman@40489
   181
    |> Pattern.rewrite_term thy rules []
huffman@40832
   182
  end
huffman@35514
   183
huffman@35514
   184
(******************************************************************************)
huffman@35514
   185
(********************* declaring definitions and theorems *********************)
huffman@35514
   186
(******************************************************************************)
huffman@35514
   187
huffman@35773
   188
fun add_qualified_def name (dbind, eqn) =
wenzelm@39557
   189
    yield_singleton (Global_Theory.add_defs false)
huffman@40832
   190
     ((Binding.qualified true name dbind, eqn), [])
huffman@35514
   191
huffman@35773
   192
fun add_qualified_thm name (dbind, thm) =
wenzelm@39557
   193
    yield_singleton Global_Theory.add_thms
huffman@40832
   194
      ((Binding.qualified true name dbind, thm), [])
huffman@35650
   195
huffman@35773
   196
fun add_qualified_simp_thm name (dbind, thm) =
wenzelm@39557
   197
    yield_singleton Global_Theory.add_thms
huffman@40832
   198
      ((Binding.qualified true name dbind, thm), [Simplifier.simp_add])
huffman@35573
   199
huffman@35514
   200
(******************************************************************************)
huffman@35514
   201
(************************** defining take functions ***************************)
huffman@35514
   202
(******************************************************************************)
huffman@35514
   203
huffman@35514
   204
fun define_take_functions
huffman@35514
   205
    (spec : (binding * iso_info) list)
huffman@35514
   206
    (thy : theory) =
huffman@35514
   207
  let
huffman@35514
   208
huffman@35514
   209
    (* retrieve components of spec *)
huffman@40832
   210
    val dbinds = map fst spec
huffman@40832
   211
    val iso_infos = map snd spec
huffman@40832
   212
    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos
huffman@40832
   213
    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos
huffman@35514
   214
huffman@44080
   215
    fun mk_projs []      _ = []
huffman@35514
   216
      | mk_projs (x::[]) t = [(x, t)]
huffman@40832
   217
      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
huffman@35514
   218
huffman@35514
   219
    fun mk_cfcomp2 ((rep_const, abs_const), f) =
huffman@40832
   220
        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const))
huffman@35514
   221
huffman@35514
   222
    (* define take functional *)
huffman@40832
   223
    val newTs : typ list = map fst dom_eqns
huffman@40832
   224
    val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs)
huffman@40832
   225
    val copy_arg = Free ("f", copy_arg_type)
huffman@40832
   226
    val copy_args = map snd (mk_projs dbinds copy_arg)
huffman@44080
   227
    fun one_copy_rhs (rep_abs, (_, rhsT)) =
huffman@35514
   228
      let
huffman@40832
   229
        val body = map_of_typ thy (newTs ~~ copy_args) rhsT
huffman@35514
   230
      in
huffman@35514
   231
        mk_cfcomp2 (rep_abs, body)
huffman@40832
   232
      end
huffman@35514
   233
    val take_functional =
huffman@35514
   234
        big_lambda copy_arg
huffman@40832
   235
          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)))
huffman@35514
   236
    val take_rhss =
huffman@35514
   237
      let
huffman@40832
   238
        val n = Free ("n", HOLogic.natT)
huffman@40832
   239
        val rhs = mk_iterate (n, take_functional)
huffman@35514
   240
      in
huffman@35773
   241
        map (lambda n o snd) (mk_projs dbinds rhs)
huffman@40832
   242
      end
huffman@35514
   243
huffman@35514
   244
    (* define take constants *)
huffman@44080
   245
    fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy =
huffman@35514
   246
      let
huffman@40832
   247
        val take_type = HOLogic.natT --> lhsT ->> lhsT
huffman@40832
   248
        val take_bind = Binding.suffix_name "_take" dbind
huffman@35514
   249
        val (take_const, thy) =
wenzelm@42375
   250
          Sign.declare_const_global ((take_bind, take_type), NoSyn) thy
huffman@40832
   251
        val take_eqn = Logic.mk_equals (take_const, take_rhs)
huffman@35514
   252
        val (take_def_thm, thy) =
huffman@40832
   253
            add_qualified_def "take_def" (dbind, take_eqn) thy
huffman@40832
   254
      in ((take_const, take_def_thm), thy) end
huffman@35514
   255
    val ((take_consts, take_defs), thy) = thy
huffman@35773
   256
      |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns)
huffman@40832
   257
      |>> ListPair.unzip
huffman@35514
   258
huffman@35514
   259
    (* prove chain_take lemmas *)
huffman@35773
   260
    fun prove_chain_take (take_const, dbind) thy =
huffman@35514
   261
      let
huffman@40832
   262
        val goal = mk_trp (mk_chain take_const)
huffman@40832
   263
        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}
wenzelm@54895
   264
        fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
wenzelm@54895
   265
        val thm = Goal.prove_global thy [] [] goal (tac o #context)
huffman@35514
   266
      in
huffman@35773
   267
        add_qualified_simp_thm "chain_take" (dbind, thm) thy
huffman@40832
   268
      end
huffman@35514
   269
    val (chain_take_thms, thy) =
huffman@40832
   270
      fold_map prove_chain_take (take_consts ~~ dbinds) thy
huffman@35514
   271
huffman@35514
   272
    (* prove take_0 lemmas *)
huffman@44080
   273
    fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy =
huffman@35514
   274
      let
huffman@40832
   275
        val lhs = take_const $ @{term "0::nat"}
huffman@40832
   276
        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
huffman@40832
   277
        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}
wenzelm@54895
   278
        fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
wenzelm@54895
   279
        val take_0_thm = Goal.prove_global thy [] [] goal (tac o #context)
huffman@35514
   280
      in
huffman@40016
   281
        add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy
huffman@40832
   282
      end
huffman@35514
   283
    val (take_0_thms, thy) =
huffman@40832
   284
      fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy
huffman@35514
   285
huffman@35514
   286
    (* prove take_Suc lemmas *)
huffman@40832
   287
    val n = Free ("n", natT)
huffman@40832
   288
    val take_is = map (fn t => t $ n) take_consts
huffman@35514
   289
    fun prove_take_Suc
huffman@44080
   290
          (((take_const, rep_abs), dbind), (_, rhsT)) thy =
huffman@35514
   291
      let
huffman@40832
   292
        val lhs = take_const $ (@{term Suc} $ n)
huffman@40832
   293
        val body = map_of_typ thy (newTs ~~ take_is) rhsT
huffman@40832
   294
        val rhs = mk_cfcomp2 (rep_abs, body)
huffman@40832
   295
        val goal = mk_eqs (lhs, rhs)
huffman@35514
   296
        val simps = @{thms iterate_Suc fst_conv snd_conv}
huffman@40832
   297
        val rules = take_defs @ simps
wenzelm@54895
   298
        fun tac ctxt = simp_tac (put_simpset beta_ss ctxt addsimps rules) 1
wenzelm@54895
   299
        val take_Suc_thm = Goal.prove_global thy [] [] goal (tac o #context)
huffman@35514
   300
      in
huffman@35773
   301
        add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy
huffman@40832
   302
      end
huffman@35514
   303
    val (take_Suc_thms, thy) =
huffman@35514
   304
      fold_map prove_take_Suc
huffman@40832
   305
        (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy
huffman@35514
   306
huffman@35514
   307
    (* prove deflation theorems for take functions *)
huffman@40832
   308
    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos
huffman@35514
   309
    val deflation_take_thm =
huffman@35514
   310
      let
huffman@40832
   311
        val n = Free ("n", natT)
huffman@40832
   312
        fun mk_goal take_const = mk_deflation (take_const $ n)
huffman@40832
   313
        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts))
huffman@35514
   314
        val bottom_rules =
huffman@41430
   315
          take_0_thms @ @{thms deflation_bottom simp_thms}
huffman@35514
   316
        val deflation_rules =
huffman@35514
   317
          @{thms conjI deflation_ID}
huffman@35514
   318
          @ deflation_abs_rep_thms
huffman@40832
   319
          @ get_deflation_thms thy
huffman@35514
   320
      in
wenzelm@54895
   321
        Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} =>
huffman@35514
   322
         EVERY
huffman@35514
   323
          [rtac @{thm nat.induct} 1,
wenzelm@54895
   324
           simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
wenzelm@54895
   325
           asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1,
huffman@35514
   326
           REPEAT (etac @{thm conjE} 1
huffman@35514
   327
                   ORELSE resolve_tac deflation_rules 1
huffman@35514
   328
                   ORELSE atac 1)])
huffman@40832
   329
      end
huffman@44080
   330
    fun conjuncts [] _ = []
huffman@35514
   331
      | conjuncts (n::[]) thm = [(n, thm)]
huffman@35514
   332
      | conjuncts (n::ns) thm = let
huffman@40832
   333
          val thmL = thm RS @{thm conjunct1}
huffman@40832
   334
          val thmR = thm RS @{thm conjunct2}
huffman@40832
   335
        in (n, thmL):: conjuncts ns thmR end
huffman@35514
   336
    val (deflation_take_thms, thy) =
huffman@35514
   337
      fold_map (add_qualified_thm "deflation_take")
huffman@36241
   338
        (map (apsnd Drule.zero_var_indexes)
huffman@40832
   339
          (conjuncts dbinds deflation_take_thm)) thy
huffman@35514
   340
huffman@35514
   341
    (* prove strictness of take functions *)
huffman@35773
   342
    fun prove_take_strict (deflation_take, dbind) thy =
huffman@35514
   343
      let
huffman@35572
   344
        val take_strict_thm =
huffman@36241
   345
            Drule.zero_var_indexes
huffman@40832
   346
              (@{thm deflation_strict} OF [deflation_take])
huffman@35514
   347
      in
huffman@40016
   348
        add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy
huffman@40832
   349
      end
huffman@35514
   350
    val (take_strict_thms, thy) =
huffman@35572
   351
      fold_map prove_take_strict
huffman@40832
   352
        (deflation_take_thms ~~ dbinds) thy
huffman@35514
   353
huffman@35514
   354
    (* prove take/take rules *)
huffman@35773
   355
    fun prove_take_take ((chain_take, deflation_take), dbind) thy =
huffman@35514
   356
      let
huffman@35514
   357
        val take_take_thm =
huffman@36241
   358
            Drule.zero_var_indexes
huffman@40832
   359
              (@{thm deflation_chain_min} OF [chain_take, deflation_take])
huffman@35514
   360
      in
huffman@35773
   361
        add_qualified_thm "take_take" (dbind, take_take_thm) thy
huffman@40832
   362
      end
huffman@44080
   363
    val (_, thy) =
huffman@35514
   364
      fold_map prove_take_take
huffman@40832
   365
        (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy
huffman@35514
   366
huffman@35572
   367
    (* prove take_below rules *)
huffman@35773
   368
    fun prove_take_below (deflation_take, dbind) thy =
huffman@35572
   369
      let
huffman@35572
   370
        val take_below_thm =
huffman@36241
   371
            Drule.zero_var_indexes
huffman@40832
   372
              (@{thm deflation.below} OF [deflation_take])
huffman@35572
   373
      in
huffman@35773
   374
        add_qualified_thm "take_below" (dbind, take_below_thm) thy
huffman@40832
   375
      end
huffman@44080
   376
    val (_, thy) =
huffman@35572
   377
      fold_map prove_take_below
huffman@40832
   378
        (deflation_take_thms ~~ dbinds) thy
huffman@35572
   379
huffman@35515
   380
    (* define finiteness predicates *)
huffman@44080
   381
    fun define_finite_const ((dbind, take_const), (lhsT, _)) thy =
huffman@35515
   382
      let
huffman@40832
   383
        val finite_type = lhsT --> boolT
huffman@40832
   384
        val finite_bind = Binding.suffix_name "_finite" dbind
huffman@35515
   385
        val (finite_const, thy) =
wenzelm@42375
   386
          Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy
huffman@40832
   387
        val x = Free ("x", lhsT)
huffman@40832
   388
        val n = Free ("n", natT)
huffman@35515
   389
        val finite_rhs =
huffman@35515
   390
          lambda x (HOLogic.exists_const natT $
huffman@40832
   391
            (lambda n (mk_eq (mk_capply (take_const $ n, x), x))))
huffman@40832
   392
        val finite_eqn = Logic.mk_equals (finite_const, finite_rhs)
huffman@35515
   393
        val (finite_def_thm, thy) =
huffman@40832
   394
            add_qualified_def "finite_def" (dbind, finite_eqn) thy
huffman@40832
   395
      in ((finite_const, finite_def_thm), thy) end
huffman@35515
   396
    val ((finite_consts, finite_defs), thy) = thy
huffman@35773
   397
      |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns)
huffman@40832
   398
      |>> ListPair.unzip
huffman@35515
   399
huffman@35514
   400
    val result =
huffman@35514
   401
      {
huffman@35514
   402
        take_consts = take_consts,
huffman@35514
   403
        take_defs = take_defs,
huffman@35514
   404
        chain_take_thms = chain_take_thms,
huffman@35514
   405
        take_0_thms = take_0_thms,
huffman@35514
   406
        take_Suc_thms = take_Suc_thms,
huffman@35515
   407
        deflation_take_thms = deflation_take_thms,
huffman@40015
   408
        take_strict_thms = take_strict_thms,
huffman@35515
   409
        finite_consts = finite_consts,
huffman@35515
   410
        finite_defs = finite_defs
huffman@40832
   411
      }
huffman@35514
   412
huffman@35514
   413
  in
huffman@35514
   414
    (result, thy)
huffman@40832
   415
  end
huffman@35514
   416
huffman@35655
   417
fun prove_finite_take_induct
huffman@35655
   418
    (spec : (binding * iso_info) list)
huffman@35655
   419
    (take_info : take_info)
huffman@35655
   420
    (lub_take_thms : thm list)
huffman@35655
   421
    (thy : theory) =
huffman@35655
   422
  let
huffman@40832
   423
    val dbinds = map fst spec
huffman@40832
   424
    val iso_infos = map snd spec
huffman@40832
   425
    val absTs = map #absT iso_infos
huffman@40832
   426
    val {take_consts, ...} = take_info
huffman@40832
   427
    val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info
huffman@40832
   428
    val {finite_consts, finite_defs, ...} = take_info
huffman@35655
   429
huffman@35655
   430
    val decisive_lemma =
huffman@35655
   431
      let
wenzelm@37165
   432
        fun iso_locale (info : iso_info) =
huffman@40832
   433
            @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info]
huffman@40832
   434
        val iso_locale_thms = map iso_locale iso_infos
huffman@35655
   435
        val decisive_abs_rep_thms =
huffman@40832
   436
            map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms
huffman@40832
   437
        val n = Free ("n", @{typ nat})
huffman@35655
   438
        fun mk_decisive t =
huffman@40832
   439
            Const (@{const_name decisive}, fastype_of t --> boolT) $ t
huffman@40832
   440
        fun f take_const = mk_decisive (take_const $ n)
huffman@40832
   441
        val goal = mk_trp (foldr1 mk_conj (map f take_consts))
huffman@40832
   442
        val rules0 = @{thm decisive_bottom} :: take_0_thms
huffman@35655
   443
        val rules1 =
huffman@35655
   444
            take_Suc_thms @ decisive_abs_rep_thms
huffman@40832
   445
            @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}
wenzelm@54895
   446
        fun tac ctxt = EVERY [
huffman@35655
   447
            rtac @{thm nat.induct} 1,
wenzelm@54895
   448
            simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1,
wenzelm@54895
   449
            asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1]
wenzelm@54895
   450
      in Goal.prove_global thy [] [] goal (tac o #context) end
huffman@35655
   451
    fun conjuncts 1 thm = [thm]
huffman@35655
   452
      | conjuncts n thm = let
huffman@40832
   453
          val thmL = thm RS @{thm conjunct1}
huffman@40832
   454
          val thmR = thm RS @{thm conjunct2}
huffman@40832
   455
        in thmL :: conjuncts (n-1) thmR end
huffman@40832
   456
    val decisive_thms = conjuncts (length spec) decisive_lemma
huffman@35655
   457
huffman@35655
   458
    fun prove_finite_thm (absT, finite_const) =
huffman@35655
   459
      let
huffman@40832
   460
        val goal = mk_trp (finite_const $ Free ("x", absT))
wenzelm@54742
   461
        fun tac ctxt =
huffman@35655
   462
            EVERY [
wenzelm@54742
   463
            rewrite_goals_tac ctxt finite_defs,
huffman@35655
   464
            rtac @{thm lub_ID_finite} 1,
huffman@35655
   465
            resolve_tac chain_take_thms 1,
huffman@35655
   466
            resolve_tac lub_take_thms 1,
huffman@40832
   467
            resolve_tac decisive_thms 1]
huffman@35655
   468
      in
wenzelm@54742
   469
        Goal.prove_global thy [] [] goal (tac o #context)
huffman@40832
   470
      end
huffman@35655
   471
    val finite_thms =
huffman@40832
   472
        map prove_finite_thm (absTs ~~ finite_consts)
huffman@35655
   473
huffman@35655
   474
    fun prove_take_induct ((ch_take, lub_take), decisive) =
huffman@35655
   475
        Drule.export_without_context
huffman@40832
   476
          (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive])
huffman@35655
   477
    val take_induct_thms =
huffman@35655
   478
        map prove_take_induct
huffman@40832
   479
          (chain_take_thms ~~ lub_take_thms ~~ decisive_thms)
huffman@35655
   480
huffman@35655
   481
    val thy = thy
huffman@35655
   482
        |> fold (snd oo add_qualified_thm "finite")
huffman@35773
   483
            (dbinds ~~ finite_thms)
huffman@35655
   484
        |> fold (snd oo add_qualified_thm "take_induct")
huffman@40832
   485
            (dbinds ~~ take_induct_thms)
huffman@35655
   486
  in
huffman@35655
   487
    ((finite_thms, take_induct_thms), thy)
huffman@40832
   488
  end
huffman@35655
   489
huffman@35654
   490
fun add_lub_take_theorems
huffman@35654
   491
    (spec : (binding * iso_info) list)
huffman@35654
   492
    (take_info : take_info)
huffman@35654
   493
    (lub_take_thms : thm list)
huffman@35654
   494
    (thy : theory) =
huffman@35654
   495
  let
huffman@35654
   496
huffman@35654
   497
    (* retrieve components of spec *)
huffman@40832
   498
    val dbinds = map fst spec
huffman@40832
   499
    val iso_infos = map snd spec
huffman@40832
   500
    val absTs = map #absT iso_infos
huffman@40832
   501
    val repTs = map #repT iso_infos
huffman@44080
   502
    val {chain_take_thms, ...} = take_info
huffman@35654
   503
huffman@35654
   504
    (* prove take lemmas *)
huffman@35773
   505
    fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
huffman@35654
   506
      let
huffman@35654
   507
        val take_lemma =
huffman@35654
   508
            Drule.export_without_context
huffman@40832
   509
              (@{thm lub_ID_take_lemma} OF [chain_take, lub_take])
huffman@35654
   510
      in
huffman@35773
   511
        add_qualified_thm "take_lemma" (dbind, take_lemma) thy
huffman@40832
   512
      end
huffman@35654
   513
    val (take_lemma_thms, thy) =
huffman@35654
   514
      fold_map prove_take_lemma
huffman@40832
   515
        (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy
huffman@35654
   516
huffman@35654
   517
    (* prove reach lemmas *)
huffman@35773
   518
    fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
huffman@35654
   519
      let
huffman@35654
   520
        val thm =
huffman@36241
   521
            Drule.zero_var_indexes
huffman@40832
   522
              (@{thm lub_ID_reach} OF [chain_take, lub_take])
huffman@35654
   523
      in
huffman@35773
   524
        add_qualified_thm "reach" (dbind, thm) thy
huffman@40832
   525
      end
huffman@35654
   526
    val (reach_thms, thy) =
huffman@35654
   527
      fold_map prove_reach_lemma
huffman@40832
   528
        (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy
huffman@35654
   529
huffman@35655
   530
    (* test for finiteness of domain definitions *)
huffman@35655
   531
    local
huffman@40832
   532
      val types = [@{type_name ssum}, @{type_name sprod}]
haftmann@36692
   533
      fun finite d T = if member (op =) absTs T then d else finite' d T
huffman@35655
   534
      and finite' d (Type (c, Ts)) =
huffman@40832
   535
          let val d' = d andalso member (op =) types c
huffman@35655
   536
          in forall (finite d') Ts end
huffman@44080
   537
        | finite' _ _ = true
huffman@35655
   538
    in
huffman@40832
   539
      val is_finite = forall (finite true) repTs
huffman@40832
   540
    end
huffman@35654
   541
huffman@44080
   542
    val ((_, take_induct_thms), thy) =
huffman@35655
   543
      if is_finite
huffman@35655
   544
      then
huffman@35655
   545
        let
huffman@35655
   546
          val ((finites, take_inducts), thy) =
huffman@40832
   547
              prove_finite_take_induct spec take_info lub_take_thms thy
huffman@35655
   548
        in
huffman@35655
   549
          ((SOME finites, take_inducts), thy)
huffman@35655
   550
        end
huffman@35655
   551
      else
huffman@35655
   552
        let
huffman@35655
   553
          fun prove_take_induct (chain_take, lub_take) =
huffman@36241
   554
              Drule.zero_var_indexes
huffman@40832
   555
                (@{thm lub_ID_take_induct} OF [chain_take, lub_take])
huffman@35655
   556
          val take_inducts =
huffman@40832
   557
              map prove_take_induct (chain_take_thms ~~ lub_take_thms)
huffman@35655
   558
          val thy = fold (snd oo add_qualified_thm "take_induct")
huffman@40832
   559
                         (dbinds ~~ take_inducts) thy
huffman@35655
   560
        in
huffman@35655
   561
          ((NONE, take_inducts), thy)
huffman@40832
   562
        end
huffman@35655
   563
huffman@35656
   564
    val result =
huffman@35656
   565
      {
huffman@35659
   566
        take_consts         = #take_consts take_info,
huffman@35659
   567
        take_defs           = #take_defs take_info,
huffman@35659
   568
        chain_take_thms     = #chain_take_thms take_info,
huffman@35659
   569
        take_0_thms         = #take_0_thms take_info,
huffman@35659
   570
        take_Suc_thms       = #take_Suc_thms take_info,
huffman@35659
   571
        deflation_take_thms = #deflation_take_thms take_info,
huffman@40015
   572
        take_strict_thms    = #take_strict_thms take_info,
huffman@35659
   573
        finite_consts       = #finite_consts take_info,
huffman@35659
   574
        finite_defs         = #finite_defs take_info,
huffman@35659
   575
        lub_take_thms       = lub_take_thms,
huffman@35659
   576
        reach_thms          = reach_thms,
huffman@35659
   577
        take_lemma_thms     = take_lemma_thms,
huffman@35659
   578
        is_finite           = is_finite,
huffman@35659
   579
        take_induct_thms    = take_induct_thms
huffman@40832
   580
      }
huffman@35654
   581
  in
huffman@35654
   582
    (result, thy)
huffman@40832
   583
  end
huffman@35654
   584
huffman@40832
   585
end