# HG changeset patch # User blanchet # Date 1347909210 -7200 # Node ID 64ac3471005ab6d2b5002adaf46606f50619fd98 # Parent 93f158d59ead03cb80be1c2c3eae4b4d156967c0 cleaner way of dealing with the set functions of sums and products diff -r 93f158d59ead -r 64ac3471005a src/HOL/Codatatype/BNF_FP.thy --- 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: "(\y. y \ A \ y \ {x}) = (x \ 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: "\b \ A; c \ F b\ \ \x. x \ A \ c \ F x" "\B \ A; c \ f B\ \ \C. (\a \ A. C = f a) \c \ C" diff -r 93f158d59ead -r 64ac3471005a src/HOL/Codatatype/Tools/bnf_fp_sugar.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 @@ -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 diff -r 93f158d59ead -r 64ac3471005a src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- 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;