# HG changeset patch # User blanchet # Date 1377794643 -7200 # Node ID c8628119d18efc7af3012e3086a59fb85a22c02d # Parent 854fbb41e6cd4d3a10c92f0d133f61848ec95411 renamed BNF axiom diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Thu Aug 29 18:44:03 2013 +0200 @@ -376,7 +376,7 @@ qed qed -lemma mmap_id: "mmap id = id" +lemma mmap_id0: "mmap id = id" proof (intro ext multiset_eqI) fix f a show "count (mmap id f) a = count (id f) a" proof (cases "count f a = 0") @@ -872,7 +872,7 @@ (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def) bnf mmap [set_of] "\_::'a multiset. natLeq" ["{#}"] -by (auto simp add: mmap_id mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd +by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd intro: mmap_cong wpull_mmap) inductive multiset_rel' where diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 18:44:03 2013 +0200 @@ -149,9 +149,9 @@ (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd); - fun map_id_tac _ = - mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong0_of_bnf outer) - (map map_id_of_bnf inners); + fun map_id0_tac _ = + mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer) + (map map_id0_of_bnf inners); fun map_comp_tac _ = mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) @@ -233,7 +233,7 @@ rtac thm 1 end; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; @@ -300,7 +300,7 @@ val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd; - fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; + fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; fun map_comp_tac {context = ctxt, prems = _} = unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN rtac refl 1; @@ -339,7 +339,7 @@ rtac thm 1 end; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; @@ -390,7 +390,7 @@ val bd = mk_bd_of_bnf Ds As bnf; - fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; + fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; fun map_comp_tac {context = ctxt, prems = _} = unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN rtac refl 1; @@ -424,7 +424,7 @@ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -474,7 +474,7 @@ val bd = mk_bd_of_bnf Ds As bnf; - fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; + fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1; fun map_cong0_tac {context = ctxt, prems = _} = rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); @@ -497,7 +497,7 @@ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -630,7 +630,7 @@ (rtac (unfold_all thm) THEN' SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; - val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) + val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac (map_wpull_of_bnf bnf)) diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 18:44:03 2013 +0200 @@ -13,7 +13,7 @@ val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic - val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic + val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic val mk_comp_set_alt_tac: Proof.context -> thm -> tactic val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic @@ -58,9 +58,9 @@ unfold_thms_tac ctxt [collect_set_map RS sym] THEN rtac refl 1; -fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids = +fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s = EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @ - map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1; + map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1; fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps = EVERY' ([rtac ext, rtac sym, rtac trans_o_apply, diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 18:44:03 2013 +0200 @@ -55,8 +55,8 @@ val map_cong0_of_bnf: bnf -> thm val map_cong_of_bnf: bnf -> thm val map_def_of_bnf: bnf -> thm + val map_id0_of_bnf: bnf -> thm val map_id'_of_bnf: bnf -> thm - val map_id_of_bnf: bnf -> thm val map_transfer_of_bnf: bnf -> thm val map_wppull_of_bnf: bnf -> thm val map_wpull_of_bnf: bnf -> thm @@ -113,7 +113,7 @@ val fundef_cong_attrs = @{attributes [fundef_cong]}; type axioms = { - map_id: thm, + map_id0: thm, map_comp: thm, map_cong0: thm, set_map: thm list, @@ -125,7 +125,7 @@ }; fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) = - {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o, + {map_id0 = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o, bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel}; fun dest_cons [] = raise List.Empty @@ -147,14 +147,14 @@ fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel = [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel]; -fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, +fun dest_axioms {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, map_wpull, rel_OO_Grp} = - zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull + zip_axioms map_id0 map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull rel_OO_Grp; -fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, +fun map_axioms f {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, map_wpull, rel_OO_Grp} = - {map_id = f map_id, + {map_id0 = f map_id0, map_comp = f map_comp, map_cong0 = f map_cong0, set_map = map f set_map, @@ -380,7 +380,7 @@ val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf; val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf; val map_def_of_bnf = #map_def o #defs o rep_bnf; -val map_id_of_bnf = #map_id o #axioms o rep_bnf; +val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf; val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf; val map_comp_of_bnf = #map_comp o #axioms o rep_bnf; val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf; @@ -508,7 +508,7 @@ val in_bdN = "in_bd"; val in_monoN = "in_mono"; val in_relN = "in_rel"; -val map_idN = "map_id"; +val map_id0N = "map_id0"; val map_id'N = "map_id'"; val map_compN = "map_comp"; val map_comp'N = "map_comp'"; @@ -559,7 +559,7 @@ (in_monoN, [Lazy.force (#in_mono facts)]), (in_relN, [Lazy.force (#in_rel facts)]), (map_compN, [#map_comp axioms]), - (map_idN, [#map_id axioms]), + (map_id0N, [#map_id0 axioms]), (map_transferN, [Lazy.force (#map_transfer facts)]), (map_wpullN, [#map_wpull axioms]), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), @@ -845,7 +845,7 @@ | defs => Proof_Display.print_consts true lthy_old (K false) (map (dest_Free o fst o Logic.dest_equals o prop_of) defs); - val map_id_goal = + val map_id0_goal = let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA') end; @@ -922,8 +922,8 @@ val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp)); - val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal - cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal; + val goals = zip_axioms map_id0_goal map_comp_goal map_cong0_goal set_maps_goal + card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal; fun mk_wit_goals (I, wit) = let @@ -1000,7 +1000,7 @@ val in_cong = Lazy.lazy mk_in_cong; - val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id axioms)); + val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id0 axioms)); val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms)); fun mk_map_cong () = @@ -1086,7 +1086,7 @@ (Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) in Goal.prove_sorry lthy [] [] goal - (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms) + (fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms) (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map')) |> Thm.close_derivation end; @@ -1102,7 +1102,7 @@ val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs)); in Goal.prove_sorry lthy [] [] goal - (mk_rel_Grp_tac rel_OO_Grps (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id') + (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id') (Lazy.force map_comp') (map Lazy.force set_map')) |> Thm.close_derivation end; @@ -1142,7 +1142,7 @@ Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'), HOLogic.eq_const CA')) - (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms))) + (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms))) |> Thm.close_derivation; val rel_eq = Lazy.lazy mk_rel_eq; diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 18:44:03 2013 +0200 @@ -66,9 +66,9 @@ rtac set_map) set_maps) THEN' rtac @{thm image_empty}) 1; -fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_maps = +fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps = if null set_maps then - EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 + EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, @@ -82,14 +82,14 @@ rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; -fun mk_rel_Grp_tac rel_OO_Grps map_id map_cong0 map_id' map_comp set_maps +fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id' map_comp set_maps {context = ctxt, prems = _} = let val n = length set_maps; val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans); in if null set_maps then - unfold_thms_tac ctxt ((map_id RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN + unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN rtac @{thm Grp_UNIV_idI[OF refl]} 1 else EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, @@ -104,8 +104,8 @@ rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE], hyp_subst_tac ctxt, rtac @{thm relcomppI}, rtac @{thm conversepI}, - EVERY' (map2 (fn convol => fn map_id => - EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]), + EVERY' (map2 (fn convol => fn map_id0 => + EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]), REPEAT_DETERM_N n o rtac (convol RS fun_cong), REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, @@ -116,13 +116,13 @@ @{thms fst_convol snd_convol} [map_id', refl])] 1 end; -fun mk_rel_eq_tac n rel_Grp rel_cong map_id = +fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 = (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN' rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN' (if n = 0 then rtac refl else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ "Grp"]}, rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI, - CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id])) 1; + CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id0])) 1; fun mk_rel_mono_tac rel_OO_Grps in_mono = let diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 18:44:03 2013 +0200 @@ -602,8 +602,8 @@ val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; - val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs; - val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs; + val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; + val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs; val nested_set_map's = maps set_map'_of_bnf nested_bnfs; val fp_b_names = map base_name_of_typ fpTs; @@ -763,7 +763,7 @@ val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_rel_defs = map rel_def_of_bnf pre_bnfs; - val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs; + val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs; val fp_b_names = map base_name_of_typ fpTs; diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 18:44:03 2013 +0200 @@ -218,7 +218,7 @@ val sym_map_comps = map mk_sym map_comps; val map_comp's = map map_comp'_of_bnf bnfs; val map_cong0s = map map_cong0_of_bnf bnfs; - val map_ids = map map_id_of_bnf bnfs; + val map_id0s = map map_id0_of_bnf bnfs; val map_id's = map map_id'_of_bnf bnfs; val map_wpulls = map map_wpull_of_bnf bnfs; val set_bdss = map set_bd_of_bnf bnfs; @@ -2007,7 +2007,7 @@ `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ - map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); + map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); val timer = time (timer "corec definitions & thms"); @@ -2074,8 +2074,8 @@ val timer = time (timer "coinduction"); - fun mk_dtor_map_DEADID_thm dtor_inject map_id = - trans OF [iffD2 OF [dtor_inject, id_apply], map_id RS sym]; + fun mk_dtor_map_DEADID_thm dtor_inject map_id0 = + trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym]; fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf = trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym; @@ -2457,8 +2457,8 @@ val timer = time (timer "helpers for BNF properties"); - val map_id_tacs = - map2 (K oo mk_map_id_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms; + val map_id0_tacs = + map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms; val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms; val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; val set_nat_tacss = @@ -2476,7 +2476,7 @@ val rel_OO_Grp_tacs = replicate n (K (rtac refl 1)); - val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss + val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs; val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 18:44:03 2013 +0200 @@ -55,7 +55,7 @@ val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list list -> tactic - val mk_map_id_tac: thm list -> thm -> thm -> tactic + val mk_map_id0_tac: thm list -> thm -> thm -> tactic val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> 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 @@ -1030,7 +1030,7 @@ REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least}, EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1; -fun mk_map_id_tac maps unfold_unique unfold_dtor = +fun mk_map_id0_tac maps unfold_unique unfold_dtor = EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps), rtac unfold_dtor] 1; diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 18:44:03 2013 +0200 @@ -162,7 +162,7 @@ val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs; val map_comp's = map map_comp'_of_bnf bnfs; val map_cong0s = map map_cong0_of_bnf bnfs; - val map_ids = map map_id_of_bnf bnfs; + val map_id0s = map map_id0_of_bnf bnfs; val map_id's = map map_id'_of_bnf bnfs; val map_wpulls = map map_wpull_of_bnf bnfs; val set_map'ss = map set_map'_of_bnf bnfs; @@ -1303,7 +1303,7 @@ `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @ - map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); + map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); val timer = time (timer "rec definitions & thms"); @@ -1385,8 +1385,8 @@ val timer = time (timer "induction"); - fun mk_ctor_map_DEADID_thm ctor_inject map_id = - trans OF [id_apply, iffD2 OF [ctor_inject, map_id RS sym]]; + fun mk_ctor_map_DEADID_thm ctor_inject map_id0 = + trans OF [id_apply, iffD2 OF [ctor_inject, map_id0 RS sym]]; fun mk_ctor_Irel_DEADID_thm ctor_inject bnf = trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym]; @@ -1691,7 +1691,7 @@ val timer = time (timer "helpers for BNF properties"); - val map_id_tacs = map (K o mk_map_id_tac map_ids) ctor_map_unique_thms; + val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms; val map_comp_tacs = map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks; val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; @@ -1703,7 +1703,7 @@ val rel_OO_Grp_tacs = replicate n (K (rtac refl 1)); - val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss + val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs; val ctor_witss = diff -r 854fbb41e6cd -r c8628119d18e src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 18:31:23 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 18:44:03 2013 +0200 @@ -40,7 +40,7 @@ val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list list -> thm list list list -> thm list -> tactic val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic - val mk_map_id_tac: thm list -> thm -> tactic + val mk_map_id0_tac: thm list -> thm -> tactic val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list -> @@ -704,11 +704,11 @@ (* BNF tactics *) -fun mk_map_id_tac map_ids unique = +fun mk_map_id0_tac map_id0s unique = (rtac sym THEN' rtac unique THEN' EVERY' (map (fn thm => EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id}, - rtac (thm RS sym RS arg_cong)]) map_ids)) 1; + rtac (thm RS sym RS arg_cong)]) map_id0s)) 1; fun mk_map_comp_tac map_comps ctor_maps unique iplus1 = let