fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
authorblanchet
Mon Oct 01 11:04:30 2012 +0200 (2012-10-01)
changeset 49672902b24e0ffb4
parent 49671 61729b149397
child 49673 2a088cff1e7b
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:46:30 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 11:04:30 2012 +0200
     1.3 @@ -604,8 +604,8 @@
     1.4                    if s = s' then build_map (build_ctor_rec_arg mk_proj) T U else mk_proj T
     1.5                  | _ => mk_proj T);
     1.6  
     1.7 -            fun mk_U proj (T as Type (@{type_name prod}, [T', U])) =
     1.8 -                if member (op =) fpTs T' then proj (T', U) else T
     1.9 +            fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) =
    1.10 +                if member (op =) fpTs T' then proj (T', U) else Type (s, map (mk_U proj) Ts)
    1.11                | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
    1.12                | mk_U _ T = T;
    1.13  
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 10:46:30 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 11:04:30 2012 +0200
     2.3 @@ -100,7 +100,7 @@
     2.4  
     2.5  (*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*)
     2.6  val rec_like_unfold_thms =
     2.7 -  @{thms comp_def convol_def fst_conv id_def map_pair_def prod_case_Pair_iden snd_conv split_conv
     2.8 +  @{thms comp_def convol_def fst_conv id_def map_pair_simp prod_case_Pair_iden snd_conv split_conv
     2.9        sum.simps(5,6) sum_map.simps unit_case_Unity};
    2.10  
    2.11  fun mk_rec_like_tac pre_map_defs map_comp's map_ids'' rec_like_defs ctor_rec_like ctr_def ctxt =