src/HOL/Tools/BNF/bnf_lfp_tactics.ML
author wenzelm
Sat, 30 Jul 2016 21:10:02 +0200
changeset 63568 e63c8f2fbd28
parent 63312 d75d1e399698
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned;
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
58315
6d8458bc6e27 tuning terminology
blanchet
parents: 57967
diff changeset
     6
Tactics for the datatype construction.
48975
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
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    11
  val mk_alg_min_alg_tac: Proof.context -> int -> thm -> thm list -> thm -> thm -> thm list list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    12
    thm list -> 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
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    15
  val mk_alg_set_tac: Proof.context -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    16
  val mk_bd_card_order_tac: Proof.context -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    17
  val mk_bd_limit_tac: Proof.context -> int -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    18
  val mk_card_of_min_alg_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    19
  val mk_copy_tac: Proof.context -> 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
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    24
  val mk_ctor_set_tac: Proof.context -> thm -> thm -> thm list -> tactic
58444
ed95293f14b6 generate 'ctor_rec_transfer' for datatypes
desharna
parents: 58315
diff changeset
    25
  val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
ed95293f14b6 generate 'ctor_rec_transfer' for datatypes
desharna
parents: 58315
diff changeset
    26
    thm list -> tactic
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
    27
  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
    28
    thm -> thm -> thm list -> thm list -> thm list list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    29
  val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    30
  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
    31
    tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    32
  val mk_init_induct_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    33
  val mk_init_unique_mor_tac: Proof.context -> cterm list -> int -> thm -> thm -> thm list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    34
    thm list -> thm list -> thm list -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    35
  val mk_fold_unique_mor_tac: Proof.context -> thm list -> thm list -> thm list -> thm -> thm ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    36
    thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    37
  val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    38
  val mk_least_min_alg_tac: Proof.context -> thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    39
  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
    40
    thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    41
  val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> int -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    42
  val mk_map_id0_tac: Proof.context -> thm list -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    43
  val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    44
  val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    45
  val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    46
    thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    47
  val mk_min_algs_card_of_tac: Proof.context -> ctyp -> cterm -> int -> thm -> thm list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    48
    thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    49
  val mk_min_algs_least_tac: Proof.context -> ctyp -> cterm -> thm -> thm list -> thm list -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    50
  val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    51
  val mk_min_algs_tac: Proof.context -> thm -> thm list -> tactic
56263
9b32aafecec1 made tactic more robust
traytel
parents: 56262
diff changeset
    52
  val mk_mor_Abs_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list ->
9b32aafecec1 made tactic more robust
traytel
parents: 56262
diff changeset
    53
    tactic
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
    54
  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
    55
    thm list list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    56
  val mk_mor_UNIV_tac: Proof.context -> int -> thm list -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    57
  val mk_mor_comp_tac: Proof.context -> thm -> thm list list -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    58
  val mk_mor_elim_tac: Proof.context -> thm -> tactic
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
    59
  val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
    60
  val mk_mor_fold_tac: Proof.context -> ctyp -> cterm -> thm list -> thm -> thm -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    61
  val mk_mor_select_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    62
    thm list list -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    63
  val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    64
  val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    65
    thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    66
  val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    67
  val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    68
  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
    69
    int -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    70
  val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    71
    cterm list -> thm list -> int -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    72
  val mk_set_map0_tac: Proof.context -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    73
  val mk_set_tac: Proof.context -> thm -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    74
  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
    75
end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    76
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    77
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
    78
struct
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    79
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    80
open BNF_Tactics
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    81
open BNF_LFP_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    82
open BNF_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    83
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    84
val fst_snd_convs = @{thms fst_conv snd_conv};
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    85
val ord_eq_le_trans = @{thm ord_eq_le_trans};
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    86
val subset_trans = @{thm subset_trans};
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    87
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
    88
val rev_bspec = Drule.rotate_prems 1 bspec;
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
    89
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
    90
val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]};
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
    91
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    92
fun mk_alg_set_tac ctxt alg_def =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    93
  EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
    94
   REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    95
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    96
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    97
  (EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    98
  REPEAT_DETERM o FIRST'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
    99
    [EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits],
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   100
    EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits],
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   101
    EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   102
      FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   103
  etac ctxt @{thm emptyE}) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   104
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   105
fun mk_mor_elim_tac ctxt mor_def =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   106
  (dtac ctxt (mor_def RS iffD1) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   107
  REPEAT o etac ctxt conjE THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   108
  TRY o rtac ctxt @{thm image_subsetI} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   109
  etac ctxt bspec THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   110
  assume_tac ctxt) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   111
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   112
fun mk_mor_incl_tac ctxt mor_def map_ids =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   113
  (rtac ctxt (mor_def RS iffD2) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   114
  rtac ctxt conjI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   115
  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   116
    map_ids THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   117
  CONJ_WRAP' (fn thm =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   118
    (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   119
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   120
fun mk_mor_comp_tac ctxt 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
   121
  let
56114
bc7335979247 tuned tactics
traytel
parents: 55990
diff changeset
   122
    val fbetw_tac =
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   123
      EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   124
        etac ctxt bspec, etac ctxt bspec, assume_tac ctxt];
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   125
    fun mor_tac (set_map, map_comp_id) =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   126
      EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   127
        rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   128
         REPEAT o eresolve_tac ctxt [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   129
      CONJ_WRAP' (fn thm =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   130
        FIRST' [rtac ctxt subset_UNIV,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   131
          (EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   132
            etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   133
      rtac ctxt (map_comp_id RS arg_cong);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   134
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   135
    (dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   136
    REPEAT o etac ctxt conjE THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   137
    rtac ctxt conjI THEN'
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   138
    CONJ_WRAP' (K fbetw_tac) set_maps THEN'
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   139
    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
   140
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   141
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   142
fun mk_mor_str_tac ctxt ks mor_def =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   143
  (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   144
  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   145
  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   146
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   147
fun mk_mor_UNIV_tac ctxt m morEs mor_def =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   148
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   149
    val n = length morEs;
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   150
    fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   151
      rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   152
      rtac ctxt sym, rtac ctxt o_apply];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   153
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   154
    EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   155
    rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   156
    REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM_N n o dtac ctxt (@{thm fun_eq_iff} RS iffD1),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   157
    CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   158
      etac ctxt (o_apply RS sym RS trans), rtac ctxt o_apply])) morEs] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   159
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   160
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   161
fun mk_copy_tac ctxt 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
   162
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   163
    val n = length alg_sets;
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   164
    fun set_tac thm =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   165
      EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono},
62906
75ca185db27f removed duplicate lemma
traytel
parents: 62343
diff changeset
   166
        rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}];
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   167
    val alg_tac =
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   168
      CONJ_WRAP' (fn (set_maps, alg_set) =>
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   169
        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
62906
75ca185db27f removed duplicate lemma
traytel
parents: 62343
diff changeset
   170
          rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   171
          rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   172
      (set_mapss ~~ alg_sets);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   173
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   174
    val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN'
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   175
      CONJ_WRAP' (fn (set_maps, alg_set) =>
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   176
        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   177
          etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set,
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   178
          EVERY' (map set_tac (drop m set_maps))])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   179
      (set_mapss ~~ alg_sets);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   180
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   181
    (REPEAT_DETERM_N n o rtac ctxt exI THEN' rtac ctxt conjI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   182
    rtac ctxt (alg_def RS iffD2) THEN' alg_tac THEN' rtac ctxt (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
   183
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   184
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   185
fun mk_bd_limit_tac ctxt n bd_Cinfinite =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   186
  EVERY' [REPEAT_DETERM o etac ctxt conjE, rtac ctxt rev_mp, rtac ctxt @{thm Cinfinite_limit_finite},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   187
    REPEAT_DETERM_N n o rtac ctxt @{thm finite.insertI}, rtac ctxt @{thm finite.emptyI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   188
    REPEAT_DETERM_N n o etac ctxt @{thm insert_subsetI}, rtac ctxt @{thm empty_subsetI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   189
    rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt bexE, rtac ctxt bexI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   190
    CONJ_WRAP' (fn i =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   191
      EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   192
      (0 upto n - 1),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   193
    assume_tac ctxt] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   194
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   195
fun mk_min_algs_tac ctxt worel in_congs =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   196
  let
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   197
    val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   198
      assume_tac ctxt, etac ctxt arg_cong];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   199
    fun minH_tac thm =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   200
      EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   201
        REPEAT_DETERM_N (length in_congs) o minG_tac, rtac ctxt refl];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   202
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   203
    (rtac ctxt (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ctxt iffD2 THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   204
    rtac ctxt meta_eq_to_obj_eq THEN' rtac ctxt (worel RS @{thm wo_rel.adm_wo_def}) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   205
    REPEAT_DETERM_N 3 o rtac ctxt allI THEN' rtac ctxt impI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   206
    CONJ_WRAP_GEN' (EVERY' [rtac ctxt prod_injectI, rtac ctxt 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
   207
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   208
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   209
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   210
  rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   211
  rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   212
  assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD},
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   213
  hyp_subst_tac ctxt, rtac ctxt refl] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   214
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   215
fun mk_min_algs_card_of_tac ctxt 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
60801
7664e0916eec tuned signature;
wenzelm
parents: 60784
diff changeset
   219
      Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
48975
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)
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   223
      else EVERY' [rtac ctxt @{thm ordIso_transitive}, rtac ctxt @{thm csum_cong1},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   224
        rtac ctxt @{thm ordIso_transitive},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   225
        BNF_Tactics.mk_rotate_eq_tac ctxt (rtac ctxt @{thm ordIso_refl} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   226
          FIRST' [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   227
            rtac ctxt @{thm Card_order_cexp}])
48975
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,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   230
        rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt ctrans, rtac ctxt @{thm ordLeq_csum1},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   231
        FIRST' [rtac ctxt @{thm Card_order_csum}, rtac ctxt @{thm card_of_Card_order}],
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   232
        rtac ctxt @{thm ordLeq_cexp1}, rtac ctxt suc_Cnotzero, rtac ctxt @{thm Card_order_csum}];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   233
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   234
    val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   235
      rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   236
      assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   237
      dtac ctxt mp, etac ctxt @{thm underS_E},
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   238
      dtac ctxt mp, etac ctxt @{thm underS_Field},
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   239
      REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   240
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   241
    fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   242
      rtac ctxt @{thm card_of_ordIso_subst}, etac ctxt min_alg, rtac ctxt @{thm Un_Cinfinite_bound},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   243
      minG_tac, rtac ctxt ctrans, rtac ctxt @{thm card_of_image}, rtac ctxt ctrans, rtac ctxt in_bd, rtac ctxt ctrans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   244
      rtac ctxt @{thm cexp_mono1}, rtac ctxt @{thm csum_mono1},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   245
      REPEAT_DETERM_N m o rtac ctxt @{thm csum_mono2},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   246
      CONJ_WRAP_GEN' (rtac ctxt @{thm csum_cinfinite_bound}) (K minG_tac) min_algs,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   247
      REPEAT_DETERM o FIRST'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   248
        [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   249
        rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order],
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   250
      rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1}, absorbAs_tac,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   251
      rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt @{thm ctwo_ordLeq_Cinfinite},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   252
      rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   253
      rtac ctxt @{thm ordIso_imp_ordLeq}, rtac ctxt @{thm cexp_cprod_ordLeq},
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   254
      resolve_tac ctxt @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   255
      rtac ctxt bd_Cnotzero, rtac ctxt @{thm cardSuc_ordLeq}, rtac ctxt bd_Card_order, rtac ctxt Asuc_Cinfinite];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   256
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   257
    (rtac ctxt induct THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   258
    rtac ctxt impI THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   259
    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
   260
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   261
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   262
fun mk_min_algs_least_tac ctxt cT ct worel min_algs alg_sets =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   263
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   264
    val induct = worel RS
60801
7664e0916eec tuned signature;
wenzelm
parents: 60784
diff changeset
   265
      Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   266
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   267
    val minG_tac =
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   268
      EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   269
        dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   270
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   271
    fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   272
      rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   273
      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   274
      REPEAT_DETERM o (etac ctxt 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
   275
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   276
    (rtac ctxt induct THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   277
    rtac ctxt impI THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   278
    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
   279
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   280
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   281
fun mk_alg_min_alg_tac ctxt m alg_def min_alg_defs bd_limit bd_Cinfinite
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   282
    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
   283
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   284
    val n = length min_algs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   285
    fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   286
      [rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   287
       etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   288
    fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   289
      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   290
        EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   291
        rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   292
        rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   293
        rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   294
        assume_tac ctxt, rtac ctxt set_mp,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   295
        rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   296
        rtac ctxt @{thm image_eqI}, rtac ctxt refl,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   297
        rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   298
        REPEAT_DETERM o etac ctxt conjE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   299
        CONJ_WRAP' (K (FIRST' [assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   300
          EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   301
            etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]]))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   302
          set_bds];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   303
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   304
    (rtac ctxt (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
   305
    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
   306
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   307
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   308
fun mk_card_of_min_alg_tac ctxt min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   309
  EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   310
    rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   311
    rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   312
    rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   313
    REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   314
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   315
fun mk_least_min_alg_tac ctxt min_alg_def least =
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   316
  EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least},
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   317
    dtac ctxt least, dtac ctxt mp, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   318
    REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   319
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   320
fun mk_alg_select_tac ctxt Abs_inverse =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   321
  EVERY' [rtac ctxt ballI,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   322
    REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   323
  unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   324
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   325
fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   326
    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
   327
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   328
    val n = length alg_sets;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   329
    val fbetw_tac =
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   330
      CONJ_WRAP'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   331
        (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   332
          etac ctxt CollectE, assume_tac ctxt])) alg_sets;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   333
    val mor_tac =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   334
      CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   335
    fun alg_epi_tac ((alg_set, str_init_def), set_map) =
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   336
      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
60777
ee811a49c8f6 eliminated alias;
wenzelm
parents: 60757
diff changeset
   337
        rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec],
ee811a49c8f6 eliminated alias;
wenzelm
parents: 60757
diff changeset
   338
        rtac ctxt (str_init_def RS @{thm ssubst_mem}),
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   339
        etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   340
          rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   341
          assume_tac ctxt]];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   342
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   343
    EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   344
      rtac ctxt (Thm.permute_prems 0 1 mor_comp), etac ctxt (Thm.permute_prems 0 1 mor_comp),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   345
      rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, fbetw_tac, mor_tac, rtac ctxt mor_incl_min_alg,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   346
      rtac ctxt (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
   347
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   348
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   349
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
   350
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   351
    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
   352
  in
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 61424
diff changeset
   353
    EVERY' [Method.insert_tac ctxt (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
61334
8d40ddaa427f collect the names from goals in favor of fragile exports
traytel
parents: 60801
diff changeset
   354
      REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
8d40ddaa427f collect the names from goals in favor of fragile exports
traytel
parents: 60801
diff changeset
   355
      rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   356
      rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   357
      rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   358
      rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   359
      SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   360
      etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   361
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   362
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   363
fun mk_init_unique_mor_tac ctxt cts m
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   364
    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
   365
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   366
    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
   367
    val ks = (1 upto n);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   368
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   369
    fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   370
      REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   371
      REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
56263
9b32aafecec1 made tactic more robust
traytel
parents: 56262
diff changeset
   372
    fun cong_tac ct map_cong0 = EVERY'
60784
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 60777
diff changeset
   373
      [rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   374
      REPEAT_DETERM_N m o rtac ctxt refl,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   375
      REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   376
56263
9b32aafecec1 made tactic more robust
traytel
parents: 56262
diff changeset
   377
    fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   378
      EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   379
        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   380
        REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   381
        rtac ctxt trans, mor_tac morE in_mono,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   382
        rtac ctxt trans, cong_tac ct map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   383
        rtac ctxt sym, mor_tac morE in_mono];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   384
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   385
    fun mk_unique_tac (k, least_min_alg) =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   386
      select_prem_tac ctxt n (etac ctxt @{thm prop_restrict}) k THEN' rtac ctxt least_min_alg THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   387
      rtac ctxt (alg_def RS iffD2) THEN'
56263
9b32aafecec1 made tactic more robust
traytel
parents: 56262
diff changeset
   388
      CONJ_WRAP' mk_alg_tac (cts ~~ (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
   389
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   390
    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
   391
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   392
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   393
fun mk_init_induct_tac ctxt m alg_def alg_min_alg least_min_algs alg_sets =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   394
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   395
    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
   396
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   397
    fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   398
      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   399
      REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   400
      rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   401
      REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   402
      CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   403
      CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   404
        alg_sets];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   405
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   406
    fun mk_induct_tac least_min_alg =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   407
      rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   408
      rtac ctxt (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
   409
      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
   410
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   411
    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
   412
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   413
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   414
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
   415
  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   416
  EVERY' [rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   417
    CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps,
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   418
    CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   419
      EVERY' [rtac ctxt ballI, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set),
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   420
        EVERY' (map2 (fn Rep => fn set_map =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   421
          EVERY' [rtac ctxt (set_map RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt Rep])
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   422
        Reps (drop m set_maps))])
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   423
    (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
   424
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   425
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
   426
  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   427
  EVERY' [rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   428
    CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   429
    CONJ_WRAP' (fn (ct, thm) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   430
      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
60784
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 60777
diff changeset
   431
        rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   432
        EVERY' (map (fn Abs_inverse =>
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   433
          EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   434
            assume_tac ctxt])
