theory QuotMain

imports QuotScript QuotList Prove

uses ("quotient_info.ML") 

     ("quotient.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 equiv: "EQUIV 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 equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)

  then have "R x (Eps (R x))" by (rule someI)

  then show "R (Eps (R x)) = R x"

    using equiv unfolding EQUIV_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: equiv[simplified EQUIV_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: equiv[simplified EQUIV_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: equiv[simplified EQUIV_def])

done

lemma R_trans:

  assumes ab: "R a b"

  and     bc: "R b c"

  shows "R a c"

proof -

  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

  moreover have ab: "R a b" by fact

  moreover have bc: "R b c" by fact

  ultimately show "R a c" unfolding TRANS_def by blast

qed

lemma R_sym:

  assumes ab: "R a b"

  shows "R b a"

proof -

  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

  then show "R b a" using ab unfolding SYM_def by blast

qed

lemma R_trans2:

  assumes ac: "R a c"

  and     bd: "R b d"

  shows "R a b = R c d"

using ac bd

by (blast intro: R_trans R_sym)

lemma REPS_same:

  shows "R (REP a) (REP b) \<equiv> (a = b)"

proof -

  have "R (REP a) (REP b) = (a = b)"

  proof

    assume as: "R (REP a) (REP b)"

    from rep_prop

    obtain x y

      where eqs: "Rep a = R x" "Rep b = R y" by blast

    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp

    then have "R x (Eps (R y))" using lem9 by simp

    then have "R (Eps (R y)) x" using R_sym by blast

    then have "R y x" using lem9 by simp

    then have "R x y" using R_sym by blast

    then have "ABS x = ABS y" using thm11 by simp

    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp

    then show "a = b" using rep_inverse by simp

  next

    assume ab: "a = b"

    have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

    then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto

  qed

  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

qed

end

section {* type definition for the quotient type *}

(* the auxiliary data for the quotient types *)

use "quotient_info.ML"

declare [[map list = (map, LIST_REL)]]

declare [[map * = (prod_fun, prod_rel)]]

declare [[map "fun" = (fun_map, FUN_REL)]]

ML {* maps_lookup @{theory} "List.list" *}

ML {* maps_lookup @{theory} "*" *}

ML {* maps_lookup @{theory} "fun" *}

(* definition of the quotient types *)

(* FIXME: should be called quotient_typ.ML *)

use "quotient.ML"

(* lifting of constants *)

use "quotient_def.ML"

section {* ATOMIZE *}

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

ML {*

fun atomize_thm thm =

let

  val thm' = Thm.freezeT (forall_intr_vars thm)

  val thm'' = ObjectLogic.atomize (cprop_of thm')

in

  @{thm Pure.equal_elim_rule1} OF [thm'', thm']

end

*}

ML {* atomize_thm @{thm list.induct} *}

section {* REGULARIZE *}

(*

Regularizing a theorem means:

 - Quantifiers over a type that needs lifting are replaced by

   bounded quantifiers, for example:

      \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P

 - Abstractions over a type that needs lifting are replaced

   by bounded abstractions:

      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)

 - Equalities over the type being lifted are replaced by

   appropriate relations:

      A = B     \<Longrightarrow>     A \<approx> B

   Example with more complicated types of A, B:

      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B

Regularizing is done in 3 phases:

 - First a regularized term is created

 - Next we prove that the original theorem implies the new one

 - Finally using MP we get the new theorem.

To prove that the old theorem implies the new one, we first

atomize it and then try:

 - Reflexivity of the relation

 - Assumption

 - Elimnating quantifiers on both sides of toplevel implication

 - Simplifying implications on both sides of toplevel implication

 - Ball (Respects ?E) ?P = All ?P

 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q

*)

text {* tyRel takes a type and builds a relation that a quantifier over this

  type needs to respect. *}

ML {*

fun tyRel ty rty rel lthy =

  if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)

  then rel

  else (case ty of

          Type (s, tys) =>

            let

              val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;

              val ty_out = ty --> ty --> @{typ bool};

              val tys_out = tys_rel ---> ty_out;

            in

            (case (maps_lookup (ProofContext.theory_of lthy) s) of

               SOME (info) => list_comb (Const (#relfun info, tys_out),

                              map (fn ty => tyRel ty rty rel lthy) tys)

             | NONE  => HOLogic.eq_const ty

            )

            end

        | _ => HOLogic.eq_const ty)

*}

(* 

ML {* cterm_of @{theory} 

  (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) 

         @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) 

*} 

*)

definition

  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"

where

  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"

(* TODO: Consider defining it with an "if"; sth like:

   Babs p m = \<lambda>x. if x \<in> p then m x else undefined

*)

ML {*

fun needs_lift (rty as Type (rty_s, _)) ty =

  case ty of

    Type (s, tys) =>

      (s = rty_s) orelse (exists (needs_lift rty) tys)

  | _ => false

*}

ML {*

fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)

fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})

fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})

fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})

*}

(* applies f to the subterm of an abstractions, otherwise to the given term *)

ML {*

fun apply_subt f trm =

  case trm of

    Abs (x, T, t) => 

       let 

         val (x', t') = Term.dest_abs (x, T, t)

       in

         Term.absfree (x', T, f t') 

       end

  | _ => f trm

*}

(* FIXME: if there are more than one quotient, then you have to look up the relation *)

ML {*

fun my_reg lthy rel rty trm =

  case trm of

    Abs (x, T, t) =>

       if (needs_lift rty T) then

         let

            val rrel = tyRel T rty rel lthy

         in

           (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)

         end

       else

         Abs(x, T, (apply_subt (my_reg lthy rel rty) t))

  | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>

       let

          val ty1 = domain_type ty

          val ty2 = domain_type ty1

          val rrel = tyRel T rty rel lthy

       in

         if (needs_lift rty T) then

           (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)

         else

           Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t

       end

  | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>

       let

          val ty1 = domain_type ty

          val ty2 = domain_type ty1

          val rrel = tyRel T rty rel lthy

       in

         if (needs_lift rty T) then

           (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)

         else

           Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t

       end

  | Const (@{const_name "op ="}, ty) $ t =>

      if needs_lift rty (fastype_of t) then

        (tyRel (fastype_of t) rty rel lthy) $ t   (* FIXME: t should be regularised too *)

      else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)

  | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)

  | _ => trm

*}

(* For polymorphic types we need to find the type of the Relation term. *)

(* TODO: we assume that the relation is a Constant. Is this always true? *)

ML {*

fun my_reg_inst lthy rel rty trm =

  case rel of

    Const (n, _) => Syntax.check_term lthy

      (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)

*}

(*

ML {*

  val r = Free ("R", dummyT);

  val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});

  val t2 = Syntax.check_term @{context} t;

  cterm_of @{theory} t2

*}

*)

text {* Assumes that the given theorem is atomized *}

ML {*

  fun build_regularize_goal thm rty rel lthy =

     Logic.mk_implies

       ((prop_of thm),

       (my_reg_inst lthy rel rty (prop_of thm)))

*}

lemma universal_twice:

  assumes *: "\<And>x. (P x \<longrightarrow> Q x)"

  shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"

using * by auto

lemma implication_twice:

  assumes a: "c \<longrightarrow> a"

  assumes b: "a \<Longrightarrow> b \<longrightarrow> d"

  shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"

using a b by auto

ML {*

fun regularize thm rty rel rel_eqv rel_refl lthy =

  let

    val goal = build_regularize_goal thm rty rel lthy;

    fun tac ctxt =

      (ObjectLogic.full_atomize_tac) THEN'

      REPEAT_ALL_NEW (FIRST' [

        rtac rel_refl,

        atac,

        rtac @{thm universal_twice},

        (rtac @{thm impI} THEN' atac),

        rtac @{thm implication_twice},

        EqSubst.eqsubst_tac ctxt [0]

          [(@{thm equiv_res_forall} OF [rel_eqv]),

           (@{thm equiv_res_exists} OF [rel_eqv])],

        (* For a = b \<longrightarrow> a \<approx> b *)

        (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),

        (rtac @{thm RIGHT_RES_FORALL_REGULAR})

      ]);

    val cthm = Goal.prove lthy [] [] goal

      (fn {context, ...} => tac context 1);

  in

    cthm OF [thm]

  end

*}

section {* RepAbs injection *}

(*

RepAbs injection is done in the following phases:

 1) build_repabs_term inserts rep-abs pairs in the term

 2) we prove the equality between the original theorem and this one

 3) we use Pure.equal_elim_rule1 to get the new theorem.

build_repabs_term does:

  For abstractions:

  * If the type of the abstraction doesn't need lifting we recurse.

  * If it does we add RepAbs around the whole term and check if the

    variable needs lifting.

    * If it doesn't then we recurse

    * If it does we recurse and put 'RepAbs' around all occurences

      of the variable in the obtained subterm. This in combination

      with the RepAbs above will let us change the type of the

      abstraction with rewriting.

  For applications:

  * If the term is 'Respects' applied to anything we leave it unchanged

  * If the term needs lifting and the head is a constant that we know

    how to lift, we put a RepAbs and recurse

  * If the term needs lifting and the head is a free applied to subterms

    (if it is not applied we treated it in Abs branch) then we

    put RepAbs and recurse

  * Otherwise just recurse.

To prove that the old theorem implies the new one, we first

atomize it and then try:

 1) theorems 'trans2' from the appropriate QUOT_TYPE

 2) remove lambdas from both sides (LAMBDA_RES_TAC)

 3) remove Ball/Bex from the right hand side

 4) use user-supplied RSP theorems

 5) remove rep_abs from the right side

 6) reflexivity of equality

 7) split applications of lifted type (apply_rsp)

 8) split applications of non-lifted type (cong_tac)

 9) apply extentionality

10) reflexivity of the relation

11) assumption

    (Lambdas under respects may have left us some assumptions)

12) proving obvious higher order equalities by simplifying fun_rel

    (not sure if it is still needed?)

13) unfolding lambda on one side

14) simplifying (= ===> =) for simpler respectfullness

*)

(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)

ML {*

fun exchange_ty lthy rty qty ty =

  let

    val thy = ProofContext.theory_of lthy

  in

    if Sign.typ_instance thy (ty, rty) then

      let

        val inst = Sign.typ_match thy (rty, ty) Vartab.empty

      in

        Envir.subst_type inst qty

      end

    else

      let

        val (s, tys) = dest_Type ty

      in

        Type (s, map (exchange_ty lthy rty qty) tys)

      end

  end

  handle TYPE _ => ty (* for dest_Type *)

*}

(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

axioms Rl_eq: "EQUIV Rl"

quotient ql = "'a list" / "Rl"

  by (rule Rl_eq)

ML {*

  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});

  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})

*}

*)

ML {*

fun negF absF = repF