nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:f51e2b3e3149
+:6348c2a57ec2
 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"
+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)"
 and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
 begin
 "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)
+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:
 shows "ABS (REP a) \<equiv> a"
 apply  (rule eq_reflection)
 qed
 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))"
 apply(rule iffI)
 apply(simp)
 done
 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:
 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:
+lemma Quotient:
-"QUOTIENT R ABS REP"
+"Quotient R ABS REP"
-apply(unfold QUOTIENT_def)
+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:
 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
+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
+have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp
-then show "R b a" using ab unfolding SYM_def by blast
+then show "R b a" using ab unfolding symp_def by blast
 qed
 lemma R_trans2:
 assumes ac: "R a c"
 and     bd: "R b d"
 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
+have "reflp R" using equiv equivp_reflp_symp_transp[of R] by simp
-then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+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
 end
 declare [[map list = (map, LIST_REL)]]
 declare [[map * = (prod_fun, prod_rel)]]
 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} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
 (* cu: Changed the lookup\<dots>not sure whether this works *)
 (* TODO: Should no longer be needed *)
 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
 *}
 let
 val thy = ProofContext.theory_of lthy;
 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
 *}
 by blast
 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 IDENTITY_equivp},
-rtac @{thm LIST_EQUIV}])
+rtac @{thm LIST_equivp}])
 *}
 ML {*
 fun ball_reg_eqv_simproc rel_eqvs ss redex =
 let
 in
 case redex of
 (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]]);
 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
 in
 in
 case redex of
 (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]]);
 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
 in
 in
 case redex of
 (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);
 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
 val R1c = cterm_of thy R1;
 in
 case redex of
 (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);
 val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
 val R1c = cterm_of thy R1;
 )
 | _ => NONE
 end
 *}
-lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
+lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
-by (simp add: EQUIV_REFL)
+by (simp add: equivp_reflp)
 ML {*
 fun regularize_tac ctxt rel_eqvs =
 let
 val pat1 = [@{term "Ball (Respects R) P"}];
 *}
 ML {*
 fun quotient_tac ctxt =
 REPEAT_ALL_NEW (FIRST'
-[rtac @{thm IDENTITY_QUOTIENT},
+[rtac @{thm IDENTITY_Quotient},
 resolve_tac (quotient_rules_get ctxt)])
 *}
 lemma FUN_REL_I:
 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
 SOME (_ $ (_ $ (f $ a))) => (f, a)
 | _ => error "find_qt_asm"
 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
 val tac =
 (compose_tac (false, thm, i)) THEN_ALL_NEW
 \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f
 - 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
 Abs (Rep x)  ---->  x
 fun clean_tac lthy =
 let
 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)
 in
 EVERY' [
 THEN' gen_frees_tac lthy
 THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
 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}
 in
 EVERY1

changeset 529	6348c2a57ec2
parent 527	9b1ad366827f
child 536	44fa9df44e6f