make 'typedef' optional, depending on size of original type
authorblanchet
Mon Mar 03 12:48:20 2014 +0100 (2014-03-03)
changeset 55854ee270328a781
parent 55853 e776a4b813d1
child 55855 98ad5680173a
make 'typedef' optional, depending on size of original type
src/HOL/BNF_Comp.thy
src/HOL/BNF_FP_Base.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
     1.1 --- a/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:19 2014 +0100
     1.2 +++ b/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -128,6 +128,12 @@
     1.4  
     1.5  end
     1.6  
     1.7 +definition id_rep :: "'a \<Rightarrow> 'a" where "id_rep = (\<lambda>x. x)"
     1.8 +definition id_abs :: "'a \<Rightarrow> 'a" where "id_abs = (\<lambda>x. x)"
     1.9 +
    1.10 +lemma type_definition_id_rep_abs_UNIV: "type_definition id_rep id_abs UNIV"
    1.11 +  unfolding id_rep_def id_abs_def by unfold_locales auto
    1.12 +
    1.13  lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
    1.14  by (metis csum_absorb2' ordIso_transitive ordLeq_refl)
    1.15  
    1.16 @@ -137,4 +143,7 @@
    1.17  ML_file "Tools/BNF/bnf_comp_tactics.ML"
    1.18  ML_file "Tools/BNF/bnf_comp.ML"
    1.19  
    1.20 +hide_const id_rep id_abs
    1.21 +hide_fact id_rep_def id_abs_def type_definition_id_rep_abs_UNIV
    1.22 +
    1.23  end
     2.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Mar 03 12:48:19 2014 +0100
     2.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Mar 03 12:48:20 2014 +0100
     2.3 @@ -177,6 +177,9 @@
     2.4      type_definition.Abs_inverse[OF assms(1) UNIV_I]
     2.5      type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
     2.6  
     2.7 +lemma vimage2p_id: "vimage2p id id R = R"
     2.8 +  unfolding vimage2p_def by auto
     2.9 +
    2.10  lemma vimage2p_comp: "vimage2p (f1 o f2) (g1 o g2) = vimage2p f2 g2 o vimage2p f1 g1"
    2.11    unfolding fun_eq_iff vimage2p_def o_apply by simp
    2.12  
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:19 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:20 2014 +0100
     3.3 @@ -6,6 +6,8 @@
     3.4  Composition of bounded natural functors.
     3.5  *)
     3.6  
     3.7 +val inline_ref = Unsynchronized.ref true;
     3.8 +
     3.9  signature BNF_COMP =
    3.10  sig
    3.11    val ID_bnf: BNF_Def.bnf
    3.12 @@ -628,18 +630,45 @@
    3.13    let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
    3.14    in Term.typ_subst_TVars rho absT end;
    3.15  
    3.16 -fun mk_repT (t as Type (C, Ts)) repT (u as Type (C', Us)) =
    3.17 -    if C = C' andalso length Ts = length Us then Term.typ_subst_atomic (Ts ~~ Us) repT
    3.18 -    else raise Term.TYPE ("mk_repT", [t, repT, u], [])
    3.19 -  | mk_repT t repT u =  raise Term.TYPE ("mk_repT", [t, repT, u], []);
    3.20 +fun mk_repT absT repT absU =
    3.21 +  if absT = repT then absU
    3.22 +  else
    3.23 +    (case (absT, absU) of
    3.24 +      (Type (C, Ts), Type (C', Us)) =>
    3.25 +        if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT
    3.26 +        else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
    3.27 +    | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
    3.28  
    3.29 -fun mk_abs_or_rep getT (Type (_, Us)) abs =
    3.30 -  let val Ts = snd (dest_Type (getT (fastype_of abs)))
    3.31 -  in Term.subst_atomic_types (Ts ~~ Us) abs end;
    3.32 +fun mk_abs_or_rep _ absU (Const (@{const_name id_abs}, _)) =
    3.33 +    Const (@{const_name id_abs}, absU --> absU)
    3.34 +  | mk_abs_or_rep _ absU (Const (@{const_name id_rep}, _)) =
    3.35 +    Const (@{const_name id_rep}, absU --> absU)
    3.36 +  | mk_abs_or_rep getT (Type (_, Us)) abs =
    3.37 +    let val Ts = snd (dest_Type (getT (fastype_of abs)))
    3.38 +    in Term.subst_atomic_types (Ts ~~ Us) abs end;
    3.39  
    3.40  val mk_abs = mk_abs_or_rep range_type;
    3.41  val mk_rep = mk_abs_or_rep domain_type;
    3.42  
    3.43 +val smart_max_inline_type_size = 5; (*FUDGE*)
    3.44 +
    3.45 +fun maybe_typedef (b, As, mx) set opt_morphs tac =
    3.46 +  let
    3.47 +    val repT = HOLogic.dest_setT (fastype_of set);
    3.48 +    val inline = Term.size_of_typ repT <= smart_max_inline_type_size;
    3.49 +  in
    3.50 +    if inline then
    3.51 +      pair (repT,
    3.52 +        (@{const_name id_rep}, @{const_name id_abs}, @{thm type_definition_id_rep_abs_UNIV},
    3.53 +         @{thm type_definition.Abs_inverse[OF type_definition_id_rep_abs_UNIV]},
    3.54 +         @{thm type_definition.Abs_inject[OF type_definition_id_rep_abs_UNIV]}))
    3.55 +    else
    3.56 +      typedef (b, As, mx) set opt_morphs tac
    3.57 +      #>> (fn (T_name, ({Rep_name, Abs_name, ...},
    3.58 +          {type_definition, Abs_inverse, Abs_inject, ...}) : Typedef.info) =>
    3.59 +        (Type (T_name, map TFree As), (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)))
    3.60 +  end;
    3.61 +
    3.62  fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
    3.63    let
    3.64      val live = live_of_bnf bnf;
    3.65 @@ -670,25 +699,23 @@
    3.66      fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
    3.67  
    3.68      val repTA = mk_T_of_bnf Ds As bnf;
    3.69 -    val repTB = mk_T_of_bnf Ds Bs bnf;
    3.70      val T_bind = qualify b;
    3.71      val TA_params = Term.add_tfreesT repTA [];
    3.72 -    val TB_params = Term.add_tfreesT repTB [];
    3.73 -    val ((T_name, (T_glob_info, T_loc_info)), lthy) =
    3.74 -      typedef (T_bind, TA_params, NoSyn)
    3.75 +    val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)), lthy) =
    3.76 +      maybe_typedef (T_bind, TA_params, NoSyn)
    3.77          (HOLogic.mk_UNIV repTA) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    3.78 -    val TA = Type (T_name, map TFree TA_params);
    3.79 -    val TB = Type (T_name, map TFree TB_params);
    3.80 -    val RepA = Const (#Rep_name T_glob_info, TA --> repTA);
    3.81 -    val RepB = Const (#Rep_name T_glob_info, TB --> repTB);
    3.82 -    val AbsA = Const (#Abs_name T_glob_info, repTA --> TA);
    3.83 -    val AbsB = Const (#Abs_name T_glob_info, repTB --> TB);
    3.84 -    val typedef_thm = #type_definition T_loc_info;
    3.85 -    val Abs_inject' = #Abs_inject T_loc_info OF @{thms UNIV_I UNIV_I};
    3.86 -    val Abs_inverse' = #Abs_inverse T_loc_info OF @{thms UNIV_I};
    3.87 +
    3.88 +    val repTB = mk_T_of_bnf Ds Bs bnf;
    3.89 +    val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
    3.90 +    val RepA = Const (Rep_name, TA --> repTA);
    3.91 +    val RepB = Const (Rep_name, TB --> repTB);
    3.92 +    val AbsA = Const (Abs_name, repTA --> TA);
    3.93 +    val AbsB = Const (Abs_name, repTB --> TB);
    3.94 +    val Abs_inject' = Abs_inject OF @{thms UNIV_I UNIV_I};
    3.95 +    val Abs_inverse' = Abs_inverse OF @{thms UNIV_I};
    3.96  
    3.97      val absT_info = {absT = TA, repT = repTA, abs = AbsA, rep = RepA, abs_inject = Abs_inject',
    3.98 -      abs_inverse = Abs_inverse', type_definition = typedef_thm};
    3.99 +      abs_inverse = Abs_inverse', type_definition = type_definition};
   3.100  
   3.101      val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
   3.102        Term.list_comb (expand_maps (mk_map_of_bnf Ds As Bs bnf), fs)), RepA));
   3.103 @@ -722,15 +749,16 @@
   3.104        (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
   3.105  
   3.106      fun map_id0_tac ctxt =
   3.107 -      rtac (@{thm type_copy_map_id0} OF [typedef_thm, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
   3.108 +      rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
   3.109      fun map_comp0_tac ctxt =
   3.110 -      rtac (@{thm type_copy_map_comp0} OF [typedef_thm, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
   3.111 +      rtac (@{thm type_copy_map_comp0} OF
   3.112 +        [type_definition, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
   3.113      fun map_cong0_tac ctxt =
   3.114        EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (unfold_all ctxt (map_cong0_of_bnf bnf)) ::
   3.115          map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp,
   3.116            etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
   3.117      fun set_map0_tac thm ctxt =
   3.118 -      rtac (@{thm type_copy_set_map0} OF [typedef_thm, unfold_all ctxt thm]) 1;
   3.119 +      rtac (@{thm type_copy_set_map0} OF [type_definition, unfold_all ctxt thm]) 1;
   3.120      val set_bd_tacs = map (fn thm => fn ctxt => rtac (@{thm ordLeq_ordIso_trans} OF
   3.121          [unfold_sets ctxt thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1)
   3.122        (set_bd_of_bnf bnf);
   3.123 @@ -738,8 +766,9 @@
   3.124        rtac (unfold_rels ctxt (le_rel_OO_of_bnf bnf) RS @{thm vimage2p_relcompp_mono}) 1;
   3.125      fun rel_OO_Grp_tac ctxt =
   3.126        (rtac (unfold_all ctxt (rel_OO_Grp_of_bnf bnf) RS @{thm vimage2p_cong} RS trans) THEN'
   3.127 -      SELECT_GOAL (unfold_thms_tac ctxt [o_apply, typedef_thm RS @{thm type_copy_vimage2p_Grp_Rep},
   3.128 -        typedef_thm RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
   3.129 +      SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
   3.130 +        type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
   3.131 +        type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
   3.132  
   3.133      val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac
   3.134        (map set_map0_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1))
   3.135 @@ -750,7 +779,7 @@
   3.136            (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
   3.137        (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   3.138  
   3.139 -    fun wit_tac ctxt = ALLGOALS (dtac (typedef_thm RS @{thm type_copy_wit})) THEN
   3.140 +    fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
   3.141        mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
   3.142  
   3.143      val (bnf', lthy') =
     4.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 03 12:48:19 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 03 12:48:20 2014 +0100
     4.3 @@ -90,7 +90,7 @@
     4.4  
     4.5    val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
     4.6  
     4.7 -  datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
     4.8 +  datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
     4.9    datatype fact_policy = Dont_Note | Note_Some | Note_All
    4.10  
    4.11    val bnf_note_all: bool Config.T
    4.12 @@ -100,7 +100,7 @@
    4.13      Proof.context
    4.14  
    4.15    val print_bnfs: Proof.context -> unit
    4.16 -  val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    4.17 +  val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    4.18      (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
    4.19      binding -> binding -> binding list ->
    4.20      (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
    4.21 @@ -109,7 +109,7 @@
    4.22      ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
    4.23      local_theory * thm list
    4.24  
    4.25 -  val define_bnf_consts: const_policy -> fact_policy -> typ list option ->
    4.26 +  val define_bnf_consts: inline_policy -> fact_policy -> typ list option ->
    4.27      binding -> binding -> binding list ->
    4.28      (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
    4.29        ((typ list * typ list * typ list * typ) *
    4.30 @@ -121,7 +121,7 @@
    4.31          (typ list -> typ list -> typ list -> term) *
    4.32          (typ list -> typ list -> typ list -> term))) * local_theory
    4.33  
    4.34 -  val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    4.35 +  val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    4.36      (Proof.context -> tactic) list ->
    4.37      (Proof.context -> tactic) -> typ list option -> binding ->
    4.38      binding -> binding list ->
    4.39 @@ -583,7 +583,7 @@
    4.40  val rel_comppN = "rel_compp";
    4.41  val rel_compp_GrpN = "rel_compp_Grp";
    4.42  
    4.43 -datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
    4.44 +datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
    4.45  
    4.46  datatype fact_policy = Dont_Note | Note_Some | Note_All;
    4.47  
    4.48 @@ -592,7 +592,7 @@
    4.49  
    4.50  fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
    4.51  
    4.52 -val smart_max_inline_size = 25; (*FUDGE*)
    4.53 +val smart_max_inline_term_size = 25; (*FUDGE*)
    4.54  
    4.55  fun note_bnf_thms fact_policy qualify' bnf_b bnf =
    4.56    let
    4.57 @@ -676,7 +676,7 @@
    4.58            (case const_policy of
    4.59              Dont_Inline => false
    4.60            | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
    4.61 -          | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_size
    4.62 +          | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_term_size
    4.63            | Do_Inline => true)
    4.64        in
    4.65          if inline then
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:19 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:20 2014 +0100
     5.3 @@ -207,7 +207,7 @@
     5.4              |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
     5.5              |> funpow n (fn thm => thm RS spec)
     5.6              |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
     5.7 -            |> unfold_thms lthy (@{thms vimage2p_comp comp_apply comp_id
     5.8 +            |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
     5.9                 Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
    5.10                 maps mk_fp_type_copy_thms fp_type_definitions @
    5.11                 maps mk_type_copy_thms type_definitions)