src/HOL/Tools/BNF/bnf_gfp_tactics.ML
author haftmann
Thu, 24 Jul 2025 17:46:29 +0200
changeset 82902 99a720d3ed8f
parent 82630 2bb4a8d0111d
permissions -rw-r--r--
clarified code setup
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_gfp_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
    Author:     Jasmin Blanchette, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
Tactics for the codatatype construction.
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
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
signature BNF_GFP_TACTICS =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
sig
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    12
  val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    13
  val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    14
  val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    15
  val mk_bis_converse_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    16
  val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    17
    thm list list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    18
  val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    19
  val mk_coalg_final_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    20
    thm list list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    21
  val mk_coalg_set_tac: Proof.context -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    22
  val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    23
  val mk_col_bd_tac: Proof.context -> int -> int -> cterm option list -> thm list -> thm list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    24
    thm -> thm -> thm list list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    25
  val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    26
    thm list list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    27
  val mk_congruent_str_final_tac: Proof.context -> int -> thm -> thm -> thm -> thm list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    28
  val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    29
  val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    30
  val mk_dtor_coinduct_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
58445
86b5b02ef33a generate 'dtor_corec_transfer' for codatatypes
desharna
parents: 57983
diff changeset
    31
  val mk_dtor_corec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
86b5b02ef33a generate 'dtor_corec_transfer' for codatatypes
desharna
parents: 57983
diff changeset
    32
    thm list -> tactic
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    33
  val mk_dtor_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
    34
    thm -> thm -> thm list -> thm list -> thm list list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    35
  val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    36
  val mk_equiv_lsbis_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
    37
  val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic
56113
e3b8f8319d73 simplified internal codatatype construction
traytel
parents: 56017
diff changeset
    38
  val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    39
    tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    40
  val mk_incl_lsbis_tac: Proof.context -> int -> int -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    41
  val mk_length_Lev'_tac: Proof.context -> thm -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    42
  val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    43
  val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    44
  val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
55644
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
    45
    thm list list -> thm list list -> thm list list list -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    46
  val mk_map_id0_tac: Proof.context -> thm list -> thm -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    47
  val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    48
  val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    49
  val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
    50
  val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    51
    thm list -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    52
  val mk_mor_T_final_tac: Proof.context -> thm -> thm list -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    53
  val mk_mor_UNIV_tac: Proof.context -> thm list -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    54
  val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    55
    thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
55577
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
    56
    thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
    57
    thm list list -> thm list -> thm list -> tactic
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
    58
  val mk_mor_comp_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    59
  val mk_mor_elim_tac: Proof.context -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    60
  val mk_mor_col_tac: Proof.context -> int -> int -> cterm option list -> int -> thm list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    61
    thm list -> thm list -> thm list list -> thm list list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    62
  val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    63
  val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    64
  val mk_mor_unfold_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    65
    thm list -> thm list -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    66
  val mk_raw_coind_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    67
    thm -> thm list -> thm list -> thm list -> thm -> thm list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    68
  val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    69
    thm list -> thm list -> tactic
55644
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
    70
  val mk_rel_coinduct_coind_tac: Proof.context -> bool -> int -> thm -> int list -> thm list ->
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
    71
    thm list -> thm list -> thm list list -> thm list -> thm list -> thm list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    72
  val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    73
    int -> thm -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    74
  val mk_rv_last_tac: Proof.context -> ctyp option list -> cterm option list -> thm list ->
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    75
    thm list -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    76
  val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    77
  val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    78
    thm list -> thm list list -> tactic
75624
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
    79
  val mk_set_bd_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    80
  val mk_set_Jset_incl_Jset_tac: Proof.context -> int -> thm -> int -> tactic
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    81
  val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
    82
    thm list -> thm list -> thm list list -> thm list list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    83
  val mk_set_incl_Jset_tac: Proof.context -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    84
  val mk_set_ge_tac: Proof.context -> int  -> thm -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    85
  val mk_set_le_tac: Proof.context -> int -> thm -> thm list -> thm list list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    86
  val mk_set_map0_tac: Proof.context -> thm -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    87
  val mk_unfold_unique_mor_tac: Proof.context -> thm list -> thm -> thm -> thm list -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    88
  val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
    89
  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    90
  val mk_le_rel_OO_tac: Proof.context -> thm -> thm list -> thm list -> tactic
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    91
end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    92
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    93
structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    94
struct
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    95
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    96
open BNF_Tactics
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    97
open BNF_Util
51850
106afdf5806c renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents: 51798
diff changeset
    98
open BNF_FP_Util
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    99
open BNF_GFP_Util
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   100
63170
eae6549dbea2 tuned proofs, to allow unfold_abs_def;
wenzelm
parents: 61841
diff changeset
   101
val fst_convol_fun_cong_sym = @{thm fst_convol[simplified convol_def]} RS fun_cong RS sym;
49488
02eb07152998 use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents: 49463
diff changeset
   102
val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
49305
8241f21d104b tuned antiquotations
blanchet
parents: 49104
diff changeset
   103
val nat_induct = @{thm nat_induct};
8241f21d104b tuned antiquotations
blanchet
parents: 49104
diff changeset
   104
val o_apply_trans_sym = o_apply RS trans RS sym;
8241f21d104b tuned antiquotations
blanchet
parents: 49104
diff changeset
   105
val ord_eq_le_trans = @{thm ord_eq_le_trans};
8241f21d104b tuned antiquotations
blanchet
parents: 49104
diff changeset
   106
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
63170
eae6549dbea2 tuned proofs, to allow unfold_abs_def;
wenzelm
parents: 61841
diff changeset
   107
val snd_convol_fun_cong_sym = @{thm snd_convol[simplified convol_def]} RS fun_cong RS sym;
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57806
diff changeset
   108
val sum_case_cong_weak = @{thm sum.case_cong_weak};
49305
8241f21d104b tuned antiquotations
blanchet
parents: 49104
diff changeset
   109
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 60801
diff changeset
   110
val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   111
val rev_bspec = Drule.rotate_prems 1 @{thm bspec};
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   112
val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\<union>)"]};
52749
ed416f4ac34e more converse(p) theorems; tuned proofs;
traytel
parents: 52731
diff changeset
   113
val converse_shift = @{thm converse_subset_swap} RS iffD1;
49305
8241f21d104b tuned antiquotations
blanchet
parents: 49104
diff changeset
   114
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   115
fun mk_coalg_set_tac ctxt coalg_def =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   116
  dtac ctxt (coalg_def RS iffD1) 1 THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   117
  REPEAT_DETERM (etac ctxt conjE 1) THEN
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   118
  EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   119
  REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) 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
   120
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   121
fun mk_mor_elim_tac ctxt mor_def =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   122
  (dtac ctxt (mor_def RS iffD1) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   123
  REPEAT o etac ctxt conjE THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   124
  TRY o rtac ctxt @{thm image_subsetI} THEN'
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   125
  etac ctxt @{thm bspec} THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   126
  assume_tac ctxt) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   127
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   128
fun mk_mor_incl_tac ctxt mor_def map_ids =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   129
  (rtac ctxt (mor_def RS iffD2) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   130
  rtac ctxt conjI THEN'
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   131
  CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
56114
bc7335979247 tuned tactics
traytel
parents: 56113
diff changeset
   132
    map_ids THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   133
  CONJ_WRAP' (fn thm =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   134
    (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   135
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   136
fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   137
  let
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   138
    fun fbetw_tac image = EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   139
      etac ctxt image, assume_tac ctxt];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   140
    fun mor_tac ((mor_image, morE), map_comp_id) =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   141
      EVERY' [rtac ctxt @{thm ballI}, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   142
        etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   143
        etac ctxt mor_image, assume_tac ctxt];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   144
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   145
    (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   146
    CONJ_WRAP' fbetw_tac mor_images THEN'
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   147
    CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   148
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   149
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   150
fun mk_mor_UNIV_tac ctxt morEs mor_def =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   151
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   152
    val n = length morEs;
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   153
    fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   154
      rtac ctxt @{thm UNIV_I}, 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
   155
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   156
    EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   157
    rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) morEs,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   158
    CONJ_WRAP' (fn i =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   159
      EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt @{thm ballI}, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   160
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   161
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   162
fun mk_mor_str_tac ctxt ks mor_UNIV =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   163
  (rtac ctxt (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (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
   164
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   165
fun mk_set_incl_Jset_tac ctxt rec_Suc =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   166
  EVERY' (map (rtac ctxt) (@{thms SUP_upper2 UNIV_I ord_le_eq_trans Un_upper1 sym} @
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   167
    [rec_Suc])) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   168
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   169
fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   170
  EVERY' (map (rtac ctxt) (@{thms UN_least subsetI UN_I UNIV_I set_mp equalityD2} @
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   171
    [rec_Suc, @{thm UnI2}, mk_UnIN n i]) @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   172
56113
e3b8f8319d73 simplified internal codatatype construction
traytel
parents: 56017
diff changeset
   173
fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   174
  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   175
    REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   176
    CONJ_WRAP' (fn thm => EVERY'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   177
      [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm empty_subsetI}]) rec_0s,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   178
    REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   179
    CONJ_WRAP' (fn rec_Suc => EVERY'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   180
      [rtac ctxt ord_eq_le_trans, rtac ctxt rec_Suc,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   181
        if m = 0 then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   182
        else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   183
        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: 59498
diff changeset
   184
          (K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE],
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   185
            rtac ctxt @{thm subset_trans}, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   186
      rec_Sucs] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   187
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   188
fun mk_Jset_minimal_tac ctxt n col_minimal =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   189
  (CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm UN_least}, rtac ctxt rev_mp, rtac ctxt col_minimal,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   190
    EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac ctxt impI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   191
    REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   192
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   193
fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   194
  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   195
    REPEAT_DETERM o rtac ctxt allI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   196
    CONJ_WRAP' (fn thm => EVERY' (map (rtac ctxt) [impI, thm RS trans, thm RS sym])) rec_0s,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   197
    REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   198
    CONJ_WRAP'
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   199
      (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   200
        EVERY' [rtac ctxt impI, rtac ctxt (rec_Suc RS trans), rtac ctxt (rec_Suc RS trans RS sym),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   201
          if m = 0 then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   202
          else EVERY' [rtac ctxt Un_cong, rtac ctxt @{thm box_equals},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   203
            rtac ctxt (nth passive_set_map0s (j - 1) RS sym),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   204
            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   205
            assume_tac ctxt],
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   206
          CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong))
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   207
            (fn (i, (set_map0, coalg_set)) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   208
              EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   209
                etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   210
                rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}),
60777
ee811a49c8f6 eliminated alias;
wenzelm
parents: 60757
diff changeset
   211
                forward_tac ctxt [coalg_set], assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   212
                rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   213
                REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   214
            (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   215
      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   216
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   217
fun mk_bis_rel_tac ctxt m bis_def in_rels map_comp0s map_cong0s set_map0ss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   218
  let
56017
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   219
    val n = length in_rels;
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   220
    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   221
56017
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   222
    fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   223
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   224
        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt @{thm bexE},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   225
        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   226
        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   227
        CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   228
          REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   229
          assume_tac ctxt])
56017
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   230
        @{thms fst_diag_id snd_diag_id},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   231
        rtac ctxt @{thm CollectI},
56017
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   232
        CONJ_WRAP' (fn (i, thm) =>
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   233
          if i <= m
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   234
          then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm subset_trans},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   235
            etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   236
            rtac ctxt @{thm case_prodI}, rtac ctxt refl]
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   237
          else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 60801
diff changeset
   238
            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}])
56017
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   239
        (1 upto (m + n) ~~ set_map0s)];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   240
56017
8d3df792d47e tuned tactic
traytel
parents: 55990
diff changeset
   241
    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   242
      EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   243
        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   244
        dtac ctxt (in_rel RS @{thm iffD1}),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   245
        REPEAT_DETERM o eresolve_tac ctxt
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   246
          @{thms CollectE conjE exE CollectE Collect_case_prod_in_rel_leE},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   247
        rtac ctxt @{thm bexI}, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   248
        REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   249
        REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   250
        assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   251
        REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   252
        REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   253
        rtac ctxt trans, rtac ctxt map_cong0,
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 60801
diff changeset
   254
        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt],
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   255
        REPEAT_DETERM_N n o rtac ctxt refl,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   256
        assume_tac ctxt, rtac ctxt @{thm CollectI},
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   257
        CONJ_WRAP' (fn (i, thm) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   258
          if i <= m then rtac ctxt subset_UNIV
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   259
          else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   260
            rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   261
        (1 upto (m + n) ~~ set_map0s)];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   262
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   263
    EVERY' [rtac ctxt (bis_def RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   264
      rtac ctxt iffI, etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_if_tac thms,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   265
      etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_only_if_tac thms] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   266
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   267
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   268
fun mk_bis_converse_tac ctxt m bis_rel rel_congs rel_converseps =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   269
  EVERY' [rtac ctxt (bis_rel RS iffD2), dtac ctxt (bis_rel RS iffD1),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   270
    REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   271
    CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt @{thm subset_trans},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   272
      rtac ctxt @{thm equalityD2}, rtac ctxt @{thm converse_Times}])) rel_congs,
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   273
    CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   274
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   275
        rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   276
        REPEAT_DETERM_N m o rtac ctxt @{thm conversep_eq},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   277
        REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm conversep_in_rel},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   278
        rtac ctxt (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   279
        REPEAT_DETERM o etac ctxt allE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   280
        rtac ctxt @{thm conversepI}, etac ctxt mp, etac ctxt @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   281
57726
18b8a8f10313 simplified tactics slightly
traytel
parents: 56765
diff changeset
   282
fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   283
  EVERY' [rtac ctxt (bis_rel RS iffD2), REPEAT_DETERM o dtac ctxt (bis_rel RS iffD1),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   284
    REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   285
    CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, assume_tac ctxt])) rel_congs,
57726
18b8a8f10313 simplified tactics slightly
traytel
parents: 56765
diff changeset
   286
    CONJ_WRAP' (fn (rel_cong, le_rel_OO) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   287
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   288
        rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   289
        REPEAT_DETERM_N m o rtac ctxt @{thm eq_OO},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   290
        REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm relcompp_in_rel},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   291
        rtac ctxt (le_rel_OO RS @{thm predicate2D}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   292
        etac ctxt @{thm relcompE},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   293
        REPEAT_DETERM o dtac ctxt prod_injectD,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   294
        etac ctxt conjE, hyp_subst_tac ctxt,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   295
        REPEAT_DETERM o etac ctxt allE, rtac ctxt @{thm relcomppI},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   296
        etac ctxt mp, assume_tac ctxt, etac ctxt mp, assume_tac ctxt]) (rel_congs ~~ le_rel_OOs)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   297
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   298
fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   299
  unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   300
  EVERY' [rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   301
    CONJ_WRAP' (fn thm => rtac ctxt (@{thm Gr_incl} RS iffD2) THEN' etac ctxt thm) mor_images,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   302
    CONJ_WRAP' (fn (coalg_in, morE) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   303
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt @{thm GrpI}, etac ctxt (morE RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   304
        etac ctxt @{thm GrD1}, etac ctxt (@{thm GrD2} RS arg_cong), etac ctxt coalg_in, etac ctxt @{thm GrD1}])
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   305
    (coalg_ins ~~ morEs)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   306
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   307
fun mk_bis_Union_tac ctxt bis_def in_monos =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   308
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   309
    val n = length in_monos;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   310
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   311
  in
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   312
    unfold_thms_tac ctxt [bis_def] THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   313
    EVERY' [rtac ctxt conjI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   314
      CONJ_WRAP' (fn i =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   315
        EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt @{thm bspec}, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   316
          dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   317
      CONJ_WRAP' (fn (i, in_mono) =>
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   318
        EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   319
          dtac ctxt @{thm bspec}, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   320
          dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   321
          assume_tac ctxt, etac ctxt @{thm bexE}, rtac ctxt @{thm bexI}, assume_tac ctxt, rtac ctxt in_mono,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   322
          REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   323
          assume_tac ctxt]) (ks ~~ in_monos)] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   324
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   325
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   326
fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
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 lsbis_defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   329
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   330
    EVERY' [rtac ctxt (Thm.permute_prems 0 1 bis_cong), EVERY' (map (rtac ctxt) lsbis_defs),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   331
      rtac ctxt bis_Union, rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE exE},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   332
      hyp_subst_tac ctxt, etac ctxt bis_cong, EVERY' (map (rtac ctxt o mk_nth_conv n) (1 upto n))] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   333
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   334
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   335
fun mk_incl_lsbis_tac ctxt n i lsbis_def =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   336
  EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt @{thm CollectI},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   337
    REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   338
    rtac ctxt @{thm equalityD2}, rtac ctxt (mk_nth_conv n i)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   339
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   340
fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
82248
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   341
  EVERY' [rtac ctxt @{thm equivI},
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   342
    rtac ctxt lsbis_incl,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   343
82248
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   344
    rtac ctxt @{thm refl_onI},
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   345
    rtac ctxt set_mp,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   346
    rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI},
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   347
82248
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   348
    rtac ctxt @{thm symI},
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   349
    rtac ctxt set_mp,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   350
    rtac ctxt incl_lsbis, rtac ctxt bis_converse, rtac ctxt sbis_lsbis, etac ctxt @{thm converseI},
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   351
82248
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   352
    rtac ctxt @{thm transI},
e8c96013ea8a changed definition of refl_on
desharna
parents: 75624
diff changeset
   353
    rtac ctxt set_mp,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   354
    rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   355
    etac ctxt @{thm relcompI}, assume_tac ctxt] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   356
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   357
fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   358
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   359
    val n = length strT_defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   360
    val ks = 1 upto n;
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   361
    fun coalg_tac (i, (active_sets, def)) =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   362
      EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   363
        hyp_subst_tac ctxt, rtac ctxt (def RS trans RS @{thm ssubst_mem}), etac ctxt (arg_cong RS trans),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   364
        rtac ctxt (mk_sum_caseN n i), rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   365
        REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   366
        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   367
          rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   368
          rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   369
          rtac ctxt conjI, etac ctxt @{thm empty_Shift}, dtac ctxt set_rev_mp,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   370
            etac ctxt @{thm equalityD1}, etac ctxt @{thm CollectD},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   371
          rtac ctxt @{thm ballI},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   372
            CONJ_WRAP' (fn i => EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm CollectE}, dtac ctxt @{thm ShiftD},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   373
              dtac ctxt @{thm bspec}, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   374
              dtac ctxt @{thm bspec}, rtac ctxt @{thm CollectI}, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   375
              REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   376
              rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   377
              rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   378
              CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   379
                rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   380
                rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   381
          dtac ctxt @{thm bspec}, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt @{thm bspec},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   382
          etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   383
          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   384
          rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   385
          etac ctxt (@{thm append_Nil} RS sym RS arg_cong RS trans),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   386
          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: 59498
diff changeset
   387
          CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   388
            rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   389
            rtac ctxt (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   390
  in
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   391
    unfold_thms_tac ctxt defs THEN
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   392
    CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   393
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   394
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   395
fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   396
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   397
    val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   398
    val ks = n downto 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   399
  in
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   400
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   401
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   402
      CONJ_WRAP' (fn Lev_0 =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   403
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   404
          etac ctxt @{thm singletonE}, etac ctxt ssubst, rtac ctxt @{thm list.size(3)}]) Lev_0s,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   405
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   406
      CONJ_WRAP' (fn Lev_Suc =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   407
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   408
          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   409
            (fn i =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   410
              EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   411
                rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   412
                REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   413
                etac ctxt mp, assume_tac ctxt]) ks])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   414
      Lev_Sucs] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   415
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   416
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   417
fun mk_length_Lev'_tac ctxt length_Lev =
60777
ee811a49c8f6 eliminated alias;
wenzelm
parents: 60757
diff changeset
   418
  EVERY' [forward_tac ctxt [length_Lev], etac ctxt ssubst, assume_tac ctxt] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   419
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   420
fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   421
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   422
    val n = length rv_Nils;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   423
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   424
  in
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   425
    EVERY' [rtac ctxt (Thm.instantiate' cTs cts @{thm list.induct}),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   426
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   427
      CONJ_WRAP' (fn rv_Cons =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   428
        CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac ctxt exI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   429
          rtac ctxt (@{thm append_Nil} RS arg_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   430
          rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans), rtac ctxt rv_Nil]))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   431
        (ks ~~ rv_Nils))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   432
      rv_Conss,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   433
      REPEAT_DETERM o rtac ctxt allI, rtac ctxt (mk_sumEN n),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   434
      EVERY' (map (fn i =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   435
        CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   436
          CONJ_WRAP' (fn i' => EVERY' [dtac ctxt (mk_conjunctN n i'), etac ctxt exE, rtac ctxt exI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   437
            rtac ctxt (@{thm append_Cons} RS arg_cong RS trans), rtac ctxt (rv_Cons RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   438
            if n = 1 then K all_tac else etac ctxt (sum_case_cong_weak RS trans),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   439
            rtac ctxt (mk_sum_caseN n i RS trans), assume_tac ctxt])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   440
          ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   441
        rv_Conss)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   442
      ks)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   443
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   444
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   445
fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   446
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   447
    val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   448
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   449
  in
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   450
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   451
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   452
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   453
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   454
          etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   455
          CONJ_WRAP' (fn i' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   456
            (if i = i'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   457
            then EVERY' [dtac ctxt (mk_InN_inject n i), hyp_subst_tac ctxt,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   458
              CONJ_WRAP' (fn (i'', Lev_0'') =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   459
                EVERY' [rtac ctxt impI, rtac ctxt @{thm ssubst_mem[OF append_Nil]},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   460
                  rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp), rtac ctxt (mk_UnIN n i''),
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   461
                  rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   462
                  etac ctxt conjI, rtac ctxt (Lev_0'' RS @{thm equalityD2} RS set_mp),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   463
                  rtac ctxt @{thm singletonI}])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   464
              (ks ~~ Lev_0s)]
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   465
            else etac ctxt (mk_InN_not_InM i' i RS notE)))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   466
          ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   467
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   468
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   469
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   470
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   471
          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   472
            (fn (i, from_to_sbd) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   473
              EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   474
                CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   475
                  CONJ_WRAP' (fn i'' =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   476
                    EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   477
                      rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   478
                      rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   479
                      rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   480
                      rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   481
                      etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   482
                      dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   483
                      dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   484
                      dtac ctxt (mk_conjunctN n i''), etac ctxt mp, assume_tac ctxt])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   485
                  ks)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   486
                ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   487
          (rev (ks ~~ from_to_sbds))])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   488
      ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   489
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   490
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   491
fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   492
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   493
    val n = length Lev_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   494
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   495
  in
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   496
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   497
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   498
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   499
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   500
          etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   501
          CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   502
            CONJ_WRAP' (fn i'' => rtac ctxt impI  THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   503
              (if i = i''
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   504
              then EVERY' [dtac ctxt @{thm ssubst_mem[OF sym[OF append_Nil]]},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   505
                dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp), dtac ctxt (mk_InN_inject n i),
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51782
diff changeset
   506
                hyp_subst_tac ctxt,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   507
                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   508
                  (fn k => REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   509
                    dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   510
                    (if k = i'
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   511
                    then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt @{thm imageI}]
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   512
                    else etac ctxt (mk_InN_not_InM i' k RS notE)))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   513
                (rev ks)]
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   514
              else etac ctxt (mk_InN_not_InM i'' i RS notE)))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   515
            ks)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   516
          ks])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   517
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   518
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   519
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   520
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   521
          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   522
            (fn (i, (from_to_sbd, to_sbd_inj)) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   523
              REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN' hyp_subst_tac ctxt THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   524
              CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   525
                dtac ctxt @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   526
                dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp) THEN'
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   527
                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE})) (fn k =>
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   528
                  REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   529
                  dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   530
                  (if k = i
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   531
                  then EVERY' [dtac ctxt (mk_InN_inject n i),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   532
                    dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   533
                    assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt] THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   534
                    CONJ_WRAP' (fn i'' =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   535
                      EVERY' [rtac ctxt impI, dtac ctxt (sym RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   536
                        rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS arg_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   537
                        etac ctxt (from_to_sbd RS arg_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   538
                        REPEAT_DETERM o etac ctxt allE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   539
                        dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   540
                        dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   541
                        dtac ctxt (mk_conjunctN n i''), etac ctxt mp, etac ctxt sym])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   542
                    ks
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   543
                  else etac ctxt (mk_InN_not_InM i k RS notE)))
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   544
                (rev ks))
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   545
              ks)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   546
          (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   547
      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   548
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   549
55577
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   550
fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   551
  from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Levs length_Lev's rv_lastss set_Levsss
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   552
  set_image_Levsss set_map0ss map_comp_ids map_cong0s =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   553
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   554
    val n = length beh_defs;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   555
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   556
55577
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   557
    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'),
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   558
      (rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   559
      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (carT_def RS @{thm equalityD2} RS set_mp),
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   560
        rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   561
        rtac ctxt conjI,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   562
          rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   563
          rtac ctxt @{thm singletonI},
55577
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   564
        (**)
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   565
          rtac ctxt @{thm ballI}, etac ctxt @{thm UN_E},
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   566
          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   567
            (set_Levs, set_image_Levs))))) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   568
            EVERY' [rtac ctxt @{thm ballI},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   569
              REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   570
              rtac ctxt (rev_mp OF [rv_last, impI]), etac ctxt exE, rtac ctxt (isNode_def RS iffD2),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   571
              rtac ctxt exI, rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   572
              if n = 1 then rtac ctxt refl
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   573
              else etac ctxt (sum_case_cong_weak RS trans) THEN' rtac ctxt (mk_sum_caseN n i),
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   574
              CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   575
                EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt @{thm equalityI}, rtac ctxt @{thm image_subsetI},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   576
                  rtac ctxt @{thm CollectI}, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, etac ctxt set_Lev,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   577
                  if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt @{thm subsetI},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   578
                  REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   579
                  REPEAT_DETERM_N 4 o etac ctxt thin_rl,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   580
                  rtac ctxt set_image_Lev,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   581
                  assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   582
                  etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   583
                  if n = 1 then rtac ctxt refl else assume_tac ctxt])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   584
              (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   585
          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   586
            (set_Levss ~~ set_image_Levss))))),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   587
        (*root isNode*)
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   588
          rtac ctxt (isNode_def RS iffD2), rtac ctxt exI, rtac ctxt conjI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   589
          CONVERSION (Conv.top_conv
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   590
            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   591
          if n = 1 then rtac ctxt refl else rtac ctxt (mk_sum_caseN n i),
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   592
          CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   593
            EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt @{thm equalityI}, rtac ctxt @{thm image_subsetI},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   594
              rtac ctxt @{thm CollectI}, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, rtac ctxt set_Lev,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   595
              rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   596
              assume_tac ctxt, rtac ctxt @{thm subsetI},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   597
              REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   598
              rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   599
              rtac ctxt @{thm singletonI}, dtac ctxt length_Lev',
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   600
              etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   601
                trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   602
              rtac ctxt rv_Nil])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   603
          (drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   604
55577
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   605
    fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)),
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   606
      ((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   607
      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   608
        CONVERSION (Conv.top_conv
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   609
          (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   610
        if n = 1 then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   611
        else (rtac ctxt (sum_case_cong_weak RS trans) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   612
          rtac ctxt (mk_sum_caseN n i) THEN' rtac ctxt (mk_sum_caseN n i RS trans)),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   613
        rtac ctxt (map_comp_id RS trans), rtac ctxt (map_cong0 OF replicate m refl),
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
   614
        EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   615
          DETERM o EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt prod_injectI, rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   616
            rtac ctxt trans, rtac ctxt @{thm Shift_def},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   617
            rtac ctxt @{thm equalityI}, rtac ctxt @{thm subsetI}, etac ctxt thin_rl,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   618
            REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE UN_E}, dtac ctxt length_Lev', dtac ctxt asm_rl,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   619
            etac ctxt thin_rl, dtac ctxt @{thm set_rev_mp[OF _ equalityD1]},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   620
            rtac ctxt (@{thm length_Cons} RS arg_cong RS trans), rtac ctxt Lev_Suc,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   621
            CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE})) (fn i'' =>
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   622
              EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   623
                dtac ctxt list_inject_iffD1, etac ctxt conjE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   624
                if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   625
                  dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   626
                  assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   627
                else etac ctxt (mk_InN_not_InM i' i'' RS notE)])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   628
            (rev ks),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   629
            rtac ctxt @{thm UN_least}, rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm UN_I[OF UNIV_I]},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   630
            rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt @{thm CollectI},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   631
            REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   632
            rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   633
            CONVERSION (Conv.top_conv
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   634
              (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   635
            if n = 1 then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   636
            else rtac ctxt sum_case_cong_weak THEN' rtac ctxt (mk_sum_caseN n i' RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   637
            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac ctxt refl])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   638
        ks to_sbd_injs from_to_sbds)];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   639
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   640
    (rtac ctxt mor_cong THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   641
    EVERY' (map (fn thm => rtac ctxt (thm RS @{thm ext})) beh_defs) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   642
    rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   643
    CONJ_WRAP' fbetw_tac
55577
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   644
      (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   645
        (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN'
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   646
    CONJ_WRAP' mor_tac
55577
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   647
      (ks ~~ (strT_defs ~~ ((Lev_Sucs ~~ (rv_Nils ~~ rv_Conss)) ~~
a6c2379078c8 simplifications of internal codatatype construction
traytel
parents: 55541
diff changeset
   648
        ((map_comp_ids ~~ map_cong0s) ~~
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   649
          (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   650
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   651
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   652
fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   653
  EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   654
    REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE bexE}, rtac ctxt (o_apply RS trans),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   655
    etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   656
    rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   657
    EVERY' (map (fn equiv_LSBIS =>
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   658
      EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, assume_tac ctxt])
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   659
    equiv_LSBISs), rtac ctxt sym, rtac ctxt (o_apply RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   660
    etac ctxt (sym RS arg_cong RS trans), rtac ctxt map_comp_id] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   661
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   662
fun mk_coalg_final_tac ctxt m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   663
  EVERY' [rtac ctxt (coalg_def RS iffD2),
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   664
    CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   665
      EVERY' [rtac ctxt @{thm univ_preserves}, rtac ctxt equiv_LSBIS, rtac ctxt congruent_str_final,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   666
        rtac ctxt @{thm ballI}, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   667
        REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   668
        CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   669
          EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   670
            rtac ctxt @{thm image_subsetI}, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   671
            rtac ctxt equiv_LSBIS, etac ctxt set_rev_mp, etac ctxt coalgT_set])
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   672
        (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   673
    ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   674
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   675
fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   676
  EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   677
    CONJ_WRAP' (fn equiv_LSBIS =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   678
      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   679
        rtac ctxt equiv_LSBIS, assume_tac ctxt])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   680
    equiv_LSBISs,
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   681
    CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   682
      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   683
        rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   684
    (equiv_LSBISs ~~ congruent_str_finals)] 1;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   685
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   686
fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   687
  unfold_thms_tac ctxt defs THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   688
  EVERY' [rtac ctxt conjI,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   689
    CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' rtac ctxt thm) Reps,
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   690
    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   691
      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   692
        EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   693
          EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   694
            etac ctxt set_rev_mp, rtac ctxt coalg_final_set, rtac ctxt Rep])
55541
fd9ea8ae28f6 syntactic simplifications of internal (co)datatype constructions
traytel
parents: 55414
diff changeset
   695
        Abs_inverses coalg_final_sets)])
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   696
    (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   697
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   698
fun mk_mor_Abs_tac ctxt defs Abs_inverses =
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   699
  unfold_thms_tac ctxt defs THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   700
  EVERY' [rtac ctxt conjI,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   701
    CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) Abs_inverses,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   702
    CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   703
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   704
fun mk_mor_unfold_tac ctxt m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   705
  EVERY' [rtac ctxt iffD2, rtac ctxt mor_UNIV,
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   706
    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   707
      EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (dtor_def RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   708
        rtac ctxt (unfold_def RS arg_cong RS trans), rtac ctxt (Abs_inverse RS arg_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   709
        rtac ctxt (morE RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   710
        rtac ctxt (o_apply RS trans RS sym), rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   711
        REPEAT_DETERM_N m o rtac ctxt refl,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   712
        EVERY' (map (fn thm => rtac ctxt (thm RS trans) THEN' rtac ctxt (o_apply RS sym)) unfold_defs)])
51761
4c9f08836d87 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet
parents: 51739
diff changeset
   713
    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   714
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   715
fun mk_raw_coind_tac ctxt bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   716
  sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   717
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   718
    val n = length Rep_injects;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   719
  in
60777
ee811a49c8f6 eliminated alias;
wenzelm
parents: 60757
diff changeset
   720
    EVERY' [rtac ctxt rev_mp, forward_tac ctxt [bis_def RS iffD1],
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   721
      REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   722
      rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   723
      rtac ctxt bis_Gr, rtac ctxt tcoalg,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   724
      rtac ctxt mor_Rep, REPEAT_DETERM_N n o etac ctxt @{thm relImage_Gr},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   725
      rtac ctxt impI, rtac ctxt rev_mp, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_Gr, rtac ctxt coalgT,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   726
      rtac ctxt mor_T_final, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt bis_converse, rtac ctxt bis_Gr, rtac ctxt coalgT,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   727
      rtac ctxt mor_T_final, EVERY' (map (fn thm => rtac ctxt (thm RS @{thm relInvImage_Gr})) lsbis_incls),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   728
      rtac ctxt impI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   729
      CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   730
        EVERY' [rtac ctxt @{thm subset_trans}, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt @{thm subset_trans},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   731
          rtac ctxt @{thm relInvImage_mono}, rtac ctxt @{thm subset_trans}, etac ctxt incl_lsbis,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   732
          rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   733
          rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   734
          rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   735
          rtac ctxt @{thm subset_trans}, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   736
          rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   737
          rtac ctxt Rep_inject])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   738
      (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   739
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   740
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   741
fun mk_unfold_unique_mor_tac ctxt raw_coinds bis mor unfold_defs =
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   742
  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   743
    EVERY' [rtac ctxt @{thm ext}, etac ctxt (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac ctxt mor,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   744
      rtac ctxt @{thm image2_eqI}, rtac ctxt refl, rtac ctxt (unfold_def RS arg_cong RS trans),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   745
      rtac ctxt (o_apply RS sym), rtac ctxt @{thm UNIV_I}]) (raw_coinds ~~ unfold_defs) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   746
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   747
fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   748
  unfold_thms_tac ctxt [ctor_def] THEN 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: 59498
diff changeset
   749
    rtac ctxt trans, rtac ctxt unfold, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   750
    EVERY' (map (fn thm =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   751
      rtac ctxt @{thm ballI} THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   752
    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
   753
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   754
fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   755
  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac ctxt trans, rtac ctxt (o_apply RS arg_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   756
    rtac ctxt trans, rtac ctxt unfold, fo_rtac ctxt (@{thm sum.case(2)} RS arg_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   757
    rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt refl,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   758
    EVERY' (map (fn thm => rtac ctxt @{thm case_sum_expand_Inr} THEN' rtac ctxt thm) corec_Inls)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   759
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   760
fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51447
diff changeset
   761
  unfold_thms_tac ctxt
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55393
diff changeset
   762
    (corec_defs @ map (fn thm => thm RS @{thm case_sum_expand_Inr'}) corec_Inls) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   763
  etac ctxt unfold_unique_mor 1;
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51447
diff changeset
   764
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   765
fun mk_dtor_coinduct_tac ctxt m raw_coind bis_rel rel_congs =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   766
  EVERY' [rtac ctxt rev_mp, rtac ctxt raw_coind, rtac ctxt iffD2, rtac ctxt bis_rel, rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   767
    CONJ_WRAP' (K (rtac ctxt @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   768
    rel_congs,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   769
    CONJ_WRAP' (fn rel_cong => EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   770
      REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   771
      REPEAT_DETERM_N m o rtac ctxt refl,
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 60801
diff changeset
   772
      REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   773
      etac ctxt mp, etac ctxt @{thm CollectE}, etac ctxt @{thm case_prodD}])
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   774
    rel_congs,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   775
    rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   776
    CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   777
      rtac ctxt @{thm CollectI}, etac ctxt @{thm case_prodI}])) rel_congs] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   778
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   779
fun mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0 =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   780
  EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (o_apply RS trans RS sym),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   781
    rtac ctxt (unfold RS trans), rtac ctxt (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   782
    rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   783
    REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   784
    REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   785
    rtac ctxt map_arg_cong, rtac ctxt (o_apply RS sym)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   786
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   787
fun mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   788
  EVERY' [rtac ctxt Jset_minimal,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   789
    REPEAT_DETERM_N n o rtac ctxt @{thm Un_upper1},
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   790
    REPEAT_DETERM_N n o
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
   791
      EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   792
        EVERY' [rtac ctxt @{thm subsetI}, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   793
          etac ctxt @{thm UnE}, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt @{thm UnE},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   794
          EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)])
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   795
      (1 upto n) set_Jsets set_Jset_Jsetss)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   796
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   797
fun mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   798
  EVERY' [rtac ctxt @{thm Un_least}, rtac ctxt set_incl_Jset,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   799
    REPEAT_DETERM_N (n - 1) o rtac ctxt @{thm Un_least},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   800
    EVERY' (map (fn thm => rtac ctxt @{thm UN_least} THEN' etac ctxt thm) set_Jset_incl_Jsets)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   801
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   802
fun mk_map_id0_tac ctxt maps unfold_unique unfold_dtor =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   803
  EVERY' [rtac ctxt (unfold_unique RS trans), EVERY' (map (rtac ctxt o mk_sym) maps),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   804
    rtac ctxt unfold_dtor] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   805
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   806
fun mk_map_comp0_tac ctxt maps map_comp0s map_unique =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   807
  EVERY' [rtac ctxt map_unique,
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   808
    EVERY' (map2 (fn map_thm => fn map_comp0 =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   809
      EVERY' (map (rtac ctxt)
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   810
        [@{thm comp_assoc[symmetric]} RS trans,
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   811
        @{thm arg_cong2[of _ _ _ _ "(\<circ>)"]} OF [map_thm, refl] RS trans,
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   812
        @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans,
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   813
        @{thm comp_assoc[symmetric]} RS trans,
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   814
        @{thm arg_cong2[of _ _ _ _ "(\<circ>)"]} OF [map_comp0 RS sym, refl]]))
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   815
    maps map_comp0s)] 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   816
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   817
fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   818
  set_Jset_Jsetsss in_rels =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   819
  let
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   820
    val n = length map_comps;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   821
    val ks = 1 upto n;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   822
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   823
    EVERY' ([rtac ctxt rev_mp, coinduct_tac] @
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   824
      maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets),
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   825
        set_Jset_Jsetss), in_rel) =>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   826
        [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   827
         REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], hyp_subst_tac ctxt, rtac ctxt exI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   828
         rtac ctxt (Drule.rotate_prems 1 conjI),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   829
         rtac ctxt conjI, rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   830
         REPEAT_DETERM_N m o (rtac ctxt o_apply_trans_sym THEN' rtac ctxt @{thm fst_conv}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   831
         REPEAT_DETERM_N n o rtac ctxt fst_convol_fun_cong_sym,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   832
         rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0,
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   833
         EVERY' (maps (fn set_Jset =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   834
           [rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt @{thm CollectE},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   835
           REPEAT_DETERM o etac ctxt conjE, etac ctxt @{thm bspec}, etac ctxt set_Jset]) set_Jsets),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   836
         REPEAT_DETERM_N n o rtac ctxt snd_convol_fun_cong_sym,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   837
         rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   838
         EVERY' (map (fn set_map0 => EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   839
           rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI}, rtac ctxt refl])
55644
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
   840
        (take m set_map0s)),
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   841
         CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   842
           EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   843
             rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   844
             rtac ctxt @{thm CollectI}, etac ctxt @{thm CollectE},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   845
             REPEAT_DETERM o etac ctxt conjE,
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   846
             CONJ_WRAP' (fn set_Jset_Jset =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   847
               EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm bspec}, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   848
             rtac ctxt (conjI OF [refl, refl])])
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   849
           (drop m set_map0s ~~ set_Jset_Jsetss)])
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   850
        (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
56179
6b5c46582260 tuned internal construction
traytel
parents: 56114
diff changeset
   851
          map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   852
      [rtac ctxt impI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   853
       CONJ_WRAP' (fn k =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   854
         EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   855
           rtac ctxt conjI, rtac ctxt refl, 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
   856
  end
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   857
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   858
fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   859
  rtac ctxt unfold_unique 1 THEN
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   860
  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   861
  ALLGOALS (etac ctxt sym);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   862
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   863
fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   864
  let
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49516
diff changeset
   865
    val n = length dtor_maps;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   866
  in
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   867
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   868
      REPEAT_DETERM o rtac ctxt allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   869
      CONJ_WRAP' (K (rtac ctxt @{thm image_empty})) rec_0s,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   870
      REPEAT_DETERM o rtac ctxt allI,
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49516
diff changeset
   871
      CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   872
        [SELECT_GOAL (unfold_thms_tac ctxt
49541
32fb6e4c7f4b renamed "map_simps" to "{c,d}tor_maps"
blanchet
parents: 49516
diff changeset
   873
          (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   874
        rtac ctxt Un_cong, rtac ctxt refl,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   875
        CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong))
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   876
          (fn i => EVERY' [rtac ctxt @{thm SUP_cong[OF refl]},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   877
            REPEAT_DETERM o etac ctxt allE, etac ctxt (mk_conjunctN n i)]) (n downto 1)])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   878
      (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   879
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   880
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   881
fun mk_set_map0_tac ctxt col_natural =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   882
  EVERY' (map (rtac ctxt) [@{thm ext}, o_apply RS trans, sym, o_apply RS trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   883
    @{thm image_UN} RS trans, refl RS @{thm SUP_cong}, col_natural]) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   884
