src/HOL/Tools/BNF/bnf_def_tactics.ML
author traytel
Mon, 18 Dec 2017 11:56:12 +0100
changeset 67223 711eec20aecd
parent 67222 19809bc9d7ff
child 67399 eab6ce8368fa
permissions -rw-r--r--
removed debug output
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_def_tactics.ML
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
57668
blanchet
parents: 56903
diff changeset
     4
    Author:     Martin Desharnais, TU Muenchen
62324
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
     5
    Author:     Ondrej Kuncar, TU Muenchen
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
     6
    Copyright   2012, 2013, 2014, 2015
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
     7
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
     8
Tactics for definition of bounded natural functors.
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
     9
*)
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    10
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    11
signature BNF_DEF_TACTICS =
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    12
sig
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    13
  val mk_collect_set_map_tac: Proof.context -> thm list -> tactic
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    14
  val mk_in_mono_tac: Proof.context -> int -> tactic
57970
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    15
  val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    16
  val mk_inj_map_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
    17
  val mk_map_id: thm -> thm
56903
69b6369a98fa generate 'map_ident' theorem for BNFs
desharna
parents: 56635
diff changeset
    18
  val mk_map_ident: Proof.context -> thm -> thm
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
    19
  val mk_map_comp: thm -> thm
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51766
diff changeset
    20
  val mk_map_cong_tac: Proof.context -> thm -> tactic
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
    21
  val mk_set_map: thm -> thm
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    22
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
    23
  val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    24
  val mk_rel_eq_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
    25
  val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    26
  val mk_rel_conversep_tac: Proof.context -> thm -> thm -> tactic
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
    27
  val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
57932
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
    28
  val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    29
  val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic
57967
e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0'
desharna
parents: 57932
diff changeset
    30
  val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
61242
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
    31
  val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic
62324
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
    32
  val mk_rel_eq_onp_tac: Proof.context -> thm -> thm -> thm -> tactic
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
    33
  val mk_pred_mono_strong0_tac: Proof.context -> thm -> thm -> tactic
63714
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63399
diff changeset
    34
  val mk_pred_mono_tac: Proof.context -> thm -> thm -> tactic
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
    35
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
    36
  val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
62329
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
    37
  val mk_pred_transfer_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
    38
  val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
    39
  val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52659
diff changeset
    40
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
    41
  val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
    42
    thm -> thm -> thm -> thm -> tactic
54189
c0186a0d8cb3 define a trivial nonemptiness witness if none is provided
traytel
parents: 53562
diff changeset
    43
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
    44
  val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    45
end;
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    46
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    47
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    48
struct
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    49
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    50
open BNF_Util
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    51
open BNF_Tactics
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    52
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
    53
val ord_eq_le_trans = @{thm ord_eq_le_trans};
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
    54
val ord_le_eq_trans = @{thm ord_le_eq_trans};
52749
ed416f4ac34e more converse(p) theorems; tuned proofs;
traytel
parents: 52731
diff changeset
    55
val conversep_shift = @{thm conversep_le_swap} RS iffD1;
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
    56
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
    57
fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
56903
69b6369a98fa generate 'map_ident' theorem for BNFs
desharna
parents: 56635
diff changeset
    58
fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def};
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
    59
fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 51766
diff changeset
    60
fun mk_map_cong_tac ctxt cong0 =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    61
  (hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
    62
   REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1;
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
    63
fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest};
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
    64
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
    65
fun mk_in_mono_tac ctxt n =
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
    66
  if n = 0 then rtac ctxt subset_UNIV 1
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
    67
  else
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
    68
   (rtac ctxt @{thm subsetI} THEN' rtac ctxt @{thm CollectI}) 1 THEN
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
    69
   REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) THEN
