# HG changeset patch # User blanchet # Date 1393955837 -3600 # Node ID 8c6d49dd8ae1902b40cef20f491c51af2f16ecd0 # Parent 21aa30ea680644e240fdbd6c3621806c687a4688 renamed a pair of low-level theorems to have c/dtor in their names (like the others) diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 04 13:38:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 04 18:57:17 2014 +0100 @@ -183,8 +183,6 @@ fun co_induct_of (i :: _) = i; fun strong_co_induct_of [_, s] = s; -(* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *) - fun register_fp_sugar key fp_sugar = Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar))); diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 04 13:38:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 04 18:57:17 2014 +0100 @@ -58,6 +58,7 @@ val ctor_rec_o_mapN: string val ctor_rec_uniqueN: string val ctor_relN: string + val ctor_rel_inductN: string val ctor_set_inclN: string val ctor_set_set_inclN: string val disc_corecN: string @@ -75,6 +76,7 @@ val dtor_map_strong_coinductN: string val dtor_map_uniqueN: string val dtor_relN: string + val dtor_rel_coinductN: string val dtor_set_inclN: string val dtor_set_set_inclN: string val dtor_strong_coinductN: string @@ -323,7 +325,9 @@ val injectN = "inject" val rel_injectN = relN ^ "_" ^ injectN val rel_coinductN = relN ^ "_" ^ coinductN +val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN val rel_inductN = relN ^ "_" ^ inductN +val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN val selN = "sel" val sel_corecN = selN ^ "_" ^ corecN diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 04 13:38:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 04 18:57:17 2014 +0100 @@ -2570,7 +2570,7 @@ val common_notes = [(dtor_coinductN, [dtor_coinduct_thm]), - (rel_coinductN, [Jrel_coinduct_thm]), + (dtor_rel_coinductN, [Jrel_coinduct_thm]), (dtor_unfold_transferN, dtor_unfold_transfer_thms)] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Mar 04 13:38:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Mar 04 18:57:17 2014 +0100 @@ -1083,7 +1083,7 @@ (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1 end; -fun mk_unfold_transfer_tac ctxt m rel_coinduct map_transfers unfolds = +fun mk_unfold_transfer_tac ctxt m ctor_rel_coinduct map_transfers unfolds = let val n = length map_transfers; in @@ -1091,7 +1091,7 @@ @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN HEADGOAL (EVERY' - [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_coinduct, + [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_coinduct, EVERY' (map (fn map_transfer => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt unfolds), diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 04 13:38:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 04 18:57:17 2014 +0100 @@ -1825,8 +1825,8 @@ val common_notes = [(ctor_inductN, [ctor_induct_thm]), (ctor_induct2N, [ctor_induct2_thm]), - (rel_inductN, [Irel_induct_thm]), - (ctor_fold_transferN, ctor_fold_transfer_thms)] + (ctor_fold_transferN, ctor_fold_transfer_thms), + (ctor_rel_inductN, [Irel_induct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Mar 04 13:38:02 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Mar 04 18:57:17 2014 +0100 @@ -783,7 +783,7 @@ IHs ctor_rels rel_mono_strongs)] 1 end; -fun mk_fold_transfer_tac ctxt m rel_induct map_transfers folds = +fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds = let val n = length map_transfers; in @@ -791,7 +791,7 @@ @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN HEADGOAL (EVERY' - [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_induct, + [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_induct, EVERY' (map (fn map_transfer => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}], SELECT_GOAL (unfold_thms_tac ctxt folds),