# HG changeset patch # User kuncar # Date 1397144895 -7200 # Node ID c1048f5bbb4566310d4896fd9d8062bce041f3d5 # Parent beb3b685166588d5836ebd548142892ae0eb3a10 more appropriate name (Lifting.invariant -> eq_onp) diff -r beb3b6851665 -r c1048f5bbb45 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Apr 10 17:48:15 2014 +0200 @@ -1596,7 +1596,7 @@ @{command_def (HOL) "print_quot_maps"} & : & @{text "context \"}\\ @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\ - @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\ + @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\ @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\ @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\ @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\ @@ -1733,11 +1733,11 @@ "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files in the same directory. - \item @{attribute (HOL) invariant_commute} registers a theorem that + \item @{attribute (HOL) relator_eq_onp} registers a theorem that shows a relationship between the constant @{text - Lifting.invariant} (used for internal encoding of proper subtypes) + eq_onp} (used for internal encoding of proper subtypes) and a relator. Such theorems allows the package to hide @{text - Lifting.invariant} from a user in a user-readable form of a + eq_onp} from a user in a user-readable form of a respectfulness theorem. For examples see @{file "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory. diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:15 2014 +0200 @@ -853,7 +853,7 @@ lemma bi_total_rel_fset[transfer_rule]: "bi_total A \ bi_total (rel_fset A)" by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff) -lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred] +lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred] subsubsection {* Quotient theorem for the Lifting package *} diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Library/RBT_Set.thy Thu Apr 10 17:48:15 2014 +0200 @@ -640,7 +640,7 @@ proof - have *: "\t. RBT.impl_of t = rbt.Empty \ t = RBT rbt.Empty" by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject) - have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp + have **: "eq_onp is_rbt rbt.Empty rbt.Empty" unfolding eq_onp_def by simp show ?thesis by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split) qed @@ -672,7 +672,7 @@ fix x :: "'a :: linorder" let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" have *:"?t \ {t. is_rbt t}" unfolding is_rbt_def by auto - then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto + then have **:"eq_onp is_rbt ?t ?t" unfolding eq_onp_def by auto have "RBT.impl_of t = ?t \ the_elem (Set t) = x" by (subst(asm) RBT_inverse[symmetric, OF *]) diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Lifting.thy Thu Apr 10 17:48:15 2014 +0200 @@ -212,29 +212,29 @@ subsection {* Invariant *} -definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" - where "invariant R = (\x y. R x \ x = y)" +definition eq_onp :: "('a \ bool) \ 'a \ 'a \ bool" + where "eq_onp R = (\x y. R x \ x = y)" -lemma invariant_to_eq: - assumes "invariant P x y" +lemma eq_onp_to_eq: + assumes "eq_onp P x y" shows "x = y" -using assms by (simp add: invariant_def) +using assms by (simp add: eq_onp_def) -lemma rel_fun_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\f. \x. P(f x))" -unfolding invariant_def rel_fun_def by auto +lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\f. \x. P(f x))" +unfolding eq_onp_def rel_fun_def by auto -lemma rel_fun_invariant_rel: - shows "((invariant R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" -by (auto simp add: invariant_def rel_fun_def) +lemma rel_fun_eq_onp_rel: + shows "((eq_onp R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" +by (auto simp add: eq_onp_def rel_fun_def) -lemma invariant_same_args: - shows "invariant P x x \ P x" -using assms by (auto simp add: invariant_def) +lemma eq_onp_same_args: + shows "eq_onp P x x \ P x" +using assms by (auto simp add: eq_onp_def) -lemma invariant_transfer [transfer_rule]: +lemma eq_onp_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique A" - shows "((A ===> op=) ===> A ===> A ===> op=) Lifting.invariant Lifting.invariant" -unfolding invariant_def[abs_def] by transfer_prover + shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp" +unfolding eq_onp_def[abs_def] by transfer_prover lemma UNIV_typedef_to_Quotient: assumes "type_definition Rep Abs UNIV" @@ -256,34 +256,34 @@ lemma typedef_to_Quotient: assumes "type_definition Rep Abs S" and T_def: "T \ (\x y. x = Rep y)" - shows "Quotient (invariant (\x. x \ S)) Abs Rep T" + shows "Quotient (eq_onp (\x. x \ S)) Abs Rep T" proof - interpret type_definition Rep Abs S by fact from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis - by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) + by (auto intro!: QuotientI simp: eq_onp_def fun_eq_iff) qed lemma typedef_to_part_equivp: assumes "type_definition Rep Abs S" - shows "part_equivp (invariant (\x. x \ S))" + shows "part_equivp (eq_onp (\x. x \ S))" proof (intro part_equivpI) interpret type_definition Rep Abs S by fact - show "\x. invariant (\x. x \ S) x x" using Rep by (auto simp: invariant_def) + show "\x. eq_onp (\x. x \ S) x x" using Rep by (auto simp: eq_onp_def) next - show "symp (invariant (\x. x \ S))" by (auto intro: sympI simp: invariant_def) + show "symp (eq_onp (\x. x \ S))" by (auto intro: sympI simp: eq_onp_def) next - show "transp (invariant (\x. x \ S))" by (auto intro: transpI simp: invariant_def) + show "transp (eq_onp (\x. x \ S))" by (auto intro: transpI simp: eq_onp_def) qed lemma open_typedef_to_Quotient: assumes "type_definition Rep Abs {x. P x}" and T_def: "T \ (\x y. x = Rep y)" - shows "Quotient (invariant P) Abs Rep T" + shows "Quotient (eq_onp P) Abs Rep T" using typedef_to_Quotient [OF assms] by simp lemma open_typedef_to_part_equivp: assumes "type_definition Rep Abs {x. P x}" - shows "part_equivp (invariant P)" + shows "part_equivp (eq_onp P)" using typedef_to_part_equivp [OF assms] by simp text {* Generating transfer rules for quotients. *} @@ -391,8 +391,8 @@ shows "(T OO R OO T\\) \ op=" using assms unfolding left_unique_def by blast -lemma invariant_le_eq: - "invariant P \ op=" unfolding invariant_def by blast +lemma eq_onp_le_eq: + "eq_onp P \ op=" unfolding eq_onp_def by blast lemma reflp_ge_eq: "reflp R \ R \ op=" unfolding reflp_def by blast @@ -503,19 +503,19 @@ subsection {* Domains *} -lemma composed_equiv_rel_invariant: +lemma composed_equiv_rel_eq_onp: assumes "left_unique R" assumes "(R ===> op=) P P'" assumes "Domainp R = P''" - shows "(R OO Lifting.invariant P' OO R\\) = Lifting.invariant (inf P'' P)" -using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def invariant_def + shows "(R OO eq_onp P' OO R\\) = eq_onp (inf P'' P)" +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def fun_eq_iff by blast -lemma composed_equiv_rel_eq_invariant: +lemma composed_equiv_rel_eq_eq_onp: assumes "left_unique R" assumes "Domainp R = P" - shows "(R OO op= OO R\\) = Lifting.invariant P" -using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def + shows "(R OO op= OO R\\) = eq_onp P" +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def fun_eq_iff is_equality_def by metis lemma pcr_Domainp_par_left_total: @@ -555,10 +555,10 @@ 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" +lemma eq_onp_to_Domainp: + assumes "Quotient (eq_onp P) Abs Rep T" shows "Domainp T = P" -by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) +by (simp add: eq_onp_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) end @@ -580,6 +580,6 @@ ML_file "Tools/Lifting/lifting_setup.ML" -hide_const (open) invariant POS NEG +hide_const (open) POS NEG end diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Lifting_Option.thy --- a/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:15 2014 +0200 @@ -63,9 +63,9 @@ "bi_unique R \ bi_unique (rel_option R)" unfolding bi_unique_def split_option_all by simp -lemma option_invariant_commute [invariant_commute]: - "rel_option (Lifting.invariant P) = Lifting.invariant (pred_option P)" - by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all) +lemma option_relator_eq_onp [relator_eq_onp]: + "rel_option (eq_onp P) = eq_onp (pred_option P)" + by (auto simp add: fun_eq_iff eq_onp_def split_option_all) subsection {* Quotient theorem for the Lifting package *} diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Lifting_Product.thy --- a/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:15 2014 +0200 @@ -61,9 +61,9 @@ shows "bi_unique (rel_prod R1 R2)" using assms unfolding bi_unique_def rel_prod_def by auto -lemma prod_invariant_commute [invariant_commute]: - "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (pred_prod P1 P2)" - by (simp add: fun_eq_iff rel_prod_def pred_prod_def Lifting.invariant_def) blast +lemma prod_relator_eq_onp [relator_eq_onp]: + "rel_prod (eq_onp P1) (eq_onp P2) = eq_onp (pred_prod P1 P2)" + by (simp add: fun_eq_iff rel_prod_def pred_prod_def eq_onp_def) blast subsection {* Quotient theorem for the Lifting package *} diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:15 2014 +0200 @@ -82,9 +82,9 @@ "bi_unique A \ bi_unique (rel_set A)" unfolding bi_unique_def rel_set_def by fast -lemma set_invariant_commute [invariant_commute]: - "rel_set (Lifting.invariant P) = Lifting.invariant (\A. Ball A P)" - unfolding fun_eq_iff rel_set_def Lifting.invariant_def Ball_def by fast +lemma set_relator_eq_onp [relator_eq_onp]: + "rel_set (eq_onp P) = eq_onp (\A. Ball A P)" + unfolding fun_eq_iff rel_set_def eq_onp_def Ball_def by fast subsection {* Quotient theorem for the Lifting package *} diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Lifting_Sum.thy --- a/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:15 2014 +0200 @@ -50,9 +50,9 @@ "bi_unique R1 \ bi_unique R2 \ bi_unique (rel_sum R1 R2)" using assms unfolding bi_unique_def split_sum_all by simp -lemma sum_invariant_commute [invariant_commute]: - "rel_sum (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" - by (auto simp add: fun_eq_iff Lifting.invariant_def rel_sum_def split: sum.split) +lemma sum_relator_eq_onp [relator_eq_onp]: + "rel_sum (eq_onp P1) (eq_onp P2) = eq_onp (sum_pred P1 P2)" + by (auto simp add: fun_eq_iff eq_onp_def rel_sum_def split: sum.split) subsection {* Quotient theorem for the Lifting package *} diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/List.thy --- a/src/HOL/List.thy Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/List.thy Thu Apr 10 17:48:15 2014 +0200 @@ -6665,9 +6665,9 @@ apply (simp, force simp add: list_all2_Cons2) done -lemma list_invariant_commute [invariant_commute]: - "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)" - apply (simp add: fun_eq_iff list_all2_iff list_all_iff Lifting.invariant_def Ball_def) +lemma list_relator_eq_onp [relator_eq_onp]: + "list_all2 (eq_onp P) = eq_onp (list_all P)" + apply (simp add: fun_eq_iff list_all2_iff list_all_iff eq_onp_def Ball_def) apply (intro allI) apply (induct_tac rule: list_induct2') apply simp_all diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:15 2014 +0200 @@ -262,7 +262,7 @@ fun can_generate_code_cert quot_thm = case quot_thm_rel quot_thm of Const (@{const_name HOL.eq}, _) => true - | Const (@{const_name invariant}, _) $ _ => true + | Const (@{const_name eq_onp}, _) $ _ => true | _ => false fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) = @@ -450,7 +450,7 @@ end local - val invariant_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context}) + val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context}) [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, @{thm pcr_Domainp}] in @@ -511,33 +511,33 @@ fun simp_arrows_conv ctm = let val unfold_conv = Conv.rewrs_conv - [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, - @{thm rel_fun_invariant_rel[THEN eq_reflection]}, + [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, + @{thm rel_fun_eq_onp_rel[THEN eq_reflection]}, @{thm rel_fun_eq[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, @{thm rel_fun_def[THEN eq_reflection]}] fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 - val invariant_assms_tac_rules = @{thm left_unique_OO} :: - invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy) - val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) + val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: + eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy) + val eq_onp_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac eq_onp_assms_tac_rules) THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1 - val invariant_commute_conv = Conv.bottom_conv - (K (Conv.try_conv (assms_rewrs_conv invariant_assms_tac - (Lifting_Info.get_invariant_commute_rules lthy)))) lthy + val relator_eq_onp_conv = Conv.bottom_conv + (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac + (Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy val relator_eq_conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy in case (Thm.term_of ctm) of Const (@{const_name "rel_fun"}, _) $ _ $ _ => (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm - | _ => (invariant_commute_conv then_conv relator_eq_conv) ctm + | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm end val unfold_ret_val_invs = Conv.bottom_conv - (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy + (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy) val unfold_inv_conv = - Conv.top_sweep_conv (K (Conv.rewr_conv @{thm invariant_def[THEN eq_reflection]})) lthy + Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv)) val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu Apr 10 17:48:15 2014 +0200 @@ -25,7 +25,7 @@ val init_restore_data: string -> quotient -> Context.generic -> Context.generic val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic - val get_invariant_commute_rules: Proof.context -> thm list + val get_relator_eq_onp_rules: Proof.context -> thm list val get_reflexivity_rules: Proof.context -> thm list val add_reflexivity_rule_attribute: attribute @@ -262,15 +262,15 @@ transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.") -(* theorems that a relator of an invariant is an invariant of the corresponding predicate *) +(* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *) -structure Invariant_Commute = Named_Thms +structure Relator_Eq_Onp = Named_Thms ( - val name = @{binding invariant_commute} - val description = "theorems that a relator of an invariant is an invariant of the corresponding predicate" + val name = @{binding relator_eq_onp} + val description = "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate" ) -fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt) +fun get_relator_eq_onp_rules ctxt = map safe_mk_meta_eq (Relator_Eq_Onp.get ctxt) (* info about reflexivity rules *) @@ -505,18 +505,18 @@ val setup = quot_map_attribute_setup #> quot_del_attribute_setup - #> Invariant_Commute.setup + #> Relator_Eq_Onp.setup #> relator_distr_attribute_setup -(* setup fixed invariant rules *) +(* setup fixed eq_onp rules *) -val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) - @{thms composed_equiv_rel_invariant composed_equiv_rel_eq_invariant}) +val _ = Context.>> (fold (Relator_Eq_Onp.add_thm o Transfer.prep_transfer_domain_thm @{context}) + @{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp}) (* setup fixed reflexivity rules *) val _ = Context.>> (fold add_reflexivity_rule - @{thms order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq + @{thms order_refl[of "op="] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO}) (* outer syntax commands *) diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 10 17:48:15 2014 +0200 @@ -467,7 +467,7 @@ #pcr_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}]) + the (get_first (try(curry op RS quot_thm)) [@{thm eq_onp_to_Domainp}, @{thm Quotient_to_Domainp}]) (* Sets up the Lifting package by a quotient theorem. @@ -646,7 +646,6 @@ SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2}) | _ => NONE val dom_thm = get_Domainp_thm quot_thm - val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute) fun setup_transfer_rules_nonpar lthy = let diff -r beb3b6851665 -r c1048f5bbb45 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Apr 10 17:48:14 2014 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Apr 10 17:48:15 2014 +0200 @@ -109,7 +109,7 @@ fun simp_arrows_conv ctm = let val unfold_conv = Conv.rewrs_conv - [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, + [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, @{thm rel_fun_def[THEN eq_reflection]}] val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 @@ -121,7 +121,7 @@ end val unfold_ret_val_invs = Conv.bottom_conv - (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy + (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv) val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy