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

*)

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

*}

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

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

*}

ML {*

fun find_matching_types rty ty =

  if Type.raw_instance (Logic.varifyT ty, rty)

  then [ty]

  else

    let val (s, tys) = dest_Type ty in

    flat (map (find_matching_types rty) tys)

    end

    handle TYPE _ => []

*}

ML {*

fun negF absF = repF

  | negF repF = absF

fun get_fun flag qenv lthy ty =

let

  fun get_fun_aux s fs =

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

      SOME info => list_comb (Const (#mapfun info, dummyT), fs)

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

  fun get_const flag qty =

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

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

  end

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

in

  if (AList.defined (op=) qenv ty)

  then (get_const flag ty)

  else (case ty of

          TFree _ => mk_identity ty

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

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

            let

              val fs_ty1 = get_fun (negF flag) qenv lthy ty1

              val fs_ty2 = get_fun flag qenv lthy ty2

            in  

              get_fun_aux "fun" [fs_ty1, fs_ty2]

            end 

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

        | _ => error ("no type variables allowed"))

end

*}

ML {*

fun get_fun_OLD flag (rty, qty) lthy ty =

  let

    val tys = find_matching_types rty ty;

    val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;

    val xchg_ty = exchange_ty lthy rty qty ty

  in

    get_fun flag qenv lthy xchg_ty

  end

*}

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 goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');

    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal

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

  in

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

  end

*}

ML {*

  fun repeat_eqsubst_thm ctxt thms thm =

    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)

    handle _ => thm

*}

(* Needed to have a meta-equality *)

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

by (simp add: id_def)

(* TODO: can be also obtained with: *)

ML {* symmetric (eq_reflection OF @{thms id_def}) *}

ML {*

fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>

  let

    val pat = Drule.strip_imp_concl (cprop_of thm)

    val insts = Thm.match (pat, concl)

  in

    rtac (Drule.instantiate insts thm) 1

  end

  handle _ => no_tac)

*}

ML {*

fun CHANGED' tac = (fn i => CHANGED (tac i))

*}

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

ML {*

fun quotient_tac quot_thm =

  REPEAT_ALL_NEW (FIRST' [

    rtac @{thm FUN_QUOTIENT},

    rtac quot_thm,

    rtac @{thm IDENTITY_QUOTIENT},

    (* For functional identity quotients, (op = ---> op =) *)

    CHANGED' (

      (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}

      )))

  ])

*}

ML {*

fun LAMBDA_RES_TAC ctxt i st =

  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of

    (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>

      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'

      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})

  | _ => fn _ => no_tac) i st

*}

ML {*