# HG changeset patch # User blanchet # Date 1348101768 -7200 # Node ID 9321a9465021068b1ae922347c2201fedec564fa # Parent 1d2825673cece5ba09311b582370cca45d2ba521 tuning diff -r 1d2825673cec -r 9321a9465021 src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200 @@ -752,7 +752,7 @@ val pred = mk_bnf_pred QTs CA' CB'; - val goal_map_id = + val map_id_goal = let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As'); in @@ -760,7 +760,7 @@ (HOLogic.mk_eq (bnf_map_app_id, HOLogic.id_const CA')) end; - val goal_map_comp = + val map_comp_goal = let val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs); val comp_bnf_map_app = HOLogic.mk_comp @@ -770,7 +770,7 @@ fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app)) end; - val goal_map_cong = + val map_cong_goal = let fun mk_prem z set f f_copy = Logic.all z (Logic.mk_implies @@ -784,7 +784,7 @@ (Logic.list_implies (prems, HOLogic.mk_Trueprop eq)) end; - val goal_set_naturals = + val set_naturals_goal = let fun mk_goal setA setB f = let @@ -798,11 +798,11 @@ map3 mk_goal bnf_sets_As bnf_sets_Bs fs end; - val goal_card_order_bd = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As); + val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As); - val goal_cinfinite_bd = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As); + val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As); - val goal_set_bds = + val set_bds_goal = let fun mk_goal set = Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As)); @@ -810,7 +810,7 @@ map mk_goal bnf_sets_As end; - val goal_in_bd = + val in_bd_goal = let val bd = mk_cexp (if live = 0 then ctwo @@ -821,7 +821,7 @@ (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd)) end; - val goal_map_wpull = + val map_wpull_goal = let val prems = map HOLogic.mk_Trueprop (map8 mk_wpull Xs B1s B2s f1s f2s (replicate live NONE) p1s p2s); @@ -844,7 +844,7 @@ (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull)) end; - val goal_rel_O_Gr = + val rel_O_Gr_goal = let val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs); val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs); @@ -855,8 +855,8 @@ fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rhs)) end; - val goals = zip_goals goal_map_id goal_map_comp goal_map_cong goal_set_naturals - goal_card_order_bd goal_cinfinite_bd goal_set_bds goal_in_bd goal_map_wpull goal_rel_O_Gr; + val goals = zip_goals map_id_goal map_comp_goal map_cong_goal set_naturals_goal + card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal; fun mk_wit_goals (I, wit) = let @@ -910,12 +910,12 @@ fun mk_in_mono () = let val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_subset) As As_copy; - val goal_in_mono = + val in_mono_goal = fold_rev Logic.all (As @ As_copy) (Logic.list_implies (prems_mono, HOLogic.mk_Trueprop (mk_subset (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA')))); in - Skip_Proof.prove lthy [] [] goal_in_mono (K (mk_in_mono_tac live)) + Skip_Proof.prove lthy [] [] in_mono_goal (K (mk_in_mono_tac live)) |> Thm.close_derivation end; @@ -924,12 +924,12 @@ fun mk_in_cong () = let val prems_cong = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_eq) As As_copy; - val goal_in_cong = + val in_cong_goal = fold_rev Logic.all (As @ As_copy) (Logic.list_implies (prems_cong, HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')))); in - Skip_Proof.prove lthy [] [] goal_in_cong (K ((TRY o hyp_subst_tac THEN' rtac refl) 1)) + Skip_Proof.prove lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation end; diff -r 1d2825673cec -r 9321a9465021 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 02:42:48 2012 +0200 @@ -614,7 +614,7 @@ val giters = map (lists_bmoc gss) iters; val hrecs = map (lists_bmoc hss) recs; - fun mk_goal_iter_like fss fiter_like xctr f xs fxs = + fun mk_iter_like_goal fss fiter_like xctr f xs fxs = fold_rev (fold_rev Logic.all) (xs :: fss) (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs))); @@ -640,8 +640,8 @@ val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss; val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss; - val goal_iterss = map5 (map4 o mk_goal_iter_like gss) giters xctrss gss xsss gxsss; - val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss; + val iterss_goal = map5 (map4 o mk_iter_like_goal gss) giters xctrss gss xsss gxsss; + val recss_goal = map5 (map4 o mk_iter_like_goal hss) hrecs xctrss hss xsss hxsss; val iter_tacss = map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms @@ -651,9 +651,9 @@ ctr_defss; in (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) - goal_iterss iter_tacss, + iterss_goal iter_tacss, map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) - goal_recss rec_tacss) + recss_goal rec_tacss) end; val simp_thmss = @@ -710,11 +710,11 @@ val gcoiters = map (lists_bmoc pgss) coiters; val hcorecs = map (lists_bmoc phss) corecs; - fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not); + fun mk_cond_goal pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not); - fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' = + fun mk_coiter_like_goal pfss c cps fcoiter_like n k ctr m cfs' = fold_rev (fold_rev Logic.all) ([c] :: pfss) - (Logic.list_implies (seq_conds mk_goal_cond n k cps, + (Logic.list_implies (seq_conds mk_cond_goal n k cps, mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs')))); fun build_call fiter_likes maybe_tack (T, U) = @@ -739,10 +739,10 @@ val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss; val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss; - val goal_coiterss = - map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss crgsss'; - val goal_corecss = - map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss'; + val coiterss_goal = + map8 (map4 oooo mk_coiter_like_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss'; + val corecss_goal = + map8 (map4 oooo mk_coiter_like_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; val coiter_tacss = map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs @@ -753,11 +753,11 @@ in (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation)) - goal_coiterss coiter_tacss, + coiterss_goal coiter_tacss, map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context) |> Local_Defs.unfold lthy @{thms sum_case_if} |> Thm.close_derivation)) - goal_corecss corec_tacss) + corecss_goal corec_tacss) end; fun mk_disc_coiter_like_thms [_] = K [] diff -r 1d2825673cec -r 9321a9465021 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200 @@ -276,9 +276,9 @@ val map_arg_cong_thms = let val prems = map2 (curry mk_Trueprop_eq) xFs xFs_copy; - val maps = map (fn map => Term.list_comb (map, all_fs)) mapsAsBs; + val maps = map (fn mapx => Term.list_comb (mapx, all_fs)) mapsAsBs; val concls = - map3 (fn x => fn y => fn map => mk_Trueprop_eq (map $ x, map $ y)) xFs xFs_copy maps; + map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) xFs xFs_copy maps; val goals = map4 (fn prem => fn concl => fn x => fn y => fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl))) @@ -502,8 +502,8 @@ val mor_sum_case_thm = let - val maps = map3 (fn s => fn sum_s => fn map => - mk_sum_case (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ Inls), s), sum_s)) + val maps = map3 (fn s => fn sum_s => fn mapx => + mk_sum_case (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s)) s's sum_ss map_Inls; in Skip_Proof.prove lthy [] [] @@ -1891,9 +1891,9 @@ val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map7 (fn i => fn rep => fn str => fn map => fn unfT => fn Jz => fn Jz' => + |> fold_map7 (fn i => fn rep => fn str => fn mapx => fn unfT => fn Jz => fn Jz' => Specification.definition - (SOME (unf_bind i, NONE, NoSyn), (unf_def_bind i, unf_spec i rep str map unfT Jz Jz'))) + (SOME (unf_bind i, NONE, NoSyn), (unf_def_bind i, unf_spec i rep str mapx unfT Jz Jz'))) ks Rep_Ts str_finals map_FTs unfTs Jzs Jzs' |>> apsnd split_list o split_list ||> `Local_Theory.restore; @@ -2125,8 +2125,8 @@ fun corec_spec i T AT = let val corecT = Library.foldr (op -->) (corec_sTs, AT --> T); - val maps = map3 (fn unf => fn sum_s => fn map => mk_sum_case - (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ corec_Inls), unf), sum_s)) + val maps = map3 (fn unf => fn sum_s => fn mapx => mk_sum_case + (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), unf), sum_s)) unfs corec_ss corec_maps; val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss); @@ -2600,18 +2600,18 @@ (mk_mor thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss) UNIV''s unf''s (map2 (curry HOLogic.mk_comp) pid_maps picks)); - val goal_fst = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) + val fst_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) (Logic.mk_implies (wpull_prem, mor_fst)); - val goal_snd = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) + val snd_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) (Logic.mk_implies (wpull_prem, mor_snd)); - val goal_pick = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) + val pick_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) (Logic.mk_implies (wpull_prem, mor_pick)); in - (Skip_Proof.prove lthy [] [] goal_fst (mk_mor_thePull_fst_tac m mor_def map_wpull_thms + (Skip_Proof.prove lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms map_comp's pickWP_assms_tacs) |> Thm.close_derivation, - Skip_Proof.prove lthy [] [] goal_snd (mk_mor_thePull_snd_tac m mor_def map_wpull_thms + Skip_Proof.prove lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms map_comp's pickWP_assms_tacs) |> Thm.close_derivation, - Skip_Proof.prove lthy [] [] goal_pick (mk_mor_thePull_pick_tac mor_def coiter_thms + Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def coiter_thms map_comp's) |> Thm.close_derivation) end; @@ -2862,9 +2862,9 @@ val policy = user_policy Derive_All_Facts_Note_Most; val (Jbnfs, lthy) = - fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy => + fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy => bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads) - (((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits), @{term True}(*###*)) lthy + (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), @{term True}(*###*)) lthy |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts all_witss lthy; diff -r 1d2825673cec -r 9321a9465021 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:48 2012 +0200 @@ -434,8 +434,8 @@ val mor_convol_thm = let - val maps = map3 (fn s => fn prod_s => fn map => - mk_convol (HOLogic.mk_comp (s, Term.list_comb (map, passive_ids @ fsts)), prod_s)) + val maps = map3 (fn s => fn prod_s => fn mapx => + mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s)) s's prod_ss map_fsts; in Skip_Proof.prove lthy [] [] @@ -1011,9 +1011,9 @@ val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map6 (fn i => fn abs => fn str => fn map => fn x => fn x' => + |> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' => Specification.definition - (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i abs str map x x'))) + (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i abs str mapx x x'))) ks Abs_Ts str_inits map_FT_inits xFs xFs' |>> apsnd split_list o split_list ||> `Local_Theory.restore; @@ -1217,8 +1217,8 @@ fun rec_spec i T AT = let val recT = Library.foldr (op -->) (rec_sTs, T --> AT); - val maps = map3 (fn fld => fn prod_s => fn map => - mk_convol (HOLogic.mk_comp (fld, Term.list_comb (map, passive_ids @ rec_fsts)), prod_s)) + val maps = map3 (fn fld => fn prod_s => fn mapx => + mk_convol (HOLogic.mk_comp (fld, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) flds rec_ss rec_maps; val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss); @@ -1708,9 +1708,9 @@ val policy = user_policy Derive_All_Facts_Note_Most; val (Ibnfs, lthy) = - fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy => + fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy => bnf_def Dont_Inline policy I tacs wit_tac (SOME deads) - (((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits), @{term True}(*###*)) lthy + (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), @{term True}(*###*)) lthy |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts fld_witss lthy; diff -r 1d2825673cec -r 9321a9465021 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 02:42:48 2012 +0200 @@ -292,12 +292,12 @@ fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); - val goal_exhaust = + val exhaust_goal = let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in fold_rev Logic.all [p, v] (mk_imp_p (map2 mk_prem xctrs xss)) end; - val goal_injectss = + val injectss_goal = let fun mk_goal _ _ [] [] = [] | mk_goal xctr yctr xs ys = @@ -307,7 +307,7 @@ map4 mk_goal xctrs yctrs xss yss end; - val goal_half_distinctss = + val half_distinctss_goal = let fun mk_goal ((xs, xc), (xs', xc')) = fold_rev Logic.all (xs @ xs') @@ -316,11 +316,11 @@ map (map mk_goal) (mk_half_pairss (xss ~~ xctrs)) end; - val goal_cases = + val cases_goal = map3 (fn xs => fn xctr => fn xf => fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs; - val goalss = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; + val goalss = [exhaust_goal] :: injectss_goal @ half_distinctss_goal @ [cases_goal]; fun after_qed thmss lthy = let @@ -446,16 +446,16 @@ val infos = ms ~~ discD_thms ~~ discs ~~ no_discs; val half_pairss = mk_half_pairss infos; - val goal_halvess = map mk_goal half_pairss; + val halvess_goal = map mk_goal half_pairss; val half_thmss = map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) - goal_halvess half_pairss (flat disc_thmss'); + halvess_goal half_pairss (flat disc_thmss'); - val goal_other_halvess = map (mk_goal o map swap) half_pairss; + val other_halvess_goal = map (mk_goal o map swap) half_pairss; val other_half_thmss = map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss - goal_other_halvess; + other_halvess_goal; in interleave (flat half_thmss) (flat other_half_thmss) end; @@ -525,10 +525,10 @@ val goal = Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, mk_Trueprop_eq (fcase $ v, gcase $ w)); - val goal_weak = Logic.mk_implies (v_eq_w, mk_Trueprop_eq (fcase $ v, fcase $ w)); + val weak_goal = Logic.mk_implies (v_eq_w, mk_Trueprop_eq (fcase $ v, fcase $ w)); in (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms), - Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) + Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1))) |> pairself (singleton (Proof_Context.export names_lthy lthy)) end; @@ -544,7 +544,7 @@ val goal = mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); - val goal_asm = + val asm_goal = mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj (map3 mk_disjunct xctrs xss xfs))); @@ -553,7 +553,7 @@ (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss) |> singleton (Proof_Context.export names_lthy lthy) val split_asm_thm = - Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} => + Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} => mk_split_asm_tac ctxt split_thm) |> singleton (Proof_Context.export names_lthy lthy) in