60757
c09598a97436 prefer tactics with explicit context;
wenzelm
parents: 60752
diff changeset
    70
   REPEAT_DETERM_N (n - 1)
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
    71
     ((rtac ctxt conjI THEN' etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1) THEN
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
    72
   (etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1;
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
    73
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    74
fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
56635
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55990
diff changeset
    75
  let
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55990
diff changeset
    76
    val map_cong' = map_cong OF (asm_rl :: replicate n refl);
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55990
diff changeset
    77
    val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id});
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55990
diff changeset
    78
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    79
    HEADGOAL (rtac ctxt @{thm injI} THEN' etac ctxt (map_cong' RS box_equals) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    80
      REPEAT_DETERM_N 2 o (rtac ctxt (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
    81
        REPEAT_DETERM_N n o assume_tac ctxt))
56635
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55990
diff changeset
    82
  end;
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55990
diff changeset
    83
57970
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    84
fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    85
  let
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    86
    val rel_eq' = rel_eq RS @{thm predicate2_eqD};
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    87
    val rel_maps' = map (fn thm => thm RS iffD1) rel_maps;
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    88
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    89
    HEADGOAL (dtac ctxt (rel_eq' RS iffD2) THEN' rtac ctxt (rel_eq' RS iffD1)) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    90
    EVERY (map (HEADGOAL o dtac ctxt) rel_maps') THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    91
    HEADGOAL (etac ctxt rel_mono_strong) THEN
57970
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    92
    TRYALL (Goal.assume_rule_tac ctxt)
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    93
  end;
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
    94
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    95
fun mk_collect_set_map_tac ctxt set_map0s =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    96
  (rtac ctxt (@{thm collect_comp} RS trans) THEN' rtac ctxt @{thm arg_cong[of _ _ collect]} THEN'
53289
5e0623448bdb renamed BNF axiom
blanchet
parents: 53288
diff changeset
    97
  EVERY' (map (fn set_map0 =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    98
    rtac ctxt (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
    99
    rtac ctxt set_map0) set_map0s) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   100
  rtac ctxt @{thm image_empty}) 1;
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   101
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
   102
fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   103
  let
54792
traytel
parents: 54189
diff changeset
   104
    val n = length set_maps;
61760
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   105
    val rel_OO_Grps_tac =
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   106
      if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans);
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   107
  in
54792
traytel
parents: 54189
diff changeset
   108
    if null set_maps then
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 52986
diff changeset
   109
      unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
62617
b5ec623952d2 strengthened tactics
blanchet
parents: 62329
diff changeset
   110
      resolve_tac ctxt @{thms refl Grp_UNIV_idI[OF refl]} 1
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   111
    else
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   112
      EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   113
        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
61760
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   114
        hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp,
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   115
          rtac ctxt map_cong0,
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   116
        REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD},
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   117
          etac ctxt @{thm set_mp}, assume_tac ctxt],
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   118
        rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   119
        CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61242
diff changeset
   120
          rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   121
          etac ctxt @{thm set_mp}, assume_tac ctxt])
54792
traytel
parents: 54189
diff changeset
   122
        set_maps,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   123
        rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE],
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51798
diff changeset
   124
        hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   125
        rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
53270
c8628119d18e renamed BNF axiom
blanchet
parents: 52986
diff changeset
   126
        EVERY' (map2 (fn convol => fn map_id0 =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   127
          EVERY' [rtac ctxt @{thm GrpI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   128
            rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   129
            REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong),
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   130
            REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   131
            rtac ctxt @{thm CollectI},
49495
675b9df572df rel_Gr does not depend on map_wpull
traytel
parents: 49490
diff changeset
   132
            CONJ_WRAP' (fn thm =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   133
              EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   134
                rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt])
54792
traytel
parents: 54189
diff changeset
   135
            set_maps])
53285
f09645642984 renamed BNF fact
blanchet
parents: 53270
diff changeset
   136
          @{thms fst_convol snd_convol} [map_id, refl])] 1
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   137
  end;
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   138
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   139
fun mk_rel_eq_tac ctxt n rel_Grp rel_cong map_id0 =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   140
  (EVERY' (rtac ctxt (rel_cong RS trans) :: replicate n (rtac ctxt @{thm eq_alt})) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   141
  rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
62617
b5ec623952d2 strengthened tactics
blanchet
parents: 62329
diff changeset
   142
  (if n = 0 then SELECT_GOAL (unfold_thms_tac ctxt (no_refl [map_id0])) THEN' rtac ctxt refl
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   143
  else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]},
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   144
    rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV,
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   145
    rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   146
    CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1;
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   147
57932
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   148
fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id =
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   149
  if live = 0 then
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   150
    HEADGOAL (Goal.conjunction_tac) THEN
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   151
    unfold_thms_tac ctxt @{thms id_apply} THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   152
    ALLGOALS (rtac ctxt refl)
