src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
author wenzelm
Thu, 26 Aug 2021 14:45:19 +0200
changeset 74200 17090e27aae9
parent 69597 ff784d5a5bfb
child 74266 612b7e0d6721
permissions -rw-r--r--
more scalable data structure (but: rarely used with > 5 arguments);
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_rec_sugar_tactics.ML
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     3
    Copyright   2013
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     4
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54174
diff changeset
     5
Tactics for corecursor sugar.
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     6
*)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     7
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54174
diff changeset
     8
signature BNF_GFP_REC_SUGAR_TACTICS =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     9
sig
54044
93ab44e992ae strengthened tactic (primcorec_sel_tac) + tuning
blanchet
parents: 54043
diff changeset
    10
  val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
54978
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents: 54977
diff changeset
    11
  val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    12
  val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
53693
71b020d161c5 new tactics for constructor view
blanchet
parents: 53692
diff changeset
    13
  val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
71b020d161c5 new tactics for constructor view
blanchet
parents: 53692
diff changeset
    14
    tactic
54969
0ac0b6576d21 generate 'disc_iff' for all discriminators
blanchet
parents: 54959
diff changeset
    15
  val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm list -> thm list list ->
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    16
    thm list -> tactic
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    17
  val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
54924
44373f3560c7 refactoring
blanchet
parents: 54923
diff changeset
    18
  val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
54978
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents: 54977
diff changeset
    19
  val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents: 54977
diff changeset
    20
    int list -> thm list -> thm option -> tactic
53910
2c5055a3583d strengthen tactic
blanchet
parents: 53908
diff changeset
    21
  val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
    22
    thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    23
end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    24
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54174
diff changeset
    25
structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    26
struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    27
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    28
open BNF_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    29
open BNF_Tactics
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    30
open BNF_FP_Util
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    31
54899
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54844
diff changeset
    32
val atomize_conjL = @{thm atomize_conjL};
53905
blanchet
parents: 53904
diff changeset
    33
val falseEs = @{thms not_TrueE FalseE};
53910
2c5055a3583d strengthen tactic
blanchet
parents: 53908
diff changeset
    34
val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
62391
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
    35
val if_split = @{thm if_split};
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
    36
val if_split_asm = @{thm if_split_asm};
53902
396999552212 use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents: 53901
diff changeset
    37
val split_connectI = @{thms allI impI conjI};
54953
a2f4cf3387fc strengthen tac w.r.t. lets with tuples
blanchet
parents: 54926
diff changeset
    38
val unfold_lets = @{thms Let_def[abs_def] split_beta}
53902
396999552212 use standard "split" properties instead of ad hoc "eq_...I"
blanchet
parents: 53901
diff changeset
    39
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    40
fun exhaust_inst_as_projs ctxt frees thm =
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    41
  let
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    42
    val num_frees = length frees;
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59580
diff changeset
    43
    val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd);
60784
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 60752
diff changeset
    44
    fun find x = find_index (curry (op =) x) frees;
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 60752
diff changeset
    45
    fun mk_inst ((x, i), T) = ((x, i), Thm.cterm_of ctxt (mk_proj T num_frees (find x)));
4f590c08fd5d updated to infer_instantiate;
wenzelm
parents: 60752
diff changeset
    46
  in infer_instantiate ctxt (map mk_inst fs) thm end;
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    47
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    48
val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    49
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    50
fun distinct_in_prems_tac ctxt distincts =
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    51
  eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    52
  assume_tac ctxt;
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    53
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57399
diff changeset
    54
fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 61760
diff changeset
    55
  HEADGOAL (Method.insert_tac ctxt exhaust_discs THEN' clean_blast_tac ctxt);
54924
44373f3560c7 refactoring
blanchet
parents: 54923
diff changeset
    56
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    57
fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54843
diff changeset
    58
  let val ks = 1 upto n in
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    59
    HEADGOAL (assume_tac ctxt ORELSE'
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54900
diff changeset
    60
      cut_tac nchotomy THEN'
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54920
diff changeset
    61
      K (exhaust_inst_as_projs_tac ctxt frees) THEN'
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54900
diff changeset
    62
      EVERY' (map (fn k =>
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
    63
          (if k < n then etac ctxt disjE else K all_tac) THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    64
          REPEAT o (dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    65
            etac ctxt conjE THEN' dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    66
            assume_tac ctxt))
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54900
diff changeset
    67
        ks))
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54843
diff changeset
    68
  end;
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54843
diff changeset
    69
53903
27fd72593624 more powerful/robust tactics
blanchet
parents: 53902
diff changeset
    70
fun mk_primcorec_assumption_tac ctxt discIs =
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    71
  SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    72
      not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
61760
1647bb489522 tuned whitespace
blanchet
parents: 60801
diff changeset
    73
    SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
1647bb489522 tuned whitespace
blanchet
parents: 60801
diff changeset
    74
    etac ctxt conjE ORELSE'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
    75
    eresolve_tac ctxt falseEs ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
    76
    resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    77
    dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
    78
    etac ctxt notE THEN' assume_tac ctxt ORELSE'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
    79
    etac ctxt disjE))));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    80
60735
cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents: 60728
diff changeset
    81
fun ss_fst_snd_conv ctxt =
cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents: 60728
diff changeset
    82
  Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    83
60735
cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents: 60728
diff changeset
    84
fun case_atac ctxt =
cf291b55f3d1 made tactic more robust w.r.t. equations containing 'case_prod'
blanchet
parents: 60728
diff changeset
    85
  Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    86
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    87
fun same_case_tac ctxt m =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
    88
  HEADGOAL (if m = 0 then rtac ctxt TrueI
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
    89
    else REPEAT_DETERM_N (m - 1) o (rtac ctxt conjI THEN' case_atac ctxt) THEN' case_atac ctxt);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    90
54971
blanchet
parents: 54969
diff changeset
    91
fun different_case_tac ctxt m exclude =
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    92
  HEADGOAL (if m = 0 then
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    93
      mk_primcorec_assumption_tac ctxt []
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    94
    else
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
    95
      dtac ctxt exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
    96
      mk_primcorec_assumption_tac ctxt []);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    97
54971
blanchet
parents: 54969
diff changeset
    98
fun cases_tac ctxt k m excludesss =
blanchet
parents: 54969
diff changeset
    99
  let val n = length excludesss in
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
   100
    EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
54971
blanchet
parents: 54969
diff changeset
   101
        | [exclude] => different_case_tac ctxt m exclude)
blanchet
parents: 54969
diff changeset
   102
      (take k (nth excludesss (k - 1))))
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   103
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   104
62320
blanchet
parents: 61841
diff changeset
   105
fun prelude_tac ctxt fun_defs thm =
blanchet
parents: 61841
diff changeset
   106
  unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   107
62320
blanchet
parents: 61841
diff changeset
   108
fun mk_primcorec_disc_tac ctxt fun_defs corec_disc k m excludesss =
blanchet
parents: 61841
diff changeset
   109
  prelude_tac ctxt fun_defs corec_disc THEN cases_tac ctxt k m excludesss;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   110
54969
0ac0b6576d21 generate 'disc_iff' for all discriminators
blanchet
parents: 54959
diff changeset
   111
fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57399
diff changeset
   112
    distinct_discs =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   113
  HEADGOAL (rtac ctxt iffI THEN'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   114
    rtac ctxt fun_exhaust THEN'
54959
30ded82ff806 fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
blanchet
parents: 54955
diff changeset
   115
    K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   116
    EVERY' (map (fn [] => etac ctxt FalseE
54969
0ac0b6576d21 generate 'disc_iff' for all discriminators
blanchet
parents: 54959
diff changeset
   117
        | fun_discs' as [fun_disc'] =>
