--- 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;
--- 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 []
--- 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;
--- 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;
--- 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