src/HOL/Lifting.thy
 changeset 55945 e96383acecf9 parent 55737 84f6ac9f6e41 child 56517 7e8a369eb10d
```     1.1 --- a/src/HOL/Lifting.thy	Thu Mar 06 15:29:18 2014 +0100
1.2 +++ b/src/HOL/Lifting.thy	Thu Mar 06 15:40:33 2014 +0100
1.3 @@ -52,7 +52,7 @@
1.4    assumes [transfer_rule]: "right_total B"
1.5    assumes [transfer_rule]: "bi_unique A"
1.6    shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
1.7 -using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
1.8 +using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
1.9  by metis
1.10
1.11  lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
1.12 @@ -69,7 +69,7 @@
1.13
1.14  lemma left_total_fun:
1.15    "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
1.16 -  unfolding left_total_def fun_rel_def
1.17 +  unfolding left_total_def rel_fun_def
1.18    apply (rule allI, rename_tac f)
1.19    apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
1.20    apply clarify
1.21 @@ -83,7 +83,7 @@
1.22
1.23  lemma left_unique_fun:
1.24    "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
1.25 -  unfolding left_total_def left_unique_def fun_rel_def
1.26 +  unfolding left_total_def left_unique_def rel_fun_def
1.27    by (clarify, rule ext, fast)
1.28
1.29  lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
1.30 @@ -242,7 +242,7 @@
1.31    assumes 2: "Quotient R2 abs2 rep2 T2"
1.32    shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
1.33    using assms unfolding Quotient_alt_def2
1.34 -  unfolding fun_rel_def fun_eq_iff map_fun_apply
1.35 +  unfolding rel_fun_def fun_eq_iff map_fun_apply
1.36    by (safe, metis+)
1.37
1.38  lemma apply_rsp:
1.39 @@ -250,12 +250,12 @@
1.40    assumes q: "Quotient R1 Abs1 Rep1 T1"
1.41    and     a: "(R1 ===> R2) f g" "R1 x y"
1.42    shows "R2 (f x) (g y)"
1.43 -  using a by (auto elim: fun_relE)
1.44 +  using a by (auto elim: rel_funE)
1.45
1.46  lemma apply_rsp':
1.47    assumes a: "(R1 ===> R2) f g" "R1 x y"
1.48    shows "R2 (f x) (g y)"
1.49 -  using a by (auto elim: fun_relE)
1.50 +  using a by (auto elim: rel_funE)
1.51
1.52  lemma apply_rsp'':
1.53    assumes "Quotient R Abs Rep T"
1.54 @@ -296,12 +296,12 @@
1.55    shows "x = y"
1.56  using assms by (simp add: invariant_def)
1.57
1.58 -lemma fun_rel_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
1.59 -unfolding invariant_def fun_rel_def by auto
1.60 +lemma rel_fun_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
1.61 +unfolding invariant_def rel_fun_def by auto
1.62
1.63 -lemma fun_rel_invariant_rel:
1.64 +lemma rel_fun_invariant_rel:
1.65    shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
1.66 -by (auto simp add: invariant_def fun_rel_def)
1.67 +by (auto simp add: invariant_def rel_fun_def)
1.68
1.69  lemma invariant_same_args:
1.70    shows "invariant P x x \<equiv> P x"
1.71 @@ -376,7 +376,7 @@
1.72    using 1 unfolding Quotient_alt_def right_total_def by metis
1.73
1.74  lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
1.75 -  using 1 unfolding Quotient_alt_def fun_rel_def by simp
1.76 +  using 1 unfolding Quotient_alt_def rel_fun_def by simp
1.77
1.78  lemma Quotient_abs_induct:
1.79    assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
1.80 @@ -395,7 +395,7 @@
1.81    using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
1.82
1.83  lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
1.84 -  using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
1.85 +  using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
1.86
1.87  lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
1.88    using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
1.89 @@ -432,7 +432,7 @@
1.90    by blast
1.91
1.92  lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
1.93 -  unfolding fun_rel_def T_def by simp
1.94 +  unfolding rel_fun_def T_def by simp
1.95
1.96  end
1.97
1.98 @@ -557,10 +557,10 @@
1.99    assumes "A \<ge> C"
1.100    assumes "B \<le> D"
1.101    shows   "(A ===> B) \<le> (C ===> D)"
1.102 -using assms unfolding fun_rel_def by blast
1.103 +using assms unfolding rel_fun_def by blast
1.104
1.105  lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
1.106 -unfolding OO_def fun_rel_def by blast
1.107 +unfolding OO_def rel_fun_def by blast
1.108
1.109  lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
1.110  unfolding right_unique_def left_total_def by blast
1.111 @@ -573,7 +573,7 @@
1.112  assumes 2: "right_unique R'" "left_total R'"
1.113  shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
1.114    using functional_relation[OF 2] functional_converse_relation[OF 1]
1.115 -  unfolding fun_rel_def OO_def
1.116 +  unfolding rel_fun_def OO_def
1.117    apply clarify
1.118    apply (subst all_comm)
1.119    apply (subst all_conj_distrib[symmetric])
1.120 @@ -585,7 +585,7 @@
1.121  assumes 2: "left_unique S'" "right_total S'"
1.122  shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
1.123    using functional_converse_relation[OF 2] functional_relation[OF 1]
1.124 -  unfolding fun_rel_def OO_def
1.125 +  unfolding rel_fun_def OO_def
1.126    apply clarify
1.127    apply (subst all_comm)
1.128    apply (subst all_conj_distrib[symmetric])
1.129 @@ -599,7 +599,7 @@
1.130    assumes "(R ===> op=) P P'"
1.131    assumes "Domainp R = P''"
1.132    shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
1.133 -using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
1.134 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def invariant_def
1.135  fun_eq_iff by blast
1.136
1.137  lemma composed_equiv_rel_eq_invariant:
1.138 @@ -615,7 +615,7 @@
1.139    assumes "(A ===> op=) P' P"
1.140    shows "Domainp (A OO B) = P'"
1.141  using assms
1.142 -unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def
1.143 +unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def
1.144  by (fast intro: fun_eq_iff)
1.145
1.146  lemma pcr_Domainp_par:
1.147 @@ -623,7 +623,7 @@
1.148  assumes "Domainp A = P1"
1.149  assumes "(A ===> op=) P2' P2"
1.150  shows "Domainp (A OO B) = (inf P1 P2')"
1.151 -using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
1.152 +using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def
1.153  by (fast intro: fun_eq_iff)
1.154
1.155  definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"
```