src/HOL/Lifting.thy
 changeset 56519 c1048f5bbb45 parent 56518 beb3b6851665 child 56524 f4ba736040fa
```--- 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```