--- 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 \<rightarrow>"}\\
@{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
@{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.
--- 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 \<Longrightarrow> 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 *}
--- 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 *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> 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 \<in> {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 \<Longrightarrow> the_elem (Set t) = x"
by (subst(asm) RBT_inverse[symmetric, OF *])
--- 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 \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- where "invariant R = (\<lambda>x y. R x \<and> x = y)"
+definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "eq_onp R = (\<lambda>x y. R x \<and> 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 (\<lambda>f. \<forall>x. P(f x))"
-unfolding invariant_def rel_fun_def by auto
+lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
+unfolding eq_onp_def rel_fun_def by auto
-lemma rel_fun_invariant_rel:
- shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> 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) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
+by (auto simp add: eq_onp_def rel_fun_def)
-lemma invariant_same_args:
- shows "invariant P x x \<equiv> P x"
-using assms by (auto simp add: invariant_def)
+lemma eq_onp_same_args:
+ shows "eq_onp P x x \<equiv> 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 \<equiv> (\<lambda>x y. x = Rep y)"
- shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
+ shows "Quotient (eq_onp (\<lambda>x. x \<in> 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 (\<lambda>x. x \<in> S))"
+ shows "part_equivp (eq_onp (\<lambda>x. x \<in> S))"
proof (intro part_equivpI)
interpret type_definition Rep Abs S by fact
- show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
+ show "\<exists>x. eq_onp (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: eq_onp_def)
next
- show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
+ show "symp (eq_onp (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: eq_onp_def)
next
- show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
+ show "transp (eq_onp (\<lambda>x. x \<in> 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 \<equiv> (\<lambda>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\<inverse>\<inverse>) \<le> op="
using assms unfolding left_unique_def by blast
-lemma invariant_le_eq:
- "invariant P \<le> op=" unfolding invariant_def by blast
+lemma eq_onp_le_eq:
+ "eq_onp P \<le> op=" unfolding eq_onp_def by blast
lemma reflp_ge_eq:
"reflp R \<Longrightarrow> R \<ge> 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\<inverse>\<inverse>) = 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\<inverse>\<inverse>) = 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\<inverse>\<inverse>) = 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\<inverse>\<inverse>) = 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 = (\<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"
+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
--- 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 \<Longrightarrow> 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 *}
--- 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 *}
--- 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 \<Longrightarrow> 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 (\<lambda>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 (\<lambda>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 *}
--- 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 \<Longrightarrow> bi_unique R2 \<Longrightarrow> 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 *}
--- 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
--- 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]}
--- 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 *)
--- 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
--- 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