code simplifications (cf. 78a3d5006cf1)
authorblanchet
Fri Jun 07 17:04:55 2013 +0100 (2013-06-07)
changeset 5234907fd21c01e93
parent 52348 740923a6e530
child 52350 7e352bb76009
code simplifications (cf. 78a3d5006cf1)
src/HOL/BNF/BNF_FP_Basic.thy
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF/BNF_FP_Basic.thy	Fri Jun 07 16:19:52 2013 +0100
     1.2 +++ b/src/HOL/BNF/BNF_FP_Basic.thy	Fri Jun 07 17:04:55 2013 +0100
     1.3 @@ -105,9 +105,6 @@
     1.4  "sum_case f g \<circ> Inr = g"
     1.5  by auto
     1.6  
     1.7 -lemma ident_o_ident: "(\<lambda>x. x) \<circ> (\<lambda>x. x) = (\<lambda>x. x)"
     1.8 -by (rule o_def)
     1.9 -
    1.10  lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
    1.11  by blast
    1.12  
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 16:19:52 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 17:04:55 2013 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  (*  Title:      HOL/BNF/Tools/bnf_fp_def_sugar.ML
     2.5      Author:     Jasmin Blanchette, TU Muenchen
     2.6 -    Copyright   2012
     2.7 +    Copyright   2012, 2013
     2.8  
     2.9  Sugared datatype and codatatype constructions.
    2.10  *)
    2.11 @@ -36,8 +36,7 @@
    2.12       * (typ list list * typ list list list list * term list list
    2.13          * term list list list list) list option
    2.14       * (string * term list * term list list
    2.15 -        * ((term list list * term list list list)
    2.16 -           * (typ list * typ list list list * typ list list)) list) option)
    2.17 +        * ((term list list * term list list list) * (typ list * typ list list)) list) option)
    2.18      * Proof.context
    2.19  
    2.20    val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term ->
    2.21 @@ -47,8 +46,7 @@
    2.22      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    2.23      (term list * thm list) * Proof.context
    2.24    val define_coiters: string list -> string * term list * term list list
    2.25 -    * ((term list list * term list list list)
    2.26 -       * (typ list * typ list list list * typ list list)) list ->
    2.27 +    * ((term list list * term list list list) * (typ list * typ list list)) list ->
    2.28      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    2.29      (term list * thm list) * Proof.context
    2.30    val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
    2.31 @@ -379,10 +377,10 @@
    2.32          val q_Tssss =
    2.33            map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
    2.34          val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
    2.35 -      in (q_Tssss, f_Tssss, (f_sum_prod_Ts, f_Tsss, pf_Tss)) end;
    2.36 +      in (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss)) end;
    2.37  
    2.38 -    val (r_Tssss, g_Tssss, unfold_types) = mk_types single un_fold_of;
    2.39 -    val (s_Tssss, h_Tssss, corec_types) = mk_types unzip_corecT co_rec_of;
    2.40 +    val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types single un_fold_of;
    2.41 +    val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types unzip_corecT co_rec_of;
    2.42  
    2.43      val ((((Free (z, _), cs), pss), gssss), lthy) =
    2.44        lthy
    2.45 @@ -408,7 +406,7 @@
    2.46          mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
    2.47            (build_sum_inj Inr_const (fastype_of cf', T) $ cf');
    2.48  
    2.49 -    fun mk_args qssss fssss (_, f_Tsss, _) =
    2.50 +    fun mk_args qssss fssss f_Tsss =
    2.51        let
    2.52          val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss;
    2.53          val cqssss = map2 (map o map o map o rapp) cs qssss;
    2.54 @@ -416,8 +414,8 @@
    2.55          val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss;
    2.56        in (pfss, cqfsss) end;
    2.57  
    2.58 -    val unfold_args = mk_args rssss gssss unfold_types;
    2.59 -    val corec_args = mk_args sssss hssss corec_types;
    2.60 +    val unfold_args = mk_args rssss gssss g_Tsss;
    2.61 +    val corec_args = mk_args sssss hssss h_Tsss;
    2.62    in
    2.63      ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
    2.64    end;
    2.65 @@ -494,7 +492,7 @@
    2.66  
    2.67      val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
    2.68  
    2.69 -    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, _, pf_Tss)) dtor_coiter =
    2.70 +    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
    2.71        let
    2.72          val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
    2.73          val b = mk_binding suf;
    2.74 @@ -862,11 +860,10 @@
    2.75          val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs;
    2.76  
    2.77          val unfold_tacss =
    2.78 -          map3 (map oo mk_coiter_tac unfold_defs [] nesting_map_ids'' [])
    2.79 +          map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
    2.80              (map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss;
    2.81          val corec_tacss =
    2.82 -          map3 (map oo mk_coiter_tac corec_defs nested_map_comp's
    2.83 -              (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
    2.84 +          map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'')
    2.85              (map co_rec_of dtor_coiter_thmss) pre_map_defs ctr_defss;
    2.86  
    2.87          fun prove goal tac =
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Jun 07 16:19:52 2013 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Jun 07 17:04:55 2013 +0100
     3.3 @@ -14,8 +14,7 @@
     3.4    val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
     3.5    val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
     3.6      thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic
     3.7 -  val mk_coiter_tac: thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm ->
     3.8 -    Proof.context -> tactic
     3.9 +  val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
    3.10    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
    3.11      tactic
    3.12    val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    3.13 @@ -106,16 +105,13 @@
    3.14    unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_ids'' @
    3.15      iter_unfold_thms) THEN HEADGOAL (rtac refl);
    3.16  
    3.17 -val coiter_unfold_thms =
    3.18 -  @{thms id_def ident_o_ident sum_case_if sum_case_o_inj} @ sum_prod_thms_map;
    3.19 +val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
    3.20  
    3.21 -fun mk_coiter_tac coiter_defs map_comp's map_ids'' map_if_distribs
    3.22 -    ctor_dtor_coiter pre_map_def ctr_def ctxt =
    3.23 +fun mk_coiter_tac coiter_defs map_ids'' ctor_dtor_coiter pre_map_def ctr_def ctxt =
    3.24    unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
    3.25    HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN'
    3.26      asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE
    3.27 -  (unfold_thms_tac ctxt (pre_map_def :: map_comp's @ map_ids'' @ map_if_distribs @
    3.28 -     coiter_unfold_thms) THEN
    3.29 +  (unfold_thms_tac ctxt (pre_map_def :: map_ids'' @ coiter_unfold_thms) THEN
    3.30     HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)));
    3.31  
    3.32  fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =