--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Sat Sep 08 21:04:26 2012 +0200
@@ -137,16 +137,14 @@
val Type (_, Ts0) = List.last binders
in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end;
- val caseB = mk_case As B;
- val caseB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
-
- fun mk_caseB_term eta_fs = Term.list_comb (caseB, eta_fs);
+ val casex = mk_case As B;
+ val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
mk_Freess "x" ctr_Tss
||>> mk_Freess "y" ctr_Tss
- ||>> mk_Frees "f" caseB_Ts
- ||>> mk_Frees "g" caseB_Ts
+ ||>> mk_Frees "f" case_Ts
+ ||>> mk_Frees "g" case_Ts
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T
||>> yield_singleton (mk_Frees "w") T
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
@@ -164,7 +162,8 @@
val eta_fs = map2 eta_expand_case_arg xss xfs;
val eta_gs = map2 eta_expand_case_arg xss xgs;
- val caseB_fs = Term.list_comb (caseB, eta_fs);
+ val fcase = Term.list_comb (casex, eta_fs);
+ val gcase = Term.list_comb (casex, eta_gs);
val exist_xs_v_eq_ctrs =
map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
@@ -255,7 +254,7 @@
val goal_cases =
map3 (fn xs => fn xctr => fn xf =>
- fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (caseB_fs $ xctr, xf))) xss xctrs xfs;
+ 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];
@@ -426,7 +425,7 @@
| mk_rhs (disc :: discs) (f :: fs) (sels :: selss) =
Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $
betapply (disc, v) $ mk_core f sels $ mk_rhs discs fs selss;
- val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
+ val goal = mk_Trueprop_eq (fcase $ v, mk_rhs discs fs selss);
in
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
@@ -440,13 +439,11 @@
mk_Trueprop_eq (f, g)));
val v_eq_w = mk_Trueprop_eq (v, w);
- val case_fs = mk_caseB_term eta_fs;
- val case_gs = mk_caseB_term eta_gs;
val goal =
Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
- mk_Trueprop_eq (case_fs $ v, case_gs $ w));
- val goal_weak = Logic.mk_implies (v_eq_w, mk_Trueprop_eq (case_fs $ v, case_fs $ w));
+ mk_Trueprop_eq (fcase $ v, gcase $ w));
+ val goal_weak = 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)))
@@ -461,7 +458,7 @@
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
HOLogic.mk_not (q $ f_xs)));
- val lhs = q $ (mk_caseB_term eta_fs $ v);
+ val lhs = q $ (fcase $ v);
val goal =
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));