--- a/src/HOL/Codatatype/BNF_FP.thy Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy Mon Sep 17 21:13:30 2012 +0200
@@ -123,14 +123,17 @@
"\<exists>y. (\<exists>x\<in>A. y = F x) \<and> z \<in> y \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {y. \<exists>y'\<in>F x. y = y'}}"
by blast
-lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C"
-apply (rule exI)
-apply (rule conjI)
- apply (rule bexI)
- apply (rule refl)
- apply assumption
-apply assumption
-done
+lemma mem_compreh_eq_iff:
+"z \<in> {y. \<exists>x\<in>Axx. y = f x} = (\<exists> x. x \<in> Axx & z \<in> {f x})"
+by blast
+
+lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
+by simp
+
+lemma induct_set_step:
+"\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x"
+"\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C"
+by blast+
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_sugar_tactics.ML"
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Mon Sep 17 21:13:30 2012 +0200
@@ -602,6 +602,7 @@
end;
val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
+val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*)
val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Mon Sep 17 21:13:30 2012 +0200
@@ -43,6 +43,52 @@
val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
+fun mk_set_rhs set_lhs T =
+ let
+ val Type (_, Ts0) = domain_type (fastype_of set_lhs);
+ val Type (_, Ts) = domain_type T;
+ in
+ Term.subst_atomic_types (Ts0 ~~ Ts) set_lhs
+ end;
+
+val mk_fsts_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm fsts_def[abs_def]})));
+val mk_snds_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm snds_def[abs_def]})));
+val mk_setl_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setl_def[abs_def]})));
+val mk_setr_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setr_def[abs_def]})));
+
+(* TODO: Put this in "Balanced_Tree" *)
+fun balanced_tree_middle n = n div 2;
+
+val sum_prod_sel_defs =
+ @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
+
+fun unfold_sum_prod_sets ctxt ms thm =
+ let
+ fun unf_prod 0 f = f
+ | unf_prod 1 f = f
+ | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
+ $ (t7 $ f $ g)) =
+ t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
+ $ (t7 $ f $ unf_prod (m - 1) g)
+ | unf_prod _ f = f;
+ fun unf_sum [m] f = unf_prod m f
+ | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
+ $ (t7 $ f $ g)) =
+ let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
+ t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
+ $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
+ end
+ | unf_sum _ f = f;
+
+ val P = prop_of thm;
+ val P' = Logic.dest_equals P ||> unf_sum ms;
+ val goal = Logic.mk_implies (P, Logic.mk_equals P');
+ in
+ Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
+ Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1)
+ OF [thm]
+ end;
+
fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
(rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
@@ -88,14 +134,14 @@
Local_Defs.unfold_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
-(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
+val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
-fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
+fun mk_induct_prem_prem_endgame_tac _ 0 = maybe_singletonI_tac
| mk_induct_prem_prem_endgame_tac ctxt qq =
REPEAT_DETERM_N qq o
- (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
- etac @{thm induct_set_step}) THEN'
- atac ORELSE' SELECT_GOAL (auto_tac ctxt);
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ @{thms trans[OF Union_iff bex_simps(6)] mem_compreh_eq_iff ex_mem_singleton}) THEN'
+ eresolve_tac @{thms induct_set_step}) THEN' maybe_singletonI_tac;
fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
@@ -109,19 +155,12 @@
image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
sum_map.simps};
-(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
- delay them. *)
-val induct_prem_prem_thms_delayed =
- @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
-
fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
[select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
SELECT_GOAL (Local_Defs.unfold_tac ctxt
(pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
- SELECT_GOAL (Local_Defs.unfold_tac ctxt
- (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
- gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
+ gen_UnIN_tac pp jj, mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
let val r = length ppjjqqkks in
@@ -137,10 +176,11 @@
let
val nn = length ns;
val n = Integer.sum ns;
+ val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss;
in
Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
- pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
+ pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss)
end;
end;