# HG changeset patch # User blanchet # Date 1377809799 -7200 # Node ID 5e0623448bdba8fca415d8740822863df63a8121 # Parent 050d0bc9afa5e02e8e9738f46d476879bba140d5 renamed BNF axiom diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:56:39 2013 +0200 @@ -157,12 +157,12 @@ mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) (map map_comp0_of_bnf inners); - fun mk_single_set_map_tac i _ = - mk_comp_set_map_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) + fun mk_single_set_map0_tac i _ = + mk_comp_set_map0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) (collect_set_map_of_bnf outer) - (map ((fn thms => nth thms i) o set_map_of_bnf) inners); + (map ((fn thms => nth thms i) o set_map0_of_bnf) inners); - val set_map_tacs = map mk_single_set_map_tac (0 upto ilive - 1); + val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1); fun bd_card_order_tac _ = mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); @@ -233,7 +233,7 @@ rtac thm 1 end; - val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_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; @@ -306,7 +306,7 @@ rtac refl 1; fun map_cong0_tac {context = ctxt, prems = _} = mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); - val set_map_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map_of_bnf bnf)); + val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf)); fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf); fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); val set_bd_tacs = @@ -339,7 +339,7 @@ rtac thm 1 end; - val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_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; @@ -396,12 +396,12 @@ rtac refl 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); - val set_map_tacs = + val set_map0_tacs = if Config.get lthy quick_and_dirty then replicate (n + live) (K all_tac) else replicate n (K empty_natural_tac) @ - map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf); + map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf); fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; val set_bd_tacs = @@ -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_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_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); @@ -478,7 +478,7 @@ fun map_comp0_tac _ = rtac (map_comp0_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); - val set_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf)); + val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf)); fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); @@ -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_id0_tac map_comp0_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_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); @@ -631,7 +631,7 @@ SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf)) - (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf)) + (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map0_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)) (mk_tac (rel_OO_Grp_of_bnf bnf)); diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:56:39 2013 +0200 @@ -16,7 +16,7 @@ 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 + val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic val mk_kill_bd_card_order_tac: int -> thm -> tactic @@ -67,21 +67,21 @@ rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1; -fun mk_comp_set_map_tac Gmap_comp0 Gmap_cong0 Gset_map set_maps = +fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s = EVERY' ([rtac ext] @ replicate 3 (rtac trans_o_apply) @ [rtac (arg_cong_Union RS trans), rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ - map (fn thm => rtac (thm RS fun_cong)) set_maps @ - [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, + map (fn thm => rtac (thm RS fun_cong)) set_map0s @ + [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, - rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), + rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ - [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]}, + [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]}, rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]}, rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:56:39 2013 +0200 @@ -72,8 +72,8 @@ val rel_flip_of_bnf: bnf -> thm val set_bd_of_bnf: bnf -> thm list val set_defs_of_bnf: bnf -> thm list + val set_map0_of_bnf: bnf -> thm list val set_map'_of_bnf: bnf -> thm list - val set_map_of_bnf: bnf -> thm list val wit_thms_of_bnf: bnf -> thm list val wit_thmss_of_bnf: bnf -> thm list list @@ -116,7 +116,7 @@ map_id0: thm, map_comp0: thm, map_cong0: thm, - set_map: thm list, + set_map0: thm list, bd_card_order: thm, bd_cinfinite: thm, set_bd: thm list, @@ -124,8 +124,8 @@ rel_OO_Grp: thm }; -fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) = - {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o, +fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), wpull), rel) = + {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, 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 @@ -144,20 +144,20 @@ ||> the_single |> mk_axioms'; -fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel = - [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel]; +fun zip_axioms mid mcomp mcong smap bdco bdinf sbd wpull rel = + [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [wpull, rel]; -fun dest_axioms {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, +fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, map_wpull, rel_OO_Grp} = - zip_axioms map_id0 map_comp0 map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull + zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd map_wpull rel_OO_Grp; -fun map_axioms f {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, +fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, map_wpull, rel_OO_Grp} = {map_id0 = f map_id0, map_comp0 = f map_comp0, map_cong0 = f map_cong0, - set_map = map f set_map, + set_map0 = map f set_map0, bd_card_order = f bd_card_order, bd_cinfinite = f bd_cinfinite, set_bd = map f set_bd, @@ -394,7 +394,7 @@ val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf; val set_bd_of_bnf = #set_bd o #axioms o rep_bnf; val set_defs_of_bnf = #set_defs o #defs o rep_bnf; -val set_map_of_bnf = #set_map o #axioms o rep_bnf; +val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf; val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf; val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf; val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf; @@ -518,7 +518,7 @@ val map_wpullN = "map_wpull"; val rel_eqN = "rel_eq"; val rel_flipN = "rel_flip"; -val set_mapN = "set_map"; +val set_map0N = "set_map0"; val set_map'N = "set_map'"; val set_bdN = "set_bd"; val rel_GrpN = "rel_Grp"; @@ -563,7 +563,7 @@ (map_transferN, [Lazy.force (#map_transfer facts)]), (map_wpullN, [#map_wpull axioms]), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), - (set_mapN, #set_map axioms), + (set_map0N, #set_map0 axioms), (set_bdN, #set_bd axioms)] @ (witNs ~~ wit_thmss_of_bnf bnf) |> map (fn (thmN, thms) => @@ -873,7 +873,7 @@ fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq)) end; - val set_maps_goal = + val set_map0s_goal = let fun mk_goal setA setB f = let @@ -922,7 +922,7 @@ 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_id0_goal map_comp0_goal map_cong0_goal set_maps_goal + val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal; fun mk_wit_goals (I, wit) = @@ -965,7 +965,7 @@ (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*) val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect)); in - Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map axioms))) + Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map0 axioms))) |> Thm.close_derivation end; @@ -1018,7 +1018,7 @@ val map_cong = Lazy.lazy mk_map_cong; - val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map axioms); + val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map0 axioms); fun mk_in_bd () = let @@ -1335,12 +1335,12 @@ val _ = Outer_Syntax.improper_command @{command_spec "print_bnfs"} - "print all BNFs (bounded natural functors)" + "print all bounded natural functors" (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of))); val _ = Outer_Syntax.local_theory_to_proof @{command_spec "bnf"} - "register a type as a BNF (bounded natural functor)" + "register a type as a bounded natural functor" ((parse_opt_binding_colon -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term) diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:56:39 2013 +0200 @@ -50,7 +50,7 @@ fun mk_map_cong_tac ctxt cong0 = (hyp_subst_tac ctxt THEN' rtac cong0 THEN' REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; -fun mk_set_map' set_map = set_map RS @{thm comp_eq_dest}; +fun mk_set_map' set_map0 = set_map0 RS @{thm comp_eq_dest}; fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 else (rtac subsetI THEN' rtac CollectI) 1 THEN @@ -59,15 +59,15 @@ ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN (etac subset_trans THEN' atac) 1; -fun mk_collect_set_map_tac set_maps = +fun mk_collect_set_map_tac set_map0s = (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' - EVERY' (map (fn set_map => + EVERY' (map (fn set_map0 => rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' - rtac set_map) set_maps) THEN' + rtac set_map0) set_map0s) THEN' rtac @{thm image_empty}) 1; -fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_maps = - if null set_maps then +fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_map0s = + if null set_map0s then 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, @@ -75,20 +75,20 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) - set_maps, + set_map0s, CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp0 RS trans), rtac (map_comp0 RS trans), rtac (map_comp0 RS trans RS sym), rtac map_cong0, - REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans), + REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac (o_apply RS trans), 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_id0 map_cong0 map_id map_comp0 set_maps +fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_map0s {context = ctxt, prems = _} = let - val n = length set_maps; + val n = length set_map0s; 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 + if null set_map0s 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 @@ -100,7 +100,7 @@ rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac]) - set_maps, + set_map0s, rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE], hyp_subst_tac ctxt, rtac @{thm relcomppI}, rtac @{thm conversepI}, @@ -112,7 +112,7 @@ CONJ_WRAP' (fn thm => EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, rtac @{thm convol_mem_GrpI}, etac set_mp, atac]) - set_maps]) + set_map0s]) @{thms fst_convol snd_convol} [map_id, refl])] 1 end; @@ -135,15 +135,15 @@ rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1 end; -fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_maps +fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_map0s {context = ctxt, prems = _} = let - val n = length set_maps; + val n = length set_map0s; val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans)); in - if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1 + if null set_map0s then rtac (rel_eq RS @{thm leq_conversepI}) 1 else EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I}, REPEAT_DETERM o @@ -153,7 +153,7 @@ rtac map_cong0, REPEAT_DETERM_N n o rtac thm, rtac (map_comp0 RS sym), rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), - etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 + etac @{thm flip_pred}]) set_map0s]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 end; fun mk_rel_conversep_tac le_conversep rel_mono = @@ -161,19 +161,19 @@ rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono, REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; -fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_maps +fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_map0s {context = ctxt, prems = _} = let - val n = length set_maps; + val n = length set_map0s; fun in_tac nthO_in = rtac CollectI THEN' CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), - rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps; + rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_map0s; val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans) THEN' rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN (2, trans)); in - if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1 + if null set_map0s then rtac (rel_eq RS @{thm eq_OOI}) 1 else EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, REPEAT_DETERM o @@ -200,7 +200,7 @@ REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}], hyp_subst_tac ctxt, rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, - CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps, + CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_map0s, etac allE, etac impE, etac conjI, etac conjI, etac sym, REPEAT_DETERM o eresolve_tac [bexE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI}, @@ -216,15 +216,15 @@ REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI}, etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1; -fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} = - if null set_maps then atac 1 +fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} = + if null set_map0s then atac 1 else unfold_tac [in_rel] ctxt THEN REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN hyp_subst_tac ctxt 1 THEN - unfold_tac set_maps ctxt THEN + unfold_tac set_map0s ctxt THEN EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]}, - CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1; + CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_map0s] 1; fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp {context = ctxt, prems = _} = diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:56:39 2013 +0200 @@ -2462,7 +2462,7 @@ val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms; val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; val set_nat_tacss = - map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss); + map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss); val bd_co_tacs = replicate n (K (mk_bd_card_order_tac sbd_card_order)); val bd_cinf_tacs = replicate n (K (mk_bd_cinfinite_tac sbd_Cinfinite)); @@ -2701,10 +2701,10 @@ in map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => - fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss => + fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss => Goal.prove_sorry lthy [] [] goal (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets - dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss)) + dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)) |> Thm.close_derivation) ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss' dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 22:56:39 2013 +0200 @@ -107,7 +107,7 @@ val mk_set_incl_hin_tac: thm list -> tactic val mk_set_incl_hset_tac: thm -> thm -> tactic val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic - val mk_set_map_tac: thm -> thm -> tactic + val mk_set_map0_tac: thm -> thm -> tactic val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic @@ -234,34 +234,34 @@ EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI, REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1 -fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_mapss coalg_setss = +fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss = EVERY' [rtac (Drule.instantiate' [] cts nat_induct), REPEAT_DETERM o rtac allI, CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s, REPEAT_DETERM o rtac allI, CONJ_WRAP' - (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) => + (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) => EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym), if m = 0 then K all_tac else EVERY' [rtac Un_cong, rtac box_equals, - rtac (nth passive_set_maps (j - 1) RS sym), + rtac (nth passive_set_map0s (j - 1) RS sym), rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac], CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong)) - (fn (i, (set_map, coalg_set)) => + (fn (i, (set_map0, coalg_set)) => EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})), - etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map, + etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0, rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}), ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i), REPEAT_DETERM o etac allE, atac, atac]) - (rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))]) - (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1; + (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))]) + (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1; -fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_mapss = +fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_map0ss = let val n = length rel_OO_Grps; - val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps); + val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ rel_OO_Grps); - fun mk_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) = + fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) = EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i), etac allE, etac allE, etac impE, atac, etac bexE, etac conjE, rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}), @@ -278,10 +278,10 @@ etac @{thm Collect_split_in_relI[OF Id_onI]}] else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}]) - (1 upto (m + n) ~~ set_maps)]) + (1 upto (m + n) ~~ set_map0s)]) @{thms fst_diag_id snd_diag_id})]; - fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) = + fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) = EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI, etac allE, etac allE, etac impE, atac, dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}), @@ -304,7 +304,7 @@ rtac @{thm Id_on_fst}, etac set_mp, atac] else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, rtac trans_fun_cong_image_id_id_apply, atac]) - (1 upto (m + n) ~~ set_maps)]; + (1 upto (m + n) ~~ set_map0s)]; in EVERY' [rtac (bis_def RS trans), rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms, @@ -399,7 +399,7 @@ rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis, etac @{thm relcompI}, atac] 1; -fun mk_coalgT_tac m defs strT_defs set_mapss {context = ctxt, prems = _} = +fun mk_coalgT_tac m defs strT_defs set_map0ss {context = ctxt, prems = _} = let val n = length strT_defs; val ks = 1 upto n; @@ -444,7 +444,7 @@ rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)]; in unfold_thms_tac ctxt defs THEN - CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1 + CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_map0ss ~~ strT_defs)) 1 end; fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss = @@ -685,14 +685,14 @@ fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's - prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_mapss coalg_setss + prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} = let val n = length beh_defs; val ks = 1 upto n; fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd, - ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_maps, + ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s, (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) = EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI, @@ -708,29 +708,29 @@ rtac conjI, rtac ballI, etac @{thm UN_E}, rtac conjI, if n = 1 then K all_tac else rtac (mk_sumEN n), - EVERY' (map6 (fn i => fn isNode_def => fn set_maps => + EVERY' (map6 (fn i => fn isNode_def => fn set_map0s => fn set_rv_Levs => fn set_Levs => fn set_image_Levs => EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst), rtac exI, rtac conjI, (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN' etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)), - EVERY' (map2 (fn set_map => fn set_rv_Lev => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), + EVERY' (map2 (fn set_map0 => fn set_rv_Lev => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans), rtac trans_fun_cong_image_id_id_apply, etac set_rv_Lev, TRY o atac, etac conjI, atac]) - (take m set_maps) set_rv_Levs), - CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) => - EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI}, + (take m set_map0s) set_rv_Levs), + CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev, if n = 1 then rtac refl else atac, atac, rtac subsetI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev', etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, if n = 1 then rtac refl else atac]) - (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))]) - ks isNode_defs set_mapss set_rv_Levss set_Levss set_image_Levss), - CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_maps, + (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) + ks isNode_defs set_map0ss set_rv_Levss set_Levss set_image_Levss), + CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s, (set_rv_Levs, (set_Levs, set_image_Levs)))))) => EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], @@ -739,13 +739,13 @@ (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN' etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)), - EVERY' (map2 (fn set_map => fn set_rv_Lev => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), + EVERY' (map2 (fn set_map0 => fn set_rv_Lev => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans), rtac trans_fun_cong_image_id_id_apply, etac set_rv_Lev, TRY o atac, etac conjI, atac]) - (take m set_maps) set_rv_Levs), - CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) => - EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI}, + (take m set_map0s) set_rv_Levs), + CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev, if n = 1 then rtac refl else atac, atac, rtac subsetI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], @@ -754,8 +754,8 @@ atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev', etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, if n = 1 then rtac refl else atac]) - (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))]) - (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_mapss ~~ + (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) + (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~ (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))), (**) rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI, @@ -766,12 +766,12 @@ CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), if n = 1 then rtac refl else rtac (mk_sum_casesN n i), - EVERY' (map2 (fn set_map => fn coalg_set => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), + EVERY' (map2 (fn set_map0 => fn coalg_set => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans), rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac]) - (take m set_maps) (take m coalg_sets)), - CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) => - EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI}, + (take m set_map0s) (take m coalg_sets)), + CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev, rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil, atac, rtac subsetI, @@ -781,7 +781,7 @@ etac @{thm set_mp[OF equalityD1[OF arg_cong[OF trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]}, rtac rv_Nil]) - (drop m set_maps ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; + (drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)), ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = @@ -842,7 +842,7 @@ CONJ_WRAP' fbetw_tac (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~ ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~ - (set_mapss ~~ (coalg_setss ~~ + (set_map0ss ~~ (coalg_setss ~~ (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN' CONJ_WRAP' mor_tac (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~ @@ -860,22 +860,22 @@ equiv_LSBISs), rtac sym, rtac (o_apply RS trans), etac (sym RS arg_cong RS trans), rtac map_comp_id] 1; -fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_mapss coalgT_setss = +fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss = EVERY' [stac coalg_def, - CONJ_WRAP' (fn ((set_maps, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => + CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final, rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI, - EVERY' (map2 (fn set_map => fn coalgT_set => - EVERY' [rtac conjI, rtac (set_map RS ord_eq_le_trans), + EVERY' (map2 (fn set_map0 => fn coalgT_set => + EVERY' [rtac conjI, rtac (set_map0 RS ord_eq_le_trans), rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply, etac coalgT_set]) - (take m set_maps) (take m coalgT_sets)), - CONJ_WRAP' (fn (equiv_LSBIS, (set_map, coalgT_set)) => - EVERY' [rtac (set_map RS ord_eq_le_trans), + (take m set_map0s) (take m coalgT_sets)), + CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) => + EVERY' [rtac (set_map0 RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set]) - (equiv_LSBISs ~~ drop m (set_maps ~~ coalgT_sets))]) - ((set_mapss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; + (equiv_LSBISs ~~ drop m (set_map0s ~~ coalgT_sets))]) + ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs = EVERY' [stac mor_def, rtac conjI, @@ -1049,7 +1049,7 @@ replicate n (@{thm o_id} RS fun_cong)))) maps map_comp0s map_cong0s)] 1; -fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_mapss set_hsetss +fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss set_hset_hsetsss = let val n = length map_comps; @@ -1057,7 +1057,7 @@ in EVERY' ([rtac rev_mp, coinduct_tac] @ - maps (fn (((((map_comp_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets), + maps (fn (((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets), set_hset_hsetss) => [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI, rtac conjI, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, @@ -1068,16 +1068,16 @@ [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE, REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets), REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym, - CONJ_WRAP' (fn (set_map, set_hset_hsets) => + CONJ_WRAP' (fn (set_map0, set_hset_hsets) => EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD}, - etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map, + etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE, REPEAT_DETERM o etac conjE, CONJ_WRAP' (fn set_hset_hset => EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets]) - (drop m set_maps ~~ set_hset_hsetss)]) + (drop m set_map0s ~~ set_hset_hsetss)]) (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~ - map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @ + map_cong0s ~~ set_map0ss ~~ set_hsetss ~~ set_hset_hsetsss) @ [rtac impI, CONJ_WRAP' (fn k => EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI, @@ -1089,7 +1089,7 @@ unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN ALLGOALS (etac sym); -fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss {context = ctxt, prems = _} = let val n = length dtor_maps; @@ -1105,10 +1105,10 @@ CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong)) (fn i => EVERY' [rtac @{thm UN_cong[OF refl]}, REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)]) - (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1 + (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1 end; -fun mk_set_map_tac hset_def col_natural = +fun mk_set_map0_tac hset_def col_natural = EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym, (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans), (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1; @@ -1158,10 +1158,10 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq] end; -fun mk_coalg_thePull_tac m coalg_def map_wpulls set_mapss pickWP_assms_tacs +fun mk_coalg_thePull_tac m coalg_def map_wpulls set_map0ss pickWP_assms_tacs {context = ctxt, prems = _} = unfold_thms_tac ctxt [coalg_def] THEN - CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) => + CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_map0s)) => EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), @@ -1171,11 +1171,11 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV), - CONJ_WRAP' (fn set_map => - EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map, + CONJ_WRAP' (fn set_map0 => + EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map0, rtac trans_fun_cong_image_id_id_apply, atac]) - (drop m set_maps)]) - (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1; + (drop m set_map0s)]) + (map_wpulls ~~ (pickWP_assms_tacs ~~ set_map0ss)) 1; fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs {context = ctxt, prems = _: thm list} = @@ -1210,7 +1210,7 @@ rtac refl]) (unfolds ~~ map_comp0s) 1; -fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_map0ss map_wpulls pickWP_assms_tacs {context = ctxt, prems = _} = let val n = length rec_0s; @@ -1221,7 +1221,7 @@ CONJ_WRAP' (fn thm => EVERY' [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s, REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) => + CONJ_WRAP' (fn (rec_Suc, ((unfold, set_map0s), (map_wpull, pickWP_assms_tac))) => EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), @@ -1230,16 +1230,16 @@ rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac ord_eq_le_trans, rtac rec_Suc, rtac @{thm Un_least}, - SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_maps (j - 1), + SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_map0s (j - 1), @{thm prod.cases}]), etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply, - CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) => + CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map0) => EVERY' [rtac @{thm UN_least}, - SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]), + SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map0, @{thm prod.cases}]), etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, etac set_mp, atac]) - (ks ~~ rev (drop m set_maps))]) - (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 + (ks ~~ rev (drop m set_map0s))]) + (rec_Sucs ~~ ((unfolds ~~ set_map0ss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 end; fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick @@ -1288,26 +1288,26 @@ FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject - dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss = + dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss = let val m = length dtor_set_incls; val n = length dtor_set_set_inclss; - val (passive_set_maps, active_set_maps) = chop m set_maps; + val (passive_set_map0s, active_set_map0s) = chop m set_map0s; val in_Jrel = nth in_Jrels (i - 1); val if_tac = EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - EVERY' (map2 (fn set_map => fn set_incl => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map, + EVERY' (map2 (fn set_map0 => fn set_incl => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, etac (set_incl RS @{thm subset_trans})]) - passive_set_maps dtor_set_incls), - CONJ_WRAP' (fn (in_Jrel, (set_map, dtor_set_set_incls)) => - EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI, + passive_set_map0s dtor_set_incls), + CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) => + EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls, rtac conjI, rtac refl, rtac refl]) - (in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)), + (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, @@ -1317,14 +1317,14 @@ val only_if_tac = EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - CONJ_WRAP' (fn (dtor_set, passive_set_map) => + CONJ_WRAP' (fn (dtor_set, passive_set_map0) => EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least}, - rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map, + rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) - (fn (active_set_map, in_Jrel) => EVERY' [rtac ord_eq_le_trans, + (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans, rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]}, - rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least}, + rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least}, dtac set_rev_mp, etac @{thm image_mono}, etac imageE, dtac @{thm ssubst_mem[OF pair_collapse]}, REPEAT_DETERM o eresolve_tac (CollectE :: conjE :: @@ -1335,8 +1335,8 @@ TRY o EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt], REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) - (rev (active_set_maps ~~ in_Jrels))]) - (dtor_sets ~~ passive_set_maps), + (rev (active_set_map0s ~~ in_Jrels))]) + (dtor_sets ~~ passive_set_map0s), rtac conjI, REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map, rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans, @@ -1352,12 +1352,12 @@ EVERY' [rtac iffI, if_tac, only_if_tac] 1 end; -fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_mapss +fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps {context = ctxt, prems = _} = let val n = length ks; in EVERY' [DETERM o rtac coinduct, - EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_maps => + EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => fn dtor_unfold => fn dtor_map => EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE], select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac, @@ -1372,41 +1372,41 @@ REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}), etac (@{thm prod.cases} RS map_arg_cong RS trans), SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), - CONJ_WRAP' (fn set_map => + CONJ_WRAP' (fn set_map0 => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], - dtac (set_map RS equalityD1 RS set_mp), + dtac (set_map0 RS equalityD1 RS set_mp), REPEAT_DETERM o eresolve_tac (imageE :: conjE :: @{thms iffD1[OF Pair_eq, elim_format]}), hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac, rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)]) - (drop m set_maps)]) - ks map_comp0s map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1 + (drop m set_map0s)]) + ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1 end; val split_id_unfolds = @{thms prod.cases image_id id_apply}; -fun mk_rel_coinduct_ind_tac m ks unfolds set_mapss j set_induct {context = ctxt, prems = _} = +fun mk_rel_coinduct_ind_tac m ks unfolds set_map0ss j set_induct {context = ctxt, prems = _} = let val n = length ks; in rtac set_induct 1 THEN - EVERY' (map3 (fn unfold => fn set_maps => fn i => + EVERY' (map3 (fn unfold => fn set_map0s => fn i => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE, select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp], hyp_subst_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_maps (j - 1)] @ split_id_unfolds)), + SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)), rtac subset_refl]) - unfolds set_mapss ks) 1 THEN - EVERY' (map3 (fn unfold => fn set_maps => fn i => - EVERY' (map (fn set_map => + unfolds set_map0ss ks) 1 THEN + EVERY' (map3 (fn unfold => fn set_map0s => fn i => + EVERY' (map (fn set_map0 => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE, select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map] @ split_id_unfolds)), + SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)), etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp], rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)]) - (drop m set_maps))) - unfolds set_mapss ks) 1 + (drop m set_map0s))) + unfolds set_map0ss ks) 1 end; fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:56:39 2013 +0200 @@ -1557,13 +1557,13 @@ map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf; val setss_by_range' = transpose setss_by_bnf'; - val set_map_thmss = + val set_map0_thmss = let - fun mk_set_map f map z set set' = + fun mk_set_map0 f map z set set' = HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z)); fun mk_cphi f map z set set' = certify lthy - (Term.absfree (dest_Free z) (mk_set_map f map z set set')); + (Term.absfree (dest_Free z) (mk_set_map0 f map z set set')); val csetss = map (map (certify lthy)) setss_by_range'; @@ -1576,7 +1576,7 @@ val goals = map3 (fn f => fn sets => fn sets' => HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 (mk_set_map f) fs_maps Izs sets sets'))) + (map4 (mk_set_map0 f) fs_maps Izs sets sets'))) fs setss_by_range setss_by_range'; fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_map'ss ctor_map_thms; @@ -1695,7 +1695,7 @@ val map_comp0_tacs = map2 (K oo mk_map_comp0_tac map_comps ctor_map_thms) ctor_map_unique_thms ks; val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; - val set_nat_tacss = map (map (K o mk_set_map_tac)) (transpose set_map_thmss); + val set_nat_tacss = map (map (K o mk_set_map0_tac)) (transpose set_map0_thmss); val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders)); val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1)); val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss); @@ -1775,10 +1775,10 @@ in map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => - fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss => + fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss => Goal.prove_sorry lthy [] [] goal (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets - ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss)) + ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)) |> Thm.close_derivation) ks goals in_rels map_comps map_cong0s folded_ctor_map_thms folded_ctor_set_thmss' ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss diff -r 050d0bc9afa5 -r 5e0623448bdb src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:56:39 2013 +0200 @@ -72,7 +72,7 @@ {prems: 'a, context: Proof.context} -> tactic val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list -> thm list -> int -> {prems: 'a, context: Proof.context} -> tactic - val mk_set_map_tac: thm -> tactic + val mk_set_map0_tac: thm -> tactic val mk_set_tac: thm -> tactic val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic val mk_wpull_tac: thm -> tactic @@ -724,7 +724,7 @@ (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1 end; -fun mk_set_map_tac set_nat = +fun mk_set_map0_tac set_nat = EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1; fun mk_bd_card_order_tac bd_card_orders = @@ -747,31 +747,31 @@ REPEAT_DETERM_N n o etac UnE]))))] 1); fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject - ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss = + ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss = let val m = length ctor_set_incls; val n = length ctor_set_set_inclss; - val (passive_set_maps, active_set_maps) = chop m set_maps; + val (passive_set_map0s, active_set_map0s) = chop m set_map0s; val in_Irel = nth in_Irels (i - 1); val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans; val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans; val if_tac = EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - EVERY' (map2 (fn set_map => fn ctor_set_incl => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map, + EVERY' (map2 (fn set_map0 => fn ctor_set_incl => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor]) - passive_set_maps ctor_set_incls), - CONJ_WRAP' (fn (in_Irel, (set_map, ctor_set_set_incls)) => - EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI, + passive_set_map0s ctor_set_incls), + CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) => + EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor])) ctor_set_set_incls, rtac conjI, rtac refl, rtac refl]) - (in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)), + (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, @@ -782,13 +782,13 @@ val only_if_tac = EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - CONJ_WRAP' (fn (ctor_set, passive_set_map) => + CONJ_WRAP' (fn (ctor_set, passive_set_map0) => EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least}, rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]}, - rtac passive_set_map, rtac trans_fun_cong_image_id_id_apply, atac, + rtac passive_set_map0, rtac trans_fun_cong_image_id_id_apply, atac, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) - (fn (active_set_map, in_Irel) => EVERY' [rtac ord_eq_le_trans, - rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least}, + (fn (active_set_map0, in_Irel) => EVERY' [rtac ord_eq_le_trans, + rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least}, dtac set_rev_mp, etac @{thm image_mono}, etac imageE, dtac @{thm ssubst_mem[OF pair_collapse]}, REPEAT_DETERM o eresolve_tac (CollectE :: conjE :: @@ -798,8 +798,8 @@ TRY o EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt], REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) - (rev (active_set_maps ~~ in_Irels))]) - (ctor_sets ~~ passive_set_maps), + (rev (active_set_map0s ~~ in_Irels))]) + (ctor_sets ~~ passive_set_map0s), rtac conjI, REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2), rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,