killed dead code
authorblanchet
Fri Jun 07 16:19:52 2013 +0100 (2013-06-07)
changeset 52348740923a6e530
parent 52347 ead18e3b2c1b
child 52349 07fd21c01e93
killed dead code
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 14:45:07 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 16:19:52 2013 +0100
     1.3 @@ -59,7 +59,8 @@
     1.4      (thm list * thm * Args.src list) * (thm list list * Args.src list)
     1.5      * (thm list list * Args.src list)
     1.6    val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
     1.7 -    string * term list * term list list * ((term list list * term list list list) * 'a) list ->
     1.8 +    string * term list * term list list * ((term list list * term list list list)
     1.9 +      * (typ list * typ list list list * typ list list)) list ->
    1.10      thm list -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list ->
    1.11      typ list -> typ list -> int list list -> int list list -> int list -> thm list list ->
    1.12      BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> local_theory ->
    1.13 @@ -241,17 +242,6 @@
    1.14  
    1.15  val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
    1.16  
    1.17 -fun project_co_recT special_Tname Cs proj =
    1.18 -  let
    1.19 -    fun project (Type (s, Ts as [T, U])) =
    1.20 -        if s = special_Tname andalso member (op =) Cs U then proj (T, U)
    1.21 -        else Type (s, map project Ts)
    1.22 -      | project (Type (s, Ts)) = Type (s, map project Ts)
    1.23 -      | project T = T;
    1.24 -  in project end;
    1.25 -
    1.26 -val project_corecT = project_co_recT @{type_name sum};
    1.27 -
    1.28  fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) =
    1.29      if member (op =) Cs U then Ts else [T]
    1.30    | unzip_recT _ T = [T];
    1.31 @@ -458,7 +448,7 @@
    1.32        (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)))
    1.33    end;
    1.34  
    1.35 -fun mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqfsss dtor_coiter =
    1.36 +fun mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter =
    1.37    Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss);
    1.38  
    1.39  fun define_co_iters fp fpT Cs binding_specs lthy0 =
    1.40 @@ -504,13 +494,13 @@
    1.41  
    1.42      val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
    1.43  
    1.44 -    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, f_Tsss, pf_Tss)) dtor_coiter =
    1.45 +    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, _, pf_Tss)) dtor_coiter =
    1.46        let
    1.47          val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
    1.48          val b = mk_binding suf;
    1.49          val spec =
    1.50            mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
    1.51 -            mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqfsss dtor_coiter);
    1.52 +            mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter);
    1.53        in (b, spec) end;
    1.54    in
    1.55      define_co_iters Greatest_FP fpT Cs
    1.56 @@ -884,8 +874,6 @@
    1.57            |> Thm.close_derivation;
    1.58  
    1.59          val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
    1.60 -        val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
    1.61 -
    1.62          val corec_thmss =
    1.63            map2 (map2 prove) corec_goalss corec_tacss
    1.64            |> map (map (unfold_thms lthy @{thms sum_case_if}));