57932
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   153
  else
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   154
    let
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   155
      val ks = 1 upto live;
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   156
    in
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   157
      Goal.conjunction_tac 1 THEN
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   158
      unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   159
      TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   160
        resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
61760
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   161
        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI},
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
   162
        assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   163
        resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   164
        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58446
diff changeset
   165
        REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   166
        dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
57932
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   167
    end;
c29659f77f8d generate 'rel_map' theorem for BNFs
desharna
parents: 57668
diff changeset
   168
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   169
fun mk_rel_mono_tac ctxt rel_OO_Grps in_mono =
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   170
  let
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   171
    val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   172
      else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   173
        rtac ctxt (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans));
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   174
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   175
    EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm relcompp_mono}, rtac ctxt @{thm iffD2[OF conversep_mono]},
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61242
diff changeset
   176
      rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono},
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61242
diff changeset
   177
      rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}] 1
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   178
  end;
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   179
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
   180
fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   181
  let
54792
traytel
parents: 54189
diff changeset
   182
    val n = length set_maps;
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   183
    val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   184
      else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   185
        rtac ctxt (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans));
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   186
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   187
    if null set_maps then rtac ctxt (rel_eq RS @{thm leq_conversepI}) 1
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   188
    else
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   189
      EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51798
diff changeset
   190
        REPEAT_DETERM o
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   191
          eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   192
        hyp_subst_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   193
        EVERY' (map (fn thm => EVERY' [rtac ctxt @{thm GrpI}, rtac ctxt sym, rtac ctxt trans,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   194
          rtac ctxt map_cong0, REPEAT_DETERM_N n o rtac ctxt thm,
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   195
          rtac ctxt (map_comp RS sym), rtac ctxt @{thm CollectI},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   196
          CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   197
            etac ctxt @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   198
  end;
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   199
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   200
fun mk_rel_conversep_tac ctxt le_conversep rel_mono =
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   201
  EVERY' [rtac ctxt @{thm antisym}, rtac ctxt le_conversep, rtac ctxt @{thm xt1(6)}, rtac ctxt conversep_shift,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   202
    rtac ctxt le_conversep, rtac ctxt @{thm iffD2[OF conversep_mono]}, rtac ctxt rel_mono,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   203
    REPEAT_DETERM o rtac ctxt @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   204
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
   205
fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   206
  let
54792
traytel
parents: 54189
diff changeset
   207
    val n = length set_maps;
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   208
    fun in_tac nthO_in = rtac ctxt @{thm CollectI} THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   209
        CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   210
          rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps;
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   211
    val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   212
      else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   213
        rtac ctxt (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54792
diff changeset
   214
          (2, ord_le_eq_trans));
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   215
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   216
    if null set_maps then rtac ctxt (rel_eq RS @{thm leq_OOI}) 1
52844
66fa0f602cc4 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
traytel
parents: 52813
diff changeset
   217
    else
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   218
      EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   219
        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51798
diff changeset
   220
        hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   221
        rtac ctxt @{thm relcomppI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   222
        rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   223
        REPEAT_DETERM_N n o rtac ctxt @{thm fst_fstOp},
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51798
diff changeset
   224
        in_tac @{thm fstOp_in},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   225
        rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   226
        REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply,
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   227
          rtac ctxt @{thm ballE}, rtac ctxt subst,
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   228
          rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   229
          etac ctxt notE, etac ctxt set_mp, assume_tac ctxt],
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51798
diff changeset
   230
        in_tac @{thm fstOp_in},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   231
        rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   232
        rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   233
        REPEAT_DETERM_N n o rtac ctxt o_apply,
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51798
diff changeset
   234
        in_tac @{thm sndOp_in},
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   235
        rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   236
        REPEAT_DETERM_N n o rtac ctxt @{thm snd_sndOp},
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54792
diff changeset
   237
        in_tac @{thm sndOp_in}] 1
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   238
  end;
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   239
57967
e6d2e998c30f renamed 'rel_mono_strong' to 'rel_mono_strong0'
desharna
parents: 57932
diff changeset
   240
fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   241
  if null set_maps then assume_tac ctxt 1
51916
eac9e9a45bf5 stronger monotonicity property for relators
traytel
parents: 51915
diff changeset
   242
  else
54998
8601434fa334 tuned signature;
wenzelm
parents: 54841
diff changeset
   243
    unfold_tac ctxt [in_rel] THEN
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   244
    REPEAT_DETERM (eresolve_tac ctxt @{thms exE CollectE conjE} 1) THEN
51916
eac9e9a45bf5 stronger monotonicity property for relators
traytel
parents: 51915
diff changeset
   245
    hyp_subst_tac ctxt 1 THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   246
    EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]},
55163
a740f312d9e4 made tactic more robust
traytel
parents: 55067
diff changeset
   247
      CONJ_WRAP' (fn thm =>
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   248
        (etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' assume_tac ctxt))
55163
a740f312d9e4 made tactic more robust
traytel
parents: 55067
diff changeset
   249
      set_maps] 1;
51916
eac9e9a45bf5 stronger monotonicity property for relators
traytel
parents: 51915
diff changeset
   250
58104
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57970
diff changeset
   251
fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong =
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57970
diff changeset
   252
  let
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57970
diff changeset
   253
    fun last_tac iffD =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   254
      HEADGOAL (etac ctxt rel_mono_strong) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   255
      REPEAT_DETERM (HEADGOAL (etac ctxt (@{thm predicate2_transferD} RS iffD) THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   256
        REPEAT_DETERM o assume_tac ctxt));
58104
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57970
diff changeset
   257
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   258
    REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   259
    (HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58446
diff changeset
   260
     REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
58104
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57970
diff changeset
   261
       @{thms exE conjE CollectE}))) THEN
67222
19809bc9d7ff made tactics more robust
traytel
parents: 63714
diff changeset
   262
     HEADGOAL (hyp_subst_tac ctxt) THEN
19809bc9d7ff made tactics more robust
traytel
parents: 63714
diff changeset
   263
     REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm =>
19809bc9d7ff made tactics more robust
traytel
parents: 63714
diff changeset
   264
       [thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN
19809bc9d7ff made tactics more robust
traytel
parents: 63714
diff changeset
   265
     HEADGOAL (rtac ctxt iffI) THEN
67223
711eec20aecd removed debug output
traytel
parents: 67222
diff changeset
   266
     last_tac iffD1 THEN last_tac iffD2)
58104
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57970
diff changeset
   267
  end;
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57970
diff changeset
   268
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
   269
fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52659
diff changeset
   270
  let
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   271
    val n = length set_maps;
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   272
    val in_tac =
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   273
      if n = 0 then rtac ctxt @{thm UNIV_I}
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   274
      else
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   275
        rtac ctxt @{thm CollectI} THEN' CONJ_WRAP' (fn thm =>
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   276
          etac ctxt (thm RS
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   277
            @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   278
        set_maps;
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52659
diff changeset
   279
  in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   280
    REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55642
diff changeset
   281
    unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   282
    HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono,
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   283
      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
   284
      rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1),
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   285
      REPEAT_DETERM o eresolve_tac ctxt @{thms exE CollectE conjE}, hyp_subst_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   286
      rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   287
      rtac ctxt conjI,
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52659
diff changeset
   288
      EVERY' (map (fn convol =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   289
        rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   290
        REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong)) @{thms fst_convol snd_convol})])
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52659
diff changeset
   291
  end;
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52659
diff changeset
   292
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
   293
fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
   294
  bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero =
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   295
  if live = 0 then
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   296
    rtac ctxt @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   297
      ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   298
  else
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   299
    let
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   300
      val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   301
      val inserts =
57970
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
   302
        map (fn set_bd =>
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   303
          iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   304
            [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
57970
eaa986cd285a generate 'inj_map_strong' for BNFs
desharna
parents: 57967
diff changeset
   305
        set_bds;
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   306
    in
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   307
      EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt @{thm cprod_cinfinite_bound},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   308
        rtac ctxt (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac ctxt @{thm card_of_Card_order},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   309
        rtac ctxt @{thm ordLeq_csum2}, rtac ctxt @{thm Card_order_ctwo}, rtac ctxt @{thm Card_order_csum},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   310
        rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   311
        if live = 1 then rtac ctxt @{thm ordIso_refl[OF Card_order_csum]}
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   312
        else
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   313
          REPEAT_DETERM_N (live - 2) o rtac ctxt @{thm ordIso_transitive[OF csum_cong2]} THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   314
          REPEAT_DETERM_N (live - 1) o rtac ctxt @{thm csum_csum},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   315
        rtac ctxt bd_Card_order, rtac ctxt (@{thm cexp_mono2_Cnotzero} RS ctrans), rtac ctxt @{thm ordLeq_csum1},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   316
        rtac ctxt bd_Card_order, rtac ctxt @{thm Card_order_csum}, rtac ctxt bd_Cnotzero,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   317
        rtac ctxt @{thm csum_Cfinite_cexp_Cinfinite},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   318
        rtac ctxt (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   319
        CONJ_WRAP_GEN' (rtac ctxt @{thm Cfinite_csum}) (K (rtac ctxt @{thm Cfinite_cone})) set_maps,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   320
        rtac ctxt bd'_Cinfinite, rtac ctxt @{thm card_of_Card_order},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   321
        rtac ctxt @{thm Card_order_cexp}, rtac ctxt @{thm Cinfinite_cexp}, rtac ctxt @{thm ordLeq_csum2},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   322
        rtac ctxt @{thm Card_order_ctwo}, rtac ctxt bd'_Cinfinite,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   323
        rtac ctxt (Drule.rotate_prems 1 (@{thm cprod_mono2} RSN (2, ctrans))),
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   324
        REPEAT_DETERM_N (live - 1) o
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   325
          (rtac ctxt (bd_Cinfinite RS @{thm cprod_cexp_csum_cexp_Cinfinite} RSN (2, ctrans)) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   326
           rtac ctxt @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   327
        rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   328
      unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   329
      unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   330
      EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst,
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   331
        rtac ctxt @{thm subsetI},
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 61760
diff changeset
   332
        Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec,
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   333
        REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1],
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   334
        etac ctxt @{thm CollectE},
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   335
        if live = 1 then K all_tac
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   336
        else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   337
        rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I},
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   338
        CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI})
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   339
          (K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' assume_tac ctxt)) set_maps,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   340
        rtac ctxt sym,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   341
        rtac ctxt (Drule.rotate_prems 1
55990
41c6b99c5fb7 more antiquotations;
wenzelm
parents: 55945
diff changeset
   342
           ((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   343
             map_comp RS sym, map_id]) RSN (2, trans))),
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   344
        REPEAT_DETERM_N (2 * live) o assume_tac ctxt,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   345
        REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans),
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   346
        rtac ctxt refl,
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   347
        rtac ctxt @{thm surj_imp_ordLeq},
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   348
        rtac ctxt @{thm subsetI},
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   349
        rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   350
        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt @{thm CollectI},
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   351
        CONJ_WRAP' (fn thm =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   352
          rtac ctxt (thm RS ord_eq_le_trans) THEN' etac ctxt @{thm subset_trans[OF image_mono Un_upper1]})
53290
b6c3be868217 renamed BNF fact
blanchet
parents: 53289
diff changeset
   353
        set_maps,
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   354
        rtac ctxt sym,
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   355
        rtac ctxt (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
53288
050d0bc9afa5 renamed BNF fact
blanchet
parents: 53287
diff changeset
   356
           map_comp RS sym, map_id])] 1
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51916
diff changeset
   357
  end;
51916
eac9e9a45bf5 stronger monotonicity property for relators
traytel
parents: 51915
diff changeset
   358
55197
5a54ed681ba2 less hermetic tactics
traytel
parents: 55163
diff changeset
   359
fun mk_trivial_wit_tac ctxt wit_defs set_maps =
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   360
  unfold_thms_tac ctxt wit_defs THEN
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   361
  HEADGOAL (EVERY' (map (fn thm =>
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   362
    dtac ctxt (thm RS @{thm equalityD1} RS set_mp) THEN'
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   363
    etac ctxt @{thm imageE} THEN' assume_tac ctxt) set_maps)) THEN
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60728
diff changeset
   364
  ALLGOALS (assume_tac ctxt);
54189
c0186a0d8cb3 define a trivial nonemptiness witness if none is provided
traytel
parents: 53562
diff changeset
   365
58106
c8cba801c483 generate 'set_transfer' for BNFs
desharna
parents: 58104
diff changeset
   366
fun mk_set_transfer_tac ctxt in_rel set_maps =
c8cba801c483 generate 'set_transfer' for BNFs
desharna
parents: 58104
diff changeset
   367
  Goal.conjunction_tac 1 THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   368
  EVERY (map (fn set_map => HEADGOAL (rtac ctxt rel_funI) THEN
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58446
diff changeset
   369
  REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
58106
c8cba801c483 generate 'set_transfer' for BNFs
desharna
parents: 58104
diff changeset
   370
    @{thms exE conjE CollectE}))) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   371
  HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 59498
diff changeset
   372
    rtac ctxt @{thm rel_setI}) THEN
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   373
  REPEAT (HEADGOAL (etac ctxt @{thm imageE} THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58446
diff changeset
   374
    REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   375
    rtac ctxt @{thm bexI} THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt @{thm imageI})))
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   376
    set_maps);
58106
c8cba801c483 generate 'set_transfer' for BNFs
desharna
parents: 58104
diff changeset
   377
61242
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   378
fun mk_rel_cong_tac ctxt (eqs, prems) mono =
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   379
  let
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   380
    fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt;
62324
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   381
    fun mk_tacs iffD = etac ctxt mono ::
61242
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   382
      map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD)
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   383
        |> Drule.rotate_prems ~1 |> mk_tac) prems;
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   384
  in
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   385
    unfold_thms_tac ctxt eqs THEN
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   386
    HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2))
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   387
  end;
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 60757
diff changeset
   388
62324
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   389
fun subst_conv ctxt thm =
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   390
  Conv.arg_conv (Conv.arg_conv
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   391
   (Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) ctxt));
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   392
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   393
fun mk_rel_eq_onp_tac ctxt pred_def map_id0 rel_Grp =
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   394
  HEADGOAL (EVERY'
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   395
   [SELECT_GOAL (unfold_thms_tac ctxt (pred_def :: @{thms UNIV_def eq_onp_Grp Ball_Collect})),
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   396
   CONVERSION (subst_conv ctxt (map_id0 RS sym)),
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   397
   rtac ctxt (unfold_thms ctxt @{thms UNIV_def} rel_Grp)]);
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   398
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   399
fun mk_pred_mono_strong0_tac ctxt pred_rel rel_mono_strong0 =
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   400
   unfold_thms_tac ctxt [pred_rel] THEN
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   401
   HEADGOAL (etac ctxt rel_mono_strong0 THEN_ALL_NEW etac ctxt @{thm eq_onp_mono0});
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61841
diff changeset
   402
63714
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63399
diff changeset
   403
fun mk_pred_mono_tac ctxt rel_eq_onp rel_mono =
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63399
diff changeset
   404
  unfold_thms_tac ctxt (map mk_sym [@{thm eq_onp_mono_iff}, rel_eq_onp]) THEN
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63399
diff changeset
   405
  HEADGOAL (rtac ctxt rel_mono THEN_ALL_NEW assume_tac ctxt);
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63399
diff changeset
   406
62329
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   407
fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong =
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   408
  HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1),
63399
d1742d1b7f0f more antiquotations;
wenzelm
parents: 62617
diff changeset
   409
    REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt,
62329
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   410
    rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]),
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   411
    rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   412
      (etac ctxt @{thm rel_fun_Collect_case_prodD[where B="op ="]} THEN_ALL_NEW assume_tac ctxt)]);
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   413
49284
5f39b7940b49 spin off "bnf_def_tactics.ML"
blanchet
parents:
diff changeset
   414
end;