more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
authorblanchet
Thu May 15 20:48:14 2014 +0200 (2014-05-15)
changeset 5696601637dd1260c
parent 56965 222f46a4dbec
child 56967 c3746e999805
more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu May 15 20:48:13 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu May 15 20:48:14 2014 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4            pair (snd_const T)
     1.5          else if exists (exists_subtype_in (As @ Cs)) Ts then
     1.6            (case Symtab.lookup data s of
     1.7 -            SOME (size_name, (_, size_o_maps as _ :: _)) =>
     1.8 +            SOME (size_name, (_, size_o_maps)) =>
     1.9              let
    1.10                val (args, size_o_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
    1.11                val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);
    1.12 @@ -160,9 +160,8 @@
    1.13        end;
    1.14  
    1.15      fun mk_size_rhs recx size_o_maps =
    1.16 -      let val (args, size_o_maps') = fold_map mk_size_arg rec_arg_Ts size_o_maps in
    1.17 -        (fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)), size_o_maps')
    1.18 -      end;
    1.19 +      fold_map mk_size_arg rec_arg_Ts size_o_maps
    1.20 +      |>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)));
    1.21  
    1.22      val maybe_conceal_def_binding = Thm.def_binding
    1.23        #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
    1.24 @@ -219,7 +218,7 @@
    1.25  
    1.26      val all_overloaded_size_defs = overloaded_size_defs @
    1.27        (Spec_Rules.retrieve lthy0 @{const size ('a)}
    1.28 -       |> map_filter (try (fn (Equational, (_, [thm])) => thm)));
    1.29 +       |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
    1.30  
    1.31      val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
    1.32      val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
    1.33 @@ -323,14 +322,19 @@
    1.34              map2 (fold_rev (fold_rev Logic.all) [fsB, gs] o
    1.35                curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo
    1.36                curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss;
    1.37 -          val size_o_map_thms =
    1.38 -            map3 (fn goal => fn size_def => fn rec_o_map =>
    1.39 +
    1.40 +          (* The "size o map" theorem generation will fail if 'nested_size_maps' is incomplete,
    1.41 +             which occurs when there is recursion through non-datatypes. In this case, we simply
    1.42 +             avoid generating the theorem. The resulting characteristic lemmas are then expressed
    1.43 +             in terms of "map", which is not the end of the world. *)
    1.44 +          val size_o_map_thmss =
    1.45 +            map3 (fn goal => fn size_def => the_list o try (fn rec_o_map =>
    1.46                  Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
    1.47                    mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
    1.48 -                |> Thm.close_derivation)
    1.49 -              size_o_map_goals size_defs rec_o_map_thms;
    1.50 +                |> Thm.close_derivation))
    1.51 +              size_o_map_goals size_defs rec_o_map_thms
    1.52          in
    1.53 -          pairself (map single) (rec_o_map_thms, size_o_map_thms)
    1.54 +          (map single rec_o_map_thms, size_o_map_thmss)
    1.55          end;
    1.56  
    1.57      val massage_multi_notes =