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