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

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 simp
qed

theorem homeier_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 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 simp
qed

lemma 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 simp
qed

theorem 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])
  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
  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 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