moved get_fun into quotient_term; this simplifies the overall including structure of the package
(* Title: ??/QuotMain.thy+ −
Author: Cezary Kaliszyk and Christian Urban+ −
*)+ −
+ −
theory QuotMain+ −
imports QuotScript Prove+ −
uses ("quotient_info.ML")+ −
("quotient_typ.ML")+ −
("quotient_def.ML")+ −
("quotient_term.ML")+ −
("quotient_tacs.ML")+ −
begin+ −
+ −
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 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)"+ −
begin+ −
+ −
definition+ −
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 simp+ −
qed+ −
+ −
theorem thm10:+ −
shows "abs (rep a) \<equiv> a"+ −
apply (rule eq_reflection)+ −
unfolding abs_def rep_def+ −
proof -+ −
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 simp+ −
qed+ −
+ −
lemma rep_refl:+ −
shows "R (rep a) (rep a)"+ −
unfolding rep_def+ −
by (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)+ −
done+ −
+ −
theorem thm11:+ −
shows "R r r' = (abs r = abs r')"+ −
unfolding abs_def+ −
by (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:+ −
shows "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])+ −
done+ −
+ −
end+ −
+ −
+ −
section {* ML setup *}+ −
+ −
(* Auxiliary data for the quotient package *)+ −
use "quotient_info.ML"+ −
+ −
declare [[map "fun" = (fun_map, fun_rel)]]+ −
+ −
lemmas [quot_thm] = fun_quotient + −
lemmas [quot_respect] = quot_rel_rsp+ −
lemmas [quot_equiv] = identity_equivp+ −
+ −
(* Lemmas about simplifying id's. *)+ −
lemmas [id_simps] =+ −
fun_map_id[THEN eq_reflection]+ −
id_apply[THEN eq_reflection]+ −
id_def[THEN eq_reflection, symmetric]+ −
id_o[THEN eq_reflection]+ −
o_id[THEN eq_reflection] + −
+ −
+ −
(* The translation functions for the lifting process. *)+ −
use "quotient_term.ML" + −
+ −
+ −
(* Definition of the quotient types *)+ −
use "quotient_typ.ML"+ −
+ −
+ −
(* Definitions for quotient constants *)+ −
use "quotient_def.ML"+ −
+ −
(* Tactics for proving the lifted theorems *)+ −
+ −
lemma eq_imp_rel: + −
"equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" + −
by (simp add: equivp_reflp)+ −
+ −
(* An auxiliar 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_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)+ −
+ −
use "quotient_tacs.ML"+ −
+ −
+ −
(* Atomize infrastructure *)+ −
(* FIXME/TODO: is this really needed? *)+ −
(*+ −
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 unfold+ −
next+ −
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)+ −
qed+ −
*)+ −
+ −
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_injection_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+ −
+ −