(* Title: QuotMain.thy Author: Cezary Kaliszyk and Christian Urban*)theory QuotMainimports QuotBaseuses ("quotient_info.ML") ("quotient_typ.ML") ("quotient_def.ML") ("quotient_term.ML") ("quotient_tacs.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 equivp: "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)"begindefinition abs::"'a \<Rightarrow> 'b"where "abs x \<equiv> Abs (R x)"definition rep::"'b \<Rightarrow> 'a"where "rep a = Eps (Rep a)"lemma homeier_lem9: shows "R (Eps (R x)) = R x"proof - have a: "R x x" using equivp 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 equivp unfolding equivp_def by simpqedtheorem homeier_thm10: shows "abs (rep a) = a" 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 homeier_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 homeier_lem7: shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")proof - have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) also have "\<dots> = ?LHS" by (simp add: abs_inverse) finally show "?LHS = ?RHS" by simpqedtheorem homeier_thm11: shows "R r r' = (abs r = abs r')" unfolding abs_def by (simp only: equivp[simplified equivp_def] homeier_lem7)lemma rep_refl: shows "R (rep a) (rep a)" unfolding rep_def by (simp add: equivp[simplified equivp_def])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: homeier_thm10 homeier_thm11)lemma Quotient: shows "Quotient R abs rep" unfolding Quotient_def apply(simp add: homeier_thm10) apply(simp add: rep_refl) apply(subst homeier_thm11[symmetric]) apply(simp add: equivp[simplified equivp_def]) doneendsection {* ML setup *}text {* Auxiliary data for the quotient package *}use "quotient_info.ML"declare [[map "fun" = (fun_map, fun_rel)]]lemmas [quot_thm] = fun_quotientlemmas [quot_respect] = quot_rel_rsplemmas [quot_equiv] = identity_equivptext {* Lemmas about simplifying id's. *}lemmas [id_simps] = id_def[symmetric] fun_map_id id_apply id_o o_id eq_comp_rtext {* Translation functions for the lifting process. *}use "quotient_term.ML" text {* Definitions of the quotient types. *}use "quotient_typ.ML"text {* Definitions for quotient constants. *}use "quotient_def.ML"text {* An auxiliary constant for recording some information about the lifted theorem in a tactic.*}definition "Quot_True x \<equiv> True"lemma shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P" and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" by (simp_all add: Quot_True_def ext)lemma QT_imp: "Quot_True a \<equiv> Quot_True b" by (simp add: Quot_True_def)text {* Tactics for proving the lifted theorems *}use "quotient_tacs.ML"section {* Methods / Interface *}(* TODO inline *)ML {*fun mk_method1 tac thms ctxt = SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) fun mk_method2 tac ctxt = SIMPLE_METHOD (HEADGOAL (tac ctxt)) *}method_setup lifting = {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *} {* lifts theorems to quotient types *}method_setup lifting_setup = {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} {* sets up the three goals for the quotient lifting procedure *}method_setup regularize = {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} {* proves the regularization goals from the quotient lifting procedure *}method_setup injection = {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *} {* proves the rep/abs injection goals from the quotient lifting procedure *}method_setup cleaning = {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} {* proves the cleaning goals from the quotient lifting procedure *}attribute_setup quot_lifted = {* Scan.succeed Quotient_Tacs.lifted_attrib *} {* lifts theorems to quotient types *}end