theory QuotMain

imports QuotScript 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 equivp: "equivp 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 equivp by (simp add: equivp_reflp_symp_transp reflp_def)

  then have "R x (Eps (R x))" by (rule someI)

  then show "R (Eps (R x)) = R x"

    using equivp unfolding equivp_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: equivp[simplified equivp_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: equivp[simplified equivp_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: equivp[simplified equivp_def])

done

lemma R_trans:

  assumes ab: "R a b"

  and     bc: "R b c"

  shows "R a c"

proof -

  have tr: "transp R" using equivp equivp_reflp_symp_transp[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 transp_def by blast

qed

lemma R_sym:

  assumes ab: "R a b"

  shows "R b a"

proof -

  have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp

  then show "R b a" using ab unfolding symp_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 "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp

    then show "R (REP a) (REP b)" unfolding reflp_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 "fun" = (fun_map, fun_rel)]]

lemmas [quot_thm] = fun_quotient 

lemmas [quot_respect] = quot_rel_rsp

(* fun_map is not here since equivp is not true *)

lemmas [quot_equiv] = identity_equivp

(* definition of the quotient types *)

(* FIXME: should be called quotient_typ.ML *)

use "quotient.ML"

(* lifting of constants *)

use "quotient_def.ML"

section {* Simset setup *}

(* Since HOL_basic_ss is too "big" for us, *)

(* we set up our own minimal simpset.      *)

ML {*

fun  mk_minimal_ss ctxt =

  Simplifier.context ctxt empty_ss

    setsubgoaler asm_simp_tac

    setmksimps (mksimps [])

*}

ML {*

fun OF1 thm1 thm2 = thm2 RS thm1

*}

section {* Atomize Infrastructure *}

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

lemmas [id_simps] =

  fun_map_id[THEN eq_reflection]

  id_apply[THEN eq_reflection]

  id_def[THEN eq_reflection,symmetric]

section {* Matching of Terms and Types *}

ML {*

fun struct_match_typ (ty, ty') =

  case (ty, ty') of

    (_, TVar _) => true

  | (TFree x, TFree x') => x = x'

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

       s = s' andalso 

       if (length tys = length tys') 

       then (List.all struct_match_typ (tys ~~ tys')) 

       else false

  | _ => false

fun struct_match_term (trm, trm') = 

   case (trm, trm') of 

     (_, Var _) => true

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

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

   | (Bound i, Bound j) => i = j

   | (Abs (_, T, t), Abs (_, T', t')) => struct_match_typ (T, T') andalso struct_match_term (t, t')

   | (t $ s, t' $ s') => struct_match_term (t, t') andalso struct_match_term (s, s') 

   | _ => false

*}

section {* Computation of the Regularize Goal *} 

(*

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 trm1 trm2 =

  case (trm1, trm2) of

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

  | _ => f trm1 trm2

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

fun qnt_typ ty = domain_type (domain_type ty)  

*}

ML {*

(* produces a regularized version of rtrm     *)

(* - the result is contains dummyT            *)

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

(*   bound variables                          *)

fun regularize_trm lthy rtrm qtrm =

  case (rtrm, qtrm) of

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

       let

         val subtrm = Abs(x, ty, regularize_trm lthy t t')

       in

         if ty = ty' then subtrm

         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm

       end

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

       let

         val subtrm = apply_subt (regularize_trm lthy) t 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

  | (* equalities need to be replaced by appropriate equivalence relations *) 

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

         if ty = ty' then rtrm

         else mk_resp_arg lthy (domain_type ty, domain_type ty') 

  | (* in this case we check whether the given equivalence relation is correct *) 

    (rel, Const (@{const_name "op ="}, ty')) =>

       let 

         val exc = LIFT_MATCH "regularise (relation mismatch)"

         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 

         val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 

       in 

         if rel' = rel then rtrm else raise exc

       end  

  | (_, Const (s, Type(st, _))) =>

       let 

         fun same_name (Const (s, _)) (Const (s', _)) = (s = s')

           | same_name _ _ = false

       in

         (* TODO/FIXME: This test is not enough *)

         if same_name rtrm qtrm then rtrm

         else 

           let 

             val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)")

             val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)")

             val thy = ProofContext.theory_of lthy

             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1

           in 

             if struct_match_term (rtrm, rtrm') then rtrm else

               let

                 val _ = tracing (Syntax.string_of_term @{context} rtrm);

                 val _ = tracing (Syntax.string_of_term @{context} rtrm');

               in raise exc2 end

           end

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

  | (rt, qt) =>

       raise (LIFT_MATCH "regularize failed (default)")

*}

section {* Regularize Tactic *}

ML {*

fun equiv_tac ctxt =

  REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))

fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)

val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac

*}

ML {*

fun prep_trm thy (x, (T, t)) =

  (cterm_of thy (Var (x, T)), cterm_of thy t)

fun prep_ty thy (x, (S, ty)) =

  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)

*}

ML {*

fun matching_prs thy pat trm =

let

  val univ = Unify.matchers thy [(pat, trm)]

  val SOME (env, _) = Seq.pull univ

  val tenv = Vartab.dest (Envir.term_env env)

  val tyenv = Vartab.dest (Envir.type_env env)

in

  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)

end

*}

ML {*

fun calculate_instance ctxt thm redex R1 R2 =

let

  val thy = ProofContext.theory_of ctxt

  val goal = Const (@{const_name "equivp"}, dummyT) $ R2  

             |> Syntax.check_term ctxt

             |> HOLogic.mk_Trueprop 

  val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)

  val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])

  val R1c = cterm_of thy R1

  val thmi = Drule.instantiate' [] [SOME R1c] thm

  val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex

  val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)

in

  SOME thm2

end

handle _ => NONE

(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)

*}

ML {*

fun ball_bex_range_simproc ss redex =

let

  val ctxt = Simplifier.the_context ss

in 

 case redex of

    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ 

      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>

        calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2

  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ 

      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  

        calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2

  | _ => NONE

end

*}

lemma eq_imp_rel: 

  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"

by (simp add: equivp_reflp)

(* Regularize Tactic *)

(* 0. preliminary simplification step according to *)

thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)

    ball_reg_eqv_range bex_reg_eqv_range

(* 1. eliminating simple Ball/Bex instances*)

thm ball_reg_right bex_reg_left

(* 2. monos *)

(* 3. commutation rules for ball and bex *)

thm ball_all_comm bex_ex_comm

(* 4. then rel-equality (which need to be instantiated to avoid loops *)

thm eq_imp_rel

(* 5. then simplification like 0 *)

(* finally jump back to 1 *)

ML {*

fun regularize_tac ctxt =

let

  val thy = ProofContext.theory_of ctxt

  val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}

  val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}

  val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))

  val simpset = (mk_minimal_ss ctxt) 

                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}

                       addsimprocs [simproc] addSolver equiv_solver

  (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)

  (* can this cause loops in equiv_tac ? *)

  val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)

in

  simp_tac simpset THEN'

  REPEAT_ALL_NEW (CHANGED o FIRST' [

    resolve_tac @{thms ball_reg_right bex_reg_left},

    resolve_tac (Inductive.get_monos ctxt),

    resolve_tac @{thms ball_all_comm bex_ex_comm},

    resolve_tac eq_eqvs,  

    simp_tac simpset])

end

*}

section {* Calculation of the Injected Goal *}

(*

Injecting repabs means:

  For abstractions:

  * If the type of the abstraction doesn't need lifting we recurse.