56237
69a9dfe71aed simplified internal datatype construction
traytel
parents: 56114
diff changeset
   435
        Abs_inverses)])
63568
wenzelm
parents: 63312
diff changeset
   436
    (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
   437
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   438
fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   439
  (EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   440
  REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN'
60801
7664e0916eec tuned signature;
wenzelm
parents: 60784
diff changeset
   441
  rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   442
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   443
fun mk_fold_unique_mor_tac ctxt 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
   444
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   445
    fun mk_unique type_def =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   446
      EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
   447
        rtac ctxt ballI, resolve_tac ctxt init_unique_mors,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   448
        EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   449
        rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   450
        rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   451
  in
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   452
    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
   453
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   454
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   455
fun mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   456
  EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt (dtor_def RS fun_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   457
    rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   458
    EVERY' (map (fn thm => rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply]))
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49502
diff changeset
   459
      ctor_o_folds),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   460
    rtac ctxt sym, rtac ctxt id_apply] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   461
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   462
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
   463
  unfold_thms_tac ctxt
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   464
    (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   465
  EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt (foldx RS @{thm arg_cong[of _ _ snd]}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   466
    rtac ctxt @{thm snd_convol'}] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   467
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   468
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
   469
  unfold_thms_tac ctxt
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 49585
diff changeset
   470
    (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   471
  etac ctxt fold_unique_mor 1;
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 49585
diff changeset
   472
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   473
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
   474
  let
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   475
    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
   476
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   477
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   478
    fun mk_IH_tac Rep_inv Abs_inv set_map =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   479
      DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   480
        dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   481
        hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   482
        assume_tac ctxt, assume_tac ctxt];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   483
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   484
    fun mk_closed_tac (k, (morE, set_maps)) =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   485
      EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   486
        rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   487
        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   488
        EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   489
49227
2652319c394e open typedef for datatypes
traytel
parents: 48975
diff changeset
   490
    fun mk_induct_tac (Rep, Rep_inv) =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   491
      EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   492
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   493
    (rtac ctxt mp THEN' rtac ctxt impI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   494
    DETERM o CONJ_WRAP_GEN' (etac ctxt conjE THEN' rtac ctxt conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   495
    rtac ctxt init_induct THEN'
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   496
    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
   497
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   498
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   499
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
   500
  let
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   501
    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
   502
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   503
    fun mk_inner_induct_tac induct i =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   504
      EVERY' [rtac ctxt allI, fo_rtac ctxt induct,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   505
        select_prem_tac ctxt n (dtac ctxt @{thm meta_spec2}) i,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   506
        REPEAT_DETERM_N n o
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   507
          EVERY' [dtac ctxt meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   508
            REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   509
            assume_tac ctxt],
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   510
        assume_tac ctxt];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   511
  in
60801
7664e0916eec tuned signature;
wenzelm
parents: 60784
diff changeset
   512
    EVERY' [rtac ctxt rev_mp, rtac ctxt (Thm.instantiate' cTs cts ctor_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   513
      EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   514
      REPEAT_DETERM o eresolve_tac ctxt [conjE, allE],
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   515
      CONJ_WRAP' (K (assume_tac ctxt)) ks] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   516
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   517
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   518
fun mk_map_tac ctxt m n foldx map_comp_id map_cong0 =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   519
  EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   520
    rtac ctxt o_apply,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   521
    rtac ctxt trans, rtac ctxt (map_comp_id RS arg_cong), rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   522
    REPEAT_DETERM_N m o rtac ctxt refl,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   523
    REPEAT_DETERM_N n o (EVERY' (map (rtac ctxt) [trans, o_apply, id_apply])),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   524
    rtac ctxt sym, rtac ctxt o_apply] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   525
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   526
fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   527
  rtac ctxt fold_unique 1 THEN
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   528
  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   529
  ALLGOALS (assume_tac ctxt);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   530
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   531
fun mk_set_tac ctxt foldx = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   532
  rtac ctxt trans, rtac ctxt foldx, rtac ctxt sym, rtac ctxt o_apply] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   533
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   534
fun mk_ctor_set_tac ctxt 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
   535
  let
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   536
    val n = length set_maps;
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61841
diff changeset
   537
    fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans)
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61841
diff changeset
   538
      THEN' rtac ctxt @{thm refl};
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   539
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   540
    EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   541
      rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   542
      REPEAT_DETERM_N (n - 1) o rtac ctxt Un_cong,
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   543
      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
   544
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   545
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   546
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
   547
  let
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49518
diff changeset
   548
    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
   549
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   550
    fun useIH set_nat = EVERY' [rtac ctxt trans, rtac ctxt @{thm image_UN}, rtac ctxt trans, rtac ctxt @{thm SUP_cong},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   551
      rtac ctxt refl, Goal.assume_rule_tac ctxt, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm SUP_cong},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   552
      rtac ctxt set_nat, rtac ctxt refl, rtac ctxt @{thm UN_simps(10)}];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   553
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   554
    fun mk_set_nat cset ctor_map ctor_set set_nats =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   555
      EVERY' [rtac ctxt trans, rtac ctxt @{thm image_cong}, rtac ctxt ctor_set, rtac ctxt refl, rtac ctxt sym,
60784
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 60777
diff changeset
   556
        rtac ctxt (trans OF [ctor_map RS infer_instantiate' ctxt [NONE, NONE, SOME cset] arg_cong,
56262
251f60be62a7 inline helper function
traytel
parents: 56248
diff changeset
   557
          ctor_set RS trans]),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   558
        rtac ctxt sym, EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   559
        rtac ctxt sym, rtac ctxt (nth set_nats (i - 1)),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   560
        REPEAT_DETERM_N (n - 1) o EVERY' (map (rtac ctxt) [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
   561
        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
   562
  in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
   563
    (induct_tac THEN' EVERY' (@{map 4} 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
   564
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   565
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   566
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
   567
  let
49542
b39354db8629 renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents: 49541
diff changeset
   568
    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
   569
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   570
    fun useIH set_bd = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt set_bd, rtac ctxt ballI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   571
      Goal.assume_rule_tac ctxt, rtac ctxt bd_Cinfinite];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   572
49585
5c4a12550491 generate high-level "maps", "sets", and "rels" properties
blanchet
parents: 49544
diff changeset
   573
    fun mk_set_nat ctor_set set_bds =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   574
      EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt ctor_set,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   575
        rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_bds (i - 1)),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   576
        REPEAT_DETERM_N (n - 1) o rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   577
        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
   578
  in
