more appropriate name (Lifting.invariant -> eq_onp)
authorkuncar
Thu Apr 10 17:48:15 2014 +0200 (2014-04-10)
changeset 56519c1048f5bbb45
parent 56518 beb3b6851665
child 56520 3373f5d1e074
more appropriate name (Lifting.invariant -> eq_onp)
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Library/FSet.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Lifting.thy
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Set.thy
src/HOL/Lifting_Sum.thy
src/HOL/List.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Quotient/quotient_def.ML
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Apr 10 17:48:14 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Apr 10 17:48:15 2014 +0200
     1.3 @@ -1596,7 +1596,7 @@
     1.4      @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
     1.5      @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
     1.6      @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
     1.7 -    @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
     1.8 +    @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\
     1.9      @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
    1.10      @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
    1.11      @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
    1.12 @@ -1733,11 +1733,11 @@
    1.13      "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
    1.14      in the same directory.
    1.15  
    1.16 -  \item @{attribute (HOL) invariant_commute} registers a theorem that
    1.17 +  \item @{attribute (HOL) relator_eq_onp} registers a theorem that
    1.18      shows a relationship between the constant @{text
    1.19 -    Lifting.invariant} (used for internal encoding of proper subtypes)
    1.20 +    eq_onp} (used for internal encoding of proper subtypes)
    1.21      and a relator.  Such theorems allows the package to hide @{text
    1.22 -    Lifting.invariant} from a user in a user-readable form of a
    1.23 +    eq_onp} from a user in a user-readable form of a
    1.24      respectfulness theorem. For examples see @{file
    1.25      "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
    1.26  
     2.1 --- a/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:14 2014 +0200
     2.2 +++ b/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:15 2014 +0200
     2.3 @@ -853,7 +853,7 @@
     2.4  lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
     2.5  by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff)
     2.6  
     2.7 -lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
     2.8 +lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
     2.9  
    2.10  
    2.11  subsubsection {* Quotient theorem for the Lifting package *}
     3.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Apr 10 17:48:14 2014 +0200
     3.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Apr 10 17:48:15 2014 +0200
     3.3 @@ -640,7 +640,7 @@
     3.4  proof -
     3.5    have *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
     3.6      by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
     3.7 -  have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
     3.8 +  have **: "eq_onp is_rbt rbt.Empty rbt.Empty" unfolding eq_onp_def by simp
     3.9    show ?thesis  
    3.10      by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
    3.11  qed
    3.12 @@ -672,7 +672,7 @@
    3.13      fix x :: "'a :: linorder"
    3.14      let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
    3.15      have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
    3.16 -    then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
    3.17 +    then have **:"eq_onp is_rbt ?t ?t" unfolding eq_onp_def by auto
    3.18  
    3.19      have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
    3.20        by (subst(asm) RBT_inverse[symmetric, OF *])
     4.1 --- a/src/HOL/Lifting.thy	Thu Apr 10 17:48:14 2014 +0200
     4.2 +++ b/src/HOL/Lifting.thy	Thu Apr 10 17:48:15 2014 +0200
     4.3 @@ -212,29 +212,29 @@
     4.4  
     4.5  subsection {* Invariant *}
     4.6  
     4.7 -definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
     4.8 -  where "invariant R = (\<lambda>x y. R x \<and> x = y)"
     4.9 +definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
    4.10 +  where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
    4.11  
    4.12 -lemma invariant_to_eq:
    4.13 -  assumes "invariant P x y"
    4.14 +lemma eq_onp_to_eq:
    4.15 +  assumes "eq_onp P x y"
    4.16    shows "x = y"
    4.17 -using assms by (simp add: invariant_def)
    4.18 +using assms by (simp add: eq_onp_def)
    4.19  
    4.20 -lemma rel_fun_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
    4.21 -unfolding invariant_def rel_fun_def by auto
    4.22 +lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
    4.23 +unfolding eq_onp_def rel_fun_def by auto
    4.24  
    4.25 -lemma rel_fun_invariant_rel:
    4.26 -  shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
    4.27 -by (auto simp add: invariant_def rel_fun_def)
    4.28 +lemma rel_fun_eq_onp_rel:
    4.29 +  shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
    4.30 +by (auto simp add: eq_onp_def rel_fun_def)
    4.31  
    4.32 -lemma invariant_same_args:
    4.33 -  shows "invariant P x x \<equiv> P x"
    4.34 -using assms by (auto simp add: invariant_def)
    4.35 +lemma eq_onp_same_args:
    4.36 +  shows "eq_onp P x x \<equiv> P x"
    4.37 +using assms by (auto simp add: eq_onp_def)
    4.38  
    4.39 -lemma invariant_transfer [transfer_rule]:
    4.40 +lemma eq_onp_transfer [transfer_rule]:
    4.41    assumes [transfer_rule]: "bi_unique A"
    4.42 -  shows "((A ===> op=) ===> A ===> A ===> op=) Lifting.invariant Lifting.invariant"
    4.43 -unfolding invariant_def[abs_def] by transfer_prover
    4.44 +  shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
    4.45 +unfolding eq_onp_def[abs_def] by transfer_prover
    4.46  
    4.47  lemma UNIV_typedef_to_Quotient:
    4.48    assumes "type_definition Rep Abs UNIV"
    4.49 @@ -256,34 +256,34 @@
    4.50  lemma typedef_to_Quotient:
    4.51    assumes "type_definition Rep Abs S"
    4.52    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    4.53 -  shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
    4.54 +  shows "Quotient (eq_onp (\<lambda>x. x \<in> S)) Abs Rep T"
    4.55  proof -
    4.56    interpret type_definition Rep Abs S by fact
    4.57    from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
    4.58 -    by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
    4.59 +    by (auto intro!: QuotientI simp: eq_onp_def fun_eq_iff)
    4.60  qed
    4.61  
    4.62  lemma typedef_to_part_equivp:
    4.63    assumes "type_definition Rep Abs S"
    4.64 -  shows "part_equivp (invariant (\<lambda>x. x \<in> S))"
    4.65 +  shows "part_equivp (eq_onp (\<lambda>x. x \<in> S))"
    4.66  proof (intro part_equivpI)
    4.67    interpret type_definition Rep Abs S by fact
    4.68 -  show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
    4.69 +  show "\<exists>x. eq_onp (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: eq_onp_def)
    4.70  next
    4.71 -  show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
    4.72 +  show "symp (eq_onp (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: eq_onp_def)
    4.73  next
    4.74 -  show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
    4.75 +  show "transp (eq_onp (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: eq_onp_def)
    4.76  qed
    4.77  
    4.78  lemma open_typedef_to_Quotient:
    4.79    assumes "type_definition Rep Abs {x. P x}"
    4.80    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    4.81 -  shows "Quotient (invariant P) Abs Rep T"
    4.82 +  shows "Quotient (eq_onp P) Abs Rep T"
    4.83    using typedef_to_Quotient [OF assms] by simp
    4.84  
    4.85  lemma open_typedef_to_part_equivp:
    4.86    assumes "type_definition Rep Abs {x. P x}"
    4.87 -  shows "part_equivp (invariant P)"
    4.88 +  shows "part_equivp (eq_onp P)"
    4.89    using typedef_to_part_equivp [OF assms] by simp
    4.90  
    4.91  text {* Generating transfer rules for quotients. *}
    4.92 @@ -391,8 +391,8 @@
    4.93    shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
    4.94  using assms unfolding left_unique_def by blast
    4.95  
    4.96 -lemma invariant_le_eq:
    4.97 -  "invariant P \<le> op=" unfolding invariant_def by blast
    4.98 +lemma eq_onp_le_eq:
    4.99 +  "eq_onp P \<le> op=" unfolding eq_onp_def by blast
   4.100  
   4.101  lemma reflp_ge_eq:
   4.102    "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
   4.103 @@ -503,19 +503,19 @@
   4.104  
   4.105  subsection {* Domains *}
   4.106  
   4.107 -lemma composed_equiv_rel_invariant:
   4.108 +lemma composed_equiv_rel_eq_onp:
   4.109    assumes "left_unique R"
   4.110    assumes "(R ===> op=) P P'"
   4.111    assumes "Domainp R = P''"
   4.112 -  shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
   4.113 -using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def invariant_def
   4.114 +  shows "(R OO eq_onp P' OO R\<inverse>\<inverse>) = eq_onp (inf P'' P)"
   4.115 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def
   4.116  fun_eq_iff by blast
   4.117  
   4.118 -lemma composed_equiv_rel_eq_invariant:
   4.119 +lemma composed_equiv_rel_eq_eq_onp:
   4.120    assumes "left_unique R"
   4.121    assumes "Domainp R = P"
   4.122 -  shows "(R OO op= OO R\<inverse>\<inverse>) = Lifting.invariant P"
   4.123 -using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def
   4.124 +  shows "(R OO op= OO R\<inverse>\<inverse>) = eq_onp P"
   4.125 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def
   4.126  fun_eq_iff is_equality_def by metis
   4.127  
   4.128  lemma pcr_Domainp_par_left_total:
   4.129 @@ -555,10 +555,10 @@
   4.130    shows "Domainp T = (\<lambda>x. R x x)"  
   4.131  by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
   4.132  
   4.133 -lemma invariant_to_Domainp:
   4.134 -  assumes "Quotient (Lifting.invariant P) Abs Rep T"
   4.135 +lemma eq_onp_to_Domainp:
   4.136 +  assumes "Quotient (eq_onp P) Abs Rep T"
   4.137    shows "Domainp T = P"
   4.138 -by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
   4.139 +by (simp add: eq_onp_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
   4.140  
   4.141  end
   4.142  
   4.143 @@ -580,6 +580,6 @@
   4.144  
   4.145  ML_file "Tools/Lifting/lifting_setup.ML"
   4.146                             
   4.147 -hide_const (open) invariant POS NEG
   4.148 +hide_const (open) POS NEG
   4.149  
   4.150  end
     5.1 --- a/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:14 2014 +0200
     5.2 +++ b/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:15 2014 +0200
     5.3 @@ -63,9 +63,9 @@
     5.4    "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
     5.5    unfolding bi_unique_def split_option_all by simp
     5.6  
     5.7 -lemma option_invariant_commute [invariant_commute]:
     5.8 -  "rel_option (Lifting.invariant P) = Lifting.invariant (pred_option P)"
     5.9 -  by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
    5.10 +lemma option_relator_eq_onp [relator_eq_onp]:
    5.11 +  "rel_option (eq_onp P) = eq_onp (pred_option P)"
    5.12 +  by (auto simp add: fun_eq_iff eq_onp_def split_option_all)
    5.13  
    5.14  subsection {* Quotient theorem for the Lifting package *}
    5.15  
     6.1 --- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:14 2014 +0200
     6.2 +++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:15 2014 +0200
     6.3 @@ -61,9 +61,9 @@
     6.4    shows "bi_unique (rel_prod R1 R2)"
     6.5    using assms unfolding bi_unique_def rel_prod_def by auto
     6.6  
     6.7 -lemma prod_invariant_commute [invariant_commute]: 
     6.8 -  "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (pred_prod P1 P2)"
     6.9 -  by (simp add: fun_eq_iff rel_prod_def pred_prod_def Lifting.invariant_def) blast
    6.10 +lemma prod_relator_eq_onp [relator_eq_onp]: 
    6.11 +  "rel_prod (eq_onp P1) (eq_onp P2) = eq_onp (pred_prod P1 P2)"
    6.12 +  by (simp add: fun_eq_iff rel_prod_def pred_prod_def eq_onp_def) blast
    6.13  
    6.14  subsection {* Quotient theorem for the Lifting package *}
    6.15  
     7.1 --- a/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:14 2014 +0200
     7.2 +++ b/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:15 2014 +0200
     7.3 @@ -82,9 +82,9 @@
     7.4    "bi_unique A \<Longrightarrow> bi_unique (rel_set A)"
     7.5    unfolding bi_unique_def rel_set_def by fast
     7.6  
     7.7 -lemma set_invariant_commute [invariant_commute]:
     7.8 -  "rel_set (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
     7.9 -  unfolding fun_eq_iff rel_set_def Lifting.invariant_def Ball_def by fast
    7.10 +lemma set_relator_eq_onp [relator_eq_onp]:
    7.11 +  "rel_set (eq_onp P) = eq_onp (\<lambda>A. Ball A P)"
    7.12 +  unfolding fun_eq_iff rel_set_def eq_onp_def Ball_def by fast
    7.13  
    7.14  subsection {* Quotient theorem for the Lifting package *}
    7.15  
     8.1 --- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:14 2014 +0200
     8.2 +++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:15 2014 +0200
     8.3 @@ -50,9 +50,9 @@
     8.4    "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (rel_sum R1 R2)"
     8.5    using assms unfolding bi_unique_def split_sum_all by simp
     8.6  
     8.7 -lemma sum_invariant_commute [invariant_commute]: 
     8.8 -  "rel_sum (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
     8.9 -  by (auto simp add: fun_eq_iff Lifting.invariant_def rel_sum_def split: sum.split)
    8.10 +lemma sum_relator_eq_onp [relator_eq_onp]: 
    8.11 +  "rel_sum (eq_onp P1) (eq_onp P2) = eq_onp (sum_pred P1 P2)"
    8.12 +  by (auto simp add: fun_eq_iff eq_onp_def rel_sum_def split: sum.split)
    8.13  
    8.14  subsection {* Quotient theorem for the Lifting package *}
    8.15  
     9.1 --- a/src/HOL/List.thy	Thu Apr 10 17:48:14 2014 +0200
     9.2 +++ b/src/HOL/List.thy	Thu Apr 10 17:48:15 2014 +0200
     9.3 @@ -6665,9 +6665,9 @@
     9.4    apply (simp, force simp add: list_all2_Cons2)
     9.5    done
     9.6  
     9.7 -lemma list_invariant_commute [invariant_commute]:
     9.8 -  "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
     9.9 -  apply (simp add: fun_eq_iff list_all2_iff list_all_iff Lifting.invariant_def Ball_def) 
    9.10 +lemma list_relator_eq_onp [relator_eq_onp]:
    9.11 +  "list_all2 (eq_onp P) = eq_onp (list_all P)"
    9.12 +  apply (simp add: fun_eq_iff list_all2_iff list_all_iff eq_onp_def Ball_def) 
    9.13    apply (intro allI) 
    9.14    apply (induct_tac rule: list_induct2') 
    9.15    apply simp_all 
    10.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:14 2014 +0200
    10.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:15 2014 +0200
    10.3 @@ -262,7 +262,7 @@
    10.4  fun can_generate_code_cert quot_thm  =
    10.5    case quot_thm_rel quot_thm of
    10.6      Const (@{const_name HOL.eq}, _) => true
    10.7 -    | Const (@{const_name invariant}, _) $ _  => true
    10.8 +    | Const (@{const_name eq_onp}, _) $ _  => true
    10.9      | _ => false
   10.10  
   10.11  fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
   10.12 @@ -450,7 +450,7 @@
   10.13    end
   10.14  
   10.15  local
   10.16 -  val invariant_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
   10.17 +  val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
   10.18      [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
   10.19        @{thm pcr_Domainp}]
   10.20  in
   10.21 @@ -511,33 +511,33 @@
   10.22      fun simp_arrows_conv ctm =
   10.23        let
   10.24          val unfold_conv = Conv.rewrs_conv 
   10.25 -          [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, 
   10.26 -            @{thm rel_fun_invariant_rel[THEN eq_reflection]},
   10.27 +          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, 
   10.28 +            @{thm rel_fun_eq_onp_rel[THEN eq_reflection]},
   10.29              @{thm rel_fun_eq[THEN eq_reflection]},
   10.30              @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
   10.31              @{thm rel_fun_def[THEN eq_reflection]}]
   10.32          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   10.33 -        val invariant_assms_tac_rules = @{thm left_unique_OO} :: 
   10.34 -            invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
   10.35 -        val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) 
   10.36 +        val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: 
   10.37 +            eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
   10.38 +        val eq_onp_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac eq_onp_assms_tac_rules) 
   10.39            THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
   10.40 -        val invariant_commute_conv = Conv.bottom_conv
   10.41 -          (K (Conv.try_conv (assms_rewrs_conv invariant_assms_tac
   10.42 -            (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
   10.43 +        val relator_eq_onp_conv = Conv.bottom_conv
   10.44 +          (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac
   10.45 +            (Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy
   10.46          val relator_eq_conv = Conv.bottom_conv
   10.47            (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
   10.48        in
   10.49          case (Thm.term_of ctm) of
   10.50            Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
   10.51              (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
   10.52 -          | _ => (invariant_commute_conv then_conv relator_eq_conv) ctm
   10.53 +          | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
   10.54        end
   10.55      
   10.56      val unfold_ret_val_invs = Conv.bottom_conv 
   10.57 -      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
   10.58 +      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy
   10.59      val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
   10.60      val unfold_inv_conv = 
   10.61 -      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm invariant_def[THEN eq_reflection]})) lthy
   10.62 +      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
   10.63      val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 
   10.64        (cr_to_pcr_conv then_conv simp_arrows_conv))
   10.65      val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
    11.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 10 17:48:14 2014 +0200
    11.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 10 17:48:15 2014 +0200
    11.3 @@ -25,7 +25,7 @@
    11.4    val init_restore_data: string -> quotient -> Context.generic -> Context.generic
    11.5    val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic  
    11.6  
    11.7 -  val get_invariant_commute_rules: Proof.context -> thm list
    11.8 +  val get_relator_eq_onp_rules: Proof.context -> thm list
    11.9    
   11.10    val get_reflexivity_rules: Proof.context -> thm list
   11.11    val add_reflexivity_rule_attribute: attribute
   11.12 @@ -262,15 +262,15 @@
   11.13        transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt
   11.14      | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")
   11.15  
   11.16 -(* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
   11.17 +(* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *)
   11.18  
   11.19 -structure Invariant_Commute = Named_Thms
   11.20 +structure Relator_Eq_Onp = Named_Thms
   11.21  (
   11.22 -  val name = @{binding invariant_commute}
   11.23 -  val description = "theorems that a relator of an invariant is an invariant of the corresponding predicate"
   11.24 +  val name = @{binding relator_eq_onp}
   11.25 +  val description = "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
   11.26  )
   11.27  
   11.28 -fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
   11.29 +fun get_relator_eq_onp_rules ctxt = map safe_mk_meta_eq (Relator_Eq_Onp.get ctxt)
   11.30  
   11.31  (* info about reflexivity rules *)
   11.32  
   11.33 @@ -505,18 +505,18 @@
   11.34  val setup =
   11.35    quot_map_attribute_setup
   11.36    #> quot_del_attribute_setup
   11.37 -  #> Invariant_Commute.setup
   11.38 +  #> Relator_Eq_Onp.setup
   11.39    #> relator_distr_attribute_setup
   11.40  
   11.41 -(* setup fixed invariant rules *)
   11.42 +(* setup fixed eq_onp rules *)
   11.43  
   11.44 -val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
   11.45 -  @{thms composed_equiv_rel_invariant composed_equiv_rel_eq_invariant})
   11.46 +val _ = Context.>> (fold (Relator_Eq_Onp.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
   11.47 +  @{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp})
   11.48  
   11.49  (* setup fixed reflexivity rules *)
   11.50  
   11.51  val _ = Context.>> (fold add_reflexivity_rule 
   11.52 -  @{thms order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq
   11.53 +  @{thms order_refl[of "op="] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq
   11.54      bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO})
   11.55  
   11.56  (* outer syntax commands *)
    12.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 10 17:48:14 2014 +0200
    12.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 10 17:48:15 2014 +0200
    12.3 @@ -467,7 +467,7 @@
    12.4    #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
    12.5  
    12.6  fun get_Domainp_thm quot_thm =
    12.7 -   the (get_first (try(curry op RS quot_thm)) [@{thm invariant_to_Domainp}, @{thm Quotient_to_Domainp}])
    12.8 +   the (get_first (try(curry op RS quot_thm)) [@{thm eq_onp_to_Domainp}, @{thm Quotient_to_Domainp}])
    12.9  
   12.10  (*
   12.11    Sets up the Lifting package by a quotient theorem.
   12.12 @@ -646,7 +646,6 @@
   12.13            SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
   12.14          | _ =>  NONE
   12.15      val dom_thm = get_Domainp_thm quot_thm
   12.16 -    val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
   12.17  
   12.18      fun setup_transfer_rules_nonpar lthy =
   12.19        let
    13.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Apr 10 17:48:14 2014 +0200
    13.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Apr 10 17:48:15 2014 +0200
    13.3 @@ -109,7 +109,7 @@
    13.4      fun simp_arrows_conv ctm =
    13.5        let
    13.6          val unfold_conv = Conv.rewrs_conv 
    13.7 -          [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
    13.8 +          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
    13.9              @{thm rel_fun_def[THEN eq_reflection]}]
   13.10          val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
   13.11          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   13.12 @@ -121,7 +121,7 @@
   13.13        end
   13.14  
   13.15      val unfold_ret_val_invs = Conv.bottom_conv 
   13.16 -      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
   13.17 +      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy 
   13.18      val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
   13.19      val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
   13.20      val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy