1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -13,7 +13,8 @@
     1.4    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     1.5      -> tactic
     1.6    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     1.7 -  val mk_induct_tac: Proof.context -> tactic
     1.8 +  val mk_induct_tac: Proof.context -> int list -> int list list -> int list list -> thm list ->
     1.9 +    thm -> thm list list -> thm list -> tactic
    1.10    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
    1.11    val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    1.12  end;
    1.13 @@ -25,6 +26,23 @@
    1.14  open BNF_Util
    1.15  open BNF_FP_Util
    1.16  
    1.17 +val meta_mp = @{thm meta_mp};
    1.18 +val meta_spec = @{thm meta_spec};
    1.19 +
    1.20 +fun squash_spurious_fs lthy thm =
    1.21 +  let
    1.22 +    val spurious_fs =
    1.23 +      Term.add_vars (prop_of thm) []
    1.24 +      |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
    1.25 +    val cxs =
    1.26 +      map (fn s as (_, T) =>
    1.27 +        (certify lthy (Var s), certify lthy (id_abs (domain_type T)))) spurious_fs;
    1.28 +  in
    1.29 +    Drule.cterm_instantiate cxs thm
    1.30 +  end;
    1.31 +
    1.32 +val squash_spurious_fs_tac = PRIMITIVE o squash_spurious_fs;
    1.33 +
    1.34  fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
    1.35    Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
    1.36    (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    1.37 @@ -34,8 +52,8 @@
    1.38  fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
    1.39    Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
    1.40    Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
    1.41 -  EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec},
    1.42 -    etac @{thm meta_mp}, atac]) (1 upto n)) 1;
    1.43 +  EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec,
    1.44 +    etac meta_mp, atac]) (1 upto n)) 1;
    1.45  
    1.46  fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
    1.47    (rtac iffI THEN'
    1.48 @@ -52,9 +70,6 @@
    1.49    Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
    1.50    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
    1.51  
    1.52 -fun mk_induct_tac ctxt =
    1.53 -  Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt) (* FIXME: TODO *);
    1.54 -
    1.55  val iter_like_thms =
    1.56    @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
    1.57        split_conv};
    1.58 @@ -73,4 +88,52 @@
    1.59    Local_Defs.unfold_tac ctxt @{thms id_def} THEN
    1.60    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    1.61  
    1.62 +fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' =
    1.63 +  Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN squash_spurious_fs_tac ctxt;
    1.64 +
    1.65 +fun mk_induct_prepare_prem_tac n m k =
    1.66 +  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
    1.67 +    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
    1.68 +
    1.69 +fun mk_induct_prepare_prem_prems_tac _ _ 0 = all_tac
    1.70 +  | mk_induct_prepare_prem_prems_tac nn kk r =
    1.71 +    REPEAT_DETERM_N r (rotate_tac (~1 + kk - nn) 1 THEN dtac meta_mp 1 THEN
    1.72 +      defer_tac 2 THEN PRIMITIVE (Thm.permute_prems 0 ~1) THEN rotate_tac 1 1) THEN
    1.73 +    PRIMITIVE Raw_Simplifier.norm_hhf;
    1.74 +
    1.75 +val induct_prem_prem_thms =
    1.76 +  @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
    1.77 +      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv fsts_def[abs_def] image_def
    1.78 +      map_pair_simp o_apply snd_conv snds_def[abs_def] sum.cases sum_map.simps sum_setl_def[abs_def]
    1.79 +      sum_setr_def[abs_def] sup_bot_right};
    1.80 +
    1.81 +fun mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's =
    1.82 +  EVERY' (maps (fn i =>
    1.83 +    [dtac meta_spec, rotate_tac ~1, etac meta_mp,
    1.84 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.85 +       (set_natural's @ pre_set_defs @ induct_prem_prem_thms)),
    1.86 +     rtac (mk_UnIN r i),
    1.87 +     atac ORELSE'
    1.88 +     rtac @{thm singletonI} ORELSE'
    1.89 +     (REPEAT_DETERM o (atac ORELSE'
    1.90 +        SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.91 +        etac @{thm induct_set_step}))]) (r downto 1)) 1;
    1.92 +
    1.93 +fun mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's =
    1.94 +  EVERY [mk_induct_prepare_prem_tac n m k,
    1.95 +    mk_induct_prepare_prem_prems_tac nn kk r, atac 1,
    1.96 +    mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's];
    1.97 +
    1.98 +fun mk_induct_tac ctxt ns mss rss ctr_defs fld_induct' pre_set_defss set_natural's =
    1.99 +  let
   1.100 +    val nn = length ns;
   1.101 +    val n = Integer.sum ns;
   1.102 +  in
   1.103 +    mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
   1.104 +    EVERY (map5 (fn kk => fn pre_set_defs =>
   1.105 +        EVERY ooo map3 (fn m => fn k => fn r =>
   1.106 +            mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's))
   1.107 +      (1 upto nn) pre_set_defss mss (unflat mss (1 upto Integer.sum ns)) rss)
   1.108 +  end;
   1.109 +
   1.110  end;