export ML function
authorblanchet
Thu Dec 22 17:36:28 2016 +0100 (2016-12-22)
changeset 64636a42dbe9d2c1f
parent 64635 255741c5f862
child 64637 a15785625f7c
export ML function
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Dec 22 10:42:08 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Dec 22 17:36:28 2016 +0100
     1.3 @@ -12,6 +12,8 @@
     1.4  
     1.5    val co_induct_inst_as_projs_tac: Proof.context -> int -> tactic
     1.6    val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic
     1.7 +  val mk_coinduct_discharge_prem_tac: Proof.context -> thm list -> thm list -> int -> int -> int ->
     1.8 +    thm -> thm -> thm -> thm -> thm -> thm list -> thm list list -> thm list list -> int -> tactic
     1.9    val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
    1.10      thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
    1.11      thm list list list -> tactic
    1.12 @@ -350,13 +352,13 @@
    1.13    end;
    1.14  
    1.15  fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def pre_abs_inverse abs_inverse dtor_ctor ctr_def
    1.16 -    discs sels =
    1.17 +    discs sels extra_unfolds =
    1.18    hyp_subst_tac ctxt THEN'
    1.19    CONVERSION (hhf_concl_conv
    1.20      (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
    1.21    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
    1.22    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: pre_abs_inverse :: abs_inverse :: dtor_ctor ::
    1.23 -    sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
    1.24 +    sels @ sumprod_thms_rel @ extra_unfolds @ @{thms o_apply vimage2p_def})) THEN'
    1.25    (assume_tac ctxt ORELSE' REPEAT o etac ctxt conjE THEN'
    1.26       full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
    1.27       REPEAT o etac ctxt conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
    1.28 @@ -371,8 +373,8 @@
    1.29      full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt)
    1.30    end;
    1.31  
    1.32 -fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def pre_abs_inverse abs_inverse
    1.33 -    dtor_ctor exhaust ctr_defs discss selss =
    1.34 +fun mk_coinduct_discharge_prem_tac ctxt extra_unfolds rel_eqs' nn kk n pre_rel_def pre_abs_inverse
    1.35 +    abs_inverse dtor_ctor exhaust ctr_defs discss selss =
    1.36    let val ks = 1 upto n in
    1.37      EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
    1.38          select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, dtac ctxt meta_spec, dtac ctxt meta_mp,
    1.39 @@ -383,7 +385,7 @@
    1.40            map2 (fn k' => fn discs' =>
    1.41              if k' = k then
    1.42                mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def pre_abs_inverse abs_inverse
    1.43 -                dtor_ctor ctr_def discs sels
    1.44 +                dtor_ctor ctr_def discs sels extra_unfolds
    1.45              else
    1.46                mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss)
    1.47    end;
    1.48 @@ -391,7 +393,7 @@
    1.49  fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses abs_inverses
    1.50      dtor_ctors exhausts ctr_defss discsss selsss =
    1.51    HEADGOAL (rtac ctxt dtor_coinduct' THEN'
    1.52 -    EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
    1.53 +    EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt [] rel_eqs' nn)
    1.54        (1 upto nn) ns pre_rel_defs pre_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss
    1.55        discsss selsss));
    1.56