# HG changeset patch # User blanchet # Date 1347617367 -7200 # Node ID df359ce891ac5170b23e3fc7e4f1987234fca45f # Parent a1e811aa0fb8129d680dd6fd6c8666ff026290ca added induct tactic diff -r a1e811aa0fb8 -r df359ce891ac src/HOL/Codatatype/BNF_FP.thy --- a/src/HOL/Codatatype/BNF_FP.thy Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/BNF_FP.thy Fri Sep 14 12:09:27 2012 +0200 @@ -26,17 +26,11 @@ lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" by auto -lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" by simp - -lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" by clarsimp +lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" +by simp -(* FIXME: needed? *) -lemma False_imp_eq: "(False \ P) \ Trueprop True" -by presburger - -(* FIXME: needed? *) -lemma all_point_1: "(\z. z = b \ phi z) \ Trueprop (phi b)" -by presburger +lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" +by clarsimp lemma rev_bspec: "a \ A \ \z \ A. P z \ P a" by simp @@ -110,6 +104,20 @@ "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" by simp +lemma UN_compreh_bex: +"\{y. \x \ A. y = {}} = {}" +"\{y. \x \ A. y = {x}} = A" +by blast+ + +lemma induct_set_step: "\B \ A; c \ f B\ \ \C. (\a \ A. C = f a) \ c \ C" +apply (rule exI) +apply (rule conjI) + apply (rule bexI) + apply (rule refl) + apply assumption +apply assumption +done + ML_file "Tools/bnf_fp_util.ML" ML_file "Tools/bnf_fp_sugar_tactics.ML" ML_file "Tools/bnf_fp_sugar.ML" diff -r a1e811aa0fb8 -r df359ce891ac src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200 @@ -51,8 +51,6 @@ val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)); -fun mk_id T = Const (@{const_name id}, T --> T); - fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; fun mk_uncurried2_fun f xss = @@ -499,9 +497,10 @@ ((wrap, define_iter_likes), lthy') end; - (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there *) + (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there ### *) val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; + val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs; val nesting_map_ids = map map_id_of_bnf nesting_bnfs; fun mk_map Ts Us t = @@ -571,26 +570,36 @@ fold_rev Logic.all (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t; - fun mk_prem phi ctr ctr_Ts = + fun mk_prem_triple phi ctr ctr_Ts = let val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; val prem_prems = maps (fn x => map (close_prem_prem x) (mk_prem_prems names_lthy' x)) xs; in - fold_rev Logic.all xs - (Logic.list_implies (prem_prems, - HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))) + (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end; + val prem_tripless = map3 (map2 o mk_prem_triple) phis ctrss ctr_Tsss; + + fun mk_prem (xs, prem_prems, concl) = + fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl)); + val goal = - fold_rev (fold_rev Logic.all) [phis, vs] - (Library.foldr Logic.list_implies (map3 (map2 o mk_prem) phis ctrss ctr_Tsss, - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 (curry (op $)) phis vs)))); + Library.foldr (Logic.list_implies o apfst (map mk_prem)) (prem_tripless, + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 (curry (op $)) phis vs))); + + val rss = map (map (length o #2)) prem_tripless; + + 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); + mk_induct_tac ctxt ns mss rss (flat ctr_defss) fld_induct' pre_set_defss + nested_set_natural's) + (* TODO: thread name context properly ### *) + |> singleton (Proof_Context.export names_lthy lthy) + |> singleton (Proof_Context.export no_defs_lthy no_defs_lthy0) in `(conj_dests nn) induct_thm end; @@ -607,7 +616,7 @@ fun build_call fiter_likes maybe_tick (T, U) = if T = U then - mk_id T + id_const T else (case find_index (curry (op =) T) fpTs of ~1 => build_map (build_call fiter_likes maybe_tick) T U @@ -685,7 +694,7 @@ fun build_call fiter_likes maybe_tack (T, U) = if T = U then - mk_id T + id_const T else (case find_index (curry (op =) U) fpTs of ~1 => build_map (build_call fiter_likes maybe_tack) T U diff -r a1e811aa0fb8 -r df359ce891ac src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 12:09:27 2012 +0200 @@ -13,7 +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 -> tactic + val mk_induct_tac: Proof.context -> int list -> int list list -> int list list -> thm list -> + thm -> thm list list -> thm 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; @@ -25,6 +26,23 @@ open BNF_Util open BNF_FP_Util +val meta_mp = @{thm meta_mp}; +val meta_spec = @{thm meta_spec}; + +fun squash_spurious_fs lthy thm = + let + val spurious_fs = + Term.add_vars (prop_of thm) [] + |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false); + val cxs = + map (fn s as (_, T) => + (certify lthy (Var s), certify lthy (id_abs (domain_type T)))) spurious_fs; + in + Drule.cterm_instantiate cxs thm + end; + +val squash_spurious_fs_tac = PRIMITIVE o squash_spurious_fs; + 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' @@ -34,8 +52,8 @@ fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' = Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN - EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec}, - etac @{thm meta_mp}, atac]) (1 upto n)) 1; + EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec, + etac meta_mp, atac]) (1 upto n)) 1; fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld = (rtac iffI THEN' @@ -52,9 +70,6 @@ Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; -fun mk_induct_tac ctxt = - Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt) (* FIXME: TODO *); - val iter_like_thms = @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps split_conv}; @@ -73,4 +88,52 @@ Local_Defs.unfold_tac ctxt @{thms id_def} THEN TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); +fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' = + Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN squash_spurious_fs_tac ctxt; + +fun mk_induct_prepare_prem_tac n m k = + 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; + +fun mk_induct_prepare_prem_prems_tac _ _ 0 = all_tac + | mk_induct_prepare_prem_prems_tac nn kk r = + REPEAT_DETERM_N r (rotate_tac (~1 + kk - nn) 1 THEN dtac meta_mp 1 THEN + defer_tac 2 THEN PRIMITIVE (Thm.permute_prems 0 ~1) THEN rotate_tac 1 1) THEN + PRIMITIVE Raw_Simplifier.norm_hhf; + +val induct_prem_prem_thms = + @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left + Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv fsts_def[abs_def] image_def + map_pair_simp o_apply snd_conv snds_def[abs_def] sum.cases sum_map.simps sum_setl_def[abs_def] + sum_setr_def[abs_def] sup_bot_right}; + +fun mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's = + EVERY' (maps (fn i => + [dtac meta_spec, rotate_tac ~1, etac meta_mp, + SELECT_GOAL (Local_Defs.unfold_tac ctxt + (set_natural's @ pre_set_defs @ induct_prem_prem_thms)), + rtac (mk_UnIN r i), + atac ORELSE' + rtac @{thm singletonI} ORELSE' + (REPEAT_DETERM o (atac ORELSE' + SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN' + etac @{thm induct_set_step}))]) (r downto 1)) 1; + +fun mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's = + EVERY [mk_induct_prepare_prem_tac n m k, + mk_induct_prepare_prem_prems_tac nn kk r, atac 1, + mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's]; + +fun mk_induct_tac ctxt ns mss rss ctr_defs fld_induct' pre_set_defss set_natural's = + let + val nn = length ns; + val n = Integer.sum ns; + in + mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN + EVERY (map5 (fn kk => fn pre_set_defs => + EVERY ooo map3 (fn m => fn k => fn r => + mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's)) + (1 upto nn) pre_set_defss mss (unflat mss (1 upto Integer.sum ns)) rss) + end; + end; diff -r a1e811aa0fb8 -r df359ce891ac src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Fri Sep 14 12:09:27 2012 +0200 @@ -99,6 +99,9 @@ val mk_sumTN: typ list -> typ val mk_sumTN_balanced: typ list -> typ + val id_const: typ -> term + val id_abs: typ -> term + val Inl_const: typ -> typ -> term val Inr_const: typ -> typ -> term @@ -256,6 +259,9 @@ val mk_sumTN = Library.foldr1 mk_sumT; val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; +fun id_const T = Const (@{const_name id}, T --> T); +fun id_abs T = Abs (Name.uu, T, Bound 0); + fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT)); fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;