theory QuotMainNew

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

lemma equiv_trans2:

  assumes e: "EQUIV R"

  and     ac: "R a c"

  and     bd: "R b d"

  shows "R a b = R c d"

using ac bd e

unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def

by (blast)

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"

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

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

*)

definition

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

where

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

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 equal_elim_rule1} OF [thm'', thm']

end

*}

section {* infrastructure about id *}

lemma prod_fun_id: "prod_fun id id \<equiv> id"

  by (rule eq_reflection) (simp add: prod_fun_def)

lemma map_id: "map id \<equiv> id"

  apply (rule eq_reflection)

  apply (rule ext)

  apply (rule_tac list="x" in list.induct)

  apply (simp_all)

  done

lemmas id_simps =

  FUN_MAP_I[THEN eq_reflection]

  id_apply[THEN eq_reflection]

  id_def[THEN eq_reflection,symmetric]

  prod_fun_id map_id

ML {*

fun simp_ids thm =

  MetaSimplifier.rewrite_rule @{thms id_simps} thm

*}

section {* Debugging infrastructure for testing tactics *}

ML {*

fun my_print_tac ctxt s i thm =

let

  val prem_str = nth (prems_of thm) (i - 1)

                 |> Syntax.string_of_term ctxt

                 handle Subscript => "no subgoal"

  val _ = tracing (s ^ "\n" ^ prem_str)

in

  Seq.single thm

end *}

ML {*

fun DT ctxt s tac i thm =

let

  val before_goal = nth (prems_of thm) (i - 1)

                    |> Syntax.string_of_term ctxt

  val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]

                   |> cat_lines

in 

  EVERY [tac i, my_print_tac ctxt before_msg i] thm

end

fun NDT ctxt s tac thm = tac thm  

*}

section {* Infrastructure for special quotient identity *}

definition

  "qid TYPE('a) TYPE('b) x \<equiv> x"

ML {*

fun get_typ_aux (Type ("itself", [T])) = T 

fun get_typ (Const ("TYPE", T)) = get_typ_aux T

fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =

  (get_typ ty1, get_typ ty2)

fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true

  | is_qid _ = false

fun mk_itself ty = Type ("itself", [ty])

fun mk_TYPE ty = Const ("TYPE", mk_itself ty)

fun mk_qid (rty, qty, trm) = 

  Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) 

    $ mk_TYPE rty $ mk_TYPE qty $ trm

*}

ML {*

fun insertion_aux (rtrm, qtrm) =

  case (rtrm, qtrm) of

    (Abs (x, ty, t), Abs (x', ty', t')) =>

       let

         val (y, s) = Term.dest_abs (x, ty, t)

         val (_, s') = Term.dest_abs (x', ty', t')

         val yvar = Free (y, ty)

         val result = Term.lambda_name (y, yvar) (insertion_aux (s, s'))

       in     

         if ty = ty'

         then result

         else mk_qid (ty, ty', result)

       end

  | (_ $ _, _ $ _) =>

       let 

         val rty = fastype_of rtrm

         val qty = fastype_of qtrm

         val (rhead, rargs) = strip_comb rtrm

         val (qhead, qargs) = strip_comb qtrm

         val rargs' = map insertion_aux (rargs ~~ qargs)

         val rhead' = insertion_aux (rhead, qhead)

         val result = list_comb (rhead', rargs')

       in

         if rty = qty

         then result

         else mk_qid (rty, qty, result)

       end

  | (Free (_, ty), Free (_, ty')) =>

       if ty = ty'

       then rtrm 

       else mk_qid (ty, ty', rtrm)

  | (Const (s, ty), Const (s', ty')) =>

       if s = s'

       then rtrm

       else mk_qid (ty, ty', rtrm) 

  | (_, _) => raise (LIFT_MATCH "insertion")

*}

ML {*

fun insertion ctxt rtrm qtrm = 

  Syntax.check_term ctxt (insertion_aux (rtrm, qtrm))                          

*}

fun

  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)

where

  "intrel (x, y) (u, v) = (x + v = u + y)"

quotient my_int = "nat \<times> nat" / intrel

  apply(unfold EQUIV_def)

  apply(auto simp add: mem_def expand_fun_eq)

  done

fun

  my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

where

  "my_plus (x, y) (u, v) = (x + u, y + v)"

quotient_def 

  PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"

where

  "PLUS \<equiv> my_plus"

thm PLUS_def

ML {* MetaSimplifier.rewrite_term *}

ML {*

let 

  val rtrm = @{term "\<forall>a b. my_plus a b \<approx> my_plus b a"}

  val qtrm = @{term "\<forall>a b. PLUS a b = PLUS b a"}

  val ctxt = @{context}

in

  insertion ctxt rtrm qtrm

  (*|> Drule.term_rule @{theory} (MetaSimplifier.rewrite_rule [@{thm "qid_def"}])*)

  |> Syntax.string_of_term ctxt

  |> writeln

end

*}

section {* Regularization *} 

(*

Regularizing an rtrm 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  /  All (Respects R) P

   the relation R is given by the rty and qty;

 - 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

   corresponding relations:

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

   example with more complicated types of A, B:

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

*)

ML {*

(* builds the relation that is the argument of respects *)

fun mk_resp_arg lthy (rty, qty) =

let

  val thy = ProofContext.theory_of lthy

in  

  if rty = qty

  then HOLogic.eq_const rty

  else

    case (rty, qty) of

      (Type (s, tys), Type (s', tys')) =>

       if s = s' 

       then let

              val SOME map_info = maps_lookup thy s

              val args = map (mk_resp_arg lthy) (tys ~~ tys')

            in

              list_comb (Const (#relfun map_info, dummyT), args) 

            end  

       else let  

              val SOME qinfo = quotdata_lookup_thy thy s'

              (* FIXME: check in this case that the rty and qty *)

              (* FIXME: correspond to each other *)

              val (s, _) = dest_Const (#rel qinfo)

              (* FIXME: the relation should only be the string        *)

              (* FIXME: and the type needs to be calculated as below; *)

              (* FIXME: maybe one should actually have a term         *)

              (* FIXME: and one needs to force it to have this type   *)

            in

              Const (s, rty --> rty --> @{typ bool})

            end

      | _ => HOLogic.eq_const dummyT 

             (* FIXME: check that the types correspond to each other? *)

end

*}

ML {*

val mk_babs = Const (@{const_name "Babs"}, dummyT)

val mk_ball = Const (@{const_name "Ball"}, dummyT)

val mk_bex  = Const (@{const_name "Bex"}, dummyT)

val mk_resp = Const (@{const_name Respects}, dummyT)

*}

ML {*

(* - applies f to the subterm of an abstraction,   *)

(*   otherwise to the given term,                  *)

(* - used by regularize, therefore abstracted      *)

(*   variables do not have to be treated specially *)

fun apply_subt f trm =

  case trm of

    (Abs (x, T, t)) => Abs (x, T, f t)

  | _ => f trm

(* the major type of All and Ex quantifiers *)

fun qnt_typ ty = domain_type (domain_type ty)  

*}

ML {*

(* produces a regularized version of trm      *)

(* - the result is still not completely typed *)

(* - does not need any special treatment of   *)

(*   bound variables                          *)

fun regularize_trm lthy trm =

  case trm of

    (Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) =>

       let

         val rty = get_typ rty'

         val qty = get_typ qty'

         val subtrm = regularize_trm lthy t

       in     

         mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm)

       end

  | (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) => 

       let

         val subtrm = apply_subt (regularize_trm lthy) t

       in

         if ty = ty'

         then Const (@{const_name "All"}, ty) $ subtrm

         else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

       end

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

       let

         val subtrm = apply_subt (regularize_trm lthy) t t'

       in

         if ty = ty'

         then Const (@{const_name "Ex"}, ty) $ subtrm

         else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

       end

    (* FIXME: Should = only be replaced, when fully applied? *) 

    (* Then there must be a 2nd argument                     *)

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

       let

         val subtrm = regularize_trm lthy t t'

       in

         if ty = ty'

         then Const (@{const_name "op ="}, ty) $ subtrm

         else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm

       end 

  | (t1 $ t2, t1' $ t2') =>

       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')

  | (Free (x, ty), Free (x', ty')) => 

       (* this case cannot arrise as we start with two fully atomized terms *)

       raise (LIFT_MATCH "regularize (frees)")

  | (Bound i, Bound i') =>

       if i = i' 

       then rtrm 

       else raise (LIFT_MATCH "regularize (bounds)")

  | (Const (s, ty), Const (s', ty')) =>

       if s = s' andalso ty = ty'

       then rtrm

       else rtrm (* FIXME: check correspondence according to definitions *) 

  | (rt, qt) => 

       raise (LIFT_MATCH "regularize (default)")

*}

(*

FIXME / TODO: needs to be adapted

To prove that the raw theorem implies the regularised one, 

we try in order:

 - 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

*)

section {* Injections of REP and ABSes *}

(*

Injecting REPABS means:

  For abstractions: