# HG changeset patch # User kuncar # Date 1368446344 -7200 # Node ID a4d81cdebf8b427f65b2bb9f252389139a008dea # Parent 04d9381bebffce715d8adeb02efb970b7194c179 better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Library/Quotient_List.thy --- 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 *: "\x. (\y. A x y) = P x" using assms unfolding Domainp_iff by blast + have "(\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)" diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Library/Quotient_Option.thy --- 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 @@ | _ \ False)" by (cases x) (cases y, simp_all)+ +fun option_pred :: "('a \ bool) \ 'a option \ 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 \ True + | Some x \ P x)" +by (cases x) simp_all + lemma option_rel_map1: "option_rel R (Option.map f x) y \ option_rel (\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 \ 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 \ bool) \ 'a option \ 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) diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Library/Quotient_Product.thy --- 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 = (\(a, b) (c, d). R1 a c \ R2 b d)" +definition prod_pred :: "('a \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" +where "prod_pred R1 R2 = (\(a, b). R1 a \ R2 b)" + lemma prod_rel_apply [simp]: "prod_rel R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" by (simp add: prod_rel_def) +lemma prod_pred_apply [simp]: + "prod_pred P1 P2 (a, b) \ P1 a \ 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 \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" -where "prod_pred R1 R2 = (\(a, b). R1 a \ 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) diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Library/Quotient_Set.thy --- 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) = (\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. \x\A. T x y}" in exI, fast) +done + lemma reflp_set_rel[reflexivity_rule]: "reflp R \ 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 \) (op \)" 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) (\P. Collect (\x. P x \ 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 \) (op \)" 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) (\S. uminus S \ 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) (\S. Inter S \ 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" diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Library/Quotient_Sum.thy --- 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 @@ | _ \ False)" by (cases x) (cases y, simp_all)+ +fun sum_pred :: "('a \ bool) \ ('b \ bool) \ 'a + 'b \ 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 \ P1 x + | Inr x \ P2 x)" +by (cases x) simp_all + lemma sum_rel_map1: "sum_rel R1 R2 (sum_map f1 f2 x) y \ sum_rel (\x. R1 (f1 x)) (\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 \ reflp R2 \ 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 \ bool) \ ('b \ bool) \ 'a + 'b \ 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 *} diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Lifting.thy --- 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 "\y. R y y \ 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 (\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 =) (\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 (\x. x \ 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 \ \x. \y. R x y \ 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 = (\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" diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Rat.thy --- 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 (\x. snd x \ 0)) transfer_forall" - using rat.forall_transfer by simp - +lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp cr_rat = (\x. snd x \ 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] diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Real.thy --- 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 diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Tools/Lifting/lifting_setup.ML --- 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}))) diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Tools/transfer.ML --- 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) diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/Transfer.thy --- 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) (\x. f x) (\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 \ 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 \ (\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 \ (\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 \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" unfolding transfer_forall_def by (rule All_transfer) diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/ex/Transfer_Int_Nat.thy --- 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 \ nat \ bool" where "ZN = (\z n. z = of_nat n)" +subsection {* Transfer domain rules *} + +lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\x. x \ 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 "\xs::int list. Domainp (list_all2 ZN) xs \ + assumes "\xs::int list. list_all (\x. x \ 0) xs \ (listsum xs = 0) = list_all (\x. x = 0) xs" shows "listsum xs = (0::nat) \ list_all (\x. x = 0) xs" apply transfer @@ -170,7 +175,7 @@ involved are bi-unique. *} lemma - assumes "\xs\int list. \Domainp (list_all2 ZN) xs; xs \ []\ \ + assumes "\xs\int list. \list_all (\x. x \ 0) xs; xs \ []\ \ listsum xs < listsum (map (\x. x + 1) xs)" shows "xs \ [] \ listsum xs < listsum (map Suc xs)" apply transfer