(*  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:
  "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 {* type definition for the quotient type *}

(* 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

(* 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 for the lifting process *)
use "quotient_term.ML" 

(* tactics for proving the theorems *)

lemma eq_imp_rel:  
  "equivp R ==> a = b \<longrightarrow> R a b" 
by (simp add: equivp_reflp)

(* an auxiliar constant that records some information *) 
(* about the lifted theorem                           *)
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: 
  shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
by(auto simp add: QUOT_TRUE_def)

use "quotient_tacs.ML"

(* 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 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

(* lemmas about simplifying id *)
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] 


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