tweaked corecursor/coiterator tactic
authorblanchet
Mon Oct 01 10:46:30 2012 +0200 (2012-10-01)
changeset 4967161729b149397
parent 49670 c7a034d01936
child 49672 902b24e0ffb4
tweaked corecursor/coiterator tactic
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:34:58 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:46:30 2012 +0200
     1.3 @@ -281,8 +281,7 @@
     1.4      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     1.5      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     1.6      val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
     1.7 -    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
     1.8 -    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def}) nesting_map_ids;
     1.9 +    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.10      val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
    1.11      val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
    1.12  
    1.13 @@ -1002,10 +1001,10 @@
    1.14                map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
    1.15  
    1.16              val unfold_tacss =
    1.17 -              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids) fp_fold_thms pre_map_defs
    1.18 -                ctr_defss;
    1.19 +              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids'') fp_fold_thms
    1.20 +                pre_map_defs ctr_defss;
    1.21              val corec_tacss =
    1.22 -              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
    1.23 +              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids'') fp_rec_thms pre_map_defs
    1.24                  ctr_defss;
    1.25  
    1.26              fun prove goal tac =
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 10:34:58 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 10:46:30 2012 +0200
     2.3 @@ -107,11 +107,10 @@
     2.4    unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_comp's @
     2.5      map_ids'' @ rec_like_unfold_thms) THEN rtac refl 1;
     2.6  
     2.7 -fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
     2.8 +fun mk_corec_like_tac corec_like_defs map_ids'' ctor_dtor_corec_like pre_map_def ctr_def ctxt =
     2.9    unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
    2.10    (rtac (ctor_dtor_corec_like RS trans) THEN' asm_simp_tac ss_if_True_False) 1 THEN
    2.11 -  unfold_thms_tac ctxt (pre_map_def :: sum_prod_thms_map @ map_ids) THEN
    2.12 -  unfold_thms_tac ctxt @{thms id_def} THEN
    2.13 +  unfold_thms_tac ctxt (pre_map_def :: @{thm id_def} :: sum_prod_thms_map @ map_ids'') THEN
    2.14    (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) 1;
    2.15  
    2.16  fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =