# HG changeset patch # User blanchet # Date 1348404773 -7200 # Node ID 53b3c532a08238741c65a1f69eea8e34eb890fb4 # Parent b39354db8629642f883a381d17cd08c4ab174c1b renamed low-level "map_unique" to have "ctor" or "dtor" in the name diff -r b39354db8629 -r 53b3c532a082 src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -32,6 +32,7 @@ val ctor_fold_uniqueN: string val ctor_foldsN: string val ctor_mapN: string + val ctor_map_uniqueN: string val ctor_recN: string val ctor_recsN: string val ctor_relN: string @@ -49,6 +50,7 @@ val dtor_ctorN: string val dtor_exhaustN: string val dtor_injectN: string + val dtor_map_uniqueN: string val dtor_srelN: string val dtor_strong_coinductN: string val dtor_unfoldN: string @@ -186,6 +188,8 @@ val ctor_mapN = ctorN ^ "_" ^ mapN val dtor_mapN = dtorN ^ "_" ^ mapN val map_uniqueN = mapN ^ uniqueN +val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN +val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN val min_algN = "min_alg" val morN = "mor" val bisN = "bis" diff -r b39354db8629 -r 53b3c532a082 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -2396,7 +2396,7 @@ |> Thm.close_derivation) end; - val map_unique_thm = + val dtor_map_unique_thm = let fun mk_prem u map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), @@ -2408,7 +2408,7 @@ in Skip_Proof.prove lthy [] [] (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) - (mk_map_unique_tac dtor_unfold_unique_thm map_comps) + (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps) |> Thm.close_derivation end; @@ -2933,7 +2933,7 @@ val ls' = if m = 1 then [0] else ls; val Jbnf_common_notes = - [(map_uniqueN, [fold_maps map_unique_thm])] @ + [(dtor_map_uniqueN, [fold_maps dtor_map_unique_thm])] @ map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r b39354db8629 -r 53b3c532a082 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 @@ -59,7 +59,7 @@ thm list list -> thm list list list -> tactic val mk_map_id_tac: thm list -> thm -> thm -> tactic val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic - val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic + val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic @@ -1255,7 +1255,7 @@ rtac conjI, rtac refl, rtac refl]) ks]) 1 end -fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} = +fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} = rtac unfold_unique 1 THEN unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN ALLGOALS (etac sym); diff -r b39354db8629 -r 53b3c532a082 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -1409,7 +1409,7 @@ map (fn thm => thm RS @{thm pointfreeE}) maps end; - val (map_unique_thms, map_unique_thm) = + val (ctor_map_unique_thms, ctor_map_unique_thm) = let fun mk_prem u map ctor ctor' = mk_Trueprop_eq (HOLogic.mk_comp (u, ctor), @@ -1420,7 +1420,7 @@ (map2 (curry HOLogic.mk_eq) us fs_maps)); val unique = Skip_Proof.prove lthy [] [] (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) - (K (mk_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs)) + (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs)) |> Thm.close_derivation; in `split_conj_thm unique @@ -1659,9 +1659,9 @@ val timer = time (timer "helpers for BNF properties"); - val map_id_tacs = map (K o mk_map_id_tac map_ids) map_unique_thms; + val map_id_tacs = map (K o mk_map_id_tac map_ids) ctor_map_unique_thms; val map_comp_tacs = - map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) map_unique_thms ks; + map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks; val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms; val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss); val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders)); @@ -1776,7 +1776,7 @@ val ls' = if m = 1 then [0] else ls val Ibnf_common_notes = - [(map_uniqueN, [fold_maps map_unique_thm])] + [(ctor_map_uniqueN, [fold_maps ctor_map_unique_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r b39354db8629 -r 53b3c532a082 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 @@ -42,7 +42,7 @@ val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic val mk_map_id_tac: thm list -> thm -> tactic val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic - val mk_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic + val mk_ctor_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm -> @@ -577,7 +577,7 @@ REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])), rtac sym, rtac o_apply] 1; -fun mk_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs = +fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs = let val n = length map_congs; fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},