src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
author blanchet
Wed, 05 Sep 2012 11:08:18 +0200
changeset 49149 166f19b4677b
parent 49147 0da8120bd2aa
child 49160 056d6010b6d2
permissions -rw-r--r--
tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     3
    Copyright   2012
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     4
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     5
Tactics for the LFP/GFP sugar.
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     6
*)
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     7
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     8
signature BNF_FP_SUGAR_TACTICS =
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
     9
sig
49130
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49127
diff changeset
    10
  val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
49125
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49123
diff changeset
    11
  val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    12
  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    13
    -> tactic
49127
f7326a0d7f19 implemented "mk_half_distinct_tac"
blanchet
parents: 49126
diff changeset
    14
  val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
49126
1bbd7a37fc29 implemented "mk_inject_tac"
blanchet
parents: 49125
diff changeset
    15
  val mk_inject_tac: Proof.context -> thm -> thm -> tactic
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    16
end;
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    17
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    18
structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    19
struct
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    20
49125
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49123
diff changeset
    21
open BNF_Tactics
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    22
open BNF_Util
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    23
49130
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49127
diff changeset
    24
fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49127
diff changeset
    25
  Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49127
diff changeset
    26
  (rtac (BNF_FP_Util.mk_sum_casesN n k RS ssubst) THEN'
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49127
diff changeset
    27
   REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49127
diff changeset
    28
   rtac refl) 1;
3c26e17b2849 implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents: 49127
diff changeset
    29
49125
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49123
diff changeset
    30
fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
49135
de13b454fa31 fixed some type issues in sugar "exhaust_tac"
blanchet
parents: 49130
diff changeset
    31
  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
49125
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49123
diff changeset
    32
  Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
49147
0da8120bd2aa don't get confused by extraneous premisses
blanchet
parents: 49135
diff changeset
    33
  EVERY' (map2 (fn k => fn m =>
49149
166f19b4677b tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it
blanchet
parents: 49147
diff changeset
    34
    select_prem_tac k (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' rotate_tac ~1 THEN'
49147
0da8120bd2aa don't get confused by extraneous premisses
blanchet
parents: 49135
diff changeset
    35
      etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
49125
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49123
diff changeset
    36
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    37
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    38
  (rtac iffI THEN'
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    39
   EVERY' (map3 (fn cTs => fn cx => fn th =>
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    40
     dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    41
     SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    42
     atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    43
49127
f7326a0d7f19 implemented "mk_half_distinct_tac"
blanchet
parents: 49126
diff changeset
    44
fun mk_half_distinct_tac ctxt fld_inject ctr_defs =
f7326a0d7f19 implemented "mk_half_distinct_tac"
blanchet
parents: 49126
diff changeset
    45
  Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN
f7326a0d7f19 implemented "mk_half_distinct_tac"
blanchet
parents: 49126
diff changeset
    46
  rtac @{thm sum.distinct(1)} 1;
f7326a0d7f19 implemented "mk_half_distinct_tac"
blanchet
parents: 49126
diff changeset
    47
49126
1bbd7a37fc29 implemented "mk_inject_tac"
blanchet
parents: 49125
diff changeset
    48
fun mk_inject_tac ctxt ctr_def fld_inject =
49135
de13b454fa31 fixed some type issues in sugar "exhaust_tac"
blanchet
parents: 49130
diff changeset
    49
  Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
de13b454fa31 fixed some type issues in sugar "exhaust_tac"
blanchet
parents: 49130
diff changeset
    50
  Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
49126
1bbd7a37fc29 implemented "mk_inject_tac"
blanchet
parents: 49125
diff changeset
    51
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
diff changeset
    52
end;