75624
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   885
fun mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_regularCard sbd_Cinfinite set_sbdss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   886
  let
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   887
    val n = length rec_0s;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   888
  in
60801
7664e0916eec tuned signature;
wenzelm
parents: 60777
diff changeset
   889
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   890
      REPEAT_DETERM o rtac ctxt allI,
75624
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   891
      CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [@{thm ordIso_ordLess_trans},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   892
        @{thm card_of_ordIso_subst}, rec_0, @{thm Cinfinite_gt_empty}, sbd_Cinfinite])) rec_0s,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   893
      REPEAT_DETERM o rtac ctxt allI,
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   894
      CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
75624
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   895
        [rtac ctxt @{thm ordIso_ordLess_trans}, rtac ctxt @{thm card_of_ordIso_subst},
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   896
        rtac ctxt rec_Suc, rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})),
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   897
        rtac ctxt (nth set_sbds (j - 1)),
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   898
        REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})),
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   899
        EVERY' (map2 (fn i => fn set_sbd => EVERY' [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   900
          rtac ctxt (@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [sbd_regularCard,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   901
          sbd_Cinfinite]), rtac ctxt set_sbd, rtac ctxt @{thm ballI}, REPEAT_DETERM o etac ctxt allE,
75624
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   902
          etac ctxt (mk_conjunctN n i)]) (1 upto n) (drop m set_sbds))])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   903
      (rec_Sucs ~~ set_sbdss)] 1
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   904
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   905
75624
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   906
fun mk_set_bd_tac ctxt sbd_Cinfinite sbd_regularCard natLeq_ordLess_bd col_bd =
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   907
  EVERY' (map (rtac ctxt) [@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [
22d1c5f2b9f4 strict bounds for BNFs (by Jan van Brügge)
traytel
parents: 67399
diff changeset
   908
    sbd_regularCard, sbd_Cinfinite], @{thm ordIso_ordLess_trans}, @{thm card_of_nat},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   909
    natLeq_ordLess_bd, @{thm ballI}, col_bd]) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   910
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   911
fun mk_le_rel_OO_tac ctxt coinduct rel_Jrels le_rel_OOs =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   912
  EVERY' (rtac ctxt coinduct :: map2 (fn rel_Jrel => fn le_rel_OO =>
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   913
    let val Jrel_imp_rel = rel_Jrel RS iffD1;
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   914
    in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   915
      EVERY' [rtac ctxt (le_rel_OO RS @{thm predicate2D}), etac ctxt @{thm relcomppE},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   916
      rtac ctxt @{thm relcomppI}, etac ctxt Jrel_imp_rel, etac ctxt Jrel_imp_rel]
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54793
diff changeset
   917
    end)
57726
18b8a8f10313 simplified tactics slightly
traytel
parents: 56765
diff changeset
   918
  rel_Jrels le_rel_OOs) 1;
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   919
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   920
fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   921
  ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   922
  REPEAT_DETERM (assume_tac ctxt 1 ORELSE
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   923
    EVERY' [dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt dtor_set,
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   924
    K (unfold_thms_tac ctxt dtor_ctors),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   925
    REPEAT_DETERM_N n o etac ctxt @{thm UnE},
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   926
    REPEAT_DETERM o
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   927
      (TRY o REPEAT_DETERM o etac ctxt @{thm 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
   928
        (eresolve_tac ctxt wit ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
   929
        (dresolve_tac ctxt wit THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   930
          (etac ctxt FalseE ORELSE'
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   931
          EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt dtor_set,
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   932
            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac ctxt @{thm UnE}]))))] 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   933
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
   934
fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   935
  rtac ctxt induct 1 THEN ALLGOALS (TRY o rtac ctxt impI THEN' TRY o hyp_subst_tac ctxt) THEN
49504
df9b897fb254 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents: 49501
diff changeset
   936
  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   937
  ALLGOALS (REPEAT_DETERM o etac ctxt @{thm imageE} THEN' TRY o hyp_subst_tac ctxt) THEN
49104
6defdacd595a generate coinductive witnesses for codatatypes
traytel
parents: 49091
diff changeset
   938
  ALLGOALS (TRY o
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   939
    FIRST' [rtac ctxt TrueI, rtac ctxt refl, etac ctxt (refl RSN (2, mp)), dresolve_tac ctxt wits THEN' etac ctxt FalseE]);
58445
86b5b02ef33a generate 'dtor_corec_transfer' for codatatypes
desharna
parents: 57983
diff changeset
   940
86b5b02ef33a generate 'dtor_corec_transfer' for codatatypes
desharna
parents: 57983
diff changeset
   941
fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers
86b5b02ef33a generate 'dtor_corec_transfer' for codatatypes
desharna
parents: 57983
diff changeset
   942
    dtor_rels =
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58445
diff changeset
   943
  CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   944
      REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58445
diff changeset
   945
      unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   946
      HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN'
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58445
diff changeset
   947
        EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   948
          etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   949
          rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   950
          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: 59498
diff changeset
   951
          REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   952
          REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   953
          rtac ctxt rel_funI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   954
          etac ctxt (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   955
        etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer})))
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58445
diff changeset
   956
    (dtor_corec_defs ~~ dtor_unfold_transfer);
49104
6defdacd595a generate coinductive witnesses for codatatypes
traytel
parents: 49091
diff changeset
   957
53287
271b34513bfb renamed BNF axiom
blanchet
parents: 53285
diff changeset
   958
fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   959
    dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   960
  let
49544
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   961
    val m = length dtor_set_incls;
24094fa47e0d renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents: 49543
diff changeset
   962
    val n = length dtor_set_set_inclss;
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   963
    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: 51850
diff changeset
   964
    val in_Jrel = nth in_Jrels (i - 1);
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   965
    val if_tac =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   966
      EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   967
        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   968
        EVERY' (map2 (fn set_map0 => fn set_incl =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   969
          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: 59498
diff changeset
   970
            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: 59498
