src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
changeset 57983 6edc3529bb4e
parent 57893 7bc128647d6e
child 57999 412ec967e3b3
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -17,15 +17,16 @@
     1.4      thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
     1.5      thm list list list -> tactic
     1.6    val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
     1.7 +  val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
     1.8    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     1.9      tactic
    1.10 -  val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    1.11 -  val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
    1.12    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
    1.13    val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
    1.14    val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
    1.15      thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
    1.16    val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
    1.17 +  val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
    1.18 +  val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
    1.19    val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
    1.20      tactic
    1.21    val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
    1.22 @@ -37,13 +38,12 @@
    1.23      thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
    1.24    val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
    1.25      thm list -> thm list -> tactic
    1.26 -  val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
    1.27 -  val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
    1.28    val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic
    1.29    val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
    1.30    val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
    1.31      thm list -> thm list -> thm list -> thm list -> tactic
    1.32    val mk_set_intros_tac: Proof.context -> thm list -> tactic
    1.33 +  val mk_set_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
    1.34  end;
    1.35  
    1.36  structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
    1.37 @@ -126,22 +126,13 @@
    1.38      HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
    1.39    end;
    1.40  
    1.41 -fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt =
    1.42 +fun mk_corec_disc_iff_tac case_splits' corecs discs ctxt =
    1.43    EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
    1.44        HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
    1.45        HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
    1.46        (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
    1.47      (map rtac case_splits' @ [K all_tac]) corecs discs);
    1.48  
    1.49 -fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
    1.50 -  TRYALL Goal.conjunction_tac THEN
    1.51 -  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    1.52 -    REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.53 -  unfold_thms_tac ctxt maps THEN
    1.54 -  unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
    1.55 -    handle THM _ => thm RS eqTrueI) discs) THEN
    1.56 -  ALLGOALS (rtac refl ORELSE' rtac TrueI);
    1.57 -
    1.58  fun solve_prem_prem_tac ctxt =
    1.59    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
    1.60      hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    1.61 @@ -221,6 +212,25 @@
    1.62        (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
    1.63        selsss));
    1.64  
    1.65 +fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
    1.66 +  TRYALL Goal.conjunction_tac THEN
    1.67 +  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    1.68 +    REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.69 +  unfold_thms_tac ctxt maps THEN
    1.70 +  unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
    1.71 +    handle THM _ => thm RS eqTrueI) discs) THEN
    1.72 +  ALLGOALS (rtac refl ORELSE' rtac TrueI);
    1.73 +
    1.74 +fun mk_map_sel_tac ctxt ct exhaust discs maps sels =
    1.75 +  TRYALL Goal.conjunction_tac THEN
    1.76 +    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    1.77 +      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.78 +    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
    1.79 +      @{thms not_True_eq_False not_False_eq_True}) THEN
    1.80 +    TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
    1.81 +    unfold_thms_tac ctxt (maps @ sels) THEN
    1.82 +    ALLGOALS (rtac refl);
    1.83 +
    1.84  fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
    1.85    HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
    1.86      rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
    1.87 @@ -280,17 +290,7 @@
    1.88      (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN
    1.89    TRYALL (resolve_tac [TrueI, refl]);
    1.90  
    1.91 -fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
    1.92 -  TRYALL Goal.conjunction_tac THEN
    1.93 -    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    1.94 -      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.95 -    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
    1.96 -      @{thms not_True_eq_False not_False_eq_True}) THEN
    1.97 -    TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
    1.98 -    unfold_thms_tac ctxt (maps @ sels) THEN
    1.99 -    ALLGOALS (rtac refl);
   1.100 -
   1.101 -fun mk_sel_set_tac ctxt ct exhaust discs sels sets =
   1.102 +fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
   1.103    TRYALL Goal.conjunction_tac THEN
   1.104      ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
   1.105        REPEAT_DETERM o hyp_subst_tac ctxt) THEN