# HG changeset patch # User wenzelm # Date 1379529216 -7200 # Node ID 2a9a5dcf764f8420218776c1bdc678923926d7fd # Parent 6eb85a1cb4069856442a236dc201d35237801131# Parent 0c565fec9c78a57f15b0af2fcca8daaf0b531c17 merged; diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 20:32:49 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 20:33:36 2013 +0200 @@ -750,13 +750,17 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{discs} @{text "[simp]"}\rm:] ~ \\ -@{thm list.discs(1)[no_vars]} \\ -@{thm list.discs(2)[no_vars]} - -\item[@{text "t."}\hthm{sels} @{text "[simp]"}\rm:] ~ \\ -@{thm list.sels(1)[no_vars]} \\ -@{thm list.sels(2)[no_vars]} +\item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\ +@{thm list.disc(1)[no_vars]} \\ +@{thm list.disc(2)[no_vars]} + +\item[@{text "t."}\hthm{discI}\rm:] ~ \\ +@{thm list.discI(1)[no_vars]} \\ +@{thm list.discI(2)[no_vars]} + +\item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\ +@{thm list.sel(1)[no_vars]} \\ +@{thm list.sel(2)[no_vars]} \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\ @{thm list.collapse(1)[no_vars]} \\ @@ -792,9 +796,9 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{sets} @{text "[code]"}\rm:] ~ \\ -@{thm list.sets(1)[no_vars]} \\ -@{thm list.sets(2)[no_vars]} +\item[@{text "t."}\hthm{set} @{text "[code]"}\rm:] ~ \\ +@{thm list.set(1)[no_vars]} \\ +@{thm list.set(2)[no_vars]} \item[@{text "t."}\hthm{map} @{text "[code]"}\rm:] ~ \\ @{thm list.map(1)[no_vars]} \\ @@ -847,7 +851,7 @@ \begin{description} \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\ -@{text t.rel_distinct} @{text t.sets} +@{text t.rel_distinct} @{text t.set} \end{description} \end{indentblock} @@ -1512,11 +1516,11 @@ @{thm llist.corec(1)[no_vars]} \\ @{thm llist.corec(2)[no_vars]} -\item[@{text "t."}\hthm{disc\_unfold} @{text "[simp]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\ @{thm llist.disc_unfold(1)[no_vars]} \\ @{thm llist.disc_unfold(2)[no_vars]} -\item[@{text "t."}\hthm{disc\_corec} @{text "[simp]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\ @{thm llist.disc_corec(1)[no_vars]} \\ @{thm llist.disc_corec(2)[no_vars]} @@ -1547,7 +1551,7 @@ \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec}$^*$ @{text t.disc_corec}] ~ \\ @{text t.disc_corec_iff} @{text t.sel_corec} @{text t.unfold}$^*$ @{text t.disc_unfold} @{text t.disc_unfold_iff} ~ \\ -@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.sets} +@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set} \end{description} \end{indentblock} @@ -1721,7 +1725,7 @@ primcorec lappend :: "'a llist \ 'a llist \ 'a llist" where "lnull xs \ lnull ys \ lnull (lappend xs ys)" | "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" | - "ltl (lappend xs ys) = ltl (if lnull xs then ys else xs)" + "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)" . (*<*) end diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/BNF_FP_Base.thy --- a/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 18 20:33:36 2013 +0200 @@ -159,6 +159,9 @@ (\x. x \ P \ f x \ Q)" unfolding Grp_def by rule auto +lemma eq_ifI: "\b \ t = x; \ b \ t = y\ \ t = (if b then x else y)" + by fastforce + lemma if_if_True: "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = (if b then x else if b' then x' else f y')" diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Wed Sep 18 20:33:36 2013 +0200 @@ -23,24 +23,14 @@ lemma converse_Times: "(A \ B) ^-1 = B \ A" by auto -lemma equiv_triv1: -assumes "equiv A R" and "(a, b) \ R" and "(a, c) \ R" -shows "(b, c) \ R" -using assms unfolding equiv_def sym_def trans_def by blast - -lemma equiv_triv2: -assumes "equiv A R" and "(a, b) \ R" and "(b, c) \ R" -shows "(a, c) \ R" -using assms unfolding equiv_def trans_def by blast - lemma equiv_proj: assumes e: "equiv A R" and "z \ R" shows "(proj R o fst) z = (proj R o snd) z" proof - from assms(2) have z: "(fst z, snd z) \ R" by auto - have P: "\x. (fst z, x) \ R \ (snd z, x) \ R" by (erule equiv_triv1[OF e z]) - have "\x. (snd z, x) \ R \ (fst z, x) \ R" by (erule equiv_triv2[OF e z]) - with P show ?thesis unfolding proj_def[abs_def] by auto + with e have "\x. (fst z, x) \ R \ (snd z, x) \ R" "\x. (snd z, x) \ R \ (fst z, x) \ R" + unfolding equiv_def sym_def trans_def by blast+ + then show ?thesis unfolding proj_def[abs_def] by auto qed (* Operators: *) diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Wed Sep 18 20:33:36 2013 +0200 @@ -136,10 +136,7 @@ "\\x y. \x \ X; y \ X\ \ (f x = f y) = (x = y); \x. x \ X \ f x \ Y; \y. y \ Y \ \x \ X. y = f x\ \ bij_betw f X Y" -unfolding bij_betw_def inj_on_def -apply (rule conjI) - apply blast -by (erule thin_rl) blast +unfolding bij_betw_def inj_on_def by blast lemma surj_fun_eq: assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 o f) x = (g2 o f) x" diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Examples/Process.thy --- a/src/HOL/BNF/Examples/Process.thy Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Examples/Process.thy Wed Sep 18 20:33:36 2013 +0200 @@ -44,7 +44,7 @@ Ch: "\ p q p' q'. \ (Choice p q) (Choice p' q') \ \ p p' \ \ q q'" shows "p = p'" using assms - by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.discs(3)) + by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.disc(3)) (* Stronger coinduction, up to equality: *) theorem process_strong_coind[elim, consumes 1, case_names iss Action Choice]: @@ -54,7 +54,7 @@ Ch: "\ p q p' q'. \ (Choice p q) (Choice p' q') \ (\ p p' \ p = p') \ (\ q q' \ q = q')" shows "p = p'" using assms - by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.discs(3)) + by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.disc(3)) subsection {* Coiteration (unfold) *} diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Wed Sep 18 20:33:36 2013 +0200 @@ -33,7 +33,7 @@ *} code_datatype Stream -lemmas [code] = stream.sels stream.sets stream.case +lemmas [code] = stream.sel stream.set stream.case lemma stream_case_cert: assumes "CASE \ stream_case c" @@ -495,7 +495,7 @@ lemma sinterleave_code[code]: "sinterleave (x ## s1) s2 = x ## sinterleave s2 s1" - by (metis sinterleave_simps stream.exhaust stream.sels) + by (metis sinterleave_simps stream.exhaust stream.sel) lemma sinterleave_snth[simp]: "even n \ sinterleave s1 s2 !! n = s1 !! (n div 2)" diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 20:33:36 2013 +0200 @@ -115,22 +115,23 @@ val collapseN = "collapse"; val disc_excludeN = "disc_exclude"; val disc_exhaustN = "disc_exhaust"; -val discsN = "discs"; +val discN = "disc"; +val discIN = "discI"; val distinctN = "distinct"; val exhaustN = "exhaust"; val expandN = "expand"; val injectN = "inject"; val nchotomyN = "nchotomy"; -val selsN = "sels"; +val selN = "sel"; val splitN = "split"; val splitsN = "splits"; val split_asmN = "split_asm"; val weak_case_cong_thmsN = "weak_case_cong"; +val cong_attrs = @{attributes [cong]}; +val safe_elim_attrs = @{attributes [elim!]}; +val iff_attrs = @{attributes [iff]}; val induct_simp_attrs = @{attributes [induct_simp]}; -val cong_attrs = @{attributes [cong]}; -val iff_attrs = @{attributes [iff]}; -val safe_elim_attrs = @{attributes [elim!]}; val simp_attrs = @{attributes [simp]}; fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys); @@ -696,6 +697,8 @@ [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms) end; + val nontriv_discI_thms = if n = 1 then [] else discI_thms; + val (case_cong_thm, weak_case_cong_thm) = let fun mk_prem xctr xs xf xg = @@ -750,7 +753,8 @@ (case_congN, [case_cong_thm], []), (case_convN, case_conv_thms, []), (collapseN, collapse_thms, simp_attrs), - (discsN, disc_thms, simp_attrs), + (discN, disc_thms, simp_attrs), + (discIN, nontriv_discI_thms, []), (disc_excludeN, disc_exclude_thms, []), (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), @@ -758,7 +762,7 @@ (expandN, expand_thms, []), (injectN, inject_thms, iff_attrs @ induct_simp_attrs), (nchotomyN, [nchotomy_thm], []), - (selsN, all_sel_thms, simp_attrs), + (selN, all_sel_thms, simp_attrs), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), (splitsN, [split_thm, split_asm_thm], []), diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Wed Sep 18 20:33:36 2013 +0200 @@ -134,7 +134,6 @@ HEADGOAL (rtac uexhaust THEN' EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)); -(* TODO: More precise "simp_thms"; get rid of "blast_tac" *) fun mk_split_tac ctxt uexhaust cases injectss distinctsss = HEADGOAL (rtac uexhaust) THEN ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Sep 18 20:33:36 2013 +0200 @@ -1034,7 +1034,7 @@ ((coinduct_thms_pairs, coinduct_case_attrs), (unfold_thmss, corec_thmss, []), (safe_unfold_thmss, safe_corec_thmss), - (disc_unfold_thmss, disc_corec_thmss, simp_attrs), + (disc_unfold_thmss, disc_corec_thmss, []), (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs), (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs)) end; @@ -1395,7 +1395,7 @@ [(mapN, map_thms, code_simp_attrs), (rel_distinctN, rel_distinct_thms, code_simp_attrs), (rel_injectN, rel_inject_thms, code_simp_attrs), - (setsN, flat set_thmss, code_simp_attrs)] + (setN, flat set_thmss, code_simp_attrs)] |> massage_simple_notes fp_b_name; in (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Wed Sep 18 20:33:36 2013 +0200 @@ -156,7 +156,7 @@ fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' = hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN' - full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt); + full_simp_tac (ss_only (refl :: no_refl (union Thm.eq_thm discs discs') @ basic_simp_thms) ctxt); fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs discss selss = diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 18 20:33:36 2013 +0200 @@ -717,7 +717,7 @@ (* try to prove (automatically generated) tautologies by ourselves *) val exclss'' = exclss' |> map (map (apsnd - (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_taut_tac lthy |> K)))))); + (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_assumption_tac lthy |> K)))))); val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss''; val (obligation_idxss, obligationss) = exclss'' |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd)) @@ -772,7 +772,7 @@ |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) |> curry Logic.list_all (map dest_Free (#fun_args sel_eqn)); in - mk_primcorec_eq_tac lthy def_thms sel_corec k m exclsss + mk_primcorec_ctr_or_sel_tac lthy def_thms sel_corec k m exclsss nested_maps nested_map_idents nested_map_comps |> K |> Goal.prove lthy [] [] t end; diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 20:33:36 2013 +0200 @@ -7,12 +7,14 @@ signature BNF_FP_REC_SUGAR_TACTICS = sig - val mk_primcorec_taut_tac: Proof.context -> tactic + val mk_primcorec_assumption_tac: Proof.context -> tactic + val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic + val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic + val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic + val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int -> + thm list list list -> thm list -> thm list -> thm list -> tactic val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> tactic - val mk_primcorec_dtr_to_ctr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic - val mk_primcorec_eq_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> - thm list -> thm list -> thm list -> tactic val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic end; @@ -28,10 +30,8 @@ unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN HEADGOAL (rtac refl); -fun mk_primcorec_taut_tac ctxt = - HEADGOAL (etac FalseE) ORELSE - unfold_thms_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not not_False_eq_True} THEN - HEADGOAL (SOLVE o REPEAT o (atac ORELSE' resolve_tac @{thms disjI1 disjI2 conjI TrueI})); +fun mk_primcorec_assumption_tac ctxt = + HEADGOAL (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt)); fun mk_primcorec_same_case_tac m = HEADGOAL (if m = 0 then rtac TrueI @@ -39,7 +39,7 @@ fun mk_primcorec_different_case_tac ctxt excl = unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN - HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_taut_tac ctxt)); + HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_assumption_tac ctxt)); fun mk_primcorec_cases_tac ctxt k m exclsss = let val n = length exclsss in @@ -54,13 +54,30 @@ fun mk_primcorec_disc_tac ctxt defs disc k m exclsss = mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss; -fun mk_primcorec_eq_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps = - mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN - unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @ - maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl); +fun mk_primcorec_ctr_or_sel_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps = + mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN + mk_primcorec_cases_tac ctxt k m exclsss THEN + unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False if_cancel[of _ True] + if_cancel[of _ False] o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN + HEADGOAL (rtac refl); -fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels = +fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc sels = HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl); +fun mk_primcorec_code_of_ctr_case_tac ctxt m ctr_thm = + HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN + mk_primcorec_prelude ctxt [] (ctr_thm RS trans) THEN + REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN + HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)); + +fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms = + EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms); + +fun mk_primcorec_code_tac ctxt raw collapses = + HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN + Method.intros_tac @{thms conjI impI} [] THEN + REPEAT (HEADGOAL (rtac refl ORELSE' (etac notE THEN' atac) ORELSE' + eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses))); + end; diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Sep 18 20:33:36 2013 +0200 @@ -111,7 +111,7 @@ val set_inclN: string val set_set_inclN: string val sel_unfoldN: string - val setsN: string + val setN: string val simpsN: string val strTN: string val str_initN: string @@ -287,7 +287,7 @@ val LevN = "Lev" val rvN = "recover" val behN = "beh" -val setsN = "sets" +val setN = "set" val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN fun mk_set_inductN i = mk_setN i ^ "_induct" diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 18 20:33:36 2013 +0200 @@ -2011,11 +2011,17 @@ |> Thm.close_derivation end; + val map_id0s_o_id = + map (fn thm => + mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_o}) + map_id0s; + val (dtor_corec_unique_thms, dtor_corec_unique_thm) = `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) - |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o id_apply o_assoc sum_case_o_inj(1)} @ - map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); + |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ + map_id0s_o_id @ sym_map_comps) + OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); val timer = time (timer "corec definitions & thms"); diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Wed Sep 18 20:33:36 2013 +0200 @@ -51,7 +51,8 @@ rtac (Drule.instantiate_normalize insts thm) 1 end); -fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); +fun unfold_thms_tac _ [] = all_tac + | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; diff -r 6eb85a1cb406 -r 2a9a5dcf764f src/HOL/List.thy --- a/src/HOL/List.thy Wed Sep 18 20:32:49 2013 +0200 +++ b/src/HOL/List.thy Wed Sep 18 20:33:36 2013 +0200 @@ -710,9 +710,15 @@ lemma neq_Nil_conv: "(xs \ []) = (\y ys. xs = y # ys)" by (induct xs) auto +lemma tl_Nil: "tl xs = [] \ xs = [] \ (EX x. xs = [x])" +by (cases xs) auto + +lemma Nil_tl: "[] = tl xs \ xs = [] \ (EX x. xs = [x])" +by (cases xs) auto + lemma length_induct: "(\xs. \ys. length ys < length xs \ P ys \ P xs) \ P xs" -by (rule measure_induct [of length]) iprover +by (fact measure_induct) lemma list_nonempty_induct [consumes 1, case_names single cons]: assumes "xs \ []"