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

end

section {* type definition for the quotient type *}

(* the auxiliary data for the quotient types *)

use "quotient_info.ML"

ML {* print_mapsinfo @{context} *}

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 {* 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 Pattern.matches thy (rtrm', rtrm) then rtrm else

               let

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

                 val _ = tracing ("rtrm':= " ^ 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) =>

       let val (rts, qts) = (Syntax.string_of_term lthy rt, Syntax.string_of_term lthy qt) in

       raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")"))

       end

*}

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 quotient_tac ctxt =

  REPEAT_ALL_NEW (FIRST'

    [rtac @{thm identity_quotient},

     resolve_tac (quotient_rules_get ctxt)])

fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)

val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac

*}

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

                       addsimprocs [simproc] addSolver equiv_solver addSolver quotient_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.

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

*)

ML {*

fun mk_repabs lthy (T, T') trm = 

  Quotient_Def.get_fun repF lthy (T, T') 

    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)

*}

ML {*

(* bound variables need to be treated properly,    *)

(* as the type of subterms need to be calculated   *)

(* in the abstraction case                         *)

fun inj_repabs_trm lthy (rtrm, qtrm) =

 case (rtrm, qtrm) of

    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>

       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>

       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>

      let

        val rty = fastype_of rtrm

        val qty = fastype_of qtrm

      in

        mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))

      end

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

      let

        val rty = fastype_of rtrm

        val qty = fastype_of qtrm

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

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

        val yvar = Free (y, T)

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

      in

        if rty = qty then result

        else mk_repabs lthy (rty, qty) result

      end

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

       (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))

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