0ac0b6576d21 generate 'disc_iff' for all discriminators
blanchet
parents: 54959
diff changeset
   118
          if eq_list Thm.eq_thm (fun_discs', fun_discs) then
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   119
            REPEAT_DETERM o etac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt TrueI)
54917
a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents: 54916
diff changeset
   120
          else
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   121
            rtac ctxt FalseE THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   122
            (rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o assume_tac ctxt ORELSE'
54977
63a5e0d8ce3b strengthened tactic to handle 'disc_iff' equations of the form '... = False'
blanchet
parents: 54971
diff changeset
   123
             cut_tac fun_disc') THEN'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   124
            dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' assume_tac ctxt)
54917
a426e38a8a7e made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
blanchet
parents: 54916
diff changeset
   125
      fun_discss) THEN'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   126
    (etac ctxt FalseE ORELSE'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   127
     resolve_tac ctxt
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   128
      (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt));
54899
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54844
diff changeset
   129
62320
blanchet
parents: 61841
diff changeset
   130
fun mk_primcorec_sel_tac ctxt fun_defs distincts splits split_asms mapsx map_ident0s map_comps
blanchet
parents: 61841
diff changeset
   131
    fun_sel k m excludesss =
blanchet
parents: 61841
diff changeset
   132
  prelude_tac ctxt fun_defs (fun_sel RS trans) THEN
54971
blanchet
parents: 54969
diff changeset
   133
  cases_tac ctxt k m excludesss THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   134
  HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
   135
    eresolve_tac ctxt falseEs ORELSE'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
   136
    resolve_tac ctxt split_connectI ORELSE'
62391
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
   137
    Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
   138
    Splitter.split_tac ctxt (if_split :: splits) ORELSE'
61760
1647bb489522 tuned whitespace
blanchet
parents: 60801
diff changeset
   139
    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
1647bb489522 tuned whitespace
blanchet
parents: 60801
diff changeset
   140
    assume_tac ctxt ORELSE'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   141
    etac ctxt notE THEN' assume_tac ctxt ORELSE'
55067
a452de24a877 tuned names
blanchet
parents: 55061
diff changeset
   142
    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
57279
88263522c31e made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
blanchet
parents: 55990
diff changeset
   143
         sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
57399
cfc19f0a6261 compile
blanchet
parents: 57279
diff changeset
   144
       mapsx @ map_ident0s @ map_comps))) ORELSE'
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   145
    fo_rtac ctxt @{thm cong} ORELSE'
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   146
    rtac ctxt @{thm ext} ORELSE'
59610
8273b65620f9 strengthened tactic
blanchet
parents: 59582
diff changeset
   147
    mk_primcorec_assumption_tac ctxt []));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   148
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
   149
fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   150
  HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
61760
1647bb489522 tuned whitespace
blanchet
parents: 60801
diff changeset
   151
    (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN'
1647bb489522 tuned whitespace
blanchet
parents: 60801
diff changeset
   152
    REPEAT_DETERM_N m o assume_tac ctxt) THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   153
  unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl);
53706
9e28c41e3595 more primcorec tactics
blanchet
parents: 53702
diff changeset
   154
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   155
fun inst_split_eq ctxt split =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59580
diff changeset
   156
  (case Thm.prop_of split of
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69593
diff changeset
   157
    \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   158
    let
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   159
      val s = Name.uu;
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   160
      val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   161
    in
67700
wenzelm
parents: 64629
diff changeset
   162
      Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
74200
17090e27aae9 more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents: 69597
diff changeset
   163
      |> Drule.generalize (Symtab.empty, Symtab.make_set [s])
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   164
    end
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   165
  | _ => split);
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   166
54978
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents: 54977
diff changeset
   167
fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   168
  let
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   169
    val splits' =
