# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255381574 -7200
# Node ID c0c41fefeb0601682074948583f134e18983ec9e
# Parent  2374d50fc6dd20f7c9bae8f188b56eaa53135b29
added quotient command (you need to update isar-keywords-prove.el)

diff -r 2374d50fc6dd -r c0c41fefeb06 Prove.thy
--- a/Prove.thy	Mon Oct 12 22:44:16 2009 +0200
+++ b/Prove.thy	Mon Oct 12 23:06:14 2009 +0200
@@ -1,7 +1,148 @@
 theory Prove
-imports Main
+imports Main QuotScript QuotList
+uses ("quotient.ML")
+begin
+
+locale QUOT_TYPE =
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+  assumes equiv: "EQUIV R"
+  and     rep_prop: "\<And>y. \<exists>x. 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     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
 begin
 
+definition
+  "ABS x \<equiv> Abs (R x)"
+
+definition
+  "REP a = Eps (Rep a)"
+
+lemma lem9:
+  shows "R (Eps (R x)) = R x"
+proof -
+  have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
+  then have "R x (Eps (R x))" by (rule someI)
+  then show "R (Eps (R x)) = R x"
+    using equiv unfolding EQUIV_def by simp
+qed
+
+theorem thm10:
+  shows "ABS (REP a) \<equiv> a"
+  apply  (rule eq_reflection)
+  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 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 REP_refl:
+  shows "R (REP a) (REP a)"
+unfolding REP_def
+by (simp add: equiv[simplified EQUIV_def])
+
+lemma lem7:
+  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
+apply(rule iffI)
+apply(simp)
+apply(drule rep_inject[THEN iffD2])
+apply(simp add: abs_inverse)
+done
+
+theorem thm11:
+  shows "R r r' = (ABS r = ABS r')"
+unfolding ABS_def
+by (simp only: equiv[simplified EQUIV_def] lem7)
+
+
+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: thm10 thm11)
+
+lemma QUOTIENT:
+  "QUOTIENT R ABS REP"
+apply(unfold QUOTIENT_def)
+apply(simp add: thm10)
+apply(simp add: REP_refl)
+apply(subst thm11[symmetric])
+apply(simp add: equiv[simplified EQUIV_def])
+done
+
+lemma R_trans:
+  assumes ab: "R a b"
+  and     bc: "R b c"
+  shows "R a c"
+proof -
+  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+  moreover have ab: "R a b" by fact
+  moreover have bc: "R b c" by fact
+  ultimately show "R a c" unfolding TRANS_def by blast
+qed
+
+lemma R_sym:
+  assumes ab: "R a b"
+  shows "R b a"
+proof -
+  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+  then show "R b a" using ab unfolding SYM_def by blast
+qed
+
+lemma R_trans2:
+  assumes ac: "R a c"
+  and     bd: "R b d"
+  shows "R a b = R c d"
+proof
+  assume "R a b"
+  then have "R b a" using R_sym by blast
+  then have "R b c" using ac R_trans by blast
+  then have "R c b" using R_sym by blast
+  then show "R c d" using bd R_trans by blast
+next
+  assume "R c d"
+  then have "R a d" using ac R_trans by blast
+  then have "R d a" using R_sym by blast
+  then have "R b a" using bd R_trans by blast
+  then show "R a b" using R_sym by blast
+qed
+
+lemma REPS_same:
+  shows "R (REP a) (REP b) \<equiv> (a = b)"
+proof -
+  have "R (REP a) (REP b) = (a = b)"
+  proof
+    assume as: "R (REP a) (REP b)"
+    from rep_prop
+    obtain x y
+      where eqs: "Rep a = R x" "Rep b = R y" by blast
+    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+    then have "R x (Eps (R y))" using lem9 by simp
+    then have "R (Eps (R y)) x" using R_sym by blast
+    then have "R y x" using lem9 by simp
+    then have "R x y" using R_sym by blast
+    then have "ABS x = ABS y" using thm11 by simp
+    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+    then show "a = b" using rep_inverse by simp
+  next
+    assume ab: "a = b"
+    have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+    then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+  qed
+  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
+qed
+
+end
+
+use "quotient.ML"
+
 ML {*
 val r = ref (NONE:(unit -> term) option)
 *}
diff -r 2374d50fc6dd -r c0c41fefeb06 QuotMain.thy
--- a/QuotMain.thy	Mon Oct 12 22:44:16 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 23:06:14 2009 +0200
@@ -3,7 +3,6 @@
 uses ("quotient.ML")
 begin
 
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -143,9 +142,24 @@
 end
 
 section {* type definition for the quotient type *}
+ML {* Binding.name *}
+
+ML {* cat_lines *}
 
 use "quotient.ML"
 
+ML {*
+  mk_typedef;
+  mk_typedef_cmd;
+  quottype_parser
+*}
+
+ML {* Proof.theorem_i *}
+
+term EQUIV
+
+ML {* quottype_parser *}
+ML {* OuterSyntax.local_theory_to_proof *}
 
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -166,16 +180,24 @@
 where
   r_eq: "EQUIV RR"
 
+quotient qtrm = "trm" / "RR"
+  apply(rule r_eq)
+  done
+
+(*
 local_setup {*
   typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
 *}
+*)
 
+typ qtrm
 term Rep_qtrm
 term REP_qtrm
 term Abs_qtrm
 term ABS_qtrm
 thm QUOT_TYPE_qtrm
 thm QUOTIENT_qtrm
