src/HOL/Lifting.thy
 changeset 56524 f4ba736040fa parent 56519 c1048f5bbb45 child 57398 882091eb1e9a
```     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"
```