# HG changeset patch # User blanchet # Date 1370621095 -3600 # Node ID 07fd21c01e93bceac61cb064f60baa048d2a4980 # Parent 740923a6e53043f2c39da695a8fdd0ae33412dd4 code simplifications (cf. 78a3d5006cf1) diff -r 740923a6e530 -r 07fd21c01e93 src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Fri Jun 07 16:19:52 2013 +0100 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Fri Jun 07 17:04:55 2013 +0100 @@ -105,9 +105,6 @@ "sum_case f g \ Inr = g" by auto -lemma ident_o_ident: "(\x. x) \ (\x. x) = (\x. x)" -by (rule o_def) - lemma mem_UN_compreh_eq: "(z : \{y. \x\A. y = F x}) = (\x\A. z : F x)" by blast diff -r 740923a6e530 -r 07fd21c01e93 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 16:19:52 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 17:04:55 2013 +0100 @@ -1,6 +1,6 @@ (* Title: HOL/BNF/Tools/bnf_fp_def_sugar.ML Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Copyright 2012, 2013 Sugared datatype and codatatype constructions. *) @@ -36,8 +36,7 @@ * (typ list list * typ list list list list * term list list * term list list list list) list option * (string * term list * term list list - * ((term list list * term list list list) - * (typ list * typ list list list * typ list list)) list) option) + * ((term list list * term list list list) * (typ list * typ list list)) list) option) * Proof.context val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term -> @@ -47,8 +46,7 @@ (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> (term list * thm list) * Proof.context val define_coiters: string list -> string * term list * term list list - * ((term list list * term list list list) - * (typ list * typ list list list * typ list list)) list -> + * ((term list list * term list list list) * (typ list * typ list list)) list -> (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> (term list * thm list) * Proof.context val derive_induct_iters_thms_for_types: BNF_Def.bnf list -> @@ -379,10 +377,10 @@ val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss; val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; - in (q_Tssss, f_Tssss, (f_sum_prod_Ts, f_Tsss, pf_Tss)) end; + in (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss)) end; - val (r_Tssss, g_Tssss, unfold_types) = mk_types single un_fold_of; - val (s_Tssss, h_Tssss, corec_types) = mk_types unzip_corecT co_rec_of; + val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types single un_fold_of; + val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types unzip_corecT co_rec_of; val ((((Free (z, _), cs), pss), gssss), lthy) = lthy @@ -408,7 +406,7 @@ mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf) (build_sum_inj Inr_const (fastype_of cf', T) $ cf'); - fun mk_args qssss fssss (_, f_Tsss, _) = + fun mk_args qssss fssss f_Tsss = let val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss; val cqssss = map2 (map o map o map o rapp) cs qssss; @@ -416,8 +414,8 @@ val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; in (pfss, cqfsss) end; - val unfold_args = mk_args rssss gssss unfold_types; - val corec_args = mk_args sssss hssss corec_types; + val unfold_args = mk_args rssss gssss g_Tsss; + val corec_args = mk_args sssss hssss h_Tsss; in ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy) end; @@ -494,7 +492,7 @@ val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters))); - fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, _, pf_Tss)) dtor_coiter = + fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter = let val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT; val b = mk_binding suf; @@ -862,11 +860,10 @@ val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs; val unfold_tacss = - map3 (map oo mk_coiter_tac unfold_defs [] nesting_map_ids'' []) + map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'') (map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss; val corec_tacss = - map3 (map oo mk_coiter_tac corec_defs nested_map_comp's - (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs) + map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'') (map co_rec_of dtor_coiter_thmss) pre_map_defs ctr_defss; fun prove goal tac = diff -r 740923a6e530 -r 07fd21c01e93 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Jun 07 16:19:52 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Jun 07 17:04:55 2013 +0100 @@ -14,8 +14,7 @@ val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic - val mk_coiter_tac: thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm -> - Proof.context -> tactic + val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> tactic val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic @@ -106,16 +105,13 @@ unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_ids'' @ iter_unfold_thms) THEN HEADGOAL (rtac refl); -val coiter_unfold_thms = - @{thms id_def ident_o_ident sum_case_if sum_case_o_inj} @ sum_prod_thms_map; +val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map; -fun mk_coiter_tac coiter_defs map_comp's map_ids'' map_if_distribs - ctor_dtor_coiter pre_map_def ctr_def ctxt = +fun mk_coiter_tac coiter_defs map_ids'' ctor_dtor_coiter pre_map_def ctr_def ctxt = unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE - (unfold_thms_tac ctxt (pre_map_def :: map_comp's @ map_ids'' @ map_if_distribs @ - coiter_unfold_thms) THEN + (unfold_thms_tac ctxt (pre_map_def :: map_ids'' @ coiter_unfold_thms) THEN HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))); fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =