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"

text {* FIXME: auxiliary function *}

ML {*

val no_vars = Thm.rule_attribute (fn context => fn th =>

  let

    val ctxt = Variable.set_body false (Context.proof_of context);

    val ((_, [th']), _) = Variable.import true [th] ctxt;

  in th' end);

*}

section {* ATOMIZE *}

text {*

  Unabs_def converts a definition given as

    c \<equiv> %x. %y. f x y

  to a theorem of the form

    c x y \<equiv> f x y

  This function is needed to rewrite the right-hand

  side to the left-hand side.

*}

ML {*

fun unabs_def ctxt def =

let

  val (lhs, rhs) = Thm.dest_equals (cprop_of def)

  val xs = strip_abs_vars (term_of rhs)

  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt

  val thy = ProofContext.theory_of ctxt'

  val cxs = map (cterm_of thy o Free) xs

  val new_lhs = Drule.list_comb (lhs, cxs)

  fun get_conv [] = Conv.rewr_conv def

    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)

in

  get_conv xs new_lhs |>

  singleton (ProofContext.export ctxt' ctxt)

end

*}

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 abstactions:

      \<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 matches (ty1, ty2) =

  Type.raw_instance (ty1, Logic.varifyT ty2);

fun tyRel ty rty rel lthy =

  if matches (rty, ty)

  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)

*}

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

      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

*}

ML {*

fun my_reg_inst lthy rel rty trm =

  case rel of

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

      (my_reg lthy (Const (n, dummyT)) rty trm)

*}

(*ML {*

  (*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*)

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

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

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

  Toplevel.program (fn () => 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: 

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

by auto

lemma implication_twice: 

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

by auto

(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"

by auto*)

ML {*

fun regularize thm rty rel rel_eqv rel_refl lthy =

  let

    val g = 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},

      (*rtac @{thm equality_twice},*)

      EqSubst.eqsubst_tac ctxt [0]

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

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

      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),

      (rtac @{thm RIGHT_RES_FORALL_REGULAR})

     ]);

    val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);

  in

    cthm OF [thm]

  end

*}

section {* RepAbs injection *}

(* Needed to have a meta-equality *)

lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"

by (simp add: id_def)

ML {*

fun old_exchange_ty rty qty ty =

  if ty = rty

  then qty

  else

     (case ty of

        Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)

      | _ => ty

     )

*}

ML {*

fun old_get_fun flag rty qty lthy ty =

  get_fun flag [(qty, rty)] lthy ty 

fun old_make_const_def nconst_bname otrm mx rty qty lthy =

  make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy

*}

text {* Does the same as 'subst' in a given prop or theorem *}

ML {*

fun eqsubst_prop ctxt thms t =

  let

    val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)

    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of

      NONE => error "eqsubst_prop"

    | SOME th => cprem_of th 1

  in term_of a' end

*}

ML {*

  fun repeat_eqsubst_prop ctxt thms t =

    repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)

    handle _ => t

*}

ML {*

fun eqsubst_thm ctxt thms thm =

  let

    val goalstate = Goal.init (Thm.cprop_of thm)

    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of

      NONE => error "eqsubst_thm"

    | SOME th => cprem_of th 1

    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1

    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))

    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));

  in

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

  end

*}