--- a/QuotMain.thy Fri Dec 04 15:04:05 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 15:18:33 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}