tuning
authorblanchet
Thu Jul 16 17:25:48 2015 +0200 (2015-07-16)
changeset 60737685b169d0611
parent 60736 c4bc0691860b
child 60738 a2a376689082
tuning
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 16 17:25:44 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 16 17:25:48 2015 +0200
     1.3 @@ -1663,6 +1663,25 @@
     1.4        (transpose setss)
     1.5    end;
     1.6  
     1.7 +fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
     1.8 +  let
     1.9 +    val n = Thm.nprems_of coind;
    1.10 +    val m = Thm.nprems_of (hd rel_monos) - n;
    1.11 +    fun mk_inst phi =
    1.12 +      (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))));
    1.13 +    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
    1.14 +    fun mk_unfold rel_eq rel_mono =
    1.15 +      let
    1.16 +        val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
    1.17 +        val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
    1.18 +      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end;
    1.19 +    val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
    1.20 +      imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
    1.21 +  in
    1.22 +    Thm.instantiate ([], insts) coind
    1.23 +    |> unfold_thms ctxt unfolds
    1.24 +  end;
    1.25 +
    1.26  fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
    1.27      dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
    1.28      kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 16 17:25:44 2015 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 16 17:25:48 2015 +0200
     2.3 @@ -194,8 +194,6 @@
     2.4    val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     2.5      thm list -> thm list -> thm list
     2.6  
     2.7 -  val mk_coinduct_strong_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
     2.8 -
     2.9    val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
    2.10        BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
    2.11      binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
    2.12 @@ -603,25 +601,6 @@
    2.13      split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
    2.14    end;
    2.15  
    2.16 -fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
    2.17 -  let
    2.18 -    val n = Thm.nprems_of coind;
    2.19 -    val m = Thm.nprems_of (hd rel_monos) - n;
    2.20 -    fun mk_inst phi =
    2.21 -      (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))))
    2.22 -    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
    2.23 -    fun mk_unfold rel_eq rel_mono =
    2.24 -      let
    2.25 -        val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
    2.26 -        val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
    2.27 -      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end;
    2.28 -    val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
    2.29 -      imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
    2.30 -  in
    2.31 -    Thm.instantiate ([], insts) coind
    2.32 -    |> unfold_thms ctxt unfolds
    2.33 -  end;
    2.34 -
    2.35  fun fp_bnf construct_fp bs resBs Ds0 fp_eqs lthy =
    2.36    let
    2.37      val time = time lthy;