# HG changeset patch # User blanchet # Date 1348235609 -7200 # Node ID 92a7c1842c782266e52ce8a6101d5b91ecbb0968 # Parent acc9635a644a96d0bac27cd73437055932cc5303 tuned a few ML names diff -r acc9635a644a -r 92a7c1842c78 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -8,21 +8,21 @@ signature BNF_COMP = sig - type unfold_thms - val empty_unfold: unfold_thms - val map_unfolds_of: unfold_thms -> thm list - val set_unfoldss_of: unfold_thms -> thm list list - val pred_unfolds_of: unfold_thms -> thm list - val rel_unfolds_of: unfold_thms -> thm list + type unfold_set + val empty_unfolds: unfold_set + val map_unfolds_of: unfold_set -> thm list + val set_unfoldss_of: unfold_set -> thm list list + val pred_unfolds_of: unfold_set -> thm list + val rel_unfolds_of: unfold_set -> thm list val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> - ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context -> - (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context) + ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context -> + (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context) val default_comp_sort: (string * sort) list list -> (string * sort) list val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> - (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context -> - (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context)) - val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> + (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context -> + (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context)) + val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> (BNF_Def.BNF * typ list) * local_theory end; @@ -34,7 +34,7 @@ open BNF_Tactics open BNF_Comp_Tactics -type unfold_thms = { +type unfold_set = { map_unfolds: thm list, set_unfoldss: thm list list, pred_unfolds: thm list, @@ -46,17 +46,17 @@ fun adds_to_thms thms NONE = thms | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; -val empty_unfold = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []}; +val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []}; -fun add_to_unfold_opt map_opt sets_opt pred_opt rel_opt +fun add_to_unfolds_opt map_opt sets_opt pred_opt rel_opt {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} = {map_unfolds = add_to_thms map_unfolds map_opt, set_unfoldss = adds_to_thms set_unfoldss sets_opt, pred_unfolds = add_to_thms pred_unfolds pred_opt, rel_unfolds = add_to_thms rel_unfolds rel_opt}; -fun add_to_unfold map sets pred rel = - add_to_unfold_opt (SOME map) (SOME sets) (SOME pred) (SOME rel); +fun add_to_unfolds map sets pred rel = + add_to_unfolds_opt (SOME map) (SOME sets) (SOME pred) (SOME rel); val map_unfolds_of = #map_unfolds; val set_unfoldss_of = #set_unfoldss; @@ -77,7 +77,7 @@ val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; in Envir.expand_term get end; -fun clean_compose_bnf const_policy qualify b outer inners (unfold, lthy) = +fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) = let val olive = live_of_bnf outer; val onwits = nwits_of_bnf outer; @@ -274,15 +274,16 @@ bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) (((((b, mapx), sets), bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') - (rel_def_of_bnf bnf') unfold; + val unfold_set' = + add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (rel_def_of_bnf bnf') unfold_set; in - (bnf', (unfold', lthy')) + (bnf', (unfold_set', lthy')) end; (* Killing live variables *) -fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else +fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else let val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf); val live = live_of_bnf bnf; @@ -375,15 +376,16 @@ bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') - (rel_def_of_bnf bnf') unfold; + val unfold_set' = + add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (rel_def_of_bnf bnf') unfold_set; in - (bnf', (unfold', lthy')) + (bnf', (unfold_set', lthy')) end; (* Adding dummy live variables *) -fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else +fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else let val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf); val live = live_of_bnf bnf; @@ -462,15 +464,17 @@ bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') - (pred_def_of_bnf bnf') unfold; + val unfold_set' = + add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (pred_def_of_bnf bnf') unfold_set; in - (bnf', (unfold', lthy')) + (bnf', (unfold_set', lthy')) end; (* Changing the order of live variables *) -fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else +fun permute_bnf qualify src dest bnf (unfold_set, lthy) = + if src = dest then (bnf, (unfold_set, lthy)) else let val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf); val live = live_of_bnf bnf; @@ -540,10 +544,11 @@ bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') - (pred_def_of_bnf bnf') unfold; + val unfold_set' = + add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (pred_def_of_bnf bnf') unfold_set; in - (bnf', (unfold', lthy')) + (bnf', (unfold_set', lthy')) end; (* Composition pipeline *) @@ -558,17 +563,17 @@ |> lift_bnf qualify n #> uncurry (permute_bnf qualify src dest); -fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = +fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy = let val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; val kill_poss = map (find_indices Ds) Ass; val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; val before_kill_dest = map2 append kill_poss live_poss; val kill_ns = map length kill_poss; - val (inners', (unfold', lthy')) = + val (inners', (unfold_set', lthy')) = fold_map5 (fn i => permute_and_kill (qualify i)) (if length bnfs = 1 then [0] else (1 upto length bnfs)) - kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy); + kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy); val Ass' = map2 (map o nth) Ass live_poss; val As = sort Ass'; @@ -580,32 +585,32 @@ in ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) (if length bnfs = 1 then [0] else (1 upto length bnfs)) - lift_ns after_lift_src after_lift_dest inners' (unfold', lthy')) + lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy')) end; fun default_comp_sort Ass = Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); -fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) = +fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) = let val b = name_of_bnf outer; val Ass = map (map Term.dest_TFree) tfreess; val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; - val ((kill_poss, As), (inners', (unfold', lthy'))) = - normalize_bnfs qualify Ass Ds sort inners unfold lthy; + val ((kill_poss, As), (inners', (unfold_set', lthy'))) = + normalize_bnfs qualify Ass Ds sort inners unfold_set lthy; val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); val As = map TFree As; in apfst (rpair (Ds, As)) - (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy')) + (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy')) end; (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) -fun seal_bnf unfold b Ds bnf lthy = +fun seal_bnf unfold_set b Ds bnf lthy = let val live = live_of_bnf bnf; val nwits = nwits_of_bnf bnf; @@ -615,10 +620,10 @@ val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live HOLogic.typeS) lthy1); - val map_unfolds = map_unfolds_of unfold; - val set_unfoldss = set_unfoldss_of unfold; - val pred_unfolds = pred_unfolds_of unfold; - val rel_unfolds = rel_unfolds_of unfold; + val map_unfolds = map_unfolds_of unfold_set; + val set_unfoldss = set_unfoldss_of unfold_set; + val pred_unfolds = pred_unfolds_of unfold_set; + val rel_unfolds = rel_unfolds_of unfold_set; val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds); @@ -695,13 +700,13 @@ fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum) | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable" - | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) = + | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) = let val tfrees = Term.add_tfreesT T []; val bnf_opt = if null tfrees then NONE else bnf_of lthy C; in (case bnf_opt of - NONE => ((DEADID_bnf, ([T], [])), (unfold, lthy)) + NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy)) | SOME bnf => if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then let @@ -712,7 +717,7 @@ val deads_lives = pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) (deads, lives); - in ((bnf, deads_lives), (unfold, lthy)) end + in ((bnf, deads_lives), (unfold_set, lthy)) end else let val name = Long_Name.base_name C; @@ -725,12 +730,12 @@ (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf))); val oDs = map (nth Ts) oDs_pos; val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); - val ((inners, (Dss, Ass)), (unfold', lthy')) = + val ((inners, (Dss, Ass)), (unfold_set', lthy')) = apfst (apsnd split_list o split_list) (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort) - (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy)); + (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy)); in - compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy') + compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy') end) end; diff -r acc9635a644a -r 92a7c1842c78 src/HOL/Codatatype/Tools/bnf_fp.ML --- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -375,7 +375,7 @@ | fp_sort lhss (SOME resBs) Ass = (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss; -fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy = +fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold_set lthy = let val name = mk_common_name (map Binding.name_of bs); fun qualify i = @@ -392,13 +392,13 @@ val timer = time (timer "Construction of BNFs"); - val ((kill_poss, _), (bnfs', (unfold', lthy'))) = - normalize_bnfs qualify Ass Ds sort bnfs unfold lthy; + val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) = + normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy; val Dss = map3 (append oo map o nth) livess kill_poss deadss; val ((bnfs'', deadss), lthy'') = - fold_map3 (seal_bnf unfold') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy' + fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy' |>> split_list; val timer = time (timer "Normalization & sealing of BNFs"); @@ -416,11 +416,11 @@ val (lhss, rhss) = split_list eqs; val sort = fp_sort lhss (SOME resBs); fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); - val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) + val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list) (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss - (empty_unfold, lthy)); + (empty_unfolds, lthy)); in - mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy' + mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy' end; fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy = @@ -429,12 +429,13 @@ val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss; val sort = fp_sort lhss NONE; fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); - val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) + val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list) (fold_map2 (fn b => fn rawT => (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT))) - bs raw_bnfs (empty_unfold, lthy)); + bs raw_bnfs (empty_unfolds, lthy)); in - snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy') + snd (mk_fp_bnf timer + (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy') end; end; diff -r acc9635a644a -r 92a7c1842c78 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 15:53:29 2012 +0200 @@ -443,9 +443,9 @@ val [iter_def, rec_def] = map (Morphism.thm phi) defs; - val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts; + val [iterx, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts; in - ((wrap_res, ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy) + ((wrap_res, ctrs, iterx, recx, xss, ctr_defs, iter_def, rec_def), lthy) end; fun define_coiter_corec (wrap_res, no_defs_lthy) = diff -r acc9635a644a -r 92a7c1842c78 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -1051,7 +1051,7 @@ val iter_fun = Term.absfree iter_f' (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n iter_f) ks)); - val iter = HOLogic.choice_const iterT $ iter_fun; + val iterx = HOLogic.choice_const iterT $ iter_fun; fun iter_bind i = Binding.suffix_name ("_" ^ ctor_iterN) (nth bs (i - 1)); val iter_name = Binding.name_of o iter_bind; @@ -1062,7 +1062,7 @@ val iterT = Library.foldr (op -->) (sTs, T --> AT); val lhs = Term.list_comb (Free (iter_name i, iterT), ss); - val rhs = mk_nthN n iter i; + val rhs = mk_nthN n iterx i; in mk_Trueprop_eq (lhs, rhs) end; @@ -1175,9 +1175,9 @@ mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); val goals = map3 mk_goal dtors ctors FTs; in - map5 (fn goal => fn dtor_def => fn iter => fn map_comp_id => fn map_congL => + map5 (fn goal => fn dtor_def => fn iterx => fn map_comp_id => fn map_congL => Skip_Proof.prove lthy [] [] goal - (K (mk_dtor_o_ctor_tac dtor_def iter map_comp_id map_congL ctor_o_iter_thms)) + (K (mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iter_thms)) |> Thm.close_derivation) goals dtor_defs iter_thms map_comp_id_thms map_congL_thms end; @@ -1256,8 +1256,8 @@ end; val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs; in - map2 (fn goal => fn iter => - Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms) + map2 (fn goal => fn iterx => + Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iterx fst_rec_pair_thms) |> Thm.close_derivation) goals iter_thms end; @@ -1401,8 +1401,8 @@ HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps)))); val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's; val maps = - map4 (fn goal => fn iter => fn map_comp_id => fn map_cong => - Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iter map_comp_id map_cong)) + map4 (fn goal => fn iterx => fn map_comp_id => fn map_cong => + Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iterx map_comp_id map_cong)) |> Thm.close_derivation) goals iter_thms map_comp_id_thms map_congs; in @@ -1461,8 +1461,8 @@ HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))); val goalss = map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss; - val setss = map (map2 (fn iter => fn goal => - Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)) |> Thm.close_derivation) + val setss = map (map2 (fn iterx => fn goal => + Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iterx)) |> Thm.close_derivation) iter_thms) goalss; fun mk_simp_goal pas_set act_sets sets ctor z set = diff -r acc9635a644a -r 92a7c1842c78 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 @@ -514,17 +514,17 @@ CONJ_WRAP' mk_unique type_defs 1 end; -fun mk_dtor_o_ctor_tac dtor_def iter map_comp_id map_congL ctor_o_iters = - EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter, +fun mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iters = + EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL, EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) ctor_o_iters), rtac sym, rtac id_apply] 1; -fun mk_rec_tac rec_defs iter fst_recs {context = ctxt, prems = _}= +fun mk_rec_tac rec_defs iterx fst_recs {context = ctxt, prems = _}= unfold_defs_tac ctxt (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN - EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}), + EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iterx RS @{thm arg_cong[of _ _ snd]}), rtac @{thm snd_convol'}] 1; fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = @@ -570,8 +570,8 @@ CONJ_WRAP' (K atac) ks] 1 end; -fun mk_map_tac m n iter map_comp_id map_cong = - EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter, rtac trans, rtac o_apply, +fun mk_map_tac m n iterx map_comp_id map_cong = + EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx, rtac trans, rtac o_apply, rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong), REPEAT_DETERM_N m o rtac refl, REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])), @@ -591,8 +591,8 @@ CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1 end; -fun mk_set_tac iter = EVERY' [rtac ext, rtac trans, rtac o_apply, - rtac trans, rtac iter, rtac sym, rtac o_apply] 1; +fun mk_set_tac iterx = EVERY' [rtac ext, rtac trans, rtac o_apply, + rtac trans, rtac iterx, rtac sym, rtac o_apply] 1; fun mk_set_simp_tac set set_natural' set_natural's = let