don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
authorblanchet
Tue Nov 29 08:32:46 2016 +0100 (2016-11-29)
changeset 64532fc2835a932d9
parent 64531 166a2563e0ca
child 64534 ff59fe6b6f6a
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
NEWS
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/NEWS	Tue Nov 29 08:32:44 2016 +0100
     1.2 +++ b/NEWS	Tue Nov 29 08:32:46 2016 +0100
     1.3 @@ -6,6 +6,11 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +* (Co)datatype package:
     1.8 +  - The 'size_gen_o_map' lemma is no longer generated for datatypes
     1.9 +    with type class annotations. As a result, the tactic that derives
    1.10 +    it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
    1.11 +
    1.12  
    1.13  
    1.14  New in Isabelle2016-1 (December 2016)
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Nov 29 08:32:44 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Nov 29 08:32:46 2016 +0100
     2.3 @@ -341,7 +341,8 @@
     2.4                fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars [];
     2.5  
     2.6              val size_gen_o_map_thmss =
     2.7 -              if nested_size_gen_o_maps_complete then
     2.8 +              if nested_size_gen_o_maps_complete
     2.9 +                 andalso forall (fn TFree (_, S) => S = @{sort type}) As then
    2.10                  @{map 3} (fn goal => fn size_def => fn rec_o_map =>
    2.11                      Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
    2.12                        mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)