renamed internal constant
authorblanchet
Thu Sep 04 09:02:43 2014 +0200 (2014-09-04)
changeset 581816d527272f7b2
parent 58180 95397823f39e
child 58182 82478e6c60cb
renamed internal constant
src/HOL/BNF_Composition.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/BNF_Composition.thy	Thu Sep 04 09:02:43 2014 +0200
     1.2 +++ b/src/HOL/BNF_Composition.thy	Thu Sep 04 09:02:43 2014 +0200
     1.3 @@ -146,29 +146,29 @@
     1.4    rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.5    by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
     1.6  
     1.7 -definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
     1.8 +definition id_bnf :: "'a \<Rightarrow> 'a" where "id_bnf \<equiv> (\<lambda>x. x)"
     1.9  
    1.10 -lemma id_bnf_comp_apply: "id_bnf_comp x = x"
    1.11 -  unfolding id_bnf_comp_def by simp
    1.12 +lemma id_bnf_apply: "id_bnf x = x"
    1.13 +  unfolding id_bnf_def by simp
    1.14  
    1.15  bnf ID: 'a
    1.16 -  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.17 +  map: "id_bnf :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.18    sets: "\<lambda>x. {x}"
    1.19    bd: natLeq
    1.20 -  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.21 -  unfolding id_bnf_comp_def
    1.22 +  rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.23 +  unfolding id_bnf_def
    1.24    apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    1.25    apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    1.26    apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    1.27    done
    1.28  
    1.29 -lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
    1.30 -  unfolding id_bnf_comp_def by unfold_locales auto
    1.31 +lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
    1.32 +  unfolding id_bnf_def by unfold_locales auto
    1.33  
    1.34  ML_file "Tools/BNF/bnf_comp_tactics.ML"
    1.35  ML_file "Tools/BNF/bnf_comp.ML"
    1.36  
    1.37 -hide_const (open) id_bnf_comp
    1.38 -hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
    1.39 +hide_const (open) id_bnf
    1.40 +hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
    1.41  
    1.42  end
     2.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 04 09:02:43 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 04 09:02:43 2014 +0200
     2.3 @@ -115,9 +115,8 @@
     2.4      val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
     2.5    in Envir.expand_term get end;
     2.6  
     2.7 -val id_bnf_comp_def = @{thm id_bnf_comp_def};
     2.8 -val expand_id_bnf_comp_def =
     2.9 -  expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals];
    2.10 +val id_bnf_def = @{thm id_bnf_def};
    2.11 +val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals];
    2.12  
    2.13  fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
    2.14    | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
    2.15 @@ -198,7 +197,7 @@
    2.16      fun mk_simplified_set set =
    2.17        let
    2.18          val setT = fastype_of set;
    2.19 -        val var_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var ((Name.uu, 0), setT);
    2.20 +        val var_set' = Const (@{const_name id_bnf}, setT --> setT) $ Var ((Name.uu, 0), setT);
    2.21          val goal = mk_Trueprop_eq (var_set', set);
    2.22          fun tac {context = ctxt, prems = _} =
    2.23            mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
    2.24 @@ -342,8 +341,8 @@
    2.25          Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
    2.26  
    2.27      val phi =
    2.28 -      Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
    2.29 -      $> Morphism.term_morphism "BNF" expand_id_bnf_comp_def;
    2.30 +      Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_def])
    2.31 +      $> Morphism.term_morphism "BNF" expand_id_bnf_def;
    2.32  
    2.33      val bnf'' = morph_bnf phi bnf';
    2.34    in
    2.35 @@ -720,8 +719,8 @@
    2.36          else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
    2.37      | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
    2.38  
    2.39 -fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf_comp}, _)) =
    2.40 -    Const (@{const_name id_bnf_comp}, absU --> absU)
    2.41 +fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf}, _)) =
    2.42 +    Const (@{const_name id_bnf}, absU --> absU)
    2.43    | mk_abs_or_rep getT (Type (_, Us)) abs =
    2.44      let val Ts = snd (dest_Type (getT (fastype_of abs)))
    2.45      in Term.subst_atomic_types (Ts ~~ Us) abs end;
    2.46 @@ -738,11 +737,11 @@
    2.47    in
    2.48      if inline then
    2.49        pair (repT,
    2.50 -        (@{const_name id_bnf_comp}, @{const_name id_bnf_comp},
    2.51 -         @{thm type_definition_id_bnf_comp_UNIV},
    2.52 -         @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_comp_UNIV]},
    2.53 -         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_comp_UNIV]},
    2.54 -         @{thm type_definition.Abs_cases[OF type_definition_id_bnf_comp_UNIV]}))
    2.55 +        (@{const_name id_bnf}, @{const_name id_bnf},
    2.56 +         @{thm type_definition_id_bnf_UNIV},
    2.57 +         @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]},
    2.58 +         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]},
    2.59 +         @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]}))
    2.60      else
    2.61        typedef (b, As, mx) set opt_morphs tac
    2.62        #>> (fn (T_name, ({Rep_name, Abs_name, ...},
    2.63 @@ -858,7 +857,7 @@
    2.64          Binding.empty Binding.empty []
    2.65          ((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    2.66  
    2.67 -    val unfolds = @{thm id_bnf_comp_apply} ::
    2.68 +    val unfolds = @{thm id_bnf_apply} ::
    2.69        (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
    2.70  
    2.71      val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Thu Sep 04 09:02:43 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Thu Sep 04 09:02:43 2014 +0200
     3.3 @@ -240,7 +240,7 @@
     3.4  
     3.5  val simplified_set_simps =
     3.6    @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
     3.7 -    o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_comp_def};
     3.8 +    o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_def};
     3.9  
    3.10  fun mk_simplified_set_tac ctxt collect_set_map =
    3.11    unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 04 09:02:43 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 04 09:02:43 2014 +0200
     4.3 @@ -290,7 +290,7 @@
     4.4        unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
     4.5        unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
     4.6          abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
     4.7 -        @{thms BNF_Composition.id_bnf_comp_def rel_sum_simps rel_prod_apply vimage2p_def
     4.8 +        @{thms BNF_Composition.id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def
     4.9          Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
    4.10        REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
    4.11          (rtac refl ORELSE' atac))))
    4.12 @@ -305,7 +305,7 @@
    4.13            (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
    4.14              THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
    4.15          unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
    4.16 -          @{thms BNF_Composition.id_bnf_comp_def vimage2p_def}) THEN
    4.17 +          @{thms BNF_Composition.id_bnf_def vimage2p_def}) THEN
    4.18          TRYALL (hyp_subst_tac ctxt) THEN
    4.19          unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
    4.20            Inr_Inl_False  sum.inject prod.inject}) THEN
    4.21 @@ -354,7 +354,7 @@
    4.22      Abs_pre_inverses =
    4.23    let
    4.24      val assms_ctor_defs =
    4.25 -      map (unfold_thms ctxt (@{thm BNF_Composition.id_bnf_comp_def} :: ctor_defs)) assms;
    4.26 +      map (unfold_thms ctxt (@{thm BNF_Composition.id_bnf_def} :: ctor_defs)) assms;
    4.27      val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
    4.28        |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
    4.29    in
    4.30 @@ -364,7 +364,7 @@
    4.31           cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
    4.32          THEN' atac THEN' hyp_subst_tac ctxt)) THEN
    4.33      unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
    4.34 -      @{thms BNF_Composition.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
    4.35 +      @{thms BNF_Composition.id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
    4.36          Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN
    4.37      REPEAT_DETERM (HEADGOAL
    4.38        (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 04 09:02:43 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 04 09:02:43 2014 +0200
     5.3 @@ -64,7 +64,7 @@
     5.4  
     5.5  val rec_o_map_simps =
     5.6    @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod
     5.7 -      BNF_Composition.id_bnf_comp_def};
     5.8 +      BNF_Composition.id_bnf_def};
     5.9  
    5.10  fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
    5.11      ctor_rec_o_map =