# HG changeset patch # User Cezary Kaliszyk # Date 1313446635 -32400 # Node ID 3cdc4176638cd0e0badaba7fb9aaa9b5afa8ba52 # Parent 77881904ee91d3945b5b095c83bdb67ed2a0eeb0 Quotient Package: make quotient_type work with separate set type diff -r 77881904ee91 -r 3cdc4176638c src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Mon Aug 15 22:31:17 2011 +0200 +++ b/src/HOL/Equiv_Relations.thy Tue Aug 16 07:17:15 2011 +0900 @@ -402,8 +402,8 @@ by (erule part_equivpE, erule transpE) lemma part_equivp_typedef: - "part_equivp R \ \d. d \ (\c. \x. R x x \ c = R x)" - by (auto elim: part_equivpE simp add: mem_def) + "part_equivp R \ \d. d \ {c. \x. R x x \ c = Collect (R x)}" + by (auto elim: part_equivpE) text {* Total equivalences *} diff -r 77881904ee91 -r 3cdc4176638c src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Mon Aug 15 22:31:17 2011 +0200 +++ b/src/HOL/Quotient.thy Tue Aug 16 07:17:15 2011 +0900 @@ -603,66 +603,52 @@ locale quot_type = fixes R :: "'a \ 'a \ bool" - and Abs :: "('a \ bool) \ 'b" - and Rep :: "'b \ ('a \ bool)" + and Abs :: "'a set \ 'b" + and Rep :: "'b \ 'a set" assumes equivp: "part_equivp R" - and rep_prop: "\y. \x. R x x \ Rep y = R x" + and rep_prop: "\y. \x. R x x \ Rep y = Collect (R x)" and rep_inverse: "\x. Abs (Rep x) = x" - and abs_inverse: "\c. (\x. ((R x x) \ (c = R x))) \ (Rep (Abs c)) = c" + and abs_inverse: "\c. (\x. ((R x x) \ (c = Collect (R x)))) \ (Rep (Abs c)) = c" and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" begin definition abs :: "'a \ 'b" where - "abs x = Abs (R x)" + "abs x = Abs (Collect (R x))" definition rep :: "'b \ 'a" where - "rep a = Eps (Rep a)" - -lemma homeier5: - assumes a: "R r r" - shows "Rep (Abs (R r)) = R r" - apply (subst abs_inverse) - using a by auto + "rep a = (SOME x. x \ Rep a)" -theorem homeier6: - assumes a: "R r r" - and b: "R s s" - shows "Abs (R r) = Abs (R s) \ R r = R s" - by (metis a b homeier5) - -theorem homeier8: +lemma some_collect: assumes "R r r" - shows "R (Eps (R r)) = R r" - using assms equivp[simplified part_equivp_def] - apply clarify - by (metis assms exE_some) + shows "R (SOME x. x \ Collect (R r)) = R r" + apply simp + by (metis assms exE_some equivp[simplified part_equivp_def]) lemma Quotient: shows "Quotient R abs rep" unfolding Quotient_def abs_def rep_def proof (intro conjI allI) fix a r s - show "Abs (R (Eps (Rep a))) = a" - using [[metis_new_skolemizer = false]] - by (metis equivp exE_some part_equivp_def rep_inverse rep_prop) - show "R r s \ R r r \ R s s \ (Abs (R r) = Abs (R s))" - by (metis homeier6 equivp[simplified part_equivp_def]) - show "R (Eps (Rep a)) (Eps (Rep a))" proof - - obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto - have "R (Eps (R x)) x" using homeier8 r by simp - then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast - then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp - then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp + show x: "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" proof - + obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto + have "R (SOME x. x \ Rep a) x" using r rep some_collect by metis + then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast + then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" + using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \ Rep a) x`) qed - qed - + have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) + then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto + have "R r r \ R s s \ Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" + by (metis Collect_def abs_inverse) + then show "R r s \ R r r \ R s s \ (Abs (Collect (R r)) = Abs (Collect (R s)))" + using equivp[simplified part_equivp_def] by metis + qed end - subsection {* ML setup *} text {* Auxiliary data for the quotient package *} diff -r 77881904ee91 -r 3cdc4176638c src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Mon Aug 15 22:31:17 2011 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Aug 16 07:17:15 2011 +0900 @@ -561,9 +561,9 @@ shows "fset S = fset T \ S = T" by (descending) (simp) -lemma filter_fset [simp]: - shows "fset (filter_fset P xs) = P \ fset xs" - by (descending) (auto simp add: mem_def) +lemma filter_fset [simp]: + shows "fset (filter_fset P xs) = Collect P \ fset xs" + by (descending) (auto) lemma remove_fset [simp]: shows "fset (remove_fset x xs) = fset xs - {x}" diff -r 77881904ee91 -r 3cdc4176638c src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Mon Aug 15 22:31:17 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Tue Aug 16 07:17:15 2011 +0900 @@ -48,8 +48,8 @@ (*** definition of quotient types ***) -val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} -val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} +val mem_def1 = @{lemma "y : Collect S ==> S y" by simp} +val mem_def2 = @{lemma "S y ==> y : Collect S" by simp} (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) fun typedef_term rel rty lthy = @@ -58,9 +58,14 @@ [("x", rty), ("c", HOLogic.mk_setT rty)] |> Variable.variant_frees lthy [rel] |> map Free + fun mk_collect T = + Const (@{const_name Collect}, (T --> @{typ bool}) --> HOLogic.mk_setT T) + val collect_in = mk_collect rty + val collect_out = mk_collect (HOLogic.mk_setT rty) in - lambda c (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x)))) + collect_out $ (lambda c (HOLogic.exists_const rty $ + lambda x (HOLogic.mk_conj (rel $ x $ x, + HOLogic.mk_eq (c, collect_in $ (rel $ x)))))) end