diff changeset
   971
            etac ctxt (set_incl RS @{thm subset_trans})])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   972
        passive_set_map0s dtor_set_incls),
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   973
        CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   974
          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   975
            rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   976
            CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   977
            rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   978
        (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   979
        CONJ_WRAP' (fn conv =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   980
          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: 59498
diff changeset
   981
          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: 59498
diff changeset
   982
          REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   983
          rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt])
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   984
        @{thms fst_conv snd_conv}];
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   985
    val only_if_tac =
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   986
      EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   987
        rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
   988
        CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   989
          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   990
            rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   991
            rtac ctxt (dtor_ctor RS sym RS arg_cong), 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: 59498
diff changeset
   992
            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: 59498
diff changeset
   993
              (fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   994
                rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   995
                rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   996
                dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt @{thm imageE},
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 60801
diff changeset
   997
                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   998
                REPEAT_DETERM o eresolve_tac ctxt
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
   999
                  @{thms CollectE conjE 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: 51850
diff changeset
  1000
                hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1001
                dtac ctxt (in_Jrel RS iffD1),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1002
                dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1003
                REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, assume_tac ctxt])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1004
            (rev (active_set_map0s ~~ in_Jrels))])
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1005
        (dtor_sets ~~ passive_set_map0s),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1006
        rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1007
        REPEAT_DETERM_N 2 o EVERY'[rtac ctxt (dtor_inject RS iffD1), rtac ctxt trans, rtac ctxt dtor_map,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1008
          rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1009
          rtac ctxt map_cong0, 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
  1010
          EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 60801
diff changeset
  1011
            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1012
            REPEAT_DETERM o eresolve_tac ctxt
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1013
              @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1014
            hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1015
            dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels),
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1016
          assume_tac ctxt]]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1017
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1018
    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
  1019
  end;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1020
58445
86b5b02ef33a generate 'dtor_corec_transfer' for codatatypes
desharna
parents: 57983
diff changeset
  1021
fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
55644
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1022
  dtor_unfolds dtor_maps in_rels =
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1023
  let
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1024
    val n = length ks;
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1025
    val fst_diag_nth = if fst then @{thm fst_diag_fst} else @{thm fst_diag_snd};
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1026
    val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd};
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1027
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1028
    EVERY' [rtac ctxt coinduct,
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
  1029
      EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
55644
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1030
          fn dtor_unfold => fn dtor_map => fn in_rel =>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
  1031
        EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58634
diff changeset
  1032
          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1033
          select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1034
          REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1035
          rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1036
          rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1037
          rtac ctxt (dtor_unfold RS map_arg_cong RS trans), rtac ctxt (trans OF [map_comp0, map_cong]),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1038
          REPEAT_DETERM_N m o rtac ctxt (fst_diag_nth RS @{thm fun_cong[OF trans[OF o_id sym]]}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1039
          REPEAT_DETERM_N n o (rtac ctxt @{thm sym[OF trans[OF o_apply]]} THEN' rtac ctxt @{thm fst_conv}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1040
          rtac ctxt (map_comp0 RS trans), rtac ctxt (map_cong RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1041
          REPEAT_DETERM_N m o rtac ctxt (snd_diag_nth RS fun_cong),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1042
          REPEAT_DETERM_N n o (rtac ctxt @{thm trans[OF o_apply]} THEN' rtac ctxt @{thm snd_conv}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1043
          etac ctxt (@{thm prod.case} RS map_arg_cong RS trans),
55644
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1044
          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1045
          rtac ctxt @{thm CollectI},
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1046
          CONJ_WRAP' (fn set_map0 =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1047
            EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1048
              rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1049
              FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1050
                assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
55644
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1051
          set_map0s])
b657146dc030 only one internal coinduction rule
traytel
parents: 55642
diff changeset
  1052
      ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1053
  end;
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1054
55642
63beb38e9258 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents: 55606
diff changeset
  1055
val split_id_unfolds = @{thms prod.case image_id id_apply};
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1056
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1057
fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1058
  let val n = length ks;
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1059
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1060
    rtac ctxt set_induct 1 THEN
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
  1061
    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1062
      EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1063
        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1064
        REPEAT_DETERM o eresolve_tac ctxt [@{thm CollectE}, @{thm conjE}, Collect_splitD_set_mp, set_rev_mp],
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1065
        hyp_subst_tac ctxt,
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1066
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1067
        rtac ctxt @{thm subset_refl}])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1068
    unfolds set_map0ss ks) 1 THEN
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58446
diff changeset
  1069
    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1070
      EVERY' (map (fn set_map0 =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1071
        EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1072
        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1073
        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, hyp_subst_tac ctxt,
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1074
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1075
        etac ctxt @{thm imageE}, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1076
        rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1077
        rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1078
      (drop m set_map0s)))
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
  1079
    unfolds set_map0ss ks) 1
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1080
  end;
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1081
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55067
diff changeset
  1082
fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1083
  let val n = length in_rels;
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1084
  in
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 61424
diff changeset
  1085
    Method.insert_tac ctxt CIHs 1 THEN
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1086
    unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1087
    REPEAT_DETERM (etac ctxt exE 1) THEN
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1088
    CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1089
      EVERY' [rtac ctxt @{thm predicate2I}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1090
        if null helper_inds then rtac ctxt @{thm UNIV_I}
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1091
        else rtac ctxt @{thm CollectI} THEN'
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1092
          CONJ_WRAP' (fn helper_ind =>
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1093
            EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1094
              REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI,
82630
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1095
              REPEAT_DETERM o resolve_tac ctxt @{thms subsetI CollectI iffD2[OF split_beta]},
2bb4a8d0111d dropped unused ML bindings
haftmann
parents: 82248
diff changeset
  1096
              dtac ctxt @{thm bspec}, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1097
              etac ctxt (refl RSN (2, conjI))])
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1098
          helper_inds,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1099
        rtac ctxt conjI,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1100
        rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1101
        REPEAT_DETERM_N n o etac ctxt thin_rl,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1102
        rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI)),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1103
        rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
  1104
        REPEAT_DETERM_N n o etac ctxt thin_rl,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1105
        rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI))])
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1106
    (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1107
  end;
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51893
diff changeset
  1108
55901
8c6d49dd8ae1 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents: 55644
diff changeset
  1109
fun mk_unfold_transfer_tac ctxt m ctor_rel_coinduct map_transfers unfolds =
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1110
  let
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1111
    val n = length map_transfers;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1112
  in
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1113
    unfold_thms_tac ctxt
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55901
diff changeset
  1114
      @{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
  1115
    unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1116
    HEADGOAL (EVERY'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1117
      [REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_coinduct,
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1118
      EVERY' (map (fn map_transfer => EVERY'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1119
        [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt @{thm image2pE}, hyp_subst_tac ctxt,
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1120
        SELECT_GOAL (unfold_thms_tac ctxt unfolds),
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1121
        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: 59498
diff changeset
  1122
        REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1123
        REPEAT_DETERM_N n o rtac ctxt @{thm rel_fun_image2p},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
  1124
        etac ctxt @{thm predicate2D}, etac ctxt @{thm image2pI}])
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1125
      map_transfers)])
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1126
  end;
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52659
diff changeset
  1127
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
  1128
end;