--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 23:27:09 2013 +0200
@@ -252,16 +252,20 @@
(case ctr_sugar_of ctxt s of
SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
if case_name = c then
- let
- val n = length discs0;
- val (branches, obj :: leftovers) = chop n args;
- val discs = map (mk_disc_or_sel Ts) discs0;
- val selss = map (map (mk_disc_or_sel Ts)) selss0;
- val conds = map (rapp obj) discs;
- val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
- val branches' = map2 (curry Term.betapplys) branches branch_argss;
- in
- SOME (conds, branches')
+ let val n = length discs0 in
+ if n < length args then
+ let
+ val (branches, obj :: leftovers) = chop n args;
+ val discs = map (mk_disc_or_sel Ts) discs0;
+ val selss = map (map (mk_disc_or_sel Ts)) selss0;
+ val conds = map (rapp obj) discs;
+ val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
+ val branches' = map2 (curry Term.betapplys) branches branch_argss;
+ in
+ SOME (conds, branches')
+ end
+ else
+ NONE
end
else
NONE
@@ -310,12 +314,10 @@
val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
- fun can_definitely_rely_on_disc k =
- not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
+ fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
fun can_rely_on_disc k =
can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
- fun should_omit_disc_binding k =
- n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
+ fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
fun is_disc_binding_valid b =
not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
@@ -384,10 +386,9 @@
fun mk_case_disj xctr xf xs =
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf)));
- val case_rhs =
- fold_rev (fold_rev Term.lambda) [fs, [u]]
- (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
- Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
+ val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
+ (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
+ Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
|> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs))
@@ -811,7 +812,7 @@
|> Thm.close_derivation
end;
- val expand_thms =
+ val expand_thm =
let
fun mk_prems k udisc usels vdisc vsels =
(if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
@@ -829,12 +830,12 @@
val uncollapse_thms =
map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
in
- [Goal.prove_sorry lthy [] [] goal (fn _ =>
- mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
- (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
- disc_exclude_thmsss')]
- |> map Thm.close_derivation
- |> Proof_Context.export names_lthy lthy
+ Goal.prove_sorry lthy [] [] goal (fn _ =>
+ mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
+ (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
+ disc_exclude_thmsss')
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val (sel_split_thm, sel_split_asm_thm) =
@@ -849,20 +850,20 @@
(thm, asm_thm)
end;
- val case_conv_if_thms =
+ val case_conv_if_thm =
let
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
in
- [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
- |> map Thm.close_derivation
- |> Proof_Context.export names_lthy lthy
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
in
(all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
- all_collapse_thms, safe_collapse_thms, expand_thms, [sel_split_thm],
- [sel_split_asm_thm], case_conv_if_thms)
+ all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
+ [sel_split_asm_thm], [case_conv_if_thm])
end;
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 23:27:09 2013 +0200
@@ -65,8 +65,8 @@
val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
fun mk_sel_exhaust_tac n disc_exhaust collapses =
- if n = 1 then HEADGOAL (etac meta_mp THEN' resolve_tac collapses)
- else mk_disc_or_sel_exhaust_tac n disc_exhaust collapses;
+ mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
+ HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
fun mk_collapse_tac ctxt m discD sels =
HEADGOAL (dtac discD THEN'
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 26 23:27:09 2013 +0200
@@ -734,7 +734,7 @@
val (defs, exclss') =
co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
- fun prove_excl_tac (c, c', a) =
+ fun excl_tac (c, c', a) =
if a orelse c = c' orelse sequential then SOME (K (mk_primcorec_assumption_tac lthy []))
else if simple then SOME (K (auto_tac lthy))
else NONE;
@@ -745,7 +745,7 @@
*)
val exclss'' = exclss' |> map (map (fn (idx, t) =>
- (idx, (Option.map (Goal.prove lthy [] [] t) (prove_excl_tac idx), t))));
+ (idx, (Option.map (Goal.prove lthy [] [] t) (excl_tac idx), t))));
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))
@@ -800,7 +800,7 @@
|> HOLogic.mk_Trueprop o HOLogic.mk_eq
|> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
|> curry Logic.list_all (map dest_Free fun_args);
- val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
+ val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
in
mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
nested_map_idents nested_map_comps sel_corec k m exclsss
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Sep 26 23:27:09 2013 +0200
@@ -9,8 +9,8 @@
sig
val mk_primcorec_assumption_tac: Proof.context -> thm list -> tactic
val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
- thm list -> int list -> thm list -> tactic
- val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> thm list -> tactic
+ int list -> thm list -> tactic
+ val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> tactic
val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
tactic
@@ -40,16 +40,18 @@
fun mk_primcorec_assumption_tac ctxt discIs =
HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt
@{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
- SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE'
+ SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
- dresolve_tac discIs THEN' atac)))));
+ dresolve_tac discIs THEN' atac ORELSE'
+ etac notE THEN' atac ORELSE'
+ etac disjE)))));
fun mk_primcorec_same_case_tac m =
HEADGOAL (if m = 0 then rtac TrueI
else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
fun mk_primcorec_different_case_tac ctxt excl =
- unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN
+ unfold_thms_tac ctxt @{thms not_not not_False_eq_True not_True_eq_False} THEN
HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_assumption_tac ctxt []));
fun mk_primcorec_cases_tac ctxt k m exclsss =
@@ -83,33 +85,32 @@
(the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
-(* TODO: do we need "collapses"? *)
(* TODO: reduce code duplication with selector tactic above *)
-fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
+fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN
- HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o
+ HEADGOAL (SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
- eresolve_tac (falseEs @ map (fn thm => thm RS trans) collapses) ORELSE'
resolve_tac split_connectI ORELSE'
Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
Splitter.split_tac (split_if :: splits) ORELSE'
+ K (mk_primcorec_assumption_tac ctxt discIs) ORELSE'
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
- (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))));
+ (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))));
-fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs collapses splits split_asms ms ctr_thms =
- EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits
- split_asms) ms ctr_thms);
+fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms =
+ EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
+ ms ctr_thms);
-fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses =
+fun mk_primcorec_code_of_raw_tac splits disc_excludes raw =
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o
(rtac refl ORELSE'
(TRY o rtac sym) THEN' atac ORELSE'
resolve_tac split_connectI ORELSE'
Splitter.split_tac (split_if :: splits) ORELSE'
etac notE THEN' atac ORELSE'
- dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE'
- eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
+ (TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac));
+
end;
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 26 23:27:09 2013 +0200
@@ -70,7 +70,7 @@
val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
typ list -> term -> 'a -> 'a
val case_thms_of_term: Proof.context -> typ list -> term ->
- thm list * thm list * thm list * thm list * thm list
+ thm list * thm list * thm list * thm list
val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
((term * term list list) list) list -> local_theory ->
@@ -234,7 +234,7 @@
o fld (conds @ s_not_disj cond) else_branch
| (Const (c, _), args as _ :: _ :: _) =>
let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
- if length args > n then
+ if n >= 0 andalso n < length args then
(case fastype_of1 (bound_Ts, nth args n) of
Type (s, Ts) =>
(case dest_case ctxt s Ts t of
@@ -276,7 +276,7 @@
val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
val n = length gen_branch_Ts;
in
- if length args > n then
+ if n < length args then
(case gen_body_fun_T of
Type (_, [Type (T_name, _), _]) =>
if case_of ctxt T_name = SOME c then
@@ -397,8 +397,8 @@
val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
in
- (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
- maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
+ (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
+ maps #sel_split_asms ctr_sugars)
end;
fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
--- a/src/HOL/Fun.thy Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/Fun.thy Thu Sep 26 23:27:09 2013 +0200
@@ -491,8 +491,11 @@
apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
done
+lemma inj_on_image_eq_iff: "\<lbrakk> inj_on f C; A \<subseteq> C; B \<subseteq> C \<rbrakk> \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
+by(fastforce simp add: inj_on_def)
+
lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
-by(blast dest: inj_onD)
+by(erule inj_on_image_eq_iff) simp_all
lemma inj_on_image_Int:
"[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B"
--- a/src/HOL/Library/Product_Vector.thy Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/Library/Product_Vector.thy Thu Sep 26 23:27:09 2013 +0200
@@ -231,12 +231,7 @@
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
by (simp add: prod_eq_iff)
thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
- apply (rule disjE)
- apply (drule t0_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
- apply (simp add: open_Times mem_Times_iff)
- apply (drule t0_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
- apply (simp add: open_Times mem_Times_iff)
- done
+ by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
qed
instance prod :: (t1_space, t1_space) t1_space
@@ -245,12 +240,7 @@
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
by (simp add: prod_eq_iff)
thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
- apply (rule disjE)
- apply (drule t1_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
- apply (simp add: open_Times mem_Times_iff)
- apply (drule t1_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
- apply (simp add: open_Times mem_Times_iff)
- done
+ by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
qed
instance prod :: (t2_space, t2_space) t2_space
@@ -259,14 +249,7 @@
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
by (simp add: prod_eq_iff)
thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
- apply (rule disjE)
- apply (drule hausdorff, clarify)
- apply (rule_tac x="U \<times> UNIV" in exI, rule_tac x="V \<times> UNIV" in exI)
- apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
- apply (drule hausdorff, clarify)
- apply (rule_tac x="UNIV \<times> U" in exI, rule_tac x="UNIV \<times> V" in exI)
- apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
- done
+ by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
qed
subsection {* Product is a metric space *}
@@ -281,10 +264,10 @@
unfolding dist_prod_def by simp
lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
-unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
+ unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
-unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
+ unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
instance proof
fix x y :: "'a \<times> 'b"
@@ -362,10 +345,10 @@
end
lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
-unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
+ unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
-unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
+ unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
lemma Cauchy_Pair:
assumes "Cauchy X" and "Cauchy Y"
--- a/src/HOL/Lifting.thy Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/Lifting.thy Thu Sep 26 23:27:09 2013 +0200
@@ -38,9 +38,21 @@
obtains "(\<And>x. \<exists>y. R x y)"
using assms unfolding left_total_def by blast
+lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
+by(simp add: left_total_def right_total_def bi_total_def)
+
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
+by(auto simp add: left_unique_def right_unique_def bi_unique_def)
+
+lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
+unfolding left_unique_def by blast
+
+lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
+unfolding left_unique_def by blast
+
lemma left_total_fun:
"\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
unfolding left_total_def fun_rel_def
--- a/src/HOL/Lifting_Set.thy Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/Lifting_Set.thy Thu Sep 26 23:27:09 2013 +0200
@@ -19,6 +19,10 @@
shows "set_rel R A B"
using assms unfolding set_rel_def by simp
+lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
+ and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
+by(simp_all add: set_rel_def)
+
lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
unfolding set_rel_def by auto
@@ -153,6 +157,15 @@
set_rel set_rel"
unfolding fun_rel_def set_rel_def by fast
+lemma SUPR_parametric [transfer_rule]:
+ "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
+proof(rule fun_relI)+
+ fix A B f and g :: "'b \<Rightarrow> 'c"
+ assume AB: "set_rel R A B"
+ and fg: "(R ===> op =) f g"
+ show "SUPR A f = SUPR B g"
+ by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
+qed
subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
@@ -268,6 +281,47 @@
"bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
+lemma vimage_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_unique B"
+ shows "((A ===> B) ===> set_rel B ===> set_rel A) vimage vimage"
+unfolding vimage_def[abs_def] by transfer_prover
+
+lemma setsum_parametric [transfer_rule]:
+ assumes "bi_unique A"
+ shows "((A ===> op =) ===> set_rel A ===> op =) setsum setsum"
+proof(rule fun_relI)+
+ fix f :: "'a \<Rightarrow> 'c" and g S T
+ assume fg: "(A ===> op =) f g"
+ and ST: "set_rel A S T"
+ show "setsum f S = setsum g T"
+ proof(rule setsum_reindex_cong)
+ let ?f = "\<lambda>t. THE s. A s t"
+ show "S = ?f ` T"
+ by(blast dest: set_relD1[OF ST] set_relD2[OF ST] bi_uniqueDl[OF assms]
+ intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
+
+ show "inj_on ?f T"
+ proof(rule inj_onI)
+ fix t1 t2
+ assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
+ from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: set_relD2)
+ hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
+ moreover
+ from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: set_relD2)
+ hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
+ ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
+ with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
+ qed
+
+ fix t
+ assume "t \<in> T"
+ with ST obtain s where "A s t" "s \<in> S" by(auto dest: set_relD2)
+ hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
+ moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
+ ultimately show "g t = f (?f t)" by simp
+ qed
+qed
+
end
end
--- a/src/HOL/Transfer.thy Thu Sep 26 23:26:51 2013 +0200
+++ b/src/HOL/Transfer.thy Thu Sep 26 23:27:09 2013 +0200
@@ -158,6 +158,18 @@
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
+by(simp add: bi_unique_def)
+
+lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
+by(simp add: bi_unique_def)
+
+lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
+unfolding right_unique_def by blast
+
+lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
+unfolding right_unique_def by blast
+
lemma right_total_alt_def:
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
unfolding right_total_def fun_rel_def