theory QuotMain

imports QuotScript Prove

uses ("quotient_info.ML")

     ("quotient_typ.ML")

     ("quotient_def.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 *}

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

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 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 {* 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 =

  {* Lifting of theorems to quotient types. *}

method_setup lifting_setup =

  {* Sets up the three goals for the lifting procedure. *}

method_setup regularize =

  {* Proves automatically the regularization goals from the lifting procedure. *}

method_setup injection =

  {* Proves automatically the rep/abs injection goals from the lifting procedure. *}

method_setup cleaning =

  {* Proves automatically the cleaning goals from the lifting procedure. *}

end