src/HOL/Tools/BNF/bnf_lfp_tactics.ML
author traytel
Fri, 21 Mar 2014 08:13:23 +0100
changeset 56237 69a9dfe71aed
parent 56114 bc7335979247
child 56248 67dc9549fa15
permissions -rw-r--r--
simplified internal datatype construction
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55061
a0adf838e2d1 adjusted comments
blanchet
parents: 55060
diff changeset
     1
(*  Title:      HOL/Tools/BNF/bnf_lfp_tactics.ML
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     3
    Author:     Andrei Popescu, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     4
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
Tactics for the datatype construction.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     9
signature BNF_LFP_TACTICS =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
sig
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
  val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    12
    thm list -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    13
  val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    14
  val mk_alg_select_tac: Proof.context -> thm -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    15
  val mk_alg_set_tac: thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    16
  val mk_bd_card_order_tac: thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    17
  val mk_bd_limit_tac: int -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    18
  val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    19
  val mk_copy_tac: int -> thm -> thm -> thm list -> thm list list -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    20
  val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    21
    thm list -> thm list -> thm list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    22
  val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    23
    thm list -> tactic
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
    24
  val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
    25
  val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    26
    thm -> thm -> thm list -> thm list -> thm list list -> tactic
49506
aeb0cc8889f2 renamed "rel" to "srel"
blanchet
parents: 49504
diff changeset
    27
  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    28
  val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm ->
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    29
    tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    30
  val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    31
  val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    32
    thm list -> tactic
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
    33
  val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    34
  val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    35
  val mk_least_min_alg_tac: thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    36
  val mk_le_rel_OO_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    37
    thm list -> tactic
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
    38
  val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 52911
diff changeset
    39
  val mk_map_id0_tac: thm list -> thm -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    40
  val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    41
  val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    42
  val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    43
    thm list -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    44
  val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
51812
329c62d99979 removed unreferenced thm
blanchet
parents: 51798
diff changeset
    45
    thm -> thm -> thm -> thm -> thm -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    46
  val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    47
  val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    48
  val mk_min_algs_tac: thm -> thm list -> tactic
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    49
  val mk_mor_Abs_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    50
    thm list -> tactic
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    51
  val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list ->
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    52
    thm list list -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    53
  val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    54
  val mk_mor_comp_tac: thm -> thm list list -> thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    55
  val mk_mor_convol_tac: 'a list -> thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    56
  val mk_mor_elim_tac: thm -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    57
  val mk_mor_incl_tac: thm -> thm list -> tactic
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
    58
  val mk_mor_fold_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    59
  val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    60
    thm list -> tactic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    61
  val mk_mor_str_tac: 'a list -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    62
  val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    63
    thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    64
  val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    65
  val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    66
  val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    67
    int -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    68
  val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    69
    cterm list -> thm list -> int -> tactic
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
    70
  val mk_set_map0_tac: thm -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    71
  val mk_set_tac: thm -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    72
  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    73
end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    74
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    75
structure BNF_LFP_Tactics : BNF_LFP_TACTICS =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    76
struct
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    77
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    78
open BNF_Tactics
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    79
open BNF_LFP_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    80
open BNF_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    81
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    82
val fst_snd_convs = @{thms fst_conv snd_conv};
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    83
val ord_eq_le_trans = @{thm ord_eq_le_trans};
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    84
val subset_trans = @{thm subset_trans};
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    85
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
    86
val rev_bspec = Drule.rotate_prems 1 bspec;
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
    87
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
    88
val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]};
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    89
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    90
fun mk_alg_set_tac alg_def =
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
    91
  EVERY' [dtac (alg_def RS iffD1), REPEAT_DETERM o etac conjE, etac bspec, rtac CollectI,
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
    92
   REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    93
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    94
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    95
  (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    96
  REPEAT_DETERM o FIRST'
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
    97
    [EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    98
    EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    99
    EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   100
      FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   101
  etac @{thm emptyE}) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   102
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   103
fun mk_mor_elim_tac mor_def =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   104
  (dtac (mor_def RS iffD1) THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   105
  REPEAT o etac conjE THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   106
  TRY o rtac @{thm image_subsetI} THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   107
  etac bspec THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   108
  atac) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   109
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   110
fun mk_mor_incl_tac mor_def map_ids =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   111
  (rtac (mor_def RS iffD2) THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   112
  rtac conjI THEN'
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   113
  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, etac (id_apply RS @{thm ssubst_mem})]))
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   114
    map_ids THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   115
  CONJ_WRAP' (fn thm =>
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   116
    (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   117
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   118
fun mk_mor_comp_tac mor_def set_maps map_comp_ids =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   119
  let
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   120
    val fbetw_tac =
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   121
      EVERY' [rtac ballI, rtac (o_apply RS @{thm ssubst_mem}), etac bspec, etac bspec, atac];
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   122
    fun mor_tac (set_map, map_comp_id) =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   123
      EVERY' [rtac ballI, rtac (o_apply RS trans), rtac trans,
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
   124
        rtac trans, dtac rev_bspec, atac, etac arg_cong,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   125
         REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   126
      CONJ_WRAP' (fn thm =>
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   127
        FIRST' [rtac subset_UNIV,
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   128
          (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   129
            etac bspec, etac set_mp, atac])]) set_map THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   130
      rtac (map_comp_id RS arg_cong);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   131
  in
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   132
    (dtac (mor_def RS iffD1) THEN' dtac (mor_def RS iffD1) THEN' rtac (mor_def RS iffD2) THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   133
    REPEAT o etac conjE THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   134
    rtac conjI THEN'
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   135
    CONJ_WRAP' (K fbetw_tac) set_maps THEN'
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   136
    CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   137
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   138
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   139
fun mk_mor_str_tac ks mor_def =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   140
  (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   141
  CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   142
  CONJ_WRAP' (K (EVERY' [rtac ballI, rtac refl])) ks) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   143
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   144
fun mk_mor_convol_tac ks mor_def =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   145
  (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   146
  CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   147
  CONJ_WRAP' (K (EVERY' [rtac ballI, rtac trans, rtac @{thm fst_convol'}, rtac o_apply])) ks) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   148
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   149
fun mk_mor_UNIV_tac m morEs mor_def =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   150
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   151
    val n = length morEs;
55990
41c6b99c5fb7 more antiquotations;
wenzelm
parents: 55945
diff changeset
   152
    fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   153
      rtac CollectI, CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto m + n),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   154
      rtac sym, rtac o_apply];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   155
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   156
    EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   157
    rtac (mor_def RS iffD2), rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   158
    REPEAT_DETERM o etac conjE, REPEAT_DETERM_N n o dtac (@{thm fun_eq_iff} RS iffD1),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   159
    CONJ_WRAP' (K (EVERY' [rtac ballI, REPEAT_DETERM o etac allE, rtac trans,
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   160
      etac (o_apply RS sym RS trans), rtac o_apply])) morEs] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   161
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   162
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   163
fun mk_copy_tac m alg_def mor_def alg_sets set_mapss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   164
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   165
    val n = length alg_sets;
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   166
    fun set_tac thm =
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   167
      EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, etac @{thm image_mono},
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   168
        rtac equalityD1, etac @{thm bij_betw_imageE}];
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   169
    val alg_tac =
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   170
      CONJ_WRAP' (fn (set_maps, alg_set) =>
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   171
        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   172
          rtac equalityD1, etac @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   173
          rtac imageI, etac alg_set, EVERY' (map set_tac (drop m set_maps))])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   174
      (set_mapss ~~ alg_sets);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   175
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   176
    val mor_tac = rtac conjI THEN' CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets THEN'
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   177
      CONJ_WRAP' (fn (set_maps, alg_set) =>
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   178
        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   179
          etac @{thm f_the_inv_into_f_bij_betw}, etac alg_set,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   180
          EVERY' (map set_tac (drop m set_maps))])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   181
      (set_mapss ~~ alg_sets);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   182
  in
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   183
    (REPEAT_DETERM_N n o rtac exI THEN' rtac conjI THEN'
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   184
    rtac (alg_def RS iffD2) THEN' alg_tac THEN' rtac (mor_def RS iffD2) THEN' mor_tac) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   185
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   186
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   187
fun mk_bd_limit_tac n bd_Cinfinite =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   188
  EVERY' [REPEAT_DETERM o etac conjE, rtac rev_mp, rtac @{thm Cinfinite_limit_finite},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   189
    REPEAT_DETERM_N n o rtac @{thm finite.insertI}, rtac @{thm finite.emptyI},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   190
    REPEAT_DETERM_N n o etac @{thm insert_subsetI}, rtac @{thm empty_subsetI},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   191
    rtac bd_Cinfinite, rtac impI, etac bexE, rtac bexI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   192
    CONJ_WRAP' (fn i =>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   193
      EVERY' [etac bspec, REPEAT_DETERM_N i o rtac @{thm insertI2}, rtac @{thm insertI1}])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   194
      (0 upto n - 1),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   195
    atac] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   196
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   197
fun mk_min_algs_tac worel in_congs =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   198
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   199
    val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   200
    fun minH_tac thm =
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
   201
      EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   202
        REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   203
  in
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   204
    (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac iffD2 THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   205
    rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   206
    REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN'
49488
02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents: 49463
diff changeset
   207
    CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   208
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   209
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   210
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac relChainD, rtac allI, rtac allI, rtac impI,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   211
  rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2}, rtac subsetI,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   212
  rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac, rtac equalityD1,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   213
  dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   214
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   215
fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
51812
329c62d99979 removed unreferenced thm
blanchet
parents: 51798
diff changeset
   216
  suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   217
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   218
    val induct = worel RS
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   219
      Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   220
    val src = 1 upto m + 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   221
    val dest = (m + 1) :: (1 upto m);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   222
    val absorbAs_tac = if m = 0 then K (all_tac)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   223
      else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   224
        rtac @{thm ordIso_transitive},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   225
        BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   226
          FIRST' [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   227
            rtac @{thm Card_order_cexp}])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   228
        @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   229
        src dest,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   230
        rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac ctrans, rtac @{thm ordLeq_csum1},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   231
        FIRST' [rtac @{thm Card_order_csum}, rtac @{thm card_of_Card_order}],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   232
        rtac @{thm ordLeq_cexp1}, rtac suc_Cnotzero, rtac @{thm Card_order_csum}];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   233
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   234
    val minG_tac = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac @{thm ordLess_imp_ordLeq},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   235
      rtac @{thm ordLess_transitive}, rtac @{thm card_of_underS}, rtac suc_Card_order,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   236
      atac, rtac suc_Asuc, rtac ballI, etac allE, dtac mp, etac @{thm underS_E},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   237
      dtac mp, etac @{thm underS_Field}, REPEAT o etac conjE, atac, rtac Asuc_Cinfinite]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   238
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   239
    fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac @{thm ordIso_ordLeq_trans},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   240
      rtac @{thm card_of_ordIso_subst}, etac min_alg, rtac @{thm Un_Cinfinite_bound},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   241
      minG_tac, rtac ctrans, rtac @{thm card_of_image}, rtac ctrans, rtac in_bd, rtac ctrans,
51782
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51766
diff changeset
   242
      rtac @{thm cexp_mono1}, rtac @{thm csum_mono1},
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   243
      REPEAT_DETERM_N m o rtac @{thm csum_mono2},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   244
      CONJ_WRAP_GEN' (rtac @{thm csum_cinfinite_bound}) (K minG_tac) min_algs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   245
      REPEAT_DETERM o FIRST'
51782
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51766
diff changeset
   246
        [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum},
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51766
diff changeset
   247
        rtac Asuc_Cinfinite, rtac bd_Card_order],
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51766
diff changeset
   248
      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1}, absorbAs_tac,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   249
      rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac @{thm ctwo_ordLeq_Cinfinite},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   250
      rtac Asuc_Cinfinite, rtac bd_Card_order,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   251
      rtac @{thm ordIso_imp_ordLeq}, rtac @{thm cexp_cprod_ordLeq},
51782
84e7225f5ab6 removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents: 51766
diff changeset
   252
      resolve_tac @{thms Card_order_csum Card_order_ctwo}, rtac suc_Cinfinite,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   253
      rtac bd_Cnotzero, rtac @{thm cardSuc_ordLeq}, rtac bd_Card_order, rtac Asuc_Cinfinite];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   254
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   255
    (rtac induct THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   256
    rtac impI THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   257
    CONJ_WRAP' mk_minH_tac (min_algs ~~ in_bds)) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   258
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   259
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   260
fun mk_min_algs_least_tac cT ct worel min_algs alg_sets =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   261
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   262
    val induct = worel RS
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   263
      Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   264
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   265
    val minG_tac = EVERY' [rtac @{thm UN_least}, etac allE, dtac mp, etac @{thm underS_E},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   266
      dtac mp, etac @{thm underS_Field}, REPEAT_DETERM o etac conjE, atac];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   267
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   268
    fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ord_eq_le_trans, etac min_alg,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   269
      rtac @{thm Un_least}, minG_tac, rtac @{thm image_subsetI},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   270
      REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac alg_set,
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   271
      REPEAT_DETERM o (etac subset_trans THEN' minG_tac)];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   272
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   273
    (rtac induct THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   274
    rtac impI THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   275
    CONJ_WRAP' mk_minH_tac (min_algs ~~ alg_sets)) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   276
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   277
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   278
fun mk_alg_min_alg_tac m alg_def min_alg_defs bd_limit bd_Cinfinite
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   279
    set_bdss min_algs min_alg_monos =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   280
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   281
    val n = length min_algs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   282
    fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   283
      [rtac bexE, rtac @{thm cardSuc_UNION_Cinfinite}, rtac bd_Cinfinite, rtac mono,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   284
       etac (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac set_bds];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   285
    fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   286
      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   287
        EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac bexE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   288
        rtac bd_limit, REPEAT_DETERM_N (n - 1) o etac conjI, atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   289
        rtac (min_alg_def RS @{thm set_mp[OF equalityD2]}),
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   290
        rtac @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac thin_rl, atac, rtac set_mp,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   291
        rtac equalityD2, rtac min_alg, atac, rtac UnI2, rtac @{thm image_eqI}, rtac refl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   292
        rtac CollectI, REPEAT_DETERM_N m o dtac asm_rl, REPEAT_DETERM_N n o etac thin_rl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   293
        REPEAT_DETERM o etac conjE,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   294
        CONJ_WRAP' (K (FIRST' [atac,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   295
          EVERY' [etac subset_trans, rtac subsetI, rtac @{thm UN_I},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   296
            etac @{thm underS_I}, atac, atac]]))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   297
          set_bds];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   298
  in
