theory QuotMain

imports QuotScript QuotList Prove

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

use "quotient.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" *}

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 {* lifting of constants *}

ML {*

(* whether ty1 is an instance of ty2 *)

fun matches (ty1, ty2) =

  Type.raw_instance (ty1, Logic.varifyT ty2)

fun lookup_snd _ [] _ = NONE

  | lookup_snd eq ((value, key)::xs) key' =

      if eq (key', key) then SOME value

      else lookup_snd eq xs key';

fun lookup_qenv qenv qty =

  (case (AList.lookup matches qenv qty) of

    SOME rty => SOME (qty, rty)

  | NONE => NONE)

*}

ML {*

(* calculates the aggregate abs and rep functions for a given type; 

   repF is for constants' arguments; absF is for constants;

   function types need to be treated specially, since repF and absF

   change

*)

datatype flag = absF | repF

fun negF absF = repF

  | negF repF = absF

fun get_fun flag qenv lthy ty =

let

  fun get_fun_aux s fs_tys =

  let

    val (fs, tys) = split_list fs_tys

    val (otys, ntys) = split_list tys

    val oty = Type (s, otys)

    val nty = Type (s, ntys)

    val ftys = map (op -->) tys

  in

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

      SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))

    | NONE      => raise ERROR ("no map association for type " ^ s))

  end

  fun get_fun_fun fs_tys =

  let

    val (fs, tys) = split_list fs_tys

    val ([oty1, oty2], [nty1, nty2]) = split_list tys

    val oty = nty1 --> oty2

    val nty = oty1 --> nty2

    val ftys = map (op -->) tys

  in

    (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))

  end

  fun get_const flag (qty, rty) =

  let 

    val thy = ProofContext.theory_of lthy

    val qty_name = Long_Name.base_name (fst (dest_Type qty))

  in

    case flag of

      absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))

    | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))

  end

  fun mk_identity ty = Abs ("", ty, Bound 0)

in

  if (AList.defined matches qenv ty)

  then (get_const flag (the (lookup_qenv qenv ty)))

  else (case ty of

          TFree _ => (mk_identity ty, (ty, ty))

        | Type (_, []) => (mk_identity ty, (ty, ty)) 

        | Type ("fun" , [ty1, ty2]) => 

                 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]

        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)

        | _ => raise ERROR ("no type variables")

       )

end

*}

text {* produces the definition for a lifted constant *}

ML {*

fun get_const_def nconst otrm qenv lthy =

let

  val ty = fastype_of nconst

  val (arg_tys, res_ty) = strip_type ty

  val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys

  val abs_fn  = (fst o get_fun absF qenv lthy) res_ty

  fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2

  val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)

            |> Syntax.check_term lthy

in

  fns $ otrm

end

*}

ML {* lookup_snd *}

ML {*

fun exchange_ty qenv ty =

  case (lookup_snd matches qenv ty) of

    SOME qty => qty

  | NONE =>

    (case ty of

       Type (s, tys) => Type (s, map (exchange_ty qenv) tys)

      | _ => ty

    )

*}

ML {*

fun make_const_def nconst_bname otrm mx qenv lthy =

let

  val otrm_ty = fastype_of otrm

  val nconst_ty = exchange_ty qenv otrm_ty

  val nconst = Const (Binding.name_of nconst_bname, nconst_ty)

  val def_trm = get_const_def nconst otrm qenv lthy

in

  define (nconst_bname, mx, def_trm) lthy

end

*}

ML {*

fun build_qenv lthy qtys = 

let

  val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)

  fun find_assoc qty =

    case (AList.lookup matches qenv qty) of

      SOME rty => (qty, rty)

    | NONE => error (implode 

              ["Quotient type ",     

               quote (Syntax.string_of_typ lthy qty), 

               " does not exists"])

in

  map find_assoc qtys

end

*}

ML {*

(* taken from isar_syn.ML *)

val constdecl =

  OuterParse.binding --

    (OuterParse.where_ >> K (NONE, NoSyn) ||

      OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- 

      OuterParse.opt_mixfix' --| OuterParse.where_) ||

      Scan.ahead (OuterParse.$$$ "(") |-- 

      OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))

*}

ML {*

val qd_parser = 

  (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --

    (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))

*}

ML {* 

fun pair lthy (ty1, ty2) =

  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"

*}

ML {*

fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = 

let

  val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs

  val qenv = build_qenv lthy qtys

  val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy

  val (lhs, rhs) = Logic.dest_equals prop

in

  make_const_def bind rhs mx qenv lthy |> snd

end

*}

ML {*

val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"

  OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)

*}

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' = forall_intr_vars thm

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

in

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

end

*}

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

section {* REGULARIZE *}

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

*}

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

(* trm \<Rightarrow> new_trm *)

fun regularise trm rty rel lthy =

  case trm of

    Abs (x, T, t) =>

      if (needs_lift rty T) then let

        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;

        val v = Free (x', T);

        val t' = subst_bound (v, t);

        val rec_term = regularise t' rty rel lthy2;

        val lam_term = Term.lambda_name (x, v) rec_term;

        val sub_res_term = tyRel T rty rel lthy;

        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});

        val res_term = respects $ sub_res_term;

        val ty = fastype_of trm;

        val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);

        val rabs_term = (rabs $ res_term) $ lam_term;

      in

        rabs_term

      end else let

        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;

        val v = Free (x', T);

        val t' = subst_bound (v, t);

        val rec_term = regularise t' rty rel lthy2;

      in

        Term.lambda_name (x, v) rec_term

      end

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

      if (needs_lift rty T) then let

        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;

        val v = Free (x', T);

        val t' = subst_bound (v, t);

        val rec_term = regularise t' rty rel lthy2;

        val lam_term = Term.lambda_name (x, v) rec_term;

        val sub_res_term = tyRel T rty rel lthy;

        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});

        val res_term = respects $ sub_res_term;

        val ty = fastype_of lam_term;

        val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});

        val rall_term = (rall $ res_term) $ lam_term;

      in

        rall_term

      end else let

        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;

        val v = Free (x', T);