# HG changeset patch # User blanchet # Date 1347617367 -7200 # Node ID 1271aca16aed098aa1208c51f81d4a41a158db4a # Parent cc1d39529dd1c9852cc30860b14d035ab8802b57 make tactic more robust in the case where "asm_simp_tac" already finishes the job diff -r cc1d39529dd1 -r 1271aca16aed 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 @@ -52,7 +52,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_id_fun T = Abs (Name.uu, T, Bound 0); 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; @@ -66,8 +65,6 @@ Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z) end; -fun fold_def_rule n thm = funpow n (fn thm => thm RS fun_cong) (thm RS meta_eq_to_obj_eq) RS sym; - fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; fun merge_type_arg T T' = if T = T' then T else cannot_merge_types (); @@ -184,7 +181,7 @@ let val (needs, ss') = fold_map add Ts ss in if exists I needs then (true, insert (op =) s ss') else (false, ss') end - | add T ss = (member (op =) As T, ss); + | add T ss = (member (op =) Bs T, ss); in snd oo add end; val nested_bnfs = @@ -204,6 +201,9 @@ val flds = map (mk_fld As) flds0; val fpTs = map (domain_type o fastype_of) unfs; + + val exists_fp_subtype = exists_subtype (member (op =) fpTs); + val vs = map2 (curry Free) vs' fpTs; val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs; @@ -516,34 +516,76 @@ fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs, rec_defs), lthy) = let + fun mk_sets_nested bnf = + let + val Type (T_name, Us) = T_of_bnf bnf; + val lives = lives_of_bnf bnf; + val sets = sets_of_bnf bnf; + fun mk_set U = + (case find_index (curry (op =) U) lives of + ~1 => Term.dummy + | i => nth sets i); + in + (T_name, map mk_set Us) + end; + + val setss_nested = map mk_sets_nested nested_bnfs; + val (induct_thms, induct_thm) = let - val (ps, names_lthy) = + val ((phis, phis'), names_lthy) = lthy - |> mk_Frees "P" (map mk_predT fpTs); + |> mk_Frees' "P" (map mk_predT fpTs); - fun mk_prem_prem (x as Free (_, T)) = - map HOLogic.mk_Trueprop + fun mk_set Ts t = + let val Type (_, Ts0) = domain_type (fastype_of t) in + Term.subst_atomic_types (Ts0 ~~ Ts) t + end; + + fun mk_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) = (case find_index (curry (op =) T) fpTs of - ~1 => [] - | i => [nth ps i $ x]); + ~1 => + (case AList.lookup (op =) setss_nested T_name of + NONE => [] + | SOME raw_sets0 => + let + val (Ts, raw_sets) = + split_list (filter (exists_fp_subtype o fst) (Ts0 ~~ raw_sets0)); + val sets = map (mk_set Ts0) raw_sets; + val (ys, names_lthy') = names_lthy |> mk_Frees s Ts; + val heads = + map2 (fn y => fn set => HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x))) + ys sets; + val bodies = flat (map (mk_prem_prems names_lthy') ys); + in + map2 (curry Logic.mk_implies) heads bodies + end) + | i => [HOLogic.mk_Trueprop (nth phis i $ x)]) + | mk_prem_prems _ _ = []; - fun mk_prem p ctr ctr_Ts = - let val (xs, _) = names_lthy |> mk_Frees "x" ctr_Ts in + fun close_prem_prem (Free x') t = + fold_rev Logic.all (map Free (drop (N + 1) (rev (Term.add_frees t (x' :: phis'))))) t; + + fun mk_prem 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 (maps mk_prem_prem xs, - HOLogic.mk_Trueprop (p $ Term.list_comb (ctr, xs)))) + (Logic.list_implies (prem_prems, + HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))) end; val goal = - fold_rev (fold_rev Logic.all) [ps, vs] - (Library.foldr Logic.list_implies (map3 (map2 o mk_prem) ps ctrss ctr_Tsss, + 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 $)) ps vs)))); + (map2 (curry (op $)) phis vs)))); val induct_thm = Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)); + mk_induct_tac ctxt); in `(conj_dests N) induct_thm end; @@ -572,7 +614,7 @@ fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) = if member (op =) fpTs T then maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x] - else if exists_subtype (member (op =) fpTs) T then + else if exists_fp_subtype T then [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x] else [x]; diff -r cc1d39529dd1 -r 1271aca16aed 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,6 +13,7 @@ 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_inject_tac: Proof.context -> thm -> thm -> tactic val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic end; @@ -51,6 +52,9 @@ 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)(*###*); + 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}; @@ -67,6 +71,6 @@ subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN - (rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1; + TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); end; diff -r cc1d39529dd1 -r 1271aca16aed src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 14 12:09:27 2012 +0200 @@ -1873,7 +1873,7 @@ ||>> mk_Frees "f" coiter_fTs ||>> mk_Frees "g" coiter_fTs ||>> mk_Frees "s" corec_sTs - ||>> mk_Frees "phi" (map (fn T => T --> mk_predT T) Ts); + ||>> mk_Frees "P" (map (fn T => T --> mk_predT T) Ts); fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1)); val unf_name = Binding.name_of o unf_bind; @@ -2309,9 +2309,9 @@ ||>> mk_Frees "u" uTs ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' - ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs) + ||>> mk_Freess "P" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs) ||>> mk_Frees "R" JRTs - ||>> mk_Frees "phi" JphiTs + ||>> mk_Frees "P" JphiTs ||>> mk_Frees "B1" B1Ts ||>> mk_Frees "B2" B2Ts ||>> mk_Frees "A" AXTs diff -r cc1d39529dd1 -r 1271aca16aed src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 14 12:09:27 2012 +0200 @@ -794,7 +794,7 @@ ||>> mk_Frees' "x" init_FTs ||>> mk_Frees "f" init_fTs ||>> mk_Frees "f" init_fTs - ||>> mk_Frees "phi" (replicate n (mk_predT initT)); + ||>> mk_Frees "P" (replicate n (mk_predT initT)); val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss) (HOLogic.mk_conj (HOLogic.mk_eq (iidx, @@ -1374,7 +1374,7 @@ ||>> mk_Frees "p2" p2Ts ||>> mk_Frees' "y" passiveAs ||>> mk_Frees "R" IRTs - ||>> mk_Frees "phi" IphiTs; + ||>> mk_Frees "P" IphiTs; val map_FTFT's = map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;