author blanchet Mon, 17 Sep 2012 21:13:30 +0200 changeset 49429 64ac3471005a parent 49428 93f158d59ead child 49430 6df729c6a1a6
cleaner way of dealing with the set functions of sums and products
```--- 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
@@ -137,6 +137,18 @@
lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
by simp

+lemma prod_set_simps:
+"fsts (x, y) = {x}"
+"snds (x, y) = {y}"
+unfolding fsts_def snds_def by simp+
+
+lemma sum_set_simps:
+"sum_setl (Inl x) = {x}"
+"sum_setl (Inr x) = {}"
+"sum_setr (Inl x) = {}"
+"sum_setr (Inr x) = {x}"
+unfolding sum_setl_def sum_setr_def 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"```
```--- 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
@@ -590,25 +590,13 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry (op \$)) phis vs)));

-            fun mk_raw_prem_prems_indices pprems =
-              let
-                fun has_index kk (_, (kk', _)) = kk' = kk;
-                val buckets = Library.partition_list has_index 1 nn pprems;
-                val pps = map length buckets;
-              in
-                map (fn pprem as (xysets, (kk, _)) =>
-                  ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1),
-                   (length xysets, kk))) pprems
-              end;
-
-            val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
-val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*)
+            val kksss = map (map (map (fst o snd) o #2)) raw_premss;

val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);

val induct_thm =
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-                mk_induct_tac ctxt ns mss ppjjqqkksss (flat ctr_defss) fld_induct'
+                mk_induct_tac ctxt ns mss kksss (flat ctr_defss) fld_induct'
nested_set_natural's pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
in```
```--- 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
@@ -13,9 +13,8 @@
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
-  val mk_induct_tac: Proof.context -> int list -> int list list ->
-    ((int * int) * (int * int)) list list list -> thm list -> thm -> thm list -> thm list list ->
-    tactic
+  val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list ->
+    thm -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> tactic
val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
end;
@@ -43,53 +42,6 @@

val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;

-fun mk_set_rhs def T =
-  let
-    val lhs = snd (Logic.dest_equals (prop_of def));
-    val Type (_, Ts0) = domain_type (fastype_of lhs);
-    val Type (_, Ts) = domain_type T;
-  in
-    Term.subst_atomic_types (Ts0 ~~ Ts) lhs
-  end;
-
-val mk_fsts_rhs = mk_set_rhs @{thm fsts_def[abs_def]};
-val mk_snds_rhs = mk_set_rhs @{thm snds_def[abs_def]};
-val mk_setl_rhs = mk_set_rhs @{thm sum_setl_def[abs_def]};
-val mk_setr_rhs = mk_set_rhs @{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 (@{const_name fsts}, T1) \$
-          (t5 \$ Const (@{const_name snds}, 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 (@{const_name sum_setl}, T1) \$
-          (t5 \$ Const (@{const_name sum_setr}, 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'
@@ -137,44 +89,42 @@

val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};

-fun solve_prem_prem_tac ctxt =
-  SELECT_GOAL (Local_Defs.unfold_tac ctxt
-    @{thms Un_iff eq_UN_compreh_Un mem_Collect_eq mem_UN_compreh_eq}) THEN'
-  REPEAT o (etac @{thm rev_bexI} ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
-  (atac ORELSE' rtac refl ORELSE' rtac @{thm singletonI});
+val solve_prem_prem_tac =
+  REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
+    hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
+  (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});

val induct_prem_prem_thms =
@{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
-      UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv
-      image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
-      sum_map.simps};
+      UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff Union_Un_distrib collect_def[abs_def]
+      eq_UN_compreh_Un fst_conv image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right
+      fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps
+      sum_set_simps};

-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,
+fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
+  EVERY' (maps (fn 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)),
-     solve_prem_prem_tac ctxt]) (rev ppjjqqkks)) 1;
+     solve_prem_prem_tac]) (rev kks)) 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
+fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
+  let val r = length kks in
EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
EVERY [REPEAT_DETERM_N r
(rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1,
-      mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs]
+      mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs]
end;

-fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss =
+fun mk_induct_tac ctxt ns mss kkss ctr_defs fld_induct' set_natural's pre_set_defss =
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)) kkss)
end;

end;```