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"

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

end

*}

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

section {* RepAbs injection *}

(*

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

*)

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

fun WEAK_LAMBDA_RES_TAC ctxt i st =

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

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

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

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

  | (_ $ (_ $ (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 {* (* Legacy *)

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 APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>

  let

    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;

    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});

    val insts = Thm.match (pat, concl)

  in

    if needs_lift rty (type_of f) then

      rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1

    else no_tac

  end

  handle _ => no_tac)

*}

ML {*

val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>

  let

    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $

                 (Const (@{const_name Ball}, _) $ _)) = term_of concl

  in

    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))

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

    THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'

    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1

  end

  handle _ => no_tac)

*}

ML {*

val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>

  let

    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $

                 (Const (@{const_name Bex}, _) $ _)) = term_of concl

  in

    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))

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

    THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'

    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1

  end

  handle _ => no_tac)

*}

ML {*

fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)

*}

ML {*

fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =

  (FIRST' [

    rtac trans_thm,

    LAMBDA_RES_TAC ctxt,

    ball_rsp_tac ctxt,

    bex_rsp_tac ctxt,

    FIRST' (map rtac rsp_thms),

    rtac refl,

    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),

    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),

    Cong_Tac.cong_tac @{thm cong},

    rtac @{thm ext},

    rtac reflex_thm,

    atac,

    SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),

    WEAK_LAMBDA_RES_TAC ctxt,

    CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))

    ])

*}

section {* Cleaning the goal *}

ML {*

fun simp_ids lthy thm =

  MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm

*}

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

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