author blanchet Mon, 17 Sep 2012 21:13:30 +0200 changeset 49427 b017e1dbc77c parent 49426 6d05b8452cf3 child 49428 93f158d59ead
clean unfolding of prod and sum sets
```--- 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;```