+thm REP_qtrm_def
 
 (* Test interpretation *)
 thm QUOT_TYPE_I_qtrm.thm11
@@ -194,10 +216,15 @@
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
-
+(*
 local_setup {*
   typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
 *}
+*)
+
+quotient "'a qtrm'" = "'a trm'" / "R'"
+  apply(rule r_eq')
+  done
 
 print_theorems
 
@@ -217,9 +244,14 @@
 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
 axioms t_eq: "EQUIV Rt"
 
+(*
 local_setup {*
   typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
 *}
+*)
+
+quotient "qt" = "t" / "Rt"
+  by (rule t_eq)
 
 section {* lifting of constants *}
 
@@ -381,7 +413,7 @@
   val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
   val def_trm = get_const_def nconst oconst rty qty lthy
 in
-  make_def (nconst_bname, mx, def_trm) lthy
+  define (nconst_bname, mx, def_trm) lthy
 end
 *}
 
@@ -408,10 +440,15 @@
 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 axioms t_eq': "EQUIV Rt'"
 
-
+(*
 local_setup {*
   typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
 *}
+*)
+
+quotient "'a qt'" = "'a t'" / "Rt'"
+  apply(rule t_eq')
+  done
 
 print_theorems
 
@@ -454,9 +491,15 @@
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
+(*
 local_setup {*
   typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
 *}
+*)
+
+quotient "'a fset" = "'a list" / "list_eq"
+  apply(rule equiv_list_eq)
+  done
 
 print_theorems
 
diff -r 2374d50fc6dd -r c0c41fefeb06 quotient.ML
--- a/quotient.ML	Mon Oct 12 22:44:16 2009 +0200
+++ b/quotient.ML	Mon Oct 12 23:06:14 2009 +0200
@@ -1,13 +1,11 @@
-
-
 
 structure Quotient =
 struct
 
-(* constructs the term lambda (c::rty => bool). EX x. c= rel x *)
+(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
 let
-  val [x, c] = [("x", rty), ("c", rty --> @{typ bool})]
+  val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)]
                |> Variable.variant_frees lthy [rel]
                |> map Free
 in
@@ -80,7 +78,7 @@
 end
 
 (* two wrappers for define and note *)
-fun make_def (name, mx, rhs) lthy =
+fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
      LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy
@@ -88,7 +86,7 @@
   ((rhs, thm), lthy')
 end
 
-fun note_thm (name, thm) lthy =
+fun note (name, thm) lthy =
 let
   val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
 in
@@ -117,8 +115,8 @@
   val ABS_name = Binding.prefix_name "ABS_" qty_name
   val REP_name = Binding.prefix_name "REP_" qty_name
   val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
-         lthy1 |> make_def (ABS_name, NoSyn, ABS_trm)
-               ||>> make_def (REP_name, NoSyn, REP_trm)
+         lthy1 |> define (ABS_name, NoSyn, ABS_trm)
+               ||>> define (REP_name, NoSyn, REP_trm)
 
   (* quot_type theorem *)
   val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2
@@ -151,8 +149,8 @@
     ]))]
 in
   lthy4
-  |> note_thm (quot_thm_name, quot_thm)
-  ||>> note_thm (quotient_thm_name, quotient_thm)
+  |> note (quot_thm_name, quot_thm)
+  ||>> note (quotient_thm_name, quotient_thm)
   ||> LocalTheory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
@@ -165,23 +163,53 @@
 (* syntax setup *)
 local structure P = OuterParse in
 
+fun mk_typedef (qty, mx, rty, rel_trm) lthy = 
+let
+  val (qty_name, _) = Term.dest_Type qty 
+
+  val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+  val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm)
+		   
+  val _ = [Syntax.string_of_term lthy EQUIV_goal,
+           Syntax.string_of_typ lthy (fastype_of rel_trm),
+           Syntax.string_of_typ lthy EQUIV_ty]
+          |> cat_lines
+          |> tracing
+ 
+  fun after_qed thms lthy =
+  let
+    val thm = the_single (flat thms)
+  in
+    typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd   
+  end
+in
+  Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy
+end
+
 val quottype_parser = 
-    (P.type_args -- P.binding) -- 
-      P.opt_infix -- 
-       (P.$$$ "=" |-- P.term) -- 
+    P.typ -- P.opt_infix -- 
+       (P.$$$ "=" |-- P.typ) -- 
          (P.$$$ "/" |-- P.term)
            
-(*
-val _ =
-  OuterSyntax.command "quotient" "quotient type definition (requires equivalence proof)"
-    OuterKeyword.thy_goal
-    (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
+fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = 
+let
+  val qty = Syntax.parse_typ lthy qstr
+  val rty = Syntax.parse_typ lthy rstr
+  val rel_trm = Syntax.parse_term lthy rel_str
+                |> Syntax.check_term lthy
+in
+  mk_typedef (qty, mx, rty, rel_trm) lthy  
+end
 
-end;
-*)
+val _ = OuterKeyword.keyword "/"
 
-end;
+val _ = 
+    OuterSyntax.local_theory_to_proof "quotient" 
+      "quotient type definition (requires equivalence proof)"
+         OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd)	     
 
-end;
+end; (* local *)
+
+end; (* structure *)
 
 open Quotient
\ No newline at end of file