made typedef for the type of the bound optional (size-based)
authortraytel
Sun Mar 09 21:40:41 2014 +0100 (2014-03-09)
changeset 56012158dc03db8be
parent 56011 39d5043ce8a3
child 56013 508836bbfed4
made typedef for the type of the bound optional (size-based)
src/HOL/Tools/BNF/bnf_comp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Fri Mar 07 23:10:27 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 09 21:40:41 2014 +0100
     1.3 @@ -741,12 +741,14 @@
     1.4          (@{const_name id_bnf_comp}, @{const_name id_bnf_comp},
     1.5           @{thm type_definition_id_bnf_comp_UNIV},
     1.6           @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_comp_UNIV]},
     1.7 -         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_comp_UNIV]}))
     1.8 +         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_comp_UNIV]},
     1.9 +         @{thm type_definition.Abs_cases[OF type_definition_id_bnf_comp_UNIV]}))
    1.10      else
    1.11        typedef (b, As, mx) set opt_morphs tac
    1.12        #>> (fn (T_name, ({Rep_name, Abs_name, ...},
    1.13 -          {type_definition, Abs_inverse, Abs_inject, ...}) : Typedef.info) =>
    1.14 -        (Type (T_name, map TFree As), (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)))
    1.15 +          {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) =>
    1.16 +        (Type (T_name, map TFree As),
    1.17 +          (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases)))
    1.18    end;
    1.19  
    1.20  fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
    1.21 @@ -781,7 +783,7 @@
    1.22      val repTA = mk_T_of_bnf Ds As bnf;
    1.23      val T_bind = qualify b;
    1.24      val TA_params = Term.add_tfreesT repTA [];
    1.25 -    val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)), lthy) =
    1.26 +    val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
    1.27        maybe_typedef (T_bind, TA_params, NoSyn)
    1.28          (HOLogic.mk_UNIV repTA) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    1.29  
    1.30 @@ -809,24 +811,30 @@
    1.31      val bd_repT = fst (dest_relT (fastype_of bnf_bd));
    1.32      val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
    1.33      val params = Term.add_tfreesT bd_repT [];
    1.34 -    val deads = map TFree params;
    1.35      val all_deads = map TFree (fold Term.add_tfreesT Ds []);
    1.36  
    1.37 -    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
    1.38 -      typedef (bdT_bind, params, NoSyn)
    1.39 +    val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
    1.40 +      maybe_typedef (bdT_bind, params, NoSyn)
    1.41          (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    1.42  
    1.43 -    val bnf_bd' = mk_dir_image bnf_bd
    1.44 -      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
    1.45 -
    1.46 -    val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
    1.47 -    val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
    1.48 +    val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =
    1.49 +      if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl},
    1.50 +        bd_card_order_of_bnf bnf, bd_cinfinite_of_bnf bnf)
    1.51 +      else
    1.52 +        let
    1.53 +          val bnf_bd' = mk_dir_image bnf_bd (Const (Abs_bd_name, bd_repT --> bdT));
    1.54  
    1.55 -    val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
    1.56 -    val bd_card_order =
    1.57 -      @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
    1.58 -    val bd_cinfinite =
    1.59 -      (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
    1.60 +          val Abs_bdT_inj = mk_Abs_inj_thm Abs_bdT_inject;
    1.61 +          val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj Abs_bdT_cases;
    1.62 +      
    1.63 +          val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
    1.64 +          val bd_card_order =
    1.65 +            @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
    1.66 +          val bd_cinfinite =
    1.67 +            (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
    1.68 +        in
    1.69 +          (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite)
    1.70 +        end;
    1.71  
    1.72      fun map_id0_tac ctxt =
    1.73        rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;