52904
traytel
parents: 52731
diff changeset
   299
    (rtac (alg_def RS iffD2) THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   300
    CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   301
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   302
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   303
fun mk_card_of_min_alg_tac min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   304
  EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac (min_alg_def RS @{thm card_of_ordIso_subst}),
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   305
    rtac @{thm UNION_Cinfinite_bound}, rtac @{thm ordIso_ordLeq_trans},
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   306
    rtac @{thm card_of_Field_ordIso}, rtac suc_Card_order, rtac @{thm ordLess_imp_ordLeq},
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   307
    rtac suc_Asuc, rtac ballI, dtac rev_mp, rtac card_of,  REPEAT_DETERM o etac conjE, atac,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   308
    rtac Asuc_Cinfinite] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   309
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   310
fun mk_least_min_alg_tac min_alg_def least =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   311
  EVERY' [rtac (min_alg_def RS ord_eq_le_trans), rtac @{thm UN_least}, dtac least, dtac mp, atac,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   312
    REPEAT_DETERM o etac conjE, atac] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   313
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   314
fun mk_alg_select_tac ctxt Abs_inverse =
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   315
  EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   316
  unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   317
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   318
fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   319
    set_maps str_init_defs =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   320
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   321
    val n = length alg_sets;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   322
    val fbetw_tac =
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
   323
      CONJ_WRAP' (K (EVERY' [rtac ballI, etac rev_bspec, etac CollectE, atac])) alg_sets;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   324
    val mor_tac =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   325
      CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs;
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   326
    fun alg_epi_tac ((alg_set, str_init_def), set_map) =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   327
      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   328
        rtac ballI, ftac (alg_select RS bspec), rtac (str_init_def RS @{thm ssubst_mem}),
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   329
        etac alg_set, REPEAT_DETERM o EVERY' [rtac ord_eq_le_trans, resolve_tac set_map,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   330
          rtac subset_trans, etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   331
          atac]];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   332
  in
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   333
    EVERY' [rtac mor_cong, REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}),
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   334
      rtac (Thm.permute_prems 0 1 mor_comp), etac (Thm.permute_prems 0 1 mor_comp),
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   335
      rtac (mor_def RS iffD2), rtac conjI, fbetw_tac, mor_tac, rtac mor_incl_min_alg,
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   336
      rtac (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   337
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   338
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   339
fun mk_init_ex_mor_tac ctxt Abs_inverse copy card_of_min_algs mor_Rep mor_comp mor_select mor_incl =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   340
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   341
    val n = length card_of_min_algs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   342
  in
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   343
    EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   344
      REPEAT_DETERM o etac exE, rtac rev_mp, rtac copy, REPEAT_DETERM_N n o atac,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   345
      rtac impI, REPEAT_DETERM o eresolve_tac [exE, conjE], REPEAT_DETERM_N n o rtac exI,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   346
      rtac mor_comp, rtac mor_Rep, rtac mor_select, rtac CollectI, REPEAT_DETERM o rtac exI,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   347
      rtac conjI, rtac refl, atac,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   348
      SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   349
      etac mor_comp, rtac mor_incl, REPEAT_DETERM_N n o rtac subset_UNIV] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   350
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   351
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   352
fun mk_init_unique_mor_tac m
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   353
    alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   354
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   355
    val n = length least_min_algs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   356
    val ks = (1 upto n);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   357
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   358
    fun mor_tac morE in_mono = EVERY' [etac morE, rtac set_mp, rtac in_mono,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   359
      REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   360
      REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)];
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   361
    fun cong_tac map_cong0 = EVERY' [rtac (map_cong0 RS arg_cong),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   362
      REPEAT_DETERM_N m o rtac refl,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   363
      REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   364
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   365
    fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   366
      REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   367
      REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   368
      rtac trans, mor_tac morE in_mono,
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   369
      rtac trans, cong_tac map_cong0,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   370
      rtac sym, mor_tac morE in_mono];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   371
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   372
    fun mk_unique_tac (k, least_min_alg) =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   373
      select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   374
      rtac (alg_def RS iffD2) THEN'
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   375
      CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)));
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   376
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   377
    CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   378
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   379
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   380
fun mk_init_induct_tac m alg_def alg_min_alg least_min_algs alg_sets =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   381
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   382
    val n = length least_min_algs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   383
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   384
    fun mk_alg_tac alg_set = EVERY' [rtac ballI, rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   385
      REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   386
      REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   387
      rtac mp, etac bspec, rtac CollectI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   388
      REPEAT_DETERM_N m o (rtac conjI THEN' atac),
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   389
      CONJ_WRAP' (K (etac subset_trans THEN' rtac @{thm Collect_restrict})) alg_sets,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   390
      CONJ_WRAP' (K (rtac ballI THEN' etac @{thm prop_restrict} THEN' atac)) alg_sets];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   391
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   392
    fun mk_induct_tac least_min_alg =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   393
      rtac ballI THEN' etac @{thm prop_restrict} THEN' rtac least_min_alg THEN'
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   394
      rtac (alg_def RS iffD2) THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   395
      CONJ_WRAP' mk_alg_tac alg_sets;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   396
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   397
    CONJ_WRAP' mk_induct_tac least_min_algs 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   398
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   399
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   400
fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss =
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   401
  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   402
  EVERY' [rtac conjI,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   403
    CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   404
    CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) =>
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   405
      EVERY' [rtac ballI, rtac Abs_inverse, rtac (alg_min_alg RS alg_set),
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   406
        EVERY' (map2 (fn Rep => fn set_map =>
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   407
          EVERY' [rtac (set_map RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac Rep])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   408
        Reps (drop m set_maps))])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   409
    (Abs_inverses ~~ (set_mapss ~~ alg_sets))] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   410
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   411
fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs =
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   412
  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   413
  EVERY' [rtac conjI,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   414
    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   415
    CONJ_WRAP' (fn (ct, thm) =>
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   416
      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   417
        rtac (thm RS (cterm_instantiate_pos [NONE, NONE, ct] arg_cong) RS sym),
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   418
        EVERY' (map (fn Abs_inverse =>
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   419
          EVERY' [rtac (o_apply RS trans RS ballI), etac (set_mp RS Abs_inverse), atac])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   420
        Abs_inverses)])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   421
    (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   422
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   423
fun mk_mor_fold_tac cT ct fold_defs ex_mor mor =
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   424
  (EVERY' (map stac fold_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   425
  REPEAT_DETERM_N (length fold_defs) o etac exE THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   426
  rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   427
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   428
fun mk_fold_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   429
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   430
    fun mk_unique type_def =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   431
      EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}),
49227
2652319c394e open typedef for datatypes
traytel
parents: 48975
diff changeset
   432
        rtac ballI, resolve_tac init_unique_mors,
2652319c394e open typedef for datatypes
traytel
parents: 48975
diff changeset
   433
        EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   434
        rtac mor_comp, rtac mor_Abs, atac,
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   435
        rtac mor_comp, rtac mor_Abs, rtac mor_fold];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   436
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   437
    CONJ_WRAP' mk_unique type_defs 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   438
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   439
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   440
fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   441
  EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac (dtor_def RS fun_cong RS trans),
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   442
    rtac trans, rtac foldx, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   443
    EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   444
      ctor_o_folds),
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   445
    rtac sym, rtac id_apply] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   446
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   447
fun mk_rec_tac ctxt rec_defs foldx fst_recs =
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   448
  unfold_thms_tac ctxt
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   449
    (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   450
  EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   451
    rtac @{thm snd_convol'}] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   452
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   453
fun mk_rec_unique_mor_tac ctxt rec_defs fst_recs fold_unique_mor =
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 49585
diff changeset
   454
  unfold_thms_tac ctxt
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 49585
diff changeset
   455
    (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 49585
diff changeset
   456
  etac fold_unique_mor 1;
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 49585
diff changeset
   457
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   458
fun mk_ctor_induct_tac ctxt m set_mapss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   459
  let
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   460
    val n = length set_mapss;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   461
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   462
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   463
    fun mk_IH_tac Rep_inv Abs_inv set_map =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   464
      DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS iffD1), etac bspec,
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   465
        dtac set_rev_mp, rtac equalityD1, rtac set_map, etac imageE,
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   466
        hyp_subst_tac ctxt, rtac (Abs_inv RS @{thm ssubst_mem}), etac set_mp, atac, atac];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   467
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   468
    fun mk_closed_tac (k, (morE, set_maps)) =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   469
      EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   470
        rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   471
        REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   472
        EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   473
49227
2652319c394e open typedef for datatypes
traytel
parents: 48975
diff changeset
   474
    fun mk_induct_tac (Rep, Rep_inv) =
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   475
      EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   476
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   477
    (rtac mp THEN' rtac impI THEN'
49227
2652319c394e open typedef for datatypes
traytel
parents: 48975
diff changeset
   478
    DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   479
    rtac init_induct THEN'
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   480
    DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   481
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   482
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   483
fun mk_ctor_induct2_tac ctxt cTs cts ctor_induct weak_ctor_inducts =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   484
  let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   485
    val n = length weak_ctor_inducts;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   486
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   487
    fun mk_inner_induct_tac induct i =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   488
      EVERY' [rtac allI, fo_rtac induct ctxt,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   489
        select_prem_tac n (dtac @{thm meta_spec2}) i,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   490
        REPEAT_DETERM_N n o
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53290
diff changeset
   491
          EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   492
            REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac],
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   493
        atac];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   494
  in
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   495
    EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts ctor_induct),
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   496
      EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac impI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   497
      REPEAT_DETERM o eresolve_tac [conjE, allE],
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   498
      CONJ_WRAP' (K atac) ks] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   499
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   500
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   501
fun mk_map_tac m n foldx map_comp_id map_cong0 =
55990
41c6b99c5fb7 more antiquotations;
wenzelm
parents: 55945
diff changeset
   502
  EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans,
41c6b99c5fb7 more antiquotations;
wenzelm
parents: 55945
diff changeset
   503
    rtac o_apply,
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   504
    rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   505
    REPEAT_DETERM_N m o rtac refl,
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   506
    REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   507
    rtac sym, rtac o_apply] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   508
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   509
fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
52911
fe4c2418f069 tuned tactic;
traytel
parents: 52904
diff changeset
   510
  rtac fold_unique 1 THEN
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   511
  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
52911
fe4c2418f069 tuned tactic;
traytel
parents: 52904
diff changeset
   512
  ALLGOALS atac;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   513
55990
41c6b99c5fb7 more antiquotations;
wenzelm
parents: 55945
diff changeset
   514
fun mk_set_tac foldx = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   515
  rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   516
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   517
fun mk_ctor_set_tac set set_map set_maps =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   518
  let
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   519
    val n = length set_maps;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   520
    fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   521
      rtac @{thm Union_image_eq};
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   522
  in
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
   523
    EVERY' [rtac (set RS @{thm comp_eq_dest} RS trans), rtac Un_cong,
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   524
      rtac (trans OF [set_map, trans_fun_cong_image_id_id_apply]),
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
   525
      REPEAT_DETERM_N (n - 1) o rtac Un_cong,
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   526
      EVERY' (map mk_UN set_maps)] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   527
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   528
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   529
fun mk_set_nat_tac ctxt m induct_tac set_mapss ctor_maps csets ctor_sets i =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   530
  let
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49518
diff changeset
   531
    val n = length ctor_maps;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   532
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   533
    fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   534
      rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   535
      rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   536
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   537
    fun mk_set_nat cset ctor_map ctor_set set_nats =
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   538
      EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl,
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   539
        rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]),
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
   540
        rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   541
        rtac sym, rtac (nth set_nats (i - 1)),
