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 \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" and Rep :: "'b \ ('a \ bool)" - assumes equiv: "EQUIV R" + assumes equiv: "equivp R" and rep_prop: "\y. \x. Rep y = R x" and rep_inverse: "\x. Abs (Rep x) = x" and abs_inverse: "\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) \ (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 \ Q \ \Q \ \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 \ a = b \ R a b" -by (simp add: EQUIV_REFL) +lemma eq_imp_rel: "equivp R \ a = b \ 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}