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"