--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy Tue Nov 11 20:11:38 2014 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy Tue Nov 11 21:14:19 2014 +0100
@@ -34,6 +34,8 @@
datatype (discs_sels) 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
datatype (discs_sels) 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
+datatype ('a, 'b) ite = ITE "'a \<Rightarrow> bool" "'a \<Rightarrow> 'b" "'a \<Rightarrow> 'b"
+
datatype 'a live_and_fun = LiveAndFun nat "nat \<Rightarrow> 'a"
datatype (discs_sels) hfset = HFset "hfset fset"
--- a/src/HOL/List.thy Tue Nov 11 20:11:38 2014 +0100
+++ b/src/HOL/List.thy Tue Nov 11 21:14:19 2014 +0100
@@ -3361,6 +3361,175 @@
"distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
by force
+lemma remdups_adj_altdef: "(remdups_adj xs = ys) \<longleftrightarrow>
+ (\<exists>f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
+ \<and> (\<forall>i < size xs. xs!i = ys!(f i))
+ \<and> (\<forall>i. i + 1 < size xs \<longrightarrow> (xs!i = xs!(i+1) <-> f i = f(i+1))))" (is "?L \<longleftrightarrow> (\<exists>f. ?p f xs ys)")
+proof
+ assume ?L
+ then show "\<exists>f. ?p f xs ys"
+ proof (induct xs arbitrary: ys rule: remdups_adj.induct)
+ case (1 ys)
+ thus ?case by (intro exI[of _ id]) (auto simp: mono_def)
+ next
+ case (2 x ys)
+ thus ?case by (intro exI[of _ id]) (auto simp: mono_def)
+ next
+ case (3 x1 x2 xs ys)
+ let ?xs = "x1 # x2 # xs"
+ let ?cond = "x1 = x2"
+ def zs \<equiv> "remdups_adj (x2 # xs)"
+ from 3(1-2)[of zs]
+ obtain f where p: "?p f (x2 # xs) zs" unfolding zs_def by (cases ?cond) auto
+ then have f0: "f 0 = 0"
+ by (intro mono_image_least[where f=f]) blast+
+ from p have mono: "mono f" and f_xs_zs: "f ` {0..<length (x2 # xs)} = {0..<length zs}" by auto
+ have ys: "ys = (if x1 = x2 then zs else x1 # zs)"
+ unfolding 3(3)[symmetric] zs_def by auto
+ have zs0: "zs ! 0 = x2" unfolding zs_def by (induct xs) auto
+ have zsne: "zs \<noteq> []" unfolding zs_def by (induct xs) auto
+ let ?Succ = "if ?cond then id else Suc"
+ let ?x1 = "if ?cond then id else Cons x1"
+ let ?f = "\<lambda> i. if i = 0 then 0 else ?Succ (f (i - 1))"
+ have ys: "ys = ?x1 zs" unfolding ys by (cases ?cond, auto)
+ have mono: "mono ?f" using `mono f` unfolding mono_def by auto
+ show ?case unfolding ys
+ proof (intro exI[of _ ?f] conjI allI impI)
+ show "mono ?f" by fact
+ next
+ fix i assume i: "i < length ?xs"
+ with p show "?xs ! i = ?x1 zs ! (?f i)" using zs0 by auto
+ next
+ fix i assume i: "i + 1 < length ?xs"
+ with p show "(?xs ! i = ?xs ! (i + 1)) = (?f i = ?f (i + 1))"
+ by (cases i) (auto simp: f0)
+ next
+ have id: "{0 ..< length (?x1 zs)} = insert 0 (?Succ ` {0 ..< length zs})"
+ using zsne by (cases ?cond, auto)
+ { fix i assume "i < Suc (length xs)"
+ hence "Suc i \<in> {0..<Suc (Suc (length xs))} \<inter> Collect (op < 0)" by auto
+ from imageI[OF this, of "\<lambda>i. ?Succ (f (i - Suc 0))"]
+ have "?Succ (f i) \<in> (\<lambda>i. ?Succ (f (i - Suc 0))) ` ({0..<Suc (Suc (length xs))} \<inter> Collect (op < 0))" by auto
+ }
+ then show "?f ` {0 ..< length ?xs} = {0 ..< length (?x1 zs)}"
+ unfolding id f_xs_zs[symmetric] by auto
+ qed
+ qed
+next
+ assume "\<exists> f. ?p f xs ys"
+ then show ?L
+ proof (induct xs arbitrary: ys rule: remdups_adj.induct)
+ case 1 then show ?case by auto
+ next
+ case (2 x) then obtain f where f_img: "f ` {0 ..< size [x]} = {0 ..< size ys}"
+ and f_nth: "\<And>i. i < size [x] \<Longrightarrow> [x]!i = ys!(f i)"
+ by blast
+
+ have "length ys = card (f ` {0 ..< size [x]})"
+ using f_img by auto
+ then have "length ys = 1" by auto
+ moreover
+ then have "f 0 = 0" using f_img by auto
+ ultimately show ?case using f_nth by (cases ys) auto
+ next
+ case (3 x1 x2 xs)
+ from "3.prems" obtain f where f_mono: "mono f"
+ and f_img: "f ` {0..<length (x1 # x2 # xs)} = {0..<length ys}"
+ and f_nth:
+ "\<And>i. i < length (x1 # x2 # xs) \<Longrightarrow> (x1 # x2 # xs) ! i = ys ! f i"
+ "\<And>i. i + 1 < length (x1 # x2 #xs) \<Longrightarrow>
+ ((x1 # x2 # xs) ! i = (x1 # x2 # xs) ! (i + 1)) = (f i = f (i + 1))"
+ by blast
+
+ show ?case
+ proof cases
+ assume "x1 = x2"
+
+ let ?f' = "f o Suc"
+
+ have "remdups_adj (x1 # xs) = ys"
+ proof (intro "3.hyps" exI conjI impI allI)
+ show "mono ?f'"
+ using f_mono by (simp add: mono_iff_le_Suc)
+ next
+ have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}"
+ by safe (fastforce, rename_tac x, case_tac x, auto)
+ also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}"
+ proof -
+ have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth[of 0] by simp
+ then show ?thesis by safe (fastforce, rename_tac x, case_tac x, auto)
+ qed
+ also have "\<dots> = {0 ..< length ys}" by fact
+ finally show "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" .
+ qed (insert f_nth[of "Suc i" for i], auto simp: \<open>x1 = x2\<close>)
+ then show ?thesis using \<open>x1 = x2\<close> by simp
+ next
+ assume "x1 \<noteq> x2"
+
+ have "2 \<le> length ys"
+ proof -
+ have "2 = card {f 0, f 1}" using \<open>x1 \<noteq> x2\<close> f_nth[of 0] by auto
+ also have "\<dots> \<le> card (f ` {0..< length (x1 # x2 # xs)})"
+ by (rule card_mono) auto
+ finally show ?thesis using f_img by simp
+ qed
+
+ have "f 0 = 0" using f_mono f_img by (rule mono_image_least) simp
+
+ have "f (Suc 0) = Suc 0"
+ proof (rule ccontr)
+ assume "f (Suc 0) \<noteq> Suc 0"
+ then have "Suc 0 < f (Suc 0)" using f_nth[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close> by auto
+ then have "\<And>i. Suc 0 < f (Suc i)"
+ using f_mono
+ by (meson Suc_le_mono le0 less_le_trans monoD)
+ then have "\<And>i. Suc 0 \<noteq> f i" using \<open>f 0 = 0\<close>
+ by (case_tac i) fastforce+
+ then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
+ then show False using f_img \<open>2 \<le> length ys\<close> by auto
+ qed
+
+ obtain ys' where "ys = x1 # x2 # ys'"
+ using \<open>2 \<le> length ys\<close> f_nth[of 0] f_nth[of 1]
+ apply (cases ys)
+ apply (rename_tac [2] ys', case_tac [2] ys')
+ by (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
+
+ def f' \<equiv> "\<lambda>x. f (Suc x) - 1"
+
+ { fix i
+ have "Suc 0 \<le> f (Suc 0)" using f_nth[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close> by auto
+ also have "\<dots> \<le> f (Suc i)" using f_mono by (rule monoD) arith
+ finally have "Suc 0 \<le> f (Suc i)" .
+ } note Suc0_le_f_Suc = this
+
+ { fix i have "f (Suc i) = Suc (f' i)"
+ using Suc0_le_f_Suc[of i] by (auto simp: f'_def)
+ } note f_Suc = this
+
+ have "remdups_adj (x2 # xs) = (x2 # ys')"
+ proof (intro "3.hyps" exI conjI impI allI)
+ show "mono f'"
+ using Suc0_le_f_Suc f_mono by (auto simp: f'_def mono_iff_le_Suc le_diff_iff)
+ next
+ have "f' ` {0 ..< length (x2 # xs)} = (\<lambda>x. f x - 1) ` {0 ..< length (x1 # x2 #xs)}"
+ apply safe
+ apply (rename_tac [!] n, case_tac [!] n)
+ apply (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> intro: rev_image_eqI)
+ done
+ also have "\<dots> = (\<lambda>x. x - 1) ` f ` {0 ..< length (x1 # x2 #xs)}"
+ by (auto simp: image_comp)
+ also have "\<dots> = (\<lambda>x. x - 1) ` {0 ..< length ys}"
+ by (simp only: f_img)
+ also have "\<dots> = {0 ..< length (x2 # ys')}"
+ using \<open>ys = _\<close> by (fastforce intro: rev_image_eqI)
+ finally show "f' ` {0 ..< length (x2 # xs)} = {0 ..< length (x2 # ys')}" .
+ qed (insert f_nth[of "Suc i" for i] \<open>x1 \<noteq> x2\<close>, auto simp add: f_Suc \<open>ys = _\<close>)
+ then show ?case using \<open>ys = _\<close> \<open>x1 \<noteq> x2\<close> by simp
+ qed
+ qed
+qed
+
lemma hd_remdups_adj[simp]: "hd (remdups_adj xs) = hd xs"
by (induction xs rule: remdups_adj.induct) simp_all
--- a/src/HOL/Set_Interval.thy Tue Nov 11 20:11:38 2014 +0100
+++ b/src/HOL/Set_Interval.thy Tue Nov 11 21:14:19 2014 +0100
@@ -488,6 +488,19 @@
lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
by (simp add: Iio_eq_empty_iff bot_nat_def)
+lemma mono_image_least:
+ assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n"
+ shows "f m = m'"
+proof -
+ from f_img have "{m' ..< n'} \<noteq> {}"
+ by (metis atLeastLessThan_empty_iff image_is_empty)
+ with f_img have "m' \<in> f ` {m ..< n}" by auto
+ then obtain k where "f k = m'" "m \<le> k" by auto
+ moreover have "m' \<le> f m" using f_img by auto
+ ultimately show "f m = m'"
+ using f_mono by (auto elim: monoE[where x=m and y=k])
+qed
+
subsection {* Infinite intervals *}
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Nov 11 20:11:38 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Nov 11 21:14:19 2014 +0100
@@ -2227,12 +2227,12 @@
(Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy)
end;
- fun derive_rec_transfer_thms lthy recs rec_defs =
+ fun derive_rec_transfer_thms lthy recs rec_defs (SOME (_, _, _, xsssss)) =
let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs in
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) rec_defs
- xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
+ mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) xsssss
+ rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
|> Conjunction.elim_balanced nn
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -2318,8 +2318,7 @@
type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
val rec_transfer_thmss =
- if live = 0 then replicate nn []
- else map single (derive_rec_transfer_thms lthy recs rec_defs);
+ map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types);
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
@@ -2487,9 +2486,7 @@
val flat_corec_thms = append oo append;
- val corec_transfer_thmss =
- if live = 0 then replicate nn []
- else map single (derive_corec_transfer_thms lthy corecs corec_defs);
+ val corec_transfer_thmss = map single (derive_corec_transfer_thms lthy corecs corec_defs);
val ((rel_coinduct_thmss, common_rel_coinduct_thms),
(rel_coinduct_attrs, common_rel_coinduct_attrs)) =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Nov 11 20:11:38 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Nov 11 21:14:19 2014 +0100
@@ -39,7 +39,7 @@
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
- thm list -> thm list -> thm list -> thm list -> tactic
+ term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic
val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
thm list -> thm list -> thm list -> tactic
val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
@@ -182,12 +182,19 @@
unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
-fun mk_rec_transfer_tac ctxt nn ns actives passives rec_defs ctor_rec_transfers rel_pre_T_defs
+fun mk_rec_transfer_tac ctxt nn ns actives passives xssss rec_defs ctor_rec_transfers rel_pre_T_defs
rel_eqs =
let
val ctor_rec_transfers' =
map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
val total_n = Integer.sum ns;
+ val True = @{term True};
+ fun magic eq xs xs' = Subgoal.FOCUS (fn {prems, ...} =>
+ let
+ val thm = prems
+ |> Ctr_Sugar_Util.permute_like eq xs xs'
+ |> Library.foldl1 (fn (acc, elem) => elem RS (acc RS @{thm rel_funD}))
+ in HEADGOAL (rtac thm) end)
in
HEADGOAL Goal.conjunction_tac THEN
EVERY (map (fn ctor_rec_transfer =>
@@ -195,23 +202,27 @@
unfold_thms_tac ctxt rec_defs THEN
HEADGOAL (etac (mk_rel_funDN_rotated (nn + 1) ctor_rec_transfer)) THEN
unfold_thms_tac ctxt rel_pre_T_defs THEN
- EVERY (fst (fold_map (fn k => fn acc => rpair (k + acc)
+ EVERY (fst (@{fold_map 2} (fn k => fn xsss => fn acc =>
+ rpair (k + acc)
(HEADGOAL (rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer})) THEN
HEADGOAL (rtac @{thm vimage2p_rel_fun}) THEN
unfold_thms_tac ctxt rel_eqs THEN
- EVERY (map (fn n =>
- REPEAT_DETERM (HEADGOAL
- (rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE'
- rtac (mk_rel_funDN 2 case_sum_transfer))) THEN
+ EVERY (@{map 2} (fn n => fn xss =>
+ REPEAT_DETERM (HEADGOAL (resolve_tac
+ [mk_rel_funDN 2 case_sum_transfer_eq, mk_rel_funDN 2 case_sum_transfer])) THEN
HEADGOAL (select_prem_tac total_n (dtac asm_rl) (acc + n)) THEN
HEADGOAL (SELECT_GOAL (HEADGOAL
- ((REPEAT_DETERM o (atac ORELSE'
- rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE'
- rtac (mk_rel_funDN 1 case_prod_transfer) ORELSE'
- rtac rel_funI)) THEN_ALL_NEW
- (REPEAT_ALL_NEW (dtac rel_funD) THEN_ALL_NEW atac)))))
- (1 upto k))))
- ns 0)))
+ (REPEAT_DETERM o (atac ORELSE' resolve_tac
+ [mk_rel_funDN 1 case_prod_transfer_eq,
+ mk_rel_funDN 1 case_prod_transfer,
+ rel_funI]) THEN_ALL_NEW
+ (Subgoal.FOCUS (fn {prems, ...} =>
+ let val thm = prems
+ |> permute_like (op =) (True :: flat xss) (True :: flat_rec_arg_args xss)
+ |> Library.foldl1 (fn (acc, elem) => elem RS (acc RS rel_funD))
+ in HEADGOAL (rtac thm) end) ctxt)))))
+ (1 upto k) xsss)))
+ ns xssss 0)))
ctor_rec_transfers')
end;
@@ -240,10 +251,13 @@
val num_pgs = length pgs;
fun prem_no_of x = 1 + find_index (curry (op =) x) pgs;
- val Inl_Inr_Pair_tac = REPEAT_DETERM o
- (rtac (mk_rel_funDN 1 @{thm Inl_transfer}) ORELSE'
- rtac (mk_rel_funDN 1 @{thm Inr_transfer}) ORELSE'
- rtac (mk_rel_funDN 2 @{thm Pair_transfer}));
+ val Inl_Inr_Pair_tac = REPEAT_DETERM o (resolve_tac
+ [mk_rel_funDN 1 @{thm Inl_transfer},
+ mk_rel_funDN 1 @{thm Inl_transfer[of "op =" "op =", unfolded sum.rel_eq]},
+ mk_rel_funDN 1 @{thm Inr_transfer},
+ mk_rel_funDN 1 @{thm Inr_transfer[of "op =" "op =", unfolded sum.rel_eq]},
+ mk_rel_funDN 2 @{thm Pair_transfer},
+ mk_rel_funDN 2 @{thm Pair_transfer[of "op =" "op =", unfolded prod.rel_eq]}]);
fun mk_unfold_If_tac total pos =
HEADGOAL (Inl_Inr_Pair_tac THEN'