52659
58b87aa4dc3b eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
traytel
parents: 52635
diff changeset
   542
        REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   543
        EVERY' (map useIH (drop m set_nats))];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   544
  in
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   545
    (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   546
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   547
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   548
fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   549
  let
49542
b39354db8629 renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents: 49541
diff changeset
   550
    val n = length ctor_sets;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   551
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   552
    fun useIH set_bd = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac set_bd, rtac ballI,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   553
      Goal.assume_rule_tac ctxt, rtac bd_Cinfinite];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   554
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   555
    fun mk_set_nat ctor_set set_bds =
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   556
      EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac ctor_set,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   557
        rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_bds (i - 1)),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   558
        REPEAT_DETERM_N (n - 1) o rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   559
        EVERY' (map useIH (drop m set_bds))];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   560
  in
49542
b39354db8629 renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents: 49541
diff changeset
   561
    (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   562
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   563
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   564
fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   565
  let
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   566
    fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   567
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   568
    fun useIH set_sets = EVERY' [rtac mp, Goal.assume_rule_tac ctxt,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   569
      CONJ_WRAP' (fn thm =>
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   570
        EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   571
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   572
    fun mk_map_cong0 ctor_map map_cong0 set_setss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   573
      EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   574
        rtac trans, rtac ctor_map, rtac trans, rtac (map_cong0 RS arg_cong),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   575
        EVERY' (map use_asm (map hd set_setss)),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   576
        EVERY' (map useIH (transpose (map tl set_setss))),
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49518
diff changeset
   577
        rtac sym, rtac ctor_map];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   578
  in
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   579
    (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   580
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   581
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   582
fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs =
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   583
  EVERY' (rtac induct ::
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   584
  map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO =>
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   585
    EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   586
      REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2),
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   587
      rtac rel_mono, rtac (rel_OO RS @{thm predicate2_eqD} RS iffD2),
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   588
      rtac @{thm relcomppI}, atac, atac,
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   589
      REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac],
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   590
      REPEAT_DETERM_N (length rel_OOs) o
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   591
        EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]])
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   592
  ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   593
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   594
(* BNF tactics *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   595
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 52911
diff changeset
   596
fun mk_map_id0_tac map_id0s unique =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   597
  (rtac sym THEN' rtac unique THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   598
  EVERY' (map (fn thm =>
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   599
    EVERY' [rtac trans, rtac @{thm id_comp}, rtac trans, rtac sym, rtac @{thm comp_id},
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 52911
diff changeset
   600
      rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   601
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   602
fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   603
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   604
    val i = iplus1 - 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   605
    val unique' = Thm.permute_prems 0 i unique;
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   606
    val map_comp0s' = drop i map_comp0s @ take i map_comp0s;
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49518
diff changeset
   607
    val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   608
    fun mk_comp comp simp =
55990
41c6b99c5fb7 more antiquotations;
wenzelm
parents: 55945
diff changeset
   609
      EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   610
        rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   611
        rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   612
  in
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   613
    (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   614
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   615
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   616
fun mk_set_map0_tac set_nat =
55990
41c6b99c5fb7 more antiquotations;
wenzelm
parents: 55945
diff changeset
   617
  EVERY' (map rtac [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   618
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   619
fun mk_bd_card_order_tac bd_card_orders =
54793
c99f0fdb0886 tighter bnf bounds for (co)datatypes
traytel
parents: 54742
diff changeset
   620
  CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   621
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   622
fun mk_wit_tac ctxt n ctor_set wit =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   623
  REPEAT_DETERM (atac 1 ORELSE
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   624
    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   625
    REPEAT_DETERM o
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   626
      (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   627
        (eresolve_tac wit ORELSE'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   628
        (dresolve_tac wit THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   629
          (etac FalseE ORELSE'
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   630
          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   631
            REPEAT_DETERM_N n o etac UnE]))))] 1);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   632
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   633
fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   634
  ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   635
  let
49544
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   636
    val m = length ctor_set_incls;
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   637
    val n = length ctor_set_set_inclss;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   638
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   639
    val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   640
    val in_Irel = nth in_Irels (i - 1);
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   641
    val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   642
    val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   643
    val if_tac =
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   644
      EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   645
        rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   646
        EVERY' (map2 (fn set_map0 => fn ctor_set_incl =>
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   647
          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   648
            rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
49544
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   649
            rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   650
        passive_set_map0s ctor_set_incls),
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   651
        CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   652
          EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55197
diff changeset
   653
            rtac @{thm case_prodI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   654
            CONJ_WRAP' (fn thm =>
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   655
              EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
49544
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   656
            ctor_set_set_incls,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   657
            rtac conjI, rtac refl, rtac refl])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   658
        (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   659
        CONJ_WRAP' (fn conv =>
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   660
          EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   661
          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   662
          REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49518
diff changeset
   663
          rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   664
          etac eq_arg_cong_ctor_dtor])
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   665
        fst_snd_convs];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   666
    val only_if_tac =
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   667
      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   668
        rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   669
        CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   670
          EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   671
            rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   672
            rtac passive_set_map0, rtac trans_fun_cong_image_id_id_apply, atac,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   673
            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   674
              (fn (active_set_map0, in_Irel) => EVERY' [rtac ord_eq_le_trans,
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   675
                rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least},
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   676
                dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   677
                dtac @{thm ssubst_mem[OF pair_collapse]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   678
                REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55197
diff changeset
   679
                  @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   680
                hyp_subst_tac ctxt,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   681
                dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   682
                TRY o
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   683
                  EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   684
                REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   685
            (rev (active_set_map0s ~~ in_Irels))])
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   686
        (ctor_sets ~~ passive_set_map0s),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   687
        rtac conjI,
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49518
diff changeset
   688
        REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   689
          rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   690
          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   691
          EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   692
            dtac @{thm ssubst_mem[OF pair_collapse]},
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   693
            REPEAT_DETERM o
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55197
diff changeset
   694
              eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   695
            hyp_subst_tac ctxt,
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   696
            dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac])
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   697
          in_Irels),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   698
          atac]]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   699
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   700
    EVERY' [rtac iffI, if_tac, only_if_tac] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   701
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   702
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   703
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   704
  let val n = length ks;
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   705
  in
54998
8601434fa334 tuned signature;
wenzelm
parents: 54841
diff changeset
   706
    unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   707
    EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
52506
eb80a16a2b72 use long goal format in rel_induct theorem
traytel
parents: 52505
diff changeset
   708
      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
eb80a16a2b72 use long goal format in rel_induct theorem
traytel
parents: 52505
diff changeset
   709
        EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
eb80a16a2b72 use long goal format in rel_induct theorem
traytel
parents: 52505
diff changeset
   710
          etac rel_mono_strong,
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   711
          REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   712
          EVERY' (map (fn j =>
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   713
            EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   714
              Goal.assume_rule_tac ctxt]) ks)])
52506
eb80a16a2b72 use long goal format in rel_induct theorem
traytel
parents: 52505
diff changeset
   715
      IHs ctor_rels rel_mono_strongs)] 1
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   716
  end;
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   717
55901
8c6d49dd8ae1 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents: 55756
diff changeset
   718
fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   719
  let
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   720
    val n = length map_transfers;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   721
  in
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   722
    unfold_thms_tac ctxt
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55901
diff changeset
   723
      @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55901
diff changeset
   724
    unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   725
    HEADGOAL (EVERY'
55901
8c6d49dd8ae1 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents: 55756
diff changeset
   726
      [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_induct,
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   727
      EVERY' (map (fn map_transfer => EVERY'
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   728
        [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   729
        SELECT_GOAL (unfold_thms_tac ctxt folds),
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   730
        etac @{thm predicate2D_vimage2p},
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55901
diff changeset
   731
        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   732
        REPEAT_DETERM_N m o rtac @{thm id_transfer},
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55901
diff changeset
   733
        REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   734
        atac])
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   735
      map_transfers)])
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   736
  end;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   737
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   738
end;