theory QuotMainimports QuotScript Proveuses ("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 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 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: equivp[simplified equivp_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: equivp[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: "Quotient R abs rep"apply(unfold Quotient_def)apply(simp add: thm10)apply(simp add: rep_refl)apply(subst thm11[symmetric])apply(simp add: equivp[simplified equivp_def])doneendsection {* type definition for the quotient type *}(* the auxiliary data for the quotient types *)use "quotient_info.ML"ML {* print_mapsinfo @{context} *}declare [[map "fun" = (fun_map, fun_rel)]]lemmas [quot_thm] = fun_quotient lemmas [quot_respect] = quot_rel_rsp(* fun_map is not here since equivp is not true *)lemmas [quot_equiv] = identity_equivp(* definition of the quotient types *)use "quotient_typ.ML"(* lifting of constants *)use "quotient_def.ML"(* the translation functions *)use "quotient_term.ML" (* tactics *)lemma eq_imp_rel: "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)definition "QUOT_TRUE x \<equiv> True"lemma quot_true_dests: shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" and QT_ex: "QUOT_TRUE (Ex 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 QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"by (simp add: QUOT_TRUE_def)lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" by(auto simp add: QUOT_TRUE_def)use "quotient_tacs.ML"section {* Atomize Infrastructure *}lemma atomize_eqv[atomize]: shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"proof assume "A \<equiv> B" then show "Trueprop A \<equiv> Trueprop B" by unfoldnext assume *: "Trueprop A \<equiv> Trueprop B" have "A = B" proof (cases A) case True have "A" by fact then show "A = B" using * by simp next case False have "\<not>A" by fact then show "A = B" using * by auto qed then show "A \<equiv> B" by (rule eq_reflection)qedsection {* Infrastructure about id *}lemmas [id_simps] = fun_map_id[THEN eq_reflection] id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric]section {* Methods / Interface *}ML {*fun mk_method1 tac thm ctxt = SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) fun mk_method2 tac ctxt = SIMPLE_METHOD (HEADGOAL (tac ctxt)) *}method_setup lifting = {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *} {* Lifting of theorems to quotient types. *}method_setup lifting_setup = {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} {* Sets up the three goals for the lifting procedure. *}method_setup regularize = {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} {* Proves automatically the regularization goals from the lifting procedure. *}method_setup injection = {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *} {* Proves automatically the rep/abs injection goals from the lifting procedure. *}method_setup cleaning = {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} {* Proves automatically the cleaning goals from the lifting procedure. *}end