got rid of dead feature
authorblanchet
Tue Oct 01 14:13:24 2013 +0200 (2013-10-01)
changeset 54009f138452e8265
parent 54008 b15cfc2864de
child 54010 5ac1495fed4e
got rid of dead feature
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
src/HOL/BNF/Tools/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:13:24 2013 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature BNF_FP_N2M_SUGAR =
     1.6  sig
     1.7 -  val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     1.8 +  val mutualize_fp_sugars: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     1.9      (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
    1.10      local_theory ->
    1.11      (BNF_FP_Def_Sugar.fp_sugar list
    1.12 @@ -15,8 +15,8 @@
    1.13      * local_theory
    1.14    val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
    1.15      (term * term list list) list list -> term list list list list
    1.16 -  val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
    1.17 -    (term -> int list) -> ((term * term list list) list) list -> local_theory ->
    1.18 +  val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
    1.19 +    (term * term list list) list list -> local_theory ->
    1.20      (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
    1.21       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    1.22      * local_theory
    1.23 @@ -37,9 +37,7 @@
    1.24  (* TODO: test with sort constraints on As *)
    1.25  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    1.26     as deads? *)
    1.27 -fun mutualize_fp_sugars lose_co_rec mutualize fp bs fpTs get_indices callssss fp_sugars0
    1.28 -    no_defs_lthy0 =
    1.29 -  (* TODO: Also check whether there's any lost recursion? *)
    1.30 +fun mutualize_fp_sugars mutualize fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
    1.31    if mutualize orelse has_duplicates (op =) fpTs then
    1.32      let
    1.33        val thy = Proof_Context.theory_of no_defs_lthy0;
    1.34 @@ -79,11 +77,6 @@
    1.35          |> mk_TFrees nn
    1.36          ||>> variant_tfrees fp_b_names;
    1.37  
    1.38 -      (* If "lose_co_rec" is "true", the function "null" on "'a list" gives rise to
    1.39 -           'list = unit + 'a list
    1.40 -         instead of
    1.41 -           'list = unit + 'list
    1.42 -         resulting in a simpler (co)induction rule and (co)recursor. *)
    1.43        fun freeze_fp_default (T as Type (s, Ts)) =
    1.44            (case find_index (curry (op =) T) fpTs of
    1.45              ~1 => Type (s, map freeze_fp_default Ts)
    1.46 @@ -100,7 +93,7 @@
    1.47              [] =>
    1.48              (case union (op = o pairself fst)
    1.49                  (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
    1.50 -              [] => T |> not lose_co_rec ? freeze_fp_default
    1.51 +              [] => freeze_fp_default T
    1.52              | [(kk, _)] => nth Xs kk
    1.53              | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
    1.54            | callss =>
    1.55 @@ -201,7 +194,7 @@
    1.56  
    1.57  fun pad_and_indexify_calls fp_sugars0 = map2 indexify_callsss fp_sugars0 oo pad_list [];
    1.58  
    1.59 -fun nested_to_mutual_fps lose_co_rec fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
    1.60 +fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
    1.61    let
    1.62      val qsoty = quote o Syntax.string_of_typ lthy;
    1.63      val qsotys = space_implode " or " o map qsoty;
    1.64 @@ -264,7 +257,7 @@
    1.65      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
    1.66  
    1.67      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    1.68 -      mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.69 +      mutualize_fp_sugars mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.70          perm_fp_sugars0 lthy;
    1.71  
    1.72      val fp_sugars = unpermute perm_fp_sugars;
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 14:05:25 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 14:13:24 2013 +0200
     2.3 @@ -422,8 +422,6 @@
     2.4        | NONE => [])
     2.5    | map_thms_of_typ _ _ = [];
     2.6  
     2.7 -val lose_co_rec = false (*FIXME: try true?*);
     2.8 -
     2.9  fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
    2.10    let
    2.11      val thy = Proof_Context.theory_of lthy;
    2.12 @@ -431,7 +429,7 @@
    2.13      val ((missing_arg_Ts, perm0_kks,
    2.14            fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
    2.15              co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') =
    2.16 -      nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy;
    2.17 +      nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy;
    2.18  
    2.19      val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
    2.20  
    2.21 @@ -515,7 +513,7 @@
    2.22      val ((missing_res_Ts, perm0_kks,
    2.23            fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
    2.24              co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') =
    2.25 -      nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
    2.26 +      nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy;
    2.27  
    2.28      val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
    2.29  
     3.1 --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 14:05:25 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 14:13:24 2013 +0200
     3.3 @@ -95,8 +95,7 @@
     3.4      val has_nested = nn > nn_fp;
     3.5  
     3.6      val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
     3.7 -      mutualize_fp_sugars false has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0
     3.8 -        lthy;
     3.9 +      mutualize_fp_sugars has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy;
    3.10  
    3.11      val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
    3.12        fp_sugars;