generate 'disc_map_iff[simp]' theorem for (co)datatypes
authordesharna
Thu May 15 16:15:44 2014 +0200 (2014-05-15)
changeset 569918e9ca31e9b8e
parent 56990 299b026cc5af
child 56992 d0e5225601d3
generate 'disc_map_iff[simp]' theorem for (co)datatypes
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon May 19 09:35:35 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu May 15 16:15:44 2014 +0200
     1.3 @@ -98,6 +98,7 @@
     1.4  
     1.5  val EqN = "Eq_";
     1.6  val set_emptyN = "set_empty";
     1.7 +val disc_map_iffN = "disc_map_iff";
     1.8  
     1.9  structure Data = Generic_Data
    1.10  (
    1.11 @@ -1176,6 +1177,48 @@
    1.12                  end;
    1.13  
    1.14                val sets = map mk_set (sets_of_bnf fp_bnf);
    1.15 +
    1.16 +              val disc_map_iff_thms =
    1.17 +                let
    1.18 +                  val (((Ds, As), Bs), names_lthy) = lthy
    1.19 +                    |> mk_TFrees (dead_of_bnf fp_bnf)
    1.20 +                    ||>> mk_TFrees (live_of_bnf fp_bnf)
    1.21 +                    ||>> mk_TFrees (live_of_bnf fp_bnf);
    1.22 +                  val fTs = map2 (curry op -->) As Bs;
    1.23 +                  val T1 = mk_T_of_bnf Ds As fp_bnf;
    1.24 +                  val T2 = mk_T_of_bnf Ds Bs fp_bnf;
    1.25 +                  val ((fs, t), names_lthy) = names_lthy
    1.26 +                    |> mk_Frees "f" fTs
    1.27 +                    ||>> yield_singleton (mk_Frees "a") T1;
    1.28 +                  val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
    1.29 +                  fun mk_discs T = map (fn disc =>
    1.30 +                    subst_nonatomic_types [(domain_type (fastype_of disc), T)] disc);
    1.31 +                  val discs1 = mk_discs T1 discs;
    1.32 +                  val discs2 = mk_discs T2 discs;
    1.33 +                  val discs1_t = map (fn disc1 => Term.betapply (disc1, t)) discs1;
    1.34 +                  fun mk_goal (disc1_t, disc2) =
    1.35 +                    let
    1.36 +                      val (head, tail) = Term.strip_comb disc1_t;
    1.37 +                      val is_t_eq_t = head aconv HOLogic.eq_const T1 andalso
    1.38 +                        forall (fn u => u = t) tail;
    1.39 +                    in
    1.40 +                      if head aconv @{const Not} orelse is_t_eq_t then NONE
    1.41 +                      else
    1.42 +                        SOME (mk_Trueprop_eq
    1.43 +                          (betapply (disc2, (Term.list_comb (map_term, fs) $ t)), disc1_t))
    1.44 +                    end;
    1.45 +                  val goals = map_filter mk_goal (discs1_t ~~ discs2);
    1.46 +                in
    1.47 +                  if null goals then []
    1.48 +                  else
    1.49 +                    Goal.prove_sorry names_lthy [] [] (Logic.mk_conjunction_balanced goals)
    1.50 +                      (fn {context = ctxt, prems = _} =>
    1.51 +                        mk_disc_map_iff_tac ctxt (certify ctxt t) exhaust (flat disc_thmss)
    1.52 +                          map_thms)
    1.53 +                      |> Conjunction.elim_balanced (length goals)
    1.54 +                      |> Proof_Context.export names_lthy lthy
    1.55 +                end;
    1.56 +
    1.57                val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
    1.58                  binder_types o fastype_of) ctrs;
    1.59                val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
    1.60 @@ -1238,7 +1281,8 @@
    1.61                  |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.62  
    1.63                val notes =
    1.64 -                [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
    1.65 +                [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
    1.66 +                 (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
    1.67                   (rel_distinctN, rel_distinct_thms, simp_attrs),
    1.68                   (rel_injectN, rel_inject_thms, simp_attrs),
    1.69                   (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon May 19 09:35:35 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu May 15 16:15:44 2014 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     2.5      tactic
     2.6    val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
     2.7 +  val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
     2.8    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
     2.9    val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
    2.10    val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
    2.11 @@ -31,6 +32,7 @@
    2.12  structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
    2.13  struct
    2.14  
    2.15 +open Ctr_Sugar_Util
    2.16  open BNF_Tactics
    2.17  open BNF_Util
    2.18  open BNF_FP_Util
    2.19 @@ -113,6 +115,15 @@
    2.20        (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
    2.21      (map rtac case_splits' @ [K all_tac]) corecs discs);
    2.22  
    2.23 +fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
    2.24 +  TRYALL Goal.conjunction_tac THEN
    2.25 +    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    2.26 +      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    2.27 +    unfold_thms_tac ctxt maps THEN
    2.28 +    unfold_thms_tac ctxt (map (fn thm => thm RS @{thm iffD2[OF eq_False]}
    2.29 +      handle THM _ => thm RS @{thm iffD2[OF eq_True]}) discs) THEN
    2.30 +    ALLGOALS (rtac refl ORELSE' rtac TrueI);
    2.31 +
    2.32  fun solve_prem_prem_tac ctxt =
    2.33    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
    2.34      hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    2.35 @@ -194,10 +205,10 @@
    2.36  
    2.37  fun mk_set_empty_tac ctxt ct exhaust sets discs =
    2.38    TRYALL Goal.conjunction_tac THEN
    2.39 -  ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    2.40 +  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    2.41      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    2.42    unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
    2.43      SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
    2.44 -  ALLGOALS(rtac refl ORELSE' etac FalseE);
    2.45 +  ALLGOALS (rtac refl ORELSE' etac FalseE);
    2.46  
    2.47  end;