Quotient Package: make quotient_type work with separate set type
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue Aug 16 07:17:15 2011 +0900 (2011-08-16)
changeset 442043cdc4176638c
parent 44203 77881904ee91
child 44220 e5753e2a5944
Quotient Package: make quotient_type work with separate set type
src/HOL/Equiv_Relations.thy
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Tools/Quotient/quotient_typ.ML
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Aug 15 22:31:17 2011 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Tue Aug 16 07:17:15 2011 +0900
     1.3 @@ -402,8 +402,8 @@
     1.4    by (erule part_equivpE, erule transpE)
     1.5  
     1.6  lemma part_equivp_typedef:
     1.7 -  "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
     1.8 -  by (auto elim: part_equivpE simp add: mem_def)
     1.9 +  "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}"
    1.10 +  by (auto elim: part_equivpE)
    1.11  
    1.12  
    1.13  text {* Total equivalences *}
     2.1 --- a/src/HOL/Quotient.thy	Mon Aug 15 22:31:17 2011 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Tue Aug 16 07:17:15 2011 +0900
     2.3 @@ -603,66 +603,52 @@
     2.4  
     2.5  locale quot_type =
     2.6    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     2.7 -  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
     2.8 -  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
     2.9 +  and   Abs :: "'a set \<Rightarrow> 'b"
    2.10 +  and   Rep :: "'b \<Rightarrow> 'a set"
    2.11    assumes equivp: "part_equivp R"
    2.12 -  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
    2.13 +  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)"
    2.14    and     rep_inverse: "\<And>x. Abs (Rep x) = x"
    2.15 -  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
    2.16 +  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c"
    2.17    and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
    2.18  begin
    2.19  
    2.20  definition
    2.21    abs :: "'a \<Rightarrow> 'b"
    2.22  where
    2.23 -  "abs x = Abs (R x)"
    2.24 +  "abs x = Abs (Collect (R x))"
    2.25  
    2.26  definition
    2.27    rep :: "'b \<Rightarrow> 'a"
    2.28  where
    2.29 -  "rep a = Eps (Rep a)"
    2.30 -
    2.31 -lemma homeier5:
    2.32 -  assumes a: "R r r"
    2.33 -  shows "Rep (Abs (R r)) = R r"
    2.34 -  apply (subst abs_inverse)
    2.35 -  using a by auto
    2.36 +  "rep a = (SOME x. x \<in> Rep a)"
    2.37  
    2.38 -theorem homeier6:
    2.39 -  assumes a: "R r r"
    2.40 -  and b: "R s s"
    2.41 -  shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
    2.42 -  by (metis a b homeier5)
    2.43 -
    2.44 -theorem homeier8:
    2.45 +lemma some_collect:
    2.46    assumes "R r r"
    2.47 -  shows "R (Eps (R r)) = R r"
    2.48 -  using assms equivp[simplified part_equivp_def]
    2.49 -  apply clarify
    2.50 -  by (metis assms exE_some)
    2.51 +  shows "R (SOME x. x \<in> Collect (R r)) = R r"
    2.52 +  apply simp
    2.53 +  by (metis assms exE_some equivp[simplified part_equivp_def])
    2.54  
    2.55  lemma Quotient:
    2.56    shows "Quotient R abs rep"
    2.57    unfolding Quotient_def abs_def rep_def
    2.58    proof (intro conjI allI)
    2.59      fix a r s
    2.60 -    show "Abs (R (Eps (Rep a))) = a"
    2.61 -      using [[metis_new_skolemizer = false]]
    2.62 -      by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
    2.63 -    show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
    2.64 -      by (metis homeier6 equivp[simplified part_equivp_def])
    2.65 -    show "R (Eps (Rep a)) (Eps (Rep a))" proof -
    2.66 -      obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto
    2.67 -      have "R (Eps (R x)) x" using homeier8 r by simp
    2.68 -      then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast
    2.69 -      then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp
    2.70 -      then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp
    2.71 +    show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
    2.72 +      obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
    2.73 +      have "R (SOME x. x \<in> Rep a) x"  using r rep some_collect by metis
    2.74 +      then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
    2.75 +      then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
    2.76 +        using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`)
    2.77      qed
    2.78 -  qed
    2.79 -
    2.80 +    have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
    2.81 +    then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
    2.82 +    have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
    2.83 +      by (metis Collect_def abs_inverse)
    2.84 +    then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
    2.85 +      using equivp[simplified part_equivp_def] by metis
    2.86 +    qed
    2.87  end
    2.88  
    2.89 -
    2.90  subsection {* ML setup *}
    2.91  
    2.92  text {* Auxiliary data for the quotient package *}
     3.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Mon Aug 15 22:31:17 2011 +0200
     3.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Aug 16 07:17:15 2011 +0900
     3.3 @@ -561,9 +561,9 @@
     3.4    shows "fset S = fset T \<longleftrightarrow> S = T"
     3.5    by (descending) (simp)
     3.6  
     3.7 -lemma filter_fset [simp]: 
     3.8 -  shows "fset (filter_fset P xs) = P \<inter> fset xs"
     3.9 -  by (descending) (auto simp add: mem_def)
    3.10 +lemma filter_fset [simp]:
    3.11 +  shows "fset (filter_fset P xs) = Collect P \<inter> fset xs"
    3.12 +  by (descending) (auto)
    3.13  
    3.14  lemma remove_fset [simp]: 
    3.15    shows "fset (remove_fset x xs) = fset xs - {x}"
     4.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Aug 15 22:31:17 2011 +0200
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Tue Aug 16 07:17:15 2011 +0900
     4.3 @@ -48,8 +48,8 @@
     4.4  
     4.5  (*** definition of quotient types ***)
     4.6  
     4.7 -val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
     4.8 -val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}
     4.9 +val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
    4.10 +val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
    4.11  
    4.12  (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
    4.13  fun typedef_term rel rty lthy =
    4.14 @@ -58,9 +58,14 @@
    4.15        [("x", rty), ("c", HOLogic.mk_setT rty)]
    4.16        |> Variable.variant_frees lthy [rel]
    4.17        |> map Free
    4.18 +    fun mk_collect T =
    4.19 +      Const (@{const_name Collect}, (T --> @{typ bool}) --> HOLogic.mk_setT T)
    4.20 +    val collect_in = mk_collect rty
    4.21 +    val collect_out = mk_collect (HOLogic.mk_setT rty)
    4.22    in
    4.23 -    lambda c (HOLogic.exists_const rty $
    4.24 -        lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
    4.25 +    collect_out $ (lambda c (HOLogic.exists_const rty $
    4.26 +        lambda x (HOLogic.mk_conj (rel $ x $ x,
    4.27 +        HOLogic.mk_eq (c, collect_in $ (rel $ x))))))
    4.28    end
    4.29  
    4.30