better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
--- a/src/HOL/Library/Quotient_List.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Library/Quotient_List.thy Mon May 13 13:59:04 2013 +0200
@@ -42,6 +42,21 @@
by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
qed
+lemma Domainp_list[relator_domain]:
+ assumes "Domainp A = P"
+ shows "Domainp (list_all2 A) = (list_all P)"
+proof -
+ {
+ fix x
+ have *: "\<And>x. (\<exists>y. A x y) = P x" using assms unfolding Domainp_iff by blast
+ have "(\<exists>y. (list_all2 A x y)) = list_all P x"
+ by (induction x) (simp_all add: * list_all2_Cons1)
+ }
+ then show ?thesis
+ unfolding Domainp_iff[abs_def]
+ by (auto iff: fun_eq_iff)
+qed
+
lemma list_reflp[reflexivity_rule]:
assumes "reflp R"
shows "reflp (list_all2 R)"
--- a/src/HOL/Library/Quotient_Option.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Mon May 13 13:59:04 2013 +0200
@@ -24,6 +24,16 @@
| _ \<Rightarrow> False)"
by (cases x) (cases y, simp_all)+
+fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
+where
+ "option_pred R None = True"
+| "option_pred R (Some x) = R x"
+
+lemma option_pred_unfold:
+ "option_pred P x = (case x of None \<Rightarrow> True
+ | Some x \<Rightarrow> P x)"
+by (cases x) simp_all
+
lemma option_rel_map1:
"option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
by (simp add: option_rel_unfold split: option.split)
@@ -55,6 +65,12 @@
"(option_rel A) OO (option_rel B) = option_rel (A OO B)"
by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
+lemma Domainp_option[relator_domain]:
+ assumes "Domainp A = P"
+ shows "Domainp (option_rel A) = (option_pred P)"
+using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
+by (auto iff: fun_eq_iff split: option.split)
+
lemma option_reflp[reflexivity_rule]:
"reflp R \<Longrightarrow> reflp (option_rel R)"
unfolding reflp_def split_option_all by simp
@@ -123,11 +139,6 @@
using assms unfolding Quotient_alt_def option_rel_unfold
by (simp split: option.split)
-fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
-where
- "option_pred R None = True"
-| "option_pred R (Some x) = R x"
-
lemma option_invariant_commute [invariant_commute]:
"option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
apply (simp add: fun_eq_iff Lifting.invariant_def)
--- a/src/HOL/Library/Quotient_Product.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Mon May 13 13:59:04 2013 +0200
@@ -15,10 +15,17 @@
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
+definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
+
lemma prod_rel_apply [simp]:
"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
by (simp add: prod_rel_def)
+lemma prod_pred_apply [simp]:
+ "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
+ by (simp add: prod_pred_def)
+
lemma map_pair_id [id_simps]:
shows "map_pair id id = id"
by (simp add: fun_eq_iff)
@@ -37,6 +44,12 @@
"(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
by (rule ext)+ (auto simp: prod_rel_def OO_def)
+lemma Domainp_prod[relator_domain]:
+ assumes "Domainp T1 = P1"
+ assumes "Domainp T2 = P2"
+ shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
+using assms unfolding prod_rel_def prod_pred_def by blast
+
lemma prod_reflp [reflexivity_rule]:
assumes "reflp R1"
assumes "reflp R2"
@@ -113,9 +126,6 @@
(map_pair Rep1 Rep2) (prod_rel T1 T2)"
using assms unfolding Quotient_alt_def by auto
-definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
-
lemma prod_invariant_commute [invariant_commute]:
"prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def)
--- a/src/HOL/Library/Quotient_Set.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Mon May 13 13:59:04 2013 +0200
@@ -40,6 +40,16 @@
apply (simp add: set_rel_def, fast)
done
+lemma Domainp_set[relator_domain]:
+ assumes "Domainp T = R"
+ shows "Domainp (set_rel T) = (\<lambda>A. Ball A R)"
+using assms unfolding set_rel_def Domainp_iff[abs_def]
+apply (intro ext)
+apply (rule iffI)
+apply blast
+apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
+done
+
lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
unfolding reflp_def set_rel_def by fast
@@ -136,13 +146,19 @@
set_rel set_rel"
unfolding fun_rel_def set_rel_def by fast
-subsubsection {* Rules requiring bi-unique or bi-total relations *}
+
+subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
lemma member_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)"
using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
+lemma right_total_Collect_transfer[transfer_rule]:
+ assumes "right_total A"
+ shows "((A ===> op =) ===> set_rel A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
+ using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast
+
lemma Collect_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> set_rel A) Collect Collect"
@@ -165,21 +181,43 @@
shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"
unfolding subset_eq [abs_def] by transfer_prover
+lemma right_total_UNIV_transfer[transfer_rule]:
+ assumes "right_total A"
+ shows "(set_rel A) (Collect (Domainp A)) UNIV"
+ using assms unfolding right_total_def set_rel_def Domainp_iff by blast
+
lemma UNIV_transfer [transfer_rule]:
assumes "bi_total A"
shows "(set_rel A) UNIV UNIV"
using assms unfolding set_rel_def bi_total_def by simp
+lemma right_total_Compl_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
+ shows "(set_rel A ===> set_rel A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus"
+ unfolding Compl_eq [abs_def]
+ by (subst Collect_conj_eq[symmetric]) transfer_prover
+
lemma Compl_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
shows "(set_rel A ===> set_rel A) uminus uminus"
unfolding Compl_eq [abs_def] by transfer_prover
+lemma right_total_Inter_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
+ shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
+ unfolding Inter_eq[abs_def]
+ by (subst Collect_conj_eq[symmetric]) transfer_prover
+
lemma Inter_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter"
unfolding Inter_eq [abs_def] by transfer_prover
+lemma filter_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter"
+ unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast
+
lemma finite_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(set_rel A ===> op =) finite finite"
--- a/src/HOL/Library/Quotient_Sum.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Mon May 13 13:59:04 2013 +0200
@@ -24,6 +24,16 @@
| _ \<Rightarrow> False)"
by (cases x) (cases y, simp_all)+
+fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+where
+ "sum_pred P1 P2 (Inl a) = P1 a"
+| "sum_pred P1 P2 (Inr a) = P2 a"
+
+lemma sum_pred_unfold:
+ "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
+ | Inr x \<Rightarrow> P2 x)"
+by (cases x) simp_all
+
lemma sum_rel_map1:
"sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
by (simp add: sum_rel_unfold split: sum.split)
@@ -56,6 +66,13 @@
"(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
+lemma Domainp_sum[relator_domain]:
+ assumes "Domainp R1 = P1"
+ assumes "Domainp R2 = P2"
+ shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
+using assms
+by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
+
lemma sum_reflp[reflexivity_rule]:
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
unfolding reflp_def split_sum_all sum_rel.simps by fast
@@ -116,21 +133,9 @@
using assms unfolding Quotient_alt_def
by (simp add: split_sum_all)
-fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
-where
- "sum_pred R1 R2 (Inl a) = R1 a"
-| "sum_pred R1 R2 (Inr a) = R2 a"
-
lemma sum_invariant_commute [invariant_commute]:
"sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
- apply (simp add: fun_eq_iff Lifting.invariant_def)
- apply (intro allI)
- apply (case_tac x rule: sum.exhaust)
- apply (case_tac xa rule: sum.exhaust)
- apply auto[2]
- apply (case_tac xa rule: sum.exhaust)
- apply auto
-done
+ by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
subsection {* Rules for quotient package *}
--- a/src/HOL/Lifting.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Lifting.thy Mon May 13 13:59:04 2013 +0200
@@ -292,22 +292,6 @@
assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
using 1 assms unfolding Quotient_def by metis
-lemma Quotient_All_transfer:
- "((T ===> op =) ===> op =) (Ball (Respects R)) All"
- unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
- by (auto, metis Quotient_abs_induct)
-
-lemma Quotient_Ex_transfer:
- "((T ===> op =) ===> op =) (Bex (Respects R)) Ex"
- unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
- by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1])
-
-lemma Quotient_forall_transfer:
- "((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall"
- using Quotient_All_transfer
- unfolding transfer_forall_def transfer_bforall_def
- Ball_def [abs_def] in_respects .
-
end
text {* Generating transfer rules for total quotients. *}
@@ -356,22 +340,6 @@
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
unfolding fun_rel_def T_def by simp
-lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All"
- unfolding T_def fun_rel_def
- by (metis type_definition.Rep [OF type]
- type_definition.Abs_inverse [OF type])
-
-lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex"
- unfolding T_def fun_rel_def
- by (metis type_definition.Rep [OF type]
- type_definition.Abs_inverse [OF type])
-
-lemma typedef_forall_transfer:
- "((T ===> op =) ===> op =)
- (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
- unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
- by (rule typedef_All_transfer)
-
end
text {* Generating the correspondence rule for a constant defined with
@@ -540,6 +508,50 @@
apply (intro choice)
by metis
+subsection {* Domains *}
+
+lemma pcr_Domainp_par_left_total:
+ assumes "Domainp B = P"
+ assumes "left_total A"
+ assumes "(A ===> op=) P' P"
+ shows "Domainp (A OO B) = P'"
+using assms
+unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def
+by (fast intro: fun_eq_iff)
+
+lemma pcr_Domainp_par:
+assumes "Domainp B = P2"
+assumes "Domainp A = P1"
+assumes "(A ===> op=) P2' P2"
+shows "Domainp (A OO B) = (inf P1 P2')"
+using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
+by (fast intro: fun_eq_iff)
+
+definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool" (infixr "OP" 75)
+where "rel_pred_comp R P \<equiv> \<lambda>x. \<exists>y. R x y \<and> P y"
+
+lemma pcr_Domainp:
+assumes "Domainp B = P"
+shows "Domainp (A OO B) = (A OP P)"
+using assms unfolding rel_pred_comp_def by blast
+
+lemma pcr_Domainp_total:
+ assumes "bi_total B"
+ assumes "Domainp A = P"
+ shows "Domainp (A OO B) = P"
+using assms unfolding bi_total_def
+by fast
+
+lemma Quotient_to_Domainp:
+ assumes "Quotient R Abs Rep T"
+ shows "Domainp T = (\<lambda>x. R x x)"
+by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
+
+lemma invariant_to_Domainp:
+ assumes "Quotient (Lifting.invariant P) Abs Rep T"
+ shows "Domainp T = P"
+by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
+
subsection {* ML setup *}
ML_file "Tools/Lifting/lifting_util.ML"
--- a/src/HOL/Rat.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Rat.thy Mon May 13 13:59:04 2013 +0200
@@ -49,13 +49,8 @@
morphisms Rep_Rat Abs_Rat
by (rule part_equivp_ratrel)
-declare rat.forall_transfer [transfer_rule del]
-
-lemma forall_rat_transfer [transfer_rule]: (* TODO: generate automatically *)
- "(fun_rel (fun_rel cr_rat op =) op =)
- (transfer_bforall (\<lambda>x. snd x \<noteq> 0)) transfer_forall"
- using rat.forall_transfer by simp
-
+lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp cr_rat = (\<lambda>x. snd x \<noteq> 0)"
+by (simp add: rat.domain)
subsubsection {* Representation and basic operations *}
@@ -1126,11 +1121,13 @@
hide_const (open) normalize positive
lemmas [transfer_rule del] =
- rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer
+ rat.rel_eq_transfer
Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
uminus_rat.transfer times_rat.transfer inverse_rat.transfer
positive.transfer of_rat.transfer rat.right_unique rat.right_total
+lemmas [transfer_domain_rule del] = Domainp_cr_rat rat.domain
+
text {* De-register @{text "rat"} as a quotient type: *}
declare Quotient_rat[quot_del]
--- a/src/HOL/Real.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Real.thy Mon May 13 13:59:04 2013 +0200
@@ -391,13 +391,8 @@
using real.rel_eq_transfer
unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
-declare real.forall_transfer [transfer_rule del]
-
-lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *)
- "(fun_rel (fun_rel pcr_real op =) op =)
- (transfer_bforall cauchy) transfer_forall"
- using real.forall_transfer
- by (simp add: realrel_def)
+lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
+by (simp add: real.domain_eq realrel_def)
instantiation real :: field_inverse_zero
begin
@@ -993,11 +988,14 @@
declare Abs_real_cases [cases del]
lemmas [transfer_rule del] =
- real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
+ real.rel_eq_transfer
zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
times_real.transfer inverse_real.transfer positive.transfer real.right_unique
real.right_total
+lemmas [transfer_domain_rule del] =
+ real.domain real.domain_eq Domainp_pcr_real real.domain_par real.domain_par_left_total
+
subsection{*More Lemmas*}
text {* BH: These lemmas should not be necessary; they should be
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon May 13 13:59:04 2013 +0200
@@ -221,6 +221,38 @@
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
end
+local
+ fun importT_inst_exclude exclude ts ctxt =
+ let
+ val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []));
+ val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt;
+ in (tvars ~~ map TFree tfrees, ctxt') end
+
+ fun import_inst_exclude exclude ts ctxt =
+ let
+ val excludeT = fold (Term.add_tvarsT o snd) exclude []
+ val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt;
+ val vars = map (apsnd (Term_Subst.instantiateT instT))
+ (rev (subtract op= exclude (fold Term.add_vars ts [])));
+ val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt';
+ val inst = vars ~~ map Free (xs ~~ map #2 vars);
+ in ((instT, inst), ctxt'') end
+
+ fun import_terms_exclude exclude ts ctxt =
+ let val (inst, ctxt') = import_inst_exclude exclude ts ctxt
+ in (map (Term_Subst.instantiate inst) ts, ctxt') end
+in
+ fun reduce_goal not_fix goal tac ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val orig_ctxt = ctxt
+ val (fixed_goal, ctxt) = yield_singleton (import_terms_exclude not_fix) goal ctxt
+ val init_goal = Goal.init (cterm_of thy fixed_goal)
+ in
+ (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
+ end
+end
+
local
val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
in
@@ -319,12 +351,80 @@
end
end
-fun parametrize_quantifier lthy quant_transfer_rule =
- Lifting_Term.parametrize_transfer_rule lthy quant_transfer_rule
+local
+ fun rewrite_first_Domainp_arg rewr_thm thm = Conv.fconv_rule (Conv.concl_conv ~1 (HOLogic.Trueprop_conv
+ (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv rewr_thm))))) thm
+
+ fun fold_Domainp_pcrel pcrel_def thm =
+ let
+ val ct = thm |> cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
+ val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
+ val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
+ handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]);
+ in
+ rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
+ end
+
+ fun reduce_Domainp ctxt rules thm =
+ let
+ val goal = thm |> prems_of |> hd
+ val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var
+ val reduced_assm = reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac rules) 1)) ctxt
+ in
+ reduced_assm RS thm
+ end
+in
+ fun parametrize_domain dom_thm (pcrel_info : Lifting_Info.pcrel_info) ctxt =
+ let
+ fun reduce_first_assm ctxt rules thm =
+ let
+ val goal = thm |> prems_of |> hd
+ val reduced_assm = reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac rules) 1)) ctxt
+ in
+ reduced_assm RS thm
+ end
+
+ val pcr_cr_met_eq = #pcr_cr_eq pcrel_info RS @{thm eq_reflection}
+ val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm
+ val pcrel_def = #pcrel_def pcrel_info
+ val pcr_Domainp_par_left_total =
+ (dom_thm RS @{thm pcr_Domainp_par_left_total})
+ |> fold_Domainp_pcrel pcrel_def
+ |> reduce_first_assm ctxt (Lifting_Info.get_reflexivity_rules ctxt)
+ val pcr_Domainp_par =
+ (dom_thm RS @{thm pcr_Domainp_par})
+ |> fold_Domainp_pcrel pcrel_def
+ |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
+ val pcr_Domainp =
+ (dom_thm RS @{thm pcr_Domainp})
+ |> fold_Domainp_pcrel pcrel_def
+ val thms =
+ [("domain", pcr_Domainp),
+ ("domain_par", pcr_Domainp_par),
+ ("domain_par_left_total", pcr_Domainp_par_left_total),
+ ("domain_eq", pcr_Domainp_eq)]
+ in
+ thms
+ end
+
+ fun parametrize_total_domain bi_total pcrel_def ctxt =
+ let
+ val thm =
+ (bi_total RS @{thm pcr_Domainp_total})
+ |> fold_Domainp_pcrel pcrel_def
+ |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
+ in
+ [("domain", thm)]
+ end
+
+end
fun get_pcrel_info ctxt qty_full_name =
#pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
+fun get_Domainp_thm quot_thm =
+ the (get_first (try(curry op RS quot_thm)) [@{thm invariant_to_Domainp}, @{thm Quotient_to_Domainp}])
+
(*
Sets up the Lifting package by a quotient theorem.
@@ -341,6 +441,7 @@
val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
(**)
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
+ val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add)
val (rty, qty) = quot_thm_rty_qty quot_thm
val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
val qty_full_name = (fst o dest_Type) qty
@@ -365,6 +466,7 @@
fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr),
[quot_thm RS thm])) thms lthy
end
+ val dom_thm = get_Domainp_thm quot_thm
fun setup_transfer_rules_nonpar lthy =
let
@@ -380,15 +482,9 @@
[[quot_thm, reflp_thm] MRSL thm])) thms lthy
end
| NONE =>
- let
- val thms =
- [("All_transfer", @{thm Quotient_All_transfer} ),
- ("Ex_transfer", @{thm Quotient_Ex_transfer} ),
- ("forall_transfer",@{thm Quotient_forall_transfer})]
- in
- fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
- [quot_thm RS thm])) thms lthy
- end
+ lthy
+ |> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm])
+
val thms =
[("rel_eq_transfer", @{thm Quotient_rel_eq_transfer}),
("right_unique", @{thm Quotient_right_unique} ),
@@ -412,33 +508,36 @@
fun setup_transfer_rules_par lthy =
let
- val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+ val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
+ val pcrel_def = #pcrel_def pcrel_info
val lthy =
case opt_reflp_thm of
SOME reflp_thm =>
let
+ val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+ val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
val id_abs_transfer = generate_parametric_id lthy rty
(Lifting_Term.parametrize_transfer_rule lthy
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
- val bi_total = parametrize_class_constraint lthy pcrel_def
- ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+ val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
val thms =
[("id_abs_transfer",id_abs_transfer),
("bi_total", bi_total )]
in
- fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
- [thm])) thms lthy
+ lthy
+ |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms
+ |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
+ [thm])) domain_thms
end
| NONE =>
let
- val thms =
- [("All_transfer", @{thm Quotient_All_transfer} ),
- ("Ex_transfer", @{thm Quotient_Ex_transfer} ),
- ("forall_transfer",@{thm Quotient_forall_transfer})]
+ val thms = parametrize_domain dom_thm pcrel_info lthy
in
- fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
- [parametrize_quantifier lthy (quot_thm RS thm)])) thms lthy
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
+ [thm])) thms lthy
end
+
val rel_eq_transfer = generate_parametric_rel_eq lthy
(Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
opt_par_thm
@@ -475,6 +574,7 @@
fun setup_by_typedef_thm gen_code typedef_thm lthy =
let
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
+ val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add)
val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
val (T_def, lthy) = define_crel rep_fun lthy
(**)
@@ -497,6 +597,7 @@
Const ("Orderings.top_class.top", _) =>
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
| _ => NONE
+ val dom_thm = get_Domainp_thm quot_thm
fun setup_transfer_rules_nonpar lthy =
let
@@ -512,17 +613,8 @@
[[quot_thm, reflp_thm] MRSL thm])) thms lthy
end
| NONE =>
- let
- val thms =
- [("All_transfer", @{thm typedef_All_transfer} ),
- ("Ex_transfer", @{thm typedef_Ex_transfer} )]
- in
- lthy
- |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
- [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
- |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
- [[typedef_thm, T_def] MRSL thm])) thms
- end
+ lthy
+ |> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm])
val thms =
[("rep_transfer", @{thm typedef_rep_transfer}),
("bi_unique", @{thm typedef_bi_unique} ),
@@ -535,35 +627,37 @@
fun setup_transfer_rules_par lthy =
let
- val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+ val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
+ val pcrel_def = #pcrel_def pcrel_info
+
val lthy =
case opt_reflp_thm of
SOME reflp_thm =>
let
+ val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+ val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
+ val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
val id_abs_transfer = generate_parametric_id lthy rty
(Lifting_Term.parametrize_transfer_rule lthy
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
- val bi_total = parametrize_class_constraint lthy pcrel_def
- ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
val thms =
- [("id_abs_transfer",id_abs_transfer),
- ("bi_total", bi_total )]
+ [("bi_total", bi_total ),
+ ("id_abs_transfer",id_abs_transfer)]
in
- fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
- [thm])) thms lthy
+ lthy
+ |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms
+ |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
+ [thm])) domain_thms
end
| NONE =>
let
- val thms =
- ("forall_transfer", simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}))
- ::
- (map_snd (fn thm => [typedef_thm, T_def] MRSL thm)
- [("All_transfer", @{thm typedef_All_transfer}),
- ("Ex_transfer", @{thm typedef_Ex_transfer} )])
+ val thms = parametrize_domain dom_thm pcrel_info lthy
in
- fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
- [parametrize_quantifier lthy thm])) thms lthy
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
+ [thm])) thms lthy
end
+
val thms =
("rep_transfer", generate_parametric_id lthy rty
(Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer})))
--- a/src/HOL/Tools/transfer.ML Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Tools/transfer.ML Mon May 13 13:59:04 2013 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/transfer.ML
Author: Brian Huffman, TU Muenchen
+ Author: Ondrej Kuncar, TU Muenchen
Generic theorem transfer method.
*)
@@ -7,12 +8,15 @@
signature TRANSFER =
sig
val prep_conv: conv
+ val get_transfer_raw: Proof.context -> thm list
val get_relator_eq: Proof.context -> thm list
val get_sym_relator_eq: Proof.context -> thm list
val get_relator_eq_raw: Proof.context -> thm list
- val get_transfer_raw: Proof.context -> thm list
+ val get_relator_domain: Proof.context -> thm list
val transfer_add: attribute
val transfer_del: attribute
+ val transfer_domain_add: attribute
+ val transfer_domain_del: attribute
val transfer_rule_of_term: Proof.context -> term -> thm
val transfer_tac: bool -> Proof.context -> int -> tactic
val transfer_prover_tac: Proof.context -> int -> tactic
@@ -31,28 +35,40 @@
known_frees : (string * typ) list,
compound_rhs : unit Net.net,
relator_eq : thm Item_Net.T,
- relator_eq_raw : thm Item_Net.T }
+ relator_eq_raw : thm Item_Net.T,
+ relator_domain : thm Item_Net.T }
val empty =
{ transfer_raw = Thm.full_rules,
known_frees = [],
compound_rhs = Net.empty,
relator_eq = Thm.full_rules,
- relator_eq_raw = Thm.full_rules }
+ relator_eq_raw = Thm.full_rules,
+ relator_domain = Thm.full_rules }
val extend = I
fun merge
( { transfer_raw = t1, known_frees = k1,
compound_rhs = c1, relator_eq = r1,
- relator_eq_raw = rw1 },
+ relator_eq_raw = rw1, relator_domain = rd1 },
{ transfer_raw = t2, known_frees = k2,
compound_rhs = c2, relator_eq = r2,
- relator_eq_raw = rw2 } ) =
+ relator_eq_raw = rw2, relator_domain = rd2 } ) =
{ transfer_raw = Item_Net.merge (t1, t2),
known_frees = Library.merge (op =) (k1, k2),
compound_rhs = Net.merge (K true) (c1, c2),
relator_eq = Item_Net.merge (r1, r2),
- relator_eq_raw = Item_Net.merge (rw1, rw2) }
+ relator_eq_raw = Item_Net.merge (rw1, rw2),
+ relator_domain = Item_Net.merge (rd1, rd2) }
)
+fun get_transfer_raw ctxt = ctxt
+ |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
+
+fun get_known_frees ctxt = ctxt
+ |> (#known_frees o Data.get o Context.Proof)
+
+fun get_compound_rhs ctxt = ctxt
+ |> (#compound_rhs o Data.get o Context.Proof)
+
fun get_relator_eq ctxt = ctxt
|> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
|> map safe_mk_meta_eq
@@ -64,34 +80,30 @@
fun get_relator_eq_raw ctxt = ctxt
|> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
-fun get_transfer_raw ctxt = ctxt
- |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
-
-fun get_known_frees ctxt = ctxt
- |> (#known_frees o Data.get o Context.Proof)
+fun get_relator_domain ctxt = ctxt
+ |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
-fun get_compound_rhs ctxt = ctxt
- |> (#compound_rhs o Data.get o Context.Proof)
-
-fun map_data f1 f2 f3 f4 f5
- { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw } =
+fun map_data f1 f2 f3 f4 f5 f6
+ { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw, relator_domain } =
{ transfer_raw = f1 transfer_raw,
known_frees = f2 known_frees,
compound_rhs = f3 compound_rhs,
relator_eq = f4 relator_eq,
- relator_eq_raw = f5 relator_eq_raw }
+ relator_eq_raw = f5 relator_eq_raw,
+ relator_domain = f6 relator_domain }
-fun map_transfer_raw f = map_data f I I I I
-fun map_known_frees f = map_data I f I I I
-fun map_compound_rhs f = map_data I I f I I
-fun map_relator_eq f = map_data I I I f I
-fun map_relator_eq_raw f = map_data I I I I f
+fun map_transfer_raw f = map_data f I I I I I
+fun map_known_frees f = map_data I f I I I I
+fun map_compound_rhs f = map_data I I f I I I
+fun map_relator_eq f = map_data I I I f I I
+fun map_relator_eq_raw f = map_data I I I I f I
+fun map_relator_domain f = map_data I I I I I f
fun add_transfer_thm thm = Data.map
(map_transfer_raw (Item_Net.update thm) o
map_compound_rhs
(case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
+ (Const (@{const_name Rel}, _)) $ _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
| _ => I) o
map_known_frees (Term.add_frees (Thm.concl_of thm)))
@@ -111,20 +123,8 @@
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
(* Conversion to preprocess a transfer rule *)
-fun strip_args n = funpow n (fst o dest_comb)
-
fun safe_Rel_conv ct =
- let
- val head = ct |> term_of |> HOLogic.dest_Trueprop |> strip_args 2
- fun is_known (Const (s, _)) = (s = @{const_name DOM})
- | is_known _ = false
- in
- if not (is_known head)
- then HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) ct
- else Conv.all_conv ct
- end
- handle TERM _ => Conv.all_conv ct
-;
+ Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
fun prep_conv ct = (
Conv.implies_conv safe_Rel_conv prep_conv
@@ -185,6 +185,112 @@
gen_abstract_equalities (fn x => (x, I))
(rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
+fun abstract_equalities_domain thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((dom, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (x $ y, fn comb' =>
+ let
+ val (x', y') = dest_comb comb'
+ in
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y'))
+ end)
+ end
+ in
+ gen_abstract_equalities dest thm
+ end
+
+
+(** Replacing explicit Domainp predicates with Domainp assumptions **)
+
+fun mk_Domainp_assm (T, R) =
+ HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
+
+val Domainp_lemma =
+ @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
+ by (rule, drule meta_spec,
+ erule meta_mp, rule refl, simp)}
+
+fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
+ | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
+ | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
+ | fold_Domainp _ _ = I
+
+fun subst_terms tab t =
+ let
+ val t' = Termtab.lookup tab t
+ in
+ case t' of
+ SOME t' => t'
+ | NONE =>
+ (case t of
+ u $ v => (subst_terms tab u) $ (subst_terms tab v)
+ | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
+ | t => t)
+ end
+
+fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
+ let
+ val thy = Thm.theory_of_thm thm
+ val prop = Thm.prop_of thm
+ val (t, mk_prop') = dest prop
+ val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
+ val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
+ val used = Term.add_free_names t []
+ val rels = map (snd o dest_comb) Domainp_tms
+ val rel_names = map (fst o fst o dest_Var) rels
+ val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
+ val frees = map Free (names ~~ Domainp_Ts)
+ val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
+ val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
+ val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
+ val prop2 = Logic.list_rename_params (rev names) prop1
+ val cprop = Thm.cterm_of thy prop2
+ val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
+ fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
+ in
+ forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
+ end
+ handle TERM _ => thm
+
+fun abstract_domains_transfer thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (x, fn x' =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
+ end
+ in
+ gen_abstract_domains dest thm
+ end
+
+fun detect_transfer_rules thm =
+ let
+ fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
+ (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
+ | _ $ _ $ _ => true
+ | _ => false
+ fun safe_transfer_rule_conv ctm =
+ if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
+ in
+ Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
+ end
+
+(** Adding transfer domain rules **)
+
+fun add_transfer_domain_thm thm =
+ (add_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
+
+fun del_transfer_domain_thm thm =
+ (del_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
(** Transfer proof method **)
@@ -363,7 +469,7 @@
(* Attribute for transfer rules *)
-val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv
+val prep_rule = abstract_domains_transfer o abstract_equalities_transfer o Conv.fconv_rule prep_conv
val transfer_add =
Thm.declaration_attribute (add_transfer_thm o prep_rule)
@@ -374,6 +480,15 @@
val transfer_attribute =
Attrib.add_del transfer_add transfer_del
+(* Attributes for transfer domain rules *)
+
+val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
+
+val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
+
+val transfer_domain_attribute =
+ Attrib.add_del transfer_domain_add transfer_domain_del
+
(* Theory setup *)
val relator_eq_setup =
@@ -392,12 +507,32 @@
#> Global_Theory.add_thms_dynamic (name, content)
end
+val relator_domain_setup =
+ let
+ val name = @{binding relator_domain}
+ fun add_thm thm = Data.map (map_relator_domain (Item_Net.update thm))
+ #> add_transfer_domain_thm thm
+ fun del_thm thm = Data.map (map_relator_domain (Item_Net.remove thm))
+ #> del_transfer_domain_thm thm
+ val add = Thm.declaration_attribute add_thm
+ val del = Thm.declaration_attribute del_thm
+ val text = "declaration of relator domain rule (used by transfer method)"
+ val content = Item_Net.content o #relator_domain o Data.get
+ in
+ Attrib.setup name (Attrib.add_del add del) text
+ #> Global_Theory.add_thms_dynamic (name, content)
+ end
+
+
val setup =
relator_eq_setup
+ #> relator_domain_setup
#> Attrib.setup @{binding transfer_rule} transfer_attribute
"transfer rule for transfer method"
#> Global_Theory.add_thms_dynamic
(@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
+ #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
+ "transfer domain rule for transfer method"
#> Global_Theory.add_thms_dynamic
(@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
#> Method.setup @{binding transfer} (transfer_method true)
--- a/src/HOL/Transfer.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Transfer.thy Mon May 13 13:59:04 2013 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Transfer.thy
Author: Brian Huffman, TU Muenchen
+ Author: Ondrej Kuncar, TU Muenchen
*)
header {* Generic theorem transfer using relations *}
@@ -103,10 +104,6 @@
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
using assms unfolding Rel_def fun_rel_def by fast
-text {* Handling of domains *}
-
-definition DOM :: "('a => 'b => bool) => ('a => bool) => bool" where "DOM T R \<equiv> Domainp T = R"
-
ML_file "Tools/transfer.ML"
setup Transfer.setup
@@ -116,6 +113,10 @@
hide_const (open) Rel
+text {* Handling of domains *}
+
+lemma Domaimp_refl[transfer_domain_rule]:
+ "Domainp T = Domainp T" ..
subsection {* Predicates on relations, i.e. ``class constraints'' *}
@@ -264,6 +265,21 @@
shows "(A ===> A ===> op =) (op =) (op =)"
using assms unfolding bi_unique_def fun_rel_def by auto
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+ by auto
+
+lemma right_total_Ex_transfer[transfer_rule]:
+ assumes "right_total A"
+ shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
+using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def]
+by blast
+
+lemma right_total_All_transfer[transfer_rule]:
+ assumes "right_total A"
+ shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
+using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def]
+by blast
+
lemma All_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> op =) All All"
@@ -304,13 +320,6 @@
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
unfolding funpow_def by transfer_prover
-text {* Fallback rule for transferring universal quantifiers over
- correspondence relations that are not bi-total, and do not have
- custom transfer rules (e.g. relations between function types). *}
-
-lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
- by auto
-
lemma Domainp_forall_transfer [transfer_rule]:
assumes "right_total A"
shows "((A ===> op =) ===> op =)
@@ -319,9 +328,6 @@
unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
by metis
-text {* Preferred rule for transferring universal quantifiers over
- bi-total correspondence relations (later rules are tried first). *}
-
lemma forall_transfer [transfer_rule]:
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
unfolding transfer_forall_def by (rule All_transfer)
--- a/src/HOL/ex/Transfer_Int_Nat.thy Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Mon May 13 13:59:04 2013 +0200
@@ -13,6 +13,11 @@
definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool"
where "ZN = (\<lambda>z n. z = of_nat n)"
+subsection {* Transfer domain rules *}
+
+lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)"
+ unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int)
+
subsection {* Transfer rules *}
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
@@ -155,11 +160,11 @@
apply fact
done
-text {* Quantifiers over higher types (e.g. @{text "nat list"}) may
- generate @{text "Domainp"} assumptions when transferred. *}
+text {* Quantifiers over higher types (e.g. @{text "nat list"}) are
+ transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN} *}
lemma
- assumes "\<And>xs::int list. Domainp (list_all2 ZN) xs \<Longrightarrow>
+ assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
(listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
apply transfer
@@ -170,7 +175,7 @@
involved are bi-unique. *}
lemma
- assumes "\<And>xs\<Colon>int list. \<lbrakk>Domainp (list_all2 ZN) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
+ assumes "\<And>xs\<Colon>int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
apply transfer