--- 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 \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
"lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> 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
--- 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 @@
(\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
unfolding Grp_def by rule auto
+lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> 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')"
--- 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 \<times> B) ^-1 = B \<times> A"
by auto
-lemma equiv_triv1:
-assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
-shows "(b, c) \<in> R"
-using assms unfolding equiv_def sym_def trans_def by blast
-
-lemma equiv_triv2:
-assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
-shows "(a, c) \<in> R"
-using assms unfolding equiv_def trans_def by blast
-
lemma equiv_proj:
assumes e: "equiv A R" and "z \<in> R"
shows "(proj R o fst) z = (proj R o snd) z"
proof -
from assms(2) have z: "(fst z, snd z) \<in> R" by auto
- have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
- have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
- with P show ?thesis unfolding proj_def[abs_def] by auto
+ with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
+ unfolding equiv_def sym_def trans_def by blast+
+ then show ?thesis unfolding proj_def[abs_def] by auto
qed
(* Operators: *)
--- 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 @@
"\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
\<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
\<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> 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: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
--- 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: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> 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: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> 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) *}
--- 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 \<equiv> 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 \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
--- 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], []),
--- 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'
--- 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),
--- 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 =
--- 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;
--- 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;
--- 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"
--- 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");
--- 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;
--- 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 \<noteq> []) = (\<exists>y ys. xs = y # ys)"
by (induct xs) auto
+lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"
+by (cases xs) auto
+
+lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"
+by (cases xs) auto
+
lemma length_induct:
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> 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 \<noteq> []"