1.1 --- a/src/HOL/Lifting.thy	Thu Apr 10 17:48:17 2014 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 10 17:48:18 2014 +0200
     1.3 @@ -161,6 +161,11 @@
     1.4      (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
     1.5    unfolding Quotient_alt_def3 fun_eq_iff by auto
     1.6  
     1.7 +lemma Quotient_alt_def5:
     1.8 +  "Quotient R Abs Rep T \<longleftrightarrow>
     1.9 +    T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
    1.10 +  unfolding Quotient_alt_def4 Grp_def by blast
    1.11 +
    1.12  lemma fun_quotient:
    1.13    assumes 1: "Quotient R1 abs1 rep1 T1"
    1.14    assumes 2: "Quotient R2 abs2 rep2 T2"
    1.15 @@ -210,32 +215,6 @@
    1.16  lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
    1.17    unfolding Respects_def by simp
    1.18  
    1.19 -subsection {* Invariant *}
    1.20 -
    1.21 -definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
    1.22 -  where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
    1.23 -
    1.24 -lemma eq_onp_to_eq:
    1.25 -  assumes "eq_onp P x y"
    1.26 -  shows "x = y"
    1.27 -using assms by (simp add: eq_onp_def)
    1.28 -
    1.29 -lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
    1.30 -unfolding eq_onp_def rel_fun_def by auto
    1.31 -
    1.32 -lemma rel_fun_eq_onp_rel:
    1.33 -  shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
    1.34 -by (auto simp add: eq_onp_def rel_fun_def)
    1.35 -
    1.36 -lemma eq_onp_same_args:
    1.37 -  shows "eq_onp P x x \<equiv> P x"
    1.38 -using assms by (auto simp add: eq_onp_def)
    1.39 -
    1.40 -lemma eq_onp_transfer [transfer_rule]:
    1.41 -  assumes [transfer_rule]: "bi_unique A"
    1.42 -  shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
    1.43 -unfolding eq_onp_def[abs_def] by transfer_prover
    1.44 -
    1.45  lemma UNIV_typedef_to_Quotient:
    1.46    assumes "type_definition Rep Abs UNIV"
    1.47    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.48 @@ -574,6 +553,8 @@
    1.49  declare fun_mono[relator_mono]
    1.50  lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
    1.51  
    1.52 +ML_file "Tools/Lifting/lifting_bnf.ML"
    1.53 +
    1.54  ML_file "Tools/Lifting/lifting_term.ML"
    1.55  
    1.56  ML_file "Tools/Lifting/lifting_def.ML"