diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Thu Apr 10 17:48:17 2014 +0200 +++ b/src/HOL/Lifting.thy Thu Apr 10 17:48:18 2014 +0200 @@ -161,6 +161,11 @@ (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ R = T OO conversep T" unfolding Quotient_alt_def3 fun_eq_iff by auto +lemma Quotient_alt_def5: + "Quotient R Abs Rep T \ + T \ BNF_Util.Grp UNIV Abs \ BNF_Util.Grp UNIV Rep \ T\\ \ R = T OO T\\" + unfolding Quotient_alt_def4 Grp_def by blast + lemma fun_quotient: assumes 1: "Quotient R1 abs1 rep1 T1" assumes 2: "Quotient R2 abs2 rep2 T2" @@ -210,32 +215,6 @@ lemma in_respects: "x \ Respects R \ R x x" unfolding Respects_def by simp -subsection {* Invariant *} - -definition eq_onp :: "('a \ bool) \ 'a \ 'a \ bool" - where "eq_onp R = (\x y. R x \ x = y)" - -lemma eq_onp_to_eq: - assumes "eq_onp P x y" - shows "x = y" -using assms by (simp add: eq_onp_def) - -lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\f. \x. P(f x))" -unfolding eq_onp_def rel_fun_def by auto - -lemma rel_fun_eq_onp_rel: - shows "((eq_onp R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" -by (auto simp add: eq_onp_def rel_fun_def) - -lemma eq_onp_same_args: - shows "eq_onp P x x \ P x" -using assms by (auto simp add: eq_onp_def) - -lemma eq_onp_transfer [transfer_rule]: - assumes [transfer_rule]: "bi_unique A" - 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" and T_def: "T \ (\x y. x = Rep y)" @@ -574,6 +553,8 @@ declare fun_mono[relator_mono] lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2 +ML_file "Tools/Lifting/lifting_bnf.ML" + ML_file "Tools/Lifting/lifting_term.ML" ML_file "Tools/Lifting/lifting_def.ML"