# HG changeset patch # User blanchet # Date 1349081190 -7200 # Node ID 61729b1493972a692bf10a0fb3d5c1b2800cb29a # Parent c7a034d01936c24e7192dc922048dc710a5c2733 tweaked corecursor/coiterator tactic diff -r c7a034d01936 -r 61729b149397 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Oct 01 10:34:58 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Oct 01 10:46:30 2012 +0200 @@ -281,8 +281,7 @@ val pre_rel_defs = map rel_def_of_bnf pre_bnfs; val nested_map_comp's = map map_comp'_of_bnf nested_bnfs; val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs; - val nesting_map_ids = map map_id_of_bnf nesting_bnfs; - val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def}) nesting_map_ids; + val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs; val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs; val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs; @@ -1002,10 +1001,10 @@ map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; val unfold_tacss = - map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids) fp_fold_thms pre_map_defs - ctr_defss; + map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids'') fp_fold_thms + pre_map_defs ctr_defss; val corec_tacss = - map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs + map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids'') fp_rec_thms pre_map_defs ctr_defss; fun prove goal tac = diff -r c7a034d01936 -r 61729b149397 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Oct 01 10:34:58 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Oct 01 10:46:30 2012 +0200 @@ -107,11 +107,10 @@ unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_comp's @ map_ids'' @ rec_like_unfold_thms) THEN rtac refl 1; -fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt = +fun mk_corec_like_tac corec_like_defs map_ids'' ctor_dtor_corec_like pre_map_def ctr_def ctxt = unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN (rtac (ctor_dtor_corec_like RS trans) THEN' asm_simp_tac ss_if_True_False) 1 THEN - unfold_thms_tac ctxt (pre_map_def :: sum_prod_thms_map @ map_ids) THEN - unfold_thms_tac ctxt @{thms id_def} THEN + unfold_thms_tac ctxt (pre_map_def :: @{thm id_def} :: sum_prod_thms_map @ map_ids'') THEN (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) 1; fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =