--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 23:09:08 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 23:42:33 2012 +0200
@@ -124,7 +124,7 @@
val unfs = map (mk_unf As) raw_unfs;
val flds = map (mk_fld As) raw_flds;
- fun pour_some_sugar_on_type ((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
+ fun pour_sugar_on_type ((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
ctr_binders), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
let
val n = length ctr_binders;
@@ -168,27 +168,29 @@
val ctrs = map (Morphism.term phi) raw_ctrs;
val casex = Morphism.term phi raw_case;
- val fld_iff_unf_thm =
+ fun exhaust_tac {context = ctxt, ...} =
let
- val goal =
- fold_rev Logic.all [u, v]
- (mk_Trueprop_eq (HOLogic.mk_eq (v, fld $ u), HOLogic.mk_eq (unf $ v, u)));
+ val fld_iff_unf_thm =
+ let
+ val goal =
+ fold_rev Logic.all [u, v]
+ (mk_Trueprop_eq (HOLogic.mk_eq (v, fld $ u), HOLogic.mk_eq (unf $ v, u)));
+ in
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unf_T, T]) (certify lthy fld)
+ (certify lthy unf) fld_unf unf_fld)
+ |> Thm.close_derivation
+ |> Morphism.thm phi
+ end;
+
+ val sumEN_thm' =
+ Local_Defs.unfold lthy @{thms all_unit_eq}
+ (Drule.instantiate' (map (SOME o certifyT lthy) prod_Ts) [] (mk_sumEN n))
+ |> Morphism.thm phi;
in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unf_T, T]) (certify lthy fld)
- (certify lthy unf) fld_unf unf_fld)
- |> Thm.close_derivation
+ mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm'
end;
- val sumEN_thm = mk_sumEN n;
- val sumEN_thm' =
- let val cTs = map (SOME o certifyT lthy) prod_Ts in
- Local_Defs.unfold lthy @{thms all_unit_eq} (Drule.instantiate' cTs [] sumEN_thm)
- end;
-
- fun exhaust_tac {context = ctxt, ...} =
- mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
-
val inject_tacss =
map2 (fn 0 => K []
| _ => fn ctr_def => [fn {context = ctxt, ...} =>
@@ -228,7 +230,7 @@
end;
in
lthy'
- |> fold pour_some_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
+ |> fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
ctr_binderss ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 23:09:08 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 23:42:33 2012 +0200
@@ -28,12 +28,10 @@
rtac refl) 1;
fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
- Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
- rtac sumEN' 1 THEN
+ Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
- EVERY' (map2 (fn k => fn m =>
- select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' etac @{thm meta_mp}) k THEN'
- atac) (1 upto n) ms) 1;
+ EVERY' (map2 (fn k => fn m => select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN'
+ etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
(rtac iffI THEN'
@@ -47,9 +45,7 @@
rtac @{thm sum.distinct(1)} 1;
fun mk_inject_tac ctxt ctr_def fld_inject =
- Local_Defs.unfold_tac ctxt [ctr_def] THEN
- rtac (fld_inject RS ssubst) 1 THEN
- Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN
- rtac refl 1;
+ Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
+ Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
end;