tune the implementation of 'rel_coinduct'
authordesharna
Tue Jun 24 13:48:14 2014 +0200 (2014-06-24)
changeset 57303498a62e65f5f
parent 57302 58f02fbaa764
child 57304 d2061dc953a4
tune the implementation of 'rel_coinduct'
src/HOL/BNF_FP_Base.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Tue Jun 24 13:48:14 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Tue Jun 24 13:48:14 2014 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
     1.5  by auto
     1.6  
     1.7 -lemma predicate2D_conj: "(P \<le> Q) \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
     1.8 +lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
     1.9    by auto
    1.10  
    1.11  lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
     2.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Jun 24 13:48:14 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Jun 24 13:48:14 2014 +0200
     2.3 @@ -83,9 +83,8 @@
     2.4  
     2.5    val mk_map: int -> typ list -> typ list -> term -> term
     2.6    val mk_rel: int -> typ list -> typ list -> term -> term
     2.7 -  val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term
     2.8 -  val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term
     2.9 -  val build_rel': Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
    2.10 +  val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
    2.11 +  val build_rel: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
    2.12    val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
    2.13    val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
    2.14      'a list
    2.15 @@ -534,12 +533,12 @@
    2.16      Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    2.17    end;
    2.18  
    2.19 -fun build_map_or_rel mk const of_bnf dest blacklist ctxt build_simple =
    2.20 +fun build_map_or_rel mk const of_bnf dest ctxt simpleTs build_simple =
    2.21    let
    2.22      fun build (TU as (T, U)) =
    2.23 -      if exists (curry (op =) T) blacklist then
    2.24 +      if exists (curry (op =) T) simpleTs then
    2.25          build_simple TU
    2.26 -      else if T = U andalso not (exists_subtype_in blacklist T) then
    2.27 +      else if T = U andalso not (exists_subtype_in simpleTs T) then
    2.28          const T
    2.29        else
    2.30          (case TU of
    2.31 @@ -556,9 +555,8 @@
    2.32          | _ => build_simple TU);
    2.33    in build end;
    2.34  
    2.35 -val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT [];
    2.36 -val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T [];
    2.37 -fun build_rel' ctxt blacklist = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T blacklist ctxt;
    2.38 +val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
    2.39 +val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
    2.40  
    2.41  fun map_flattened_map_args ctxt s map_args fs =
    2.42    let
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     3.3 @@ -359,7 +359,7 @@
     3.4  
     3.5      val cpss = map2 (map o rapp) cs pss;
     3.6  
     3.7 -    fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
     3.8 +    fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd);
     3.9  
    3.10      fun build_dtor_corec_arg _ [] [cg] = cg
    3.11        | build_dtor_corec_arg T [cq] [cg, cg'] =
    3.12 @@ -574,7 +574,7 @@
    3.13            if T = U then
    3.14              x
    3.15            else
    3.16 -            build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
    3.17 +            build_map lthy [] (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
    3.18                (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
    3.19  
    3.20          val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
    3.21 @@ -634,6 +634,14 @@
    3.22      (coinduct_attrs, common_coinduct_attrs)
    3.23    end;
    3.24  
    3.25 +fun postproc_coinduct nn prop prop_conj =
    3.26 +  Drule.zero_var_indexes
    3.27 +  #> `(conj_dests nn)
    3.28 +  #>> map (fn thm => Thm.permute_prems 0 nn (thm RS prop))
    3.29 +  ##> (fn thm => Thm.permute_prems 0 nn
    3.30 +    (if nn = 1 then thm RS prop
    3.31 +     else funpow nn (fn thm => reassoc_conjs (thm RS prop_conj)) thm));
    3.32 +
    3.33  fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
    3.34    ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
    3.35    let
    3.36 @@ -666,18 +674,12 @@
    3.37           (mk_discss fpBs Bs, mk_selsss fpBs Bs))
    3.38        end;
    3.39  
    3.40 -    fun choose_relator (A, B) = the (find_first (fn t =>
    3.41 -      let
    3.42 -        val T = fastype_of t
    3.43 -        val arg1T = domain_type T;
    3.44 -        val arg2T = domain_type (range_type T);
    3.45 -      in
    3.46 -        A = arg1T andalso B = arg2T
    3.47 -      end) (Rs @ IRs));
    3.48 +    fun choose_relator AB = the (find_first
    3.49 +      (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
    3.50  
    3.51      val premises =
    3.52        let
    3.53 -        fun build_the_rel A B = build_rel' lthy fpA_Ts choose_relator (A, B);
    3.54 +        fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
    3.55  
    3.56          fun build_rel_app selA_t selB_t =
    3.57            (build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t
    3.58 @@ -685,7 +687,7 @@
    3.59          fun mk_prem_ctr_concls n k discA_t selA_ts discB_t selB_ts =
    3.60            (if k = n then [] else [HOLogic.mk_eq (discA_t, discB_t)]) @
    3.61            (case (selA_ts, selB_ts) of
    3.62 -            ([],[]) => []
    3.63 +            ([], []) => []
    3.64            | (_ :: _, _ :: _) =>
    3.65              [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [discA_t, discB_t],
    3.66                Library.foldr1 HOLogic.mk_conj (map2 build_rel_app selA_ts selB_ts))]);
    3.67 @@ -703,36 +705,19 @@
    3.68        end;
    3.69  
    3.70      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    3.71 -      (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts))));
    3.72 -
    3.73 -    (*
    3.74 -    fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]"
    3.75 -    val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises)
    3.76 -    val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal)
    3.77 -    val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts)
    3.78 -    *)
    3.79 +      (map2 mk_leq IRs (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts))));
    3.80  
    3.81      val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
    3.82        (fn {context = ctxt, prems = prems} =>
    3.83            mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
    3.84 -            (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss)
    3.85 -              ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses)
    3.86 +            (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
    3.87 +            (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
    3.88 +            rel_pre_defs abs_inverses)
    3.89        |> singleton (Proof_Context.export names_lthy lthy)
    3.90        |> Thm.close_derivation;
    3.91 -
    3.92 -    val nn = length fpA_Ts;
    3.93 -    val predicate2D = @{thm predicate2D};
    3.94 -    val predicate2D_conj = @{thm predicate2D_conj};
    3.95 -
    3.96 -    val postproc =
    3.97 -      Drule.zero_var_indexes
    3.98 -      #> `(conj_dests nn)
    3.99 -      #>> map (fn thm => Thm.permute_prems 0 nn (thm RS predicate2D))
   3.100 -      ##> (fn thm => Thm.permute_prems 0 nn
   3.101 -        (if nn = 1 then thm RS predicate2D
   3.102 -         else funpow nn (fn thm => reassoc_conjs (thm RS predicate2D_conj)) thm));
   3.103    in
   3.104 -    (postproc rel_coinduct0_thm, coinduct_attrs fpA_Ts ctr_sugars mss)
   3.105 +    (postproc_coinduct (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
   3.106 +     coinduct_attrs fpA_Ts ctr_sugars mss)
   3.107    end;
   3.108  
   3.109  fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
   3.110 @@ -785,7 +770,7 @@
   3.111              fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
   3.112  
   3.113          fun build_the_rel rs' T Xs_T =
   3.114 -          build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
   3.115 +          build_rel lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
   3.116            |> Term.subst_atomic_types (Xs ~~ fpTs);
   3.117  
   3.118          fun build_rel_app rs' usel vsel Xs_T =
   3.119 @@ -826,20 +811,12 @@
   3.120            |> singleton (Proof_Context.export names_lthy lthy)
   3.121            |> Thm.close_derivation;
   3.122  
   3.123 -        val postproc =
   3.124 -          Drule.zero_var_indexes
   3.125 -          #> `(conj_dests nn)
   3.126 -          #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp))
   3.127 -          ##> (fn thm => Thm.permute_prems 0 nn
   3.128 -            (if nn = 1 then thm RS mp
   3.129 -             else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm));
   3.130 -
   3.131          val rel_eqs = map rel_eq_of_bnf pre_bnfs;
   3.132          val rel_monos = map rel_mono_of_bnf pre_bnfs;
   3.133          val dtor_coinducts =
   3.134            [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
   3.135        in
   3.136 -        map2 (postproc oo prove) dtor_coinducts goals
   3.137 +        map2 (postproc_coinduct nn mp mp_conj oo prove) dtor_coinducts goals
   3.138        end;
   3.139  
   3.140      fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   3.141 @@ -864,7 +841,7 @@
   3.142            let val T = fastype_of cqg in
   3.143              if exists_subtype_in Cs T then
   3.144                let val U = mk_U T in
   3.145 -                build_map lthy (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
   3.146 +                build_map lthy [] (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
   3.147                    tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg
   3.148                end
   3.149              else
   3.150 @@ -1336,7 +1313,7 @@
   3.151                            val lhs = selB $ (Term.list_comb (map_term, fs) $ ta);
   3.152                            val lhsT = fastype_of lhs;
   3.153                            val map_rhsT = map_atyps (perhaps (AList.lookup (op =) (Bs ~~ As))) lhsT;
   3.154 -                          val map_rhs = build_map lthy
   3.155 +                          val map_rhs = build_map lthy []
   3.156                              (the o (AList.lookup (op =) ((As ~~ Bs) ~~ fs))) (map_rhsT, lhsT);
   3.157                            val rhs = (case map_rhs of
   3.158                              Const (@{const_name id}, _) => selA $ ta
   3.159 @@ -1592,8 +1569,8 @@
   3.160  
   3.161          val ((rel_coinduct_thms, rel_coinduct_thm),
   3.162               (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
   3.163 -          derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses abs_injects
   3.164 -          ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
   3.165 +          derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
   3.166 +            abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
   3.167  
   3.168          val sel_corec_thmss = map flat sel_corec_thmsss;
   3.169  
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Jun 24 13:48:14 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Jun 24 13:48:14 2014 +0200
     4.3 @@ -44,6 +44,7 @@
     4.4  
     4.5  val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
     4.6  val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
     4.7 +val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
     4.8  
     4.9  val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
    4.10  val sumprod_thms_set =
    4.11 @@ -218,12 +219,12 @@
    4.12          arg_cong2}) RS iffD1)) THEN'
    4.13          atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
    4.14          REPEAT_DETERM o etac conjE))) 1 THEN
    4.15 -      Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
    4.16 -        sels @ @{thms simp_thms(6,7,8,11,12,15,16,22,24)}) THEN
    4.17 +      Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
    4.18 +        @ simp_thms') THEN
    4.19        Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
    4.20 -        abs_inject :: ctor_defs @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps rel_prod_apply
    4.21 -        vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject
    4.22 -        simp_thms(6,7,8,11,12,15,16,22,24)}) THEN
    4.23 +        abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps
    4.24 +        rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject
    4.25 +        prod.inject}) THEN
    4.26        REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
    4.27          (rtac refl ORELSE' atac))))
    4.28      cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Jun 24 13:48:14 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Jun 24 13:48:14 2014 +0200
     5.3 @@ -340,11 +340,11 @@
     5.4                        val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
     5.5                        val T = mk_co_algT TY U;
     5.6                      in
     5.7 -                      (case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of
     5.8 +                      (case try (force_typ names_lthy T o build_map lthy [] co_proj1_const o dest_funT) T of
     5.9                          SOME f => mk_co_product f
    5.10                            (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    5.11                        | NONE => mk_map_co_product
    5.12 -                          (build_map lthy co_proj1_const
    5.13 +                          (build_map lthy [] co_proj1_const
    5.14                              (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
    5.15                            (HOLogic.id_const X))
    5.16                      end)
     6.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     6.3 @@ -239,7 +239,7 @@
     6.4    let
     6.5      fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
     6.6  
     6.7 -    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd);
     6.8 +    val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
     6.9  
    6.10      fun massage_mutual_call bound_Ts U T t =
    6.11        if has_call t then
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Jun 24 13:48:14 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Jun 24 13:48:14 2014 +0200
     7.3 @@ -68,7 +68,7 @@
     7.4      fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
     7.5  
     7.6      val typof = curry fastype_of1 bound_Ts;
     7.7 -    val build_map_fst = build_map ctxt (fst_const o fst);
     7.8 +    val build_map_fst = build_map ctxt [] (fst_const o fst);
     7.9  
    7.10      val yT = typof y;
    7.11      val yU = typof y';
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Jun 24 13:48:14 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Jun 24 13:48:14 2014 +0200
     8.3 @@ -275,7 +275,7 @@
     8.4  
     8.5            fun mk_rec_arg_arg (x as Free (_, T)) =
     8.6              let val U = B_ify T in
     8.7 -              if T = U then x else build_map lthy2 (the o AList.lookup (op =) ABgs) (T, U) $ x
     8.8 +              if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x
     8.9              end;
    8.10  
    8.11            fun mk_rec_o_map_arg rec_arg_T h =