added quotient command (you need to update isar-keywords-prove.el)
theory Proveimports Main QuotScript QuotListuses ("quotient.ML")beginlocale 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)"begindefinition "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 simpqedtheorem thm10: shows "ABS (REP a) \<equiv> a" apply (rule eq_reflection) unfolding ABS_def REP_defproof - 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 simpqedlemma REP_refl: shows "R (REP a) (REP a)"unfolding REP_defby (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)donetheorem thm11: shows "R r r' = (ABS r = ABS r')"unfolding ABS_defby (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])donelemma 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 blastqedlemma 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 blastqedlemma 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 blastnext 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 blastqedlemma 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 simpqedenduse "quotient.ML"ML {*val r = ref (NONE:(unit -> term) option)*}ML {*let fun after_qed thm_name thms lthy = LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd fun setup_proof (name_spec, (txt, pos)) lthy = let val trm = ML_Context.evaluate lthy true ("r", r) txt in Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy end val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_sourcein OuterSyntax.local_theory_to_proof "prove" "proving a proposition" OuterKeyword.thy_goal (parser >> setup_proof)end*}end