(*  Title:      QuotMain.thy+
−
    Author:     Cezary Kaliszyk and Christian Urban+
−
*)+
−
+
−
theory QuotMain+
−
imports QuotBase+
−
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)"+
−
+
−
text {*+
−
  The naming of the lemmas follows the quotient paper+
−
  by Peter Homeier.+
−
*}+
−
+
−
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) = a"+
−
  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 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 simp+
−
qed+
−
+
−
theorem thm11:+
−
  shows "R r r' = (abs r = abs r')"+
−
unfolding abs_def+
−
by (simp only: equivp[simplified equivp_def] 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: thm10 thm11)+
−
+
−
lemma Quotient:+
−
  shows "Quotient R abs rep"+
−
unfolding 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 *}+
−
+
−
text {* 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+
−
+
−
+
−
text {* Lemmas about simplifying id's. *}+
−
lemmas [id_simps] =+
−
  id_def[symmetric]+
−
  fun_map_id+
−
  id_apply[THEN eq_reflection]+
−
  id_o+
−
  o_id+
−
  eq_comp_r+
−
+
−
text {* 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 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_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 *}+
−
+
−
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) *}+
−
  {* 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+
−
+
−