# HG changeset patch # User blanchet # Date 1410888217 -7200 # Node ID c9f374b64d994d8eebca5f72375eda8fd87f1238 # Parent 37745650a3f43d5d7e29667f0a6dd995bb3d31c7 tuned fact visibility diff -r 37745650a3f4 -r c9f374b64d99 src/HOL/BNF_Composition.thy --- a/src/HOL/BNF_Composition.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/BNF_Composition.thy Tue Sep 16 19:23:37 2014 +0200 @@ -146,7 +146,8 @@ rel: "op = :: 'a \ 'a \ bool" by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) -definition id_bnf :: "'a \ 'a" where "id_bnf \ (\x. x)" +definition id_bnf :: "'a \ 'a" where + "id_bnf \ (\x. x)" lemma id_bnf_apply: "id_bnf x = x" unfolding id_bnf_def by simp @@ -177,7 +178,4 @@ ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer -hide_const (open) id_bnf -hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV - end diff -r 37745650a3f4 -r c9f374b64d99 src/HOL/Basic_BNF_Least_Fixpoints.thy --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy Tue Sep 16 19:23:37 2014 +0200 @@ -42,7 +42,7 @@ unfolding xtor_def by (rule refl) lemma xtor_set: "f (xtor x) = f x" - unfolding xtor_def by (rule refl) + unfolding xtor_def by (rule refl) lemma xtor_rel: "R (xtor x) (xtor y) = R x y" unfolding xtor_def by (rule refl) @@ -58,24 +58,30 @@ definition ctor_rec :: "'a \ 'a" where "ctor_rec x = x" -lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \ g \ BNF_Composition.id_bnf) x)" +lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((id_bnf \ g \ id_bnf) x)" unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) -lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (BNF_Composition.id_bnf \ g \ BNF_Composition.id_bnf))" - unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl) +lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (id_bnf \ g \ id_bnf))" + unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) -lemma xtor_rel_induct: "(\x y. vimage2p BNF_Composition.id_bnf BNF_Composition.id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR" - unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default +lemma xtor_rel_induct: "(\x y. vimage2p id_bnf id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR" + unfolding xtor_def vimage2p_def id_bnf_def by default -lemma Inl_def_alt: "Inl \ (\a. xtor (BNF_Composition.id_bnf (Inl a)))" - unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) +lemma Inl_def_alt: "Inl \ (\a. xtor (id_bnf (Inl a)))" + unfolding xtor_def id_bnf_def by (rule reflexive) -lemma Inr_def_alt: "Inr \ (\a. xtor (BNF_Composition.id_bnf (Inr a)))" - unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) +lemma Inr_def_alt: "Inr \ (\a. xtor (id_bnf (Inr a)))" + unfolding xtor_def id_bnf_def by (rule reflexive) -lemma Pair_def_alt: "Pair \ (\a b. xtor (BNF_Composition.id_bnf (a, b)))" - unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) +lemma Pair_def_alt: "Pair \ (\a b. xtor (id_bnf (a, b)))" + unfolding xtor_def id_bnf_def by (rule reflexive) ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" +hide_const (open) xtor ctor_rec + +hide_fact (open) + xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec + ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt + end diff -r 37745650a3f4 -r c9f374b64d99 src/HOL/Main.thy --- a/src/HOL/Main.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Main.thy Tue Sep 16 19:23:37 2014 +0200 @@ -32,7 +32,9 @@ hide_const (open) czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift - shift proj + shift proj id_bnf + +hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV no_syntax (xsymbols) "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) diff -r 37745650a3f4 -r c9f374b64d99 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Sep 16 19:23:37 2014 +0200 @@ -293,8 +293,8 @@ unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject :: abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ - @{thms BNF_Composition.id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def - Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN + @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False + iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN' (rtac refl ORELSE' atac)))) cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs @@ -308,7 +308,7 @@ (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2) THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @ - @{thms BNF_Composition.id_bnf_def vimage2p_def}) THEN + @{thms id_bnf_def vimage2p_def}) THEN TRYALL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False Inr_Inl_False sum.inject prod.inject}) THEN @@ -356,8 +356,7 @@ fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses = let - val assms_ctor_defs = - map (unfold_thms ctxt (@{thm BNF_Composition.id_bnf_def} :: ctor_defs)) assms; + val assms_ctor_defs = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms; val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts; in @@ -367,8 +366,8 @@ cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts) THEN' atac THEN' hyp_subst_tac ctxt)) THEN unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @ - @{thms BNF_Composition.id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert - Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN + @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left + Un_empty_right empty_iff singleton_iff}) THEN REPEAT_DETERM (HEADGOAL (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN' REPEAT_DETERM o eresolve_tac @{thms UN_E UnE singletonE} THEN' diff -r 37745650a3f4 -r c9f374b64d99 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Sep 16 19:23:37 2014 +0200 @@ -2,7 +2,7 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2014 -Sugared datatype and codatatype constructions. +Registration of basic types as BNF least fixpoints (datatypes). *) structure BNF_LFP_Basic_Sugar : sig end = @@ -20,13 +20,11 @@ fun trivial_absT_info_of fpT = {absT = fpT, repT = fpT, - abs = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT), - rep = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT), - abs_inject = @{thm type_definition.Abs_inject - [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I UNIV_I]}, - abs_inverse = @{thm type_definition.Abs_inverse - [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]}, - type_definition = @{thm BNF_Composition.type_definition_id_bnf_UNIV}}; + abs = Const (@{const_name id_bnf}, fpT --> fpT), + rep = Const (@{const_name id_bnf}, fpT --> fpT), + abs_inject = @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV UNIV_I UNIV_I]}, + abs_inverse = @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV UNIV_I]}, + type_definition = @{thm type_definition_id_bnf_UNIV}}; fun the_frozen_ctr_sugar_of ctxt fpT_name = the (ctr_sugar_of ctxt fpT_name) diff -r 37745650a3f4 -r c9f374b64d99 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Sep 16 19:23:37 2014 +0200 @@ -63,8 +63,7 @@ funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); val rec_o_map_simps = - @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod - BNF_Composition.id_bnf_def}; + @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def}; fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses ctor_rec_o_map =