1.1 --- a/src/HOL/Codatatype/BNF_Library.thy Tue Sep 11 13:06:14 2012 +0200
1.2 +++ b/src/HOL/Codatatype/BNF_Library.thy Tue Sep 11 13:06:14 2012 +0200
1.3 @@ -843,10 +843,6 @@
1.4 "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
1.5 by (metis obj_sumE)
1.6
1.7 -lemma sum_map_if:
1.8 -"sum_map f g (if p then Inl x else Inr y) = (if p then Inl (f x) else Inr (g y))"
1.9 -by simp
1.10 -
1.11 lemma sum_case_if:
1.12 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
1.13 by simp
2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 13:06:14 2012 +0200
2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 13:06:14 2012 +0200
2.3 @@ -213,8 +213,7 @@
2.4 val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
2.5
2.6 val ((iter_only as (gss, _, _), rec_only as (hss, _, _)),
2.7 - (zs, cs, cpss, coiter_only as ((pgss, _, cgssss), _),
2.8 - corec_only as ((phss, _, chssss), _))) =
2.9 + (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))) =
2.10 if lfp then
2.11 let
2.12 val y_Tsss =
2.13 @@ -245,7 +244,7 @@
2.14 val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
2.15 in
2.16 (((gss, g_Tss, yssss), (hss, h_Tss, zssss)),
2.17 - ([], [], [], (([], [], []), ([], [])), (([], [], []), ([], []))))
2.18 + ([], [], [], (([], []), ([], [])), (([], []), ([], []))))
2.19 end
2.20 else
2.21 let
2.22 @@ -254,11 +253,11 @@
2.23
2.24 val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_predT) ns Cs;
2.25
2.26 - fun zip_getterss qss fss = maps (op @) (qss ~~ fss);
2.27 + fun zip_predss_getterss qss fss = maps (op @) (qss ~~ fss);
2.28
2.29 - fun zip_preds_gettersss [] [qss] [fss] = zip_getterss qss fss
2.30 - | zip_preds_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
2.31 - p :: zip_getterss qss fss @ zip_preds_gettersss ps qsss fsss;
2.32 + fun zip_preds_predsss_gettersss [] [qss] [fss] = zip_predss_getterss qss fss
2.33 + | zip_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
2.34 + p :: zip_predss_getterss qss fss @ zip_preds_predsss_gettersss ps qsss fsss;
2.35
2.36 fun mk_types maybe_dest_sumT fun_Ts =
2.37 let
2.38 @@ -269,7 +268,7 @@
2.39 Cs mss' f_prod_Tss;
2.40 val q_Tssss =
2.41 map (map (map (fn [_] => [] | [_, C] => [mk_predT (domain_type C)]))) f_Tssss;
2.42 - val pf_Tss = map3 zip_preds_gettersss p_Tss q_Tssss f_Tssss;
2.43 + val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
2.44 in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end;
2.45
2.46 val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts;
2.47 @@ -297,12 +296,17 @@
2.48
2.49 val cpss = map2 (fn c => map (fn p => p $ c)) cs pss;
2.50
2.51 + fun mk_preds_getters_join [] [cf] = cf
2.52 + | mk_preds_getters_join [cq] [cf, cf'] =
2.53 + mk_If cq (mk_Inl (fastype_of cf') cf) (mk_Inr (fastype_of cf) cf');
2.54 +
2.55 fun mk_terms qssss fssss =
2.56 let
2.57 - val pfss = map3 zip_preds_gettersss pss qssss fssss;
2.58 + val pfss = map3 zip_preds_predsss_gettersss pss qssss fssss;
2.59 val cqssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs qssss;
2.60 val cfssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs fssss;
2.61 - in (pfss, cqssss, cfssss) end;
2.62 + val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss;
2.63 + in (pfss, cqfsss) end;
2.64 in
2.65 ((([], [], []), ([], [], [])),
2.66 ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)),
2.67 @@ -433,16 +437,11 @@
2.68 let
2.69 val B_to_fpT = C --> fpT;
2.70
2.71 - fun mk_getters_join [] [cf] = cf
2.72 - | mk_getters_join [cq] [cf, cf'] =
2.73 - mk_If cq (mk_Inl (fastype_of cf') cf) (mk_Inr (fastype_of cf) cf');
2.74 + fun mk_preds_getterss_join c n cps sum_prod_T cqfss =
2.75 + Term.lambda c (mk_IfN sum_prod_T cps
2.76 + (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
2.77
2.78 - fun mk_preds_gettersss_join c n cps sum_prod_T cqsss cfsss =
2.79 - Term.lambda c (mk_IfN sum_prod_T cps
2.80 - (map2 (mk_InN_balanced sum_prod_T n)
2.81 - (map2 (HOLogic.mk_tuple oo map2 mk_getters_join) cqsss cfsss) (1 upto n)));
2.82 -
2.83 - fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqssss, cfssss), (f_sum_prod_Ts,
2.84 + fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqfsss), (f_sum_prod_Ts,
2.85 pf_Tss))) =
2.86 let
2.87 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
2.88 @@ -452,7 +451,7 @@
2.89 val spec =
2.90 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
2.91 Term.list_comb (fp_iter_like,
2.92 - map6 mk_preds_gettersss_join cs ns cpss f_sum_prod_Ts cqssss cfssss));
2.93 + map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
2.94 in (binder, spec) end;
2.95
2.96 val coiter_like_bundles =
2.97 @@ -542,11 +541,9 @@
2.98 val rec_tacss =
2.99 map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
2.100 in
2.101 - (map2 (map2 (fn goal => fn tac =>
2.102 - Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
2.103 + (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
2.104 goal_iterss iter_tacss,
2.105 - map2 (map2 (fn goal => fn tac =>
2.106 - Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
2.107 + map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
2.108 goal_recss rec_tacss)
2.109 end;
2.110
2.111 @@ -573,10 +570,10 @@
2.112 let
2.113 fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
2.114
2.115 - fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfss' =
2.116 + fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' =
2.117 fold_rev (fold_rev Logic.all) ([c] :: pfss)
2.118 (Logic.list_implies (seq_conds mk_goal_cond n k cps,
2.119 - mk_Trueprop_eq (fcoiter_like $ c, lists_bmoc (take m cfss') ctr)));
2.120 + mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
2.121
2.122 fun build_call fiter_likes maybe_tack (T, U) =
2.123 if T = U then
2.124 @@ -589,22 +586,21 @@
2.125 fun mk_U maybe_mk_sumT =
2.126 typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
2.127
2.128 - fun repair_calls fiter_likes maybe_mk_sumT maybe_tack
2.129 - (cf as Free (_, Type (_, [_, T])) $ _) =
2.130 - if exists_subtype (member (op =) Cs) T then
2.131 - build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cf
2.132 - else
2.133 - cf;
2.134 + fun repair_calls fiter_likes maybe_mk_sumT maybe_tack cqf =
2.135 + let val T = fastype_of cqf in
2.136 + if exists_subtype (member (op =) Cs) T then
2.137 + build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
2.138 + else
2.139 + cqf
2.140 + end;
2.141
2.142 - val cgssss' =
2.143 - map (map (map (map (repair_calls gcoiters (K I) (K I))))) cgssss;
2.144 - val chssss' =
2.145 - map (map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z))))) chssss;
2.146 + val crgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) crgsss;
2.147 + val cshsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
2.148
2.149 val goal_coiterss =
2.150 - map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgssss';
2.151 + map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
2.152 val goal_corecss =
2.153 - map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chssss';
2.154 + map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss';
2.155
2.156 val coiter_tacss =
2.157 map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
2.158 @@ -613,9 +609,12 @@
2.159 map3 (map oo mk_coiter_like_tac corec_defs map_ids) fp_rec_thms pre_map_defs
2.160 ctr_defss;
2.161 in
2.162 - (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
2.163 + (map2 (map2 (fn goal => fn tac =>
2.164 + Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
2.165 goal_coiterss coiter_tacss,
2.166 - map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
2.167 + map2 (map2 (fn goal => fn tac =>
2.168 + Skip_Proof.prove lthy [] [] goal (tac o #context)
2.169 + |> Local_Defs.unfold lthy @{thms sum_case_if} |> Thm.close_derivation))
2.170 goal_corecss corec_tacss)
2.171 end;
2.172
3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 11 13:06:14 2012 +0200
3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 11 13:06:14 2012 +0200
3.3 @@ -60,8 +60,7 @@
3.4 iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
3.5
3.6 val coiter_like_ss = ss_only @{thms if_True if_False};
3.7 -val coiter_like_thms =
3.8 - @{thms id_apply map_pair_def sum_case_if sum_map.simps sum_map_if prod.cases};
3.9 +val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
3.10
3.11 fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
3.12 Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN