
diff -r 3feed4dbfa45 -r 53984a386999 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 15:19:39 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 15:20:06 2009 +0100
@@ -9,7 +9,7 @@
   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"
+  assumes equiv: "equivp 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)"
@@ -29,10 +29,10 @@
 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)
+  have a: "R x x" using equiv 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 equiv unfolding EQUIV_def by simp
+    using equiv unfolding equivp_def by simp
 qed
 
 theorem thm10:
@@ -53,7 +53,7 @@
 lemma REP_refl:
   shows "R (REP a) (REP a)"
 unfolding REP_def
-by (simp add: equiv[simplified EQUIV_def])
+by (simp add: equiv[simplified equivp_def])
 
 lemma lem7:
   shows "(R x = R y) = (Abs (R x) = Abs (R y))"
@@ -66,7 +66,7 @@
 theorem thm11:
   shows "R r r' = (ABS r = ABS r')"
 unfolding ABS_def
-by (simp only: equiv[simplified EQUIV_def] lem7)
+by (simp only: equiv[simplified equivp_def] lem7)
 
 
 lemma REP_ABS_rsp:
@@ -74,13 +74,13 @@
   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)
+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])
+apply(simp add: equiv[simplified equivp_def])
 done
 
 lemma R_trans:
@@ -88,18 +88,18 @@
   and     bc: "R b c"
   shows "R a c"
 proof -
-  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+  have tr: "transp R" using equiv equivp_reflp_symp_transp[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
+  ultimately show "R a c" unfolding transp_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
+  have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp
+  then show "R b a" using ab unfolding symp_def by blast
 qed
 
 lemma R_trans2:
@@ -128,8 +128,8 @@
     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
+    have "reflp R" using equiv equivp_reflp_symp_transp[of R] by simp
+    then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
   qed
   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
 qed
@@ -146,7 +146,7 @@
 declare [[map "fun" = (fun_map, FUN_REL)]]
 
 lemmas [quotient_thm] = 
-  FUN_QUOTIENT LIST_QUOTIENT
+  FUN_Quotient LIST_Quotient
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
@@ -265,7 +265,7 @@
     val rty = Logic.unvarifyT (#rtyp quotdata)
     val rel = #rel quotdata
     val rel_eqv = #equiv_thm quotdata
-    val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv]
+    val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
   in
     (rty, rel, rel_refl, rel_eqv)
   end
@@ -278,7 +278,7 @@
     val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
     val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
     val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
-    val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
+    val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
   in
     (trans2, reps_same, absrep, quot)
   end
@@ -455,13 +455,13 @@
 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
 by auto
 
-(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
+(* FIXME: OPTION_equivp, PAIR_equivp, ... *)
 ML {*
 fun equiv_tac rel_eqvs =
   REPEAT_ALL_NEW (FIRST' 
     [resolve_tac rel_eqvs,
-     rtac @{thm IDENTITY_EQUIV},
-     rtac @{thm LIST_EQUIV}])
+     rtac @{thm IDENTITY_equivp},
+     rtac @{thm LIST_equivp}])
 *}
 
 ML {*
@@ -474,7 +474,7 @@
       (ogl as ((Const (@{const_name "Ball"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
@@ -498,7 +498,7 @@
       (ogl as ((Const (@{const_name "Bex"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
@@ -542,7 +542,7 @@
       (ogl as ((Const (@{const_name "Ball"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 (*        val _ = tracing (Syntax.string_of_term ctxt glc);*)
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
@@ -573,7 +573,7 @@
       (ogl as ((Const (@{const_name "Bex"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 (*        val _ = tracing (Syntax.string_of_term ctxt glc); *)
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
@@ -594,8 +594,8 @@
   end
 *}
 
-lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
-by (simp add: EQUIV_REFL)
+lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+by (simp add: equivp_reflp)
 
 ML {*
 fun regularize_tac ctxt rel_eqvs =
@@ -724,7 +724,7 @@
 ML {*
 fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm IDENTITY_QUOTIENT},
+    [rtac @{thm IDENTITY_Quotient},
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
@@ -776,7 +776,7 @@
   end
 *}
 
-(* It proves the QUOTIENT assumptions by calling quotient_tac *)
+(* It proves the Quotient assumptions by calling quotient_tac *)
 ML {*
 fun solve_quotient_assum i ctxt thm =
   let
@@ -1088,7 +1088,7 @@
  - Rewriting with definitions from the argument defs
      NewConst  ---->  (rep ---> abs) oldConst
 
- - QUOTIENT_REL_REP:
+ - Quotient_REL_REP:
      Rel (Rep x) (Rep y)  ---->  x = y
 
  - ABS_REP
@@ -1107,9 +1107,9 @@
     val thy = ProofContext.theory_of lthy;
     val quotients = quotient_rules_get lthy
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-    val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients
+    val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
-    val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients
+    val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
@@ -1237,7 +1237,7 @@
     let
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
-      val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
+      val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv
       val quotients = quotient_rules_get lthy
       val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
       val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}