62391
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
   170
      map (fn th => th RS iffD2) (@{thm if_split_eq2} :: map (inst_split_eq ctxt) splits);
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   171
  in
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
   172
    HEADGOAL (REPEAT o (resolve_tac ctxt (splits' @ split_connectI))) THEN
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
   173
    prelude_tac ctxt [] (fun_ctr RS trans) THEN
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   174
    HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   175
      SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   176
      (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
   177
       resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
62391
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
   178
       Splitter.split_tac ctxt (if_split :: splits) ORELSE'
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
   179
       Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   180
       mk_primcorec_assumption_tac ctxt discIs ORELSE'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   181
       distinct_in_prems_tac ctxt distincts ORELSE'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   182
       (TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' assume_tac ctxt)))))
54138
c7119e1cde3e avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
blanchet
parents: 54133
diff changeset
   183
  end;
53903
27fd72593624 more powerful/robust tactics
blanchet
parents: 53902
diff changeset
   184
54842
a020f7d74fed renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
blanchet
parents: 54832
diff changeset
   185
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
54832
789fbbc092d2 implemented 'exhaustive' option in tactic
blanchet
parents: 54613
diff changeset
   186
54978
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents: 54977
diff changeset
   187
fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt =
54832
789fbbc092d2 implemented 'exhaustive' option in tactic
blanchet
parents: 54613
diff changeset
   188
  let
789fbbc092d2 implemented 'exhaustive' option in tactic
blanchet
parents: 54613
diff changeset
   189
    val n = length ms;
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   190
    val (ms', fun_ctrs') =
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   191
      (case nchotomy_opt of
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   192
        NONE => (ms, fun_ctrs)
54842
a020f7d74fed renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
blanchet
parents: 54832
diff changeset
   193
      | SOME nchotomy =>
54832
789fbbc092d2 implemented 'exhaustive' option in tactic
blanchet
parents: 54613
diff changeset
   194
        (ms |> split_last ||> K [n - 1] |> op @,
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   195
         fun_ctrs
54843
7f30d569da08 made tactic work with theorems with multiple assumptions
blanchet
parents: 54842
diff changeset
   196
         |> split_last
54899
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54844
diff changeset
   197
         ||> unfold_thms ctxt [atomize_conjL]
54908
f4ae538b0ba5 gracefully handle single-equation case, where 'nchotomy' is 'True'
blanchet
parents: 54907
diff changeset
   198
         ||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
54843
7f30d569da08 made tactic work with theorems with multiple assumptions
blanchet
parents: 54842
diff changeset
   199
         |> op @));
54832
789fbbc092d2 implemented 'exhaustive' option in tactic
blanchet
parents: 54613
diff changeset
   200
  in
54978
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents: 54977
diff changeset
   201
    EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN
54832
789fbbc092d2 implemented 'exhaustive' option in tactic
blanchet
parents: 54613
diff changeset
   202
    IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
   203
      HEADGOAL (REPEAT_DETERM o resolve_tac ctxt (refl :: split_connectI)))
54832
789fbbc092d2 implemented 'exhaustive' option in tactic
blanchet
parents: 54613
diff changeset
   204
  end;
53693
71b020d161c5 new tactics for constructor view
blanchet
parents: 53692
diff changeset
   205
54978
afc156c7e4f7 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
blanchet
parents: 54977
diff changeset
   206
fun mk_primcorec_code_tac ctxt distincts splits raw =
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60251
diff changeset
   207
  HEADGOAL (rtac ctxt raw ORELSE' rtac ctxt (raw RS trans) THEN'
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54953
diff changeset
   208
    SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   209
    (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59274
diff changeset
   210
     resolve_tac ctxt split_connectI ORELSE'
62391
1658fc9b2618 more canonical names
nipkow
parents: 62320
diff changeset
   211
     Splitter.split_tac ctxt (if_split :: splits) ORELSE'
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   212
     distinct_in_prems_tac ctxt distincts ORELSE'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   213
     rtac ctxt sym THEN' assume_tac ctxt ORELSE'
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60735
diff changeset
   214
     etac ctxt notE THEN' assume_tac ctxt));
53921
46fc95abef09 tactic cleanup
blanchet
parents: 53910
diff changeset
   215
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   216
end;