49542
b39354db8629 renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents: 49541
diff changeset
   579
    (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
   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_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
   583
  let
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   584
    fun use_asm thm = EVERY' [etac ctxt bspec, etac ctxt set_rev_mp, rtac ctxt thm];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   585
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   586
    fun useIH set_sets = EVERY' [rtac ctxt mp, Goal.assume_rule_tac ctxt,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   587
      CONJ_WRAP' (fn thm =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   588
        EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_rev_mp, etac ctxt thm]) set_sets];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   589
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   590
    fun mk_map_cong0 ctor_map map_cong0 set_setss =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   591
      EVERY' [rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   592
        rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt trans, rtac ctxt (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
   593
        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
   594
        EVERY' (map useIH (transpose (map tl set_setss))),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   595
        rtac ctxt sym, rtac ctxt ctor_map];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   596
  in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
   597
    (induct_tac THEN' EVERY' (@{map 3} 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
   598
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   599
57967
e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0'
desharna
parents: 57806
diff changeset
   600
fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   601
  EVERY' (rtac ctxt induct ::
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
   602
  @{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   603
    EVERY' [rtac ctxt impI, etac ctxt (nchotomy RS @{thm nchotomy_relcomppE}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   604
      REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   605
      rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   606
      rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   607
      REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt],
57726
18b8a8f10313 simplified tactics slightly
traytel
parents: 56765
diff changeset
   608
      REPEAT_DETERM_N (length le_rel_OOs) o
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   609
        EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]])
57967
e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0'
desharna
parents: 57806
diff changeset
   610
  ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   611
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   612
(* BNF tactics *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   613
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   614
fun mk_map_id0_tac ctxt map_id0s unique =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   615
  (rtac ctxt sym THEN' rtac ctxt unique THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   616
  EVERY' (map (fn thm =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   617
    EVERY' [rtac ctxt trans, rtac ctxt @{thm id_comp}, rtac ctxt trans, rtac ctxt sym, rtac ctxt @{thm comp_id},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   618
      rtac ctxt (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
   619
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   620
fun mk_map_comp0_tac ctxt 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
   621
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   622
    val i = iplus1 - 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   623
    val unique' = Thm.permute_prems 0 i unique;
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   624
    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
   625
    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
   626
    fun mk_comp comp simp =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   627
      EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt o_apply,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   628
        rtac ctxt trans, rtac ctxt (simp RS arg_cong), rtac ctxt trans, rtac ctxt simp,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   629
        rtac ctxt trans, rtac ctxt (comp RS arg_cong), rtac ctxt sym, rtac ctxt o_apply];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   630
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   631
    (rtac ctxt sym THEN' rtac ctxt 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
   632
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   633
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   634
fun mk_set_map0_tac ctxt set_nat =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   635
  EVERY' (map (rtac ctxt) [@{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
   636
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   637
fun mk_bd_card_order_tac ctxt bd_card_orders =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   638
  CONJ_WRAP_GEN' (rtac ctxt @{thm card_order_csum}) (rtac ctxt) bd_card_orders 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   639
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   640
fun mk_wit_tac ctxt n ctor_set wit =
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   641
  REPEAT_DETERM (assume_tac ctxt 1 ORELSE
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   642
    EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   643
    REPEAT_DETERM o
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   644
      (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   645
        (eresolve_tac ctxt wit ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   646
        (dresolve_tac ctxt wit THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   647
          (etac ctxt FalseE ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   648
          EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   649
            REPEAT_DETERM_N n o etac ctxt UnE]))))] 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   650
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   651
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
   652
  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
   653
  let
49544
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   654
    val m = length ctor_set_incls;
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   655
    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
   656
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   657
    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
   658
    val in_Irel = nth in_Irels (i - 1);
49501
acc9635a644a renamed "fld"/"unf" to "ctor"/"dtor"
blanchet
parents: 49490
diff changeset
   659
    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
   660
    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
   661
    val if_tac =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   662
      EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   663
        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   664
        EVERY' (map2 (fn set_map0 => fn ctor_set_incl =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   665
          EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   666
            rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   667
            rtac ctxt (ctor_set_incl RS subset_trans), etac ctxt le_arg_cong_ctor_dtor])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   668
        passive_set_map0s ctor_set_incls),
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   669
        CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   670
          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   671
            rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   672
            CONJ_WRAP' (fn thm =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   673
              EVERY' (map (etac ctxt) [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
   674
            ctor_set_set_incls,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   675
            rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   676
        (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
   677
        CONJ_WRAP' (fn conv =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   678
          EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   679
          REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   680
          REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   681
          rtac ctxt (ctor_inject RS iffD1), rtac ctxt trans, rtac ctxt sym, rtac ctxt ctor_map,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   682
          etac ctxt eq_arg_cong_ctor_dtor])
49306
c13fff97a8df tuning annotations
blanchet
parents: 49227
diff changeset
   683
        fst_snd_convs];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   684
    val only_if_tac =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   685
      EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   686
        rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   687
        CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   688
          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   689
            rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   690
            rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   691
            CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   692
              (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   693
                rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   694
                dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61334
diff changeset
   695
                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   696
                REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
56765
644f0d4820a1 cleaner 'rel_inject' theorems
blanchet
parents: 56638
diff changeset
   697
                  @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   698
                hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   699
                dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   700
                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   701
            (rev (active_set_map0s ~~ in_Irels))])
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   702
        (ctor_sets ~~ passive_set_map0s),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   703
        rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   704
        REPEAT_DETERM_N 2 o EVERY' [rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt (ctor_inject RS iffD2),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   705
          rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   706
          REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   707
          EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   708
            dtac ctxt set_rev_mp, assume_tac ctxt,
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61334
diff changeset
   709
            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   710
            REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
56765
644f0d4820a1 cleaner 'rel_inject' theorems
blanchet
parents: 56638
diff changeset
   711
              @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   712
            hyp_subst_tac ctxt,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   713
            dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex},
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   714
            REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51812
diff changeset
   715
          in_Irels),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   716
          assume_tac ctxt]]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   717
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   718
    EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   719
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   720
58444
ed95293f14b6 generate 'ctor_rec_transfer' for datatypes
desharna
parents: 58315
diff changeset
   721
fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
ed95293f14b6 generate 'ctor_rec_transfer' for datatypes
desharna
parents: 58315
diff changeset
   722
    ctor_rels =
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58444
diff changeset
   723
  CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   724
      REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58444
diff changeset
   725
      unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   726
      HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   727
        etac ctxt (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN'
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58444
diff changeset
   728
        EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   729
          etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   730
          rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   731
          rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   732
          REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   733
          REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   734
          rtac ctxt rel_funI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   735
          etac ctxt (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58444
diff changeset
   736
    (ctor_rec_defs ~~ ctor_fold_transfers);
58444
ed95293f14b6 generate 'ctor_rec_transfer' for datatypes
desharna
parents: 58315
diff changeset
   737
57967
e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0'
desharna
parents: 57806
diff changeset
   738
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   739
  let val n = length ks;
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   740
  in
54998
8601434fa334 tuned signature;
wenzelm
parents: 54841
diff changeset
   741
    unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   742
    EVERY' [REPEAT_DETERM o rtac ctxt allI, rtac ctxt ctor_induct2,
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
   743
      EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   744
        EVERY' [rtac ctxt impI, dtac ctxt (ctor_rel RS iffD1), rtac ctxt (IH RS @{thm spec2} RS mp),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   745
          etac ctxt rel_mono_strong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   746
          REPEAT_DETERM_N m o rtac ctxt @{thm ballI[OF ballI[OF imp_refl]]},
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   747
          EVERY' (map (fn j =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   748
            EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) j, rtac ctxt @{thm ballI[OF ballI]},
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   749
              Goal.assume_rule_tac ctxt]) ks)])
57967
e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0'
desharna
parents: 57806
diff changeset
   750
      IHs ctor_rels rel_mono_strong0s)] 1
51918
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   751
  end;
3c152334f794 relator induction for datatypes
traytel
parents: 51893
diff changeset
   752
55901
8c6d49dd8ae1 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents: 55756
diff changeset
   753
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
   754
  let
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   755
    val n = length map_transfers;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   756
  in
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   757
    unfold_thms_tac ctxt
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55901
diff changeset
   758
      @{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
   759
    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
   760
    HEADGOAL (EVERY'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   761
      [REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_induct,
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   762
      EVERY' (map (fn map_transfer => EVERY'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   763
        [REPEAT_DETERM o resolve_tac ctxt [allI, impI, @{thm vimage2pI}],
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   764
        SELECT_GOAL (unfold_thms_tac ctxt folds),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   765
        etac ctxt @{thm predicate2D_vimage2p},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   766
        rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   767
        REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59499
diff changeset
   768
        REPEAT_DETERM_N n o rtac ctxt @{thm vimage2p_rel_fun},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   769
        assume_tac ctxt])
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   770
      map_transfers)])
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   771
  end;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
   772
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   773
end;