Quotient package now uses Partial Equivalence instead place of equivalence

--- a/src/HOL/Quotient.thy	Wed Jun 23 08:42:41 2010 +0200
+++ b/src/HOL/Quotient.thy	Wed Jun 23 08:44:44 2010 +0200
@@ -59,7 +59,7 @@
   unfolding equivp_def
   by auto
 
-text {* Partial equivalences: not yet used anywhere *}
+text {* Partial equivalences *}
 
 definition
   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
@@ -71,6 +71,23 @@
   unfolding equivp_def part_equivp_def
   by auto
 
+lemma part_equivp_symp:
+  assumes e: "part_equivp R"
+  and a: "R x y"
+  shows "R y x"
+  using e[simplified part_equivp_def] a
+  by (metis)
+
+lemma part_equivp_typedef:
+  shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
+  unfolding part_equivp_def mem_def
+  apply clarify
+  apply (intro exI)
+  apply (rule conjI)
+  apply assumption
+  apply (rule refl)
+  done
+
 text {* Composition of Relations *}
 
 abbreviation
@@ -630,10 +647,10 @@
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
-  assumes equivp: "equivp R"
-  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+  assumes equivp: "part_equivp R"
+  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
   and     rep_inverse: "\<And>x. Abs (Rep x) = x"
-  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
   and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
 begin
 
@@ -647,64 +664,46 @@
 where
   "rep a = Eps (Rep a)"
 
-lemma homeier_lem9:
-  shows "R (Eps (R x)) = R x"
-proof -
-  have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
-  then have "R x (Eps (R x))" by (rule someI)
-  then show "R (Eps (R x)) = R x"
-    using equivp unfolding equivp_def by simp
-qed
-
-theorem homeier_thm10:
-  shows "abs (rep a) = a"
-  unfolding abs_def rep_def
-proof -
-  from rep_prop
-  obtain x where eq: "Rep a = R x" by auto
-  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
-  also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
-  also have "\<dots> = Abs (Rep a)" using eq by simp
-  also have "\<dots> = a" using rep_inverse by simp
-  finally
-  show "Abs (R (Eps (Rep a))) = a" by simp
-qed
+lemma homeier5:
+  assumes a: "R r r"
+  shows "Rep (Abs (R r)) = R r"
+  apply (subst abs_inverse)
+  using a by auto
 
-lemma homeier_lem7:
-  shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
-proof -
-  have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
-  also have "\<dots> = ?LHS" by (simp add: abs_inverse)
-  finally show "?LHS = ?RHS" by simp
-qed
+theorem homeier6:
+  assumes a: "R r r"
+  and b: "R s s"
+  shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
+  by (metis a b homeier5)
 
-theorem homeier_thm11:
-  shows "R r r' = (abs r = abs r')"
-  unfolding abs_def
-  by (simp only: equivp[simplified equivp_def] homeier_lem7)
-
-lemma rep_refl:
-  shows "R (rep a) (rep a)"
-  unfolding rep_def
-  by (simp add: equivp[simplified equivp_def])
-
-
-lemma rep_abs_rsp:
-  shows "R f (rep (abs g)) = R f g"
-  and   "R (rep (abs g)) f = R g f"
-  by (simp_all add: homeier_thm10 homeier_thm11)
+theorem homeier8:
+  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)
 
 lemma Quotient:
   shows "Quotient R abs rep"
-  unfolding Quotient_def
-  apply(simp add: homeier_thm10)
-  apply(simp add: rep_refl)
-  apply(subst homeier_thm11[symmetric])
-  apply(simp add: equivp[simplified equivp_def])
-  done
+  unfolding Quotient_def abs_def rep_def
+  proof (intro conjI allI)
+    fix a r s
+    show "Abs (R (Eps (Rep a))) = a"
+      by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
+    show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (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
+    qed
+  qed
 
 end
 
+
 subsection {* ML setup *}
 
 text {* Auxiliary data for the quotient package *}

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jun 23 08:42:41 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jun 23 08:44:44 2010 +0200
@@ -147,6 +147,14 @@
   finally jump back to 1
 *)
 
+fun reflp_get ctxt =
+  map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
+    handle THM _ => NONE) (equiv_rules_get ctxt)
+
+val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
+
+fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
+
 fun regularize_tac ctxt =
 let
   val thy = ProofContext.theory_of ctxt
@@ -157,8 +165,7 @@
                        addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
                        addsimprocs [simproc]
                        addSolver equiv_solver addSolver quotient_solver
-  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
-  val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
+  val eq_eqvs = eq_imp_rel_get ctxt
 in
   simp_tac simpset THEN'
   REPEAT_ALL_NEW (CHANGED o FIRST'
@@ -254,7 +261,7 @@
              val inst_thm = Drule.instantiate' ty_inst
                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
            in
-             (rtac inst_thm THEN' quotient_tac context) 1
+             (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
            end
     | _ => no_tac
   end)
@@ -406,7 +413,7 @@
 
 fun injection_tac ctxt =
 let
-  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
+  val rel_refl = reflp_get ctxt
 in
   injection_step_tac ctxt rel_refl
 end

--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Jun 23 08:42:41 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Jun 23 08:44:44 2010 +0200
@@ -7,13 +7,13 @@
 
 signature QUOTIENT_TYPE =
 sig
-  val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm
+  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
     -> Proof.context -> (thm * thm) * local_theory
 
-  val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
+  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
     -> Proof.context -> Proof.state
 
-  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list
+  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * (bool * string)) list
     -> Proof.context -> Proof.state
 end;
 
@@ -64,15 +64,15 @@
     |> map Free
 in
   lambda c (HOLogic.exists_const rty $
-     lambda x (HOLogic.mk_eq (c, (rel $ x))))
+     lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x))))))
 end
 
 
 (* makes the new type definitions and proves non-emptyness *)
-fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
+fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
 let
   val typedef_tac =
-    EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
+    EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
 in
 (* FIXME: purely local typedef causes at the moment 
    problems with type variables
@@ -93,14 +93,14 @@
 let
   val rep_thm = #Rep typedef_info RS mem_def1
   val rep_inv = #Rep_inverse typedef_info
-  val abs_inv = mem_def2 RS #Abs_inverse typedef_info
+  val abs_inv = #Abs_inverse typedef_info
   val rep_inj = #Rep_inject typedef_info
 in
   (rtac @{thm quot_type.intro} THEN' RANGE [
     rtac equiv_thm,
     rtac rep_thm,
     rtac rep_inv,
-    EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]),
+    rtac abs_inv THEN' rtac mem_def2 THEN' atac,
     rtac rep_inj]) 1
 end
 
@@ -137,10 +137,12 @@
 
 
 (* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
 let
+  val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp}
+
   (* generates the typedef *)
-  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
+  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
 
   (* abs and rep functions from the typedef *)
   val Abs_ty = #abs_type (#1 typedef_info)
@@ -162,7 +164,7 @@
   val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
 
   (* quot_type theorem *)
-  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
+  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
 
   (* quotient theorem *)
   val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
@@ -179,12 +181,12 @@
 in
   lthy4
   |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
-  ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add])
+  ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
 end
 
 
 (* sanity checks for the quotient type specifications *)
-fun sanity_check ((vs, qty_name, _), (rty, rel)) =
+fun sanity_check ((vs, qty_name, _), (rty, rel, _)) =
 let
   val rty_tfreesT = map fst (Term.add_tfreesT rty [])
   val rel_tfrees = map fst (Term.add_tfrees rel [])
@@ -223,7 +225,7 @@
 end
 
 (* check for existence of map functions *)
-fun map_check ctxt (_, (rty, _)) =
+fun map_check ctxt (_, (rty, _, _)) =
 let
   val thy = ProofContext.theory_of ctxt
 
@@ -263,11 +265,12 @@
   val _ = List.app sanity_check quot_list
   val _ = List.app (map_check lthy) quot_list
 
-  fun mk_goal (rty, rel) =
+  fun mk_goal (rty, rel, partial) =
   let
     val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+    val const = if partial then @{const_name part_equivp} else @{const_name equivp}
   in
-    HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
+    HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   end
 
   val goals = map (mk_goal o snd) quot_list
@@ -280,7 +283,7 @@
 
 fun quotient_type_cmd specs lthy =
 let
-  fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
+  fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
   let
     val rty = Syntax.read_typ lthy rty_str
     val lthy1 = Variable.declare_typ rty lthy
@@ -290,7 +293,7 @@
       |> Syntax.check_term lthy1 
     val lthy2 = Variable.declare_term rel lthy1 
   in
-    (((vs, qty_name, mx), (rty, rel)), lthy2)
+    (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
   end
 
   val (spec', lthy') = fold_map parse_spec specs lthy
@@ -298,11 +301,13 @@
   quotient_type spec' lthy'
 end
 
+val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
+
 val quotspec_parser =
-    Parse.and_list1
-     ((Parse.type_args -- Parse.binding) --
-        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
-         (Parse.$$$ "/" |-- Parse.term))
+  Parse.and_list1
+    ((Parse.type_args -- Parse.binding) --
+      Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
+        (Parse.$$$ "/" |-- (partial -- Parse.term)))
 
 val _ = Keyword.keyword "/"