theory QuotMain+
−
imports QuotScript QuotList Prove+
−
uses ("quotient_info.ML") +
−
     ("quotient.ML")+
−
begin+
−
+
−
ML {* Attrib.empty_binding *}+
−
+
−
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 *}+
−
+
−
use "quotient_info.ML"+
−
use "quotient.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" *}+
−
+
−
text {* FIXME: auxiliary function *}+
−
ML {*+
−
val no_vars = Thm.rule_attribute (fn context => fn th =>+
−
  let+
−
    val ctxt = Variable.set_body false (Context.proof_of context);+
−
    val ((_, [th']), _) = Variable.import true [th] ctxt;+
−
  in th' end);+
−
*}+
−
+
−
section {* lifting of constants *}+
−
+
−
ML {*+
−
fun lookup_snd _ [] _ = NONE+
−
  | lookup_snd eq ((value, key)::xs) key' =+
−
      if eq (key', key) then SOME value+
−
      else lookup_snd eq xs key';+
−
+
−
fun lookup_qenv qenv qty =+
−
  (case (AList.lookup (op =) qenv qty) of+
−
    SOME rty => SOME (qty, rty)+
−
  | NONE => NONE)+
−
*}+
−
+
−
ML {*+
−
(* calculates the aggregate abs and rep functions for a given type; +
−
   repF is for constants' arguments; absF is for constants;+
−
   function types need to be treated specially, since repF and absF+
−
   change+
−
*)+
−
datatype flag = absF | repF+
−
+
−
fun negF absF = repF+
−
  | negF repF = absF+
−
+
−
fun get_fun flag qenv lthy ty =+
−
let+
−
  +
−
  fun get_fun_aux s fs_tys =+
−
  let+
−
    val (fs, tys) = split_list fs_tys+
−
    val (otys, ntys) = split_list tys+
−
    val oty = Type (s, otys)+
−
    val nty = Type (s, ntys)+
−
    val ftys = map (op -->) tys+
−
  in+
−
   (case (maps_lookup (ProofContext.theory_of lthy) s) of+
−
      SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))+
−
    | NONE      => raise ERROR ("no map association for type " ^ s))+
−
  end+
−
+
−
  fun get_fun_fun fs_tys =+
−
  let+
−
    val (fs, tys) = split_list fs_tys+
−
    val ([oty1, oty2], [nty1, nty2]) = split_list tys+
−
    val oty = nty1 --> oty2+
−
    val nty = oty1 --> nty2+
−
    val ftys = map (op -->) tys+
−
  in+
−
    (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))+
−
  end+
−
+
−
  fun get_const flag (qty, rty) =+
−
  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), rty --> qty), (rty, qty))+
−
    | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))+
−
  end+
−
+
−
  fun mk_identity ty = Abs ("", ty, Bound 0)+
−
+
−
in+
−
  if (AList.defined (op =) qenv ty)+
−
  then (get_const flag (the (lookup_qenv qenv ty)))+
−
  else (case ty of+
−
          TFree _ => (mk_identity ty, (ty, ty))+
−
        | Type (_, []) => (mk_identity ty, (ty, ty)) +
−
        | Type ("fun" , [ty1, ty2]) => +
−
                 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]+
−
        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)+
−
        | _ => raise ERROR ("no type variables")+
−
       )+
−
end+
−
*}+
−
+
−
+
−
text {* produces the definition for a lifted constant *}+
−
+
−
ML {*+
−
fun get_const_def nconst otrm qenv lthy =+
−
let+
−
  val ty = fastype_of nconst+
−
  val (arg_tys, res_ty) = strip_type ty+
−
+
−
  val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys+
−
  val abs_fn  = (fst o get_fun absF qenv lthy) res_ty+
−
+
−
  fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2+
−
+
−
  val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)+
−
            |> Syntax.check_term lthy+
−
in+
−
  fns $ otrm+
−
end+
−
*}+
−
+
−
+
−
ML {*+
−
fun exchange_ty qenv ty =+
−
  case (lookup_snd (op =) qenv ty) of+
−
    SOME qty => qty+
−
  | NONE =>+
−
    (case ty of+
−
       Type (s, tys) => Type (s, map (exchange_ty qenv) tys)+
−
      | _ => ty+
−
    )+
−
*}+
−
+
−
ML {* +
−
fun ppair lthy (ty1, ty2) =+
−
  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"+
−
*}+
−
+
−
ML {*+
−
fun print_env qenv lthy =+
−
  map (ppair lthy) qenv+
−
  |> commas+
−
  |> tracing+
−
*}+
−
+
−
ML {*+
−
fun make_const_def nconst_bname otrm mx qenv lthy =+
−
let+
−
  val otrm_ty = fastype_of otrm+
−
  val nconst_ty = exchange_ty qenv otrm_ty+
−
  val nconst = Const (Binding.name_of nconst_bname, nconst_ty)+
−
  val def_trm = get_const_def nconst otrm qenv lthy+
−
+
−
  val _ = print_env qenv lthy+
−
  val _ = Syntax.string_of_typ lthy otrm_ty |> tracing+
−
  val _ = Syntax.string_of_typ lthy nconst_ty |> tracing+
−
  val _ = Syntax.string_of_term lthy def_trm |> tracing+
−
in+
−
  define (nconst_bname, mx, def_trm) lthy+
−
end+
−
*}+
−
+
−
ML {*+
−
fun build_qenv lthy qtys = +
−
let+
−
  val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)+
−
  val thy = ProofContext.theory_of lthy+
−
  +
−
  fun find_assoc ((qty', rty')::rest) qty =+
−
        let +
−
          val inst = Sign.typ_match thy (qty', qty) Vartab.empty+
−
        in+
−
           (Envir.norm_type inst qty, Envir.norm_type inst rty')+
−
        end+
−
    | find_assoc [] qty =+
−
        let +
−
          val qtystr =  quote (Syntax.string_of_typ lthy qty)+
−
        in+
−
          error (implode ["Quotient type ", qtystr, " does not exists"])+
−
        end+
−
in+
−
  map (find_assoc qenv) qtys+
−
end+
−
*}+
−
+
−
+
−
ML {*+
−
fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy =+
−
let    +
−
  val (lhs_, rhs) = Logic.dest_equals prop+
−
in+
−
  make_const_def bind rhs mx qenv lthy+
−
end+
−
*}+
−
+
−
ML {*+
−
val quotdef_parser = +
−
  Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --+
−
    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- +
−
       OuterParse.prop)) >> OuterParse.triple2+
−
*}+
−
+
−
ML {*+
−
fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = +
−
let+
−
  val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs)+
−
  val qenv = build_qenv lthy qtys+
−
  val qty  = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr+
−
  val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy+
−
in+
−
  quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd+
−
end+
−
*}+
−
+
−
ML {*+
−
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"+
−
  OuterKeyword.thy_decl (quotdef_parser >> quotdef)+
−
*}+
−
+
−
section {* ATOMIZE *}+
−
+
−
text {*+
−
  Unabs_def converts a definition given as+
−
+
−
    c \<equiv> %x. %y. f x y+
−
+
−
  to a theorem of the form+
−
+
−
    c x y \<equiv> f x y+
−
+
−
  This function is needed to rewrite the right-hand+
−
  side to the left-hand side.+
−
*}+
−
+
−
ML {*+
−
fun unabs_def ctxt def =+
−
let+
−
  val (lhs, rhs) = Thm.dest_equals (cprop_of def)+
−
  val xs = strip_abs_vars (term_of rhs)+
−
  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt+
−
+
−
  val thy = ProofContext.theory_of ctxt'+
−
  val cxs = map (cterm_of thy o Free) xs+
−
  val new_lhs = Drule.list_comb (lhs, cxs)+
−
+
−
  fun get_conv [] = Conv.rewr_conv def+
−
    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)+
−
in+
−
  get_conv xs new_lhs |>+
−
  singleton (ProofContext.export ctxt' ctxt)+
−
end+
−
*}+
−
+
−
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 *}+
−
+
−
text {* tyRel takes a type and builds a relation that a quantifier over this+
−
  type needs to respect. *}+
−
ML {*+
−
fun matches (ty1, ty2) =+
−
  Type.raw_instance (ty1, Logic.varifyT ty2);+
−
+
−
fun tyRel ty rty rel lthy =+
−
  if matches (rty, ty)+
−
  then rel+
−
  else (case ty of+
−
          Type (s, tys) =>+
−
            let+
−
              val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;+
−
              val ty_out = ty --> ty --> @{typ bool};+
−
              val tys_out = tys_rel ---> ty_out;+
−
            in+
−
            (case (maps_lookup (ProofContext.theory_of lthy) s) of+
−
               SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)+
−
             | NONE  => HOLogic.eq_const ty+
−
            )+
−
            end+
−
        | _ => HOLogic.eq_const ty)+
−
*}+
−
+
−
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+
−
+
−
*}+
−
+
−
ML {*+
−
fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)+
−
fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})+
−
fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})+
−
fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})+
−
*}+
−
+
−
(* applies f to the subterm of an abstractions, otherwise to the given term *)+
−
ML {*+
−
fun apply_subt f trm =+
−
  case trm of+
−
    Abs (x, T, t) => +
−
       let +
−
         val (x', t') = Term.dest_abs (x, T, t)+
−
       in+
−
         Term.absfree (x', T, f t') +
−
       end+
−
  | _ => f trm+
−
*}+
−
+
−
(* FIXME: if there are more than one quotient, then you have to look up the relation *)+
−
ML {*+
−
fun my_reg lthy rel rty trm =+
−
  case trm of+
−
    Abs (x, T, t) =>+
−
       if (needs_lift rty T) then+
−
         let+
−
            val rrel = tyRel T rty rel lthy+
−
         in+
−
           (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)+
−
         end+
−
       else+
−
         Abs(x, T, (apply_subt (my_reg lthy rel rty) t))+
−
  | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>+
−
       let+
−
          val ty1 = domain_type ty+
−
          val ty2 = domain_type ty1+
−
          val rrel = tyRel T rty rel lthy+
−
       in+
−
         if (needs_lift rty T) then+
−
           (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)+
−
         else+
−
           Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t+
−
       end+
−
  | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>+
−
       let+
−
          val ty1 = domain_type ty+
−
          val ty2 = domain_type ty1+
−
          val rrel = tyRel T rty rel lthy+
−
       in+
−
         if (needs_lift rty T) then+
−
           (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)+
−
         else+
−
           Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t+
−
       end+
−
  | Const (@{const_name "op ="}, ty) $ t =>+
−
      if needs_lift rty (fastype_of t) then+
−
        (tyRel (fastype_of t) rty rel lthy) $ t+
−
      else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)+
−
  | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)+
−
  | _ => trm+
−
*}+
−
+
−
text {* Assumes that the given theorem is atomized *}+
−
ML {*+
−
  fun build_regularize_goal thm rty rel lthy =+
−
     Logic.mk_implies+
−
       ((prop_of thm),+
−
       (my_reg lthy rel rty (prop_of thm)))+
−
*}+
−
+
−
lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"+
−
by auto+
−
+
−
lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"+
−
by auto+
−
+
−
(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"+
−
by auto*)+
−
+
−
ML {*+
−
fun regularize thm rty rel rel_eqv rel_refl lthy =+
−
  let+
−
    val g = build_regularize_goal thm rty rel lthy;+
−
    fun tac ctxt =+
−
      (ObjectLogic.full_atomize_tac) THEN'+
−
     REPEAT_ALL_NEW (FIRST' [+
−
      rtac rel_refl,+
−
      atac,+
−
      rtac @{thm universal_twice},+
−
      (rtac @{thm impI} THEN' atac),+
−
      rtac @{thm implication_twice},+
−
      (*rtac @{thm equality_twice},*)+
−
      EqSubst.eqsubst_tac ctxt [0]+
−
        [(@{thm equiv_res_forall} OF [rel_eqv]),+
−
         (@{thm equiv_res_exists} OF [rel_eqv])],+
−
      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),+
−
      (rtac @{thm RIGHT_RES_FORALL_REGULAR})+
−
     ]);+
−
    val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);+
−
  in+
−
    cthm OF [thm]+
−
  end+
−
*}+
−
+
−
section {* RepAbs injection *}+
−
+
−
(* Needed to have a meta-equality *)+
−
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"+
−
by (simp add: id_def)+
−
+
−
ML {*+
−
fun old_exchange_ty rty qty ty =+
−
  if ty = rty+
−
  then qty+
−
  else+
−
     (case ty of+
−
        Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)+
−
      | _ => ty+
−
     )+
−
*}+
−
+
−
ML {*+
−
fun old_get_fun flag rty qty lthy ty =+
−
  get_fun flag [(qty, rty)] lthy ty +
−
+
−
fun old_make_const_def nconst_bname otrm mx rty qty lthy =+
−
  make_const_def nconst_bname otrm mx [(qty, rty)] lthy+
−
*}+
−
+
−
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 cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))+
−
    val rt = Toplevel.program (fn () => 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+
−
*}+
−
+
−
ML {*+
−
fun build_repabs_term lthy thm constructors rty qty =+
−
  let+
−
    fun mk_rep tm =+
−
      let+
−
        val ty = old_exchange_ty rty qty (fastype_of tm)+
−
      in fst (old_get_fun repF rty qty lthy ty) $ tm end+
−
+
−
    fun mk_abs tm =+
−
      let+
−
        val ty = old_exchange_ty rty qty (fastype_of tm) in+
−
      fst (old_get_fun absF rty qty lthy ty) $ tm end+
−
+
−
    fun is_constructor (Const (x, _)) = member (op =) constructors x+
−
      | is_constructor _ = false;+
−
+
−
    fun build_aux lthy tm =+
−
      case tm of+
−
      Abs (a as (_, vty, _)) =>+
−
      let+
−
        val (vs, t) = Term.dest_abs a;+
−
        val v = Free(vs, vty);+
−
        val t' = lambda v (build_aux lthy t)+
−
      in+
−
      if (not (needs_lift rty (fastype_of tm))) then t'+
−
      else mk_rep (mk_abs (+
−
        if not (needs_lift rty vty) then t'+
−
        else+
−
          let+
−
            val v' = mk_rep (mk_abs v);+
−
            val t1 = Envir.beta_norm (t' $ v')+
−
          in+
−
            lambda v t1+
−
          end+
−
      ))+
−
      end+
−
    | x =>+
−
      let+
−
        val (opp, tms0) = Term.strip_comb tm+
−
        val tms = map (build_aux lthy) tms0+
−
        val ty = fastype_of tm+
−
      in+
−
        if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)+
−
          then (list_comb (opp, (hd tms0) :: (tl tms)))+
−
      else if (is_constructor opp andalso needs_lift rty ty) then+
−
          mk_rep (mk_abs (list_comb (opp,tms)))+
−
        else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then+
−
          mk_rep(mk_abs(list_comb(opp,tms)))+
−
        else if tms = [] then opp+
−
        else list_comb(opp, tms)+
−
      end+
−
  in+
−
    repeat_eqsubst_prop lthy @{thms id_def_sym}+
−
      (build_aux lthy (Thm.prop_of thm))+
−
  end+
−
*}+
−
+
−
text {* Assumes that it is given a regularized theorem *}+
−
ML {*+
−
fun build_repabs_goal ctxt thm cons rty qty =+
−
  Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))+
−
*}+
−
+
−
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 quotient_tac quot_thm =+
−
  REPEAT_ALL_NEW (FIRST' [+
−
    rtac @{thm FUN_QUOTIENT},+
−
    rtac quot_thm,+
−
    rtac @{thm IDENTITY_QUOTIENT}+
−
  ])+
−
*}+
−
+
−
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 {*+
−
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 res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>+
−
  let+
−
    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl+
−
  in+
−
    ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1+
−
  end+
−
  handle _ => no_tac+
−
  )+
−
*}+
−
+
−
ML {*+
−
val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>+
−
  let+
−
    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl+
−
  in+
−
    ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1+
−
  end+
−
  handle _ => no_tac+
−
  )+
−
*}+
−
+
−
ML {*+
−
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =+
−
  (FIRST' [+
−
(*    rtac @{thm FUN_QUOTIENT},+
−
    rtac quot_thm,+
−
    rtac @{thm IDENTITY_QUOTIENT},*)+
−
    rtac trans_thm,+
−
    LAMBDA_RES_TAC ctxt,+
−
    res_forall_rsp_tac ctxt,+
−
    res_exists_rsp_tac ctxt,+
−
    FIRST' (map rtac rsp_thms),+
−
    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),+
−
    rtac refl,+
−
(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)+
−
    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),+
−
    Cong_Tac.cong_tac @{thm cong},+
−
    rtac @{thm ext},+
−
    rtac reflex_thm,+
−
    atac,+
−
    (+
−
     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))+
−
     THEN_ALL_NEW (fn _ => no_tac)+
−
    ),+
−
    WEAK_LAMBDA_RES_TAC ctxt+
−
    ])+
−
*}+
−
+
−
ML {*+
−
fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =+
−
  let+
−
    val rt = build_repabs_term lthy thm constructors rty qty;+
−
    val rg = Logic.mk_equals ((Thm.prop_of thm), rt);+
−
    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'+
−
      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));+
−
    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);+
−
  in+
−
    @{thm Pure.equal_elim_rule1} OF [cthm, thm]+
−
  end+
−
*}+
−
+
−
section {* Cleaning the goal *}+
−
+
−
lemma prod_fun_id: "prod_fun id id = id"+
−
  apply (simp add: prod_fun_def)+
−
done+
−
lemma map_id: "map id x = x"+
−
  apply (induct x)+
−
  apply (simp_all add: map.simps)+
−
done+
−
+
−
text {* expects atomized definition *}+
−
ML {*+
−
  fun add_lower_defs_aux ctxt thm =+
−
    let+
−
      val e1 = @{thm fun_cong} OF [thm];+
−
      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;+
−
      val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;+
−
      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g+
−
    in+
−
      thm :: (add_lower_defs_aux ctxt h)+
−
    end+
−
    handle _ => [thm]+
−
*}+
−
+
−
ML {*+
−
fun add_lower_defs ctxt defs =+
−
  let+
−
    val defs_pre_sym = map symmetric defs+
−
    val defs_atom = map atomize_thm defs_pre_sym+
−
    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)+
−
  in+
−
    map Thm.varifyT defs_all+
−
  end+
−
*}+
−
+
−
ML {*+
−
  fun findabs_all rty tm =+
−
    case tm of+
−
      Abs(_, T, b) =>+
−
        let+
−
          val b' = subst_bound ((Free ("x", T)), b);+
−
          val tys = findabs_all rty b'+
−
          val ty = fastype_of tm+
−
        in if needs_lift rty ty then (ty :: tys) else tys+
−
        end+
−
    | f $ a => (findabs_all rty f) @ (findabs_all rty a)+
−
    | _ => [];+
−
  fun findabs rty tm = distinct (op =) (findabs_all rty tm)+
−
*}+
−
+
−
+
−
ML {*+
−
  fun findaps_all rty tm =+
−
    case tm of+
−
      Abs(_, T, b) =>+
−
        findaps_all rty (subst_bound ((Free ("x", T)), b))+
−
    | (f $ a) => (findaps_all rty f @ findaps_all rty a)+
−
    | Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else [])+
−
    | _ => [];+
−
  fun findaps rty tm = distinct (op =) (findaps_all rty tm)+
−
*}+
−
+
−
ML {*+
−
fun make_simp_prs_thm lthy quot_thm thm typ =+
−
  let+
−
    val (_, [lty, rty]) = dest_Type typ;+
−
    val thy = ProofContext.theory_of lthy;+
−
    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)+
−
    val inst = [SOME lcty, NONE, SOME rcty];+
−
    val lpi = Drule.instantiate' inst [] thm;+
−
    val tac =+
−
      (compose_tac (false, lpi, 2)) THEN_ALL_NEW+
−
      (quotient_tac quot_thm);+
−
    val gc = Drule.strip_imp_concl (cprop_of lpi);+
−
    val t = Goal.prove_internal [] gc (fn _ => tac 1)+
−
  in+
−
    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t+
−
  end+
−
*}+
−
+
−
ML {*+
−
  fun findallex_all rty qty tm =+
−
    case tm of+
−
      Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>+
−
        let+
−
          val (tya, tye) = findallex_all rty qty s+
−
        in if needs_lift rty T then+
−
          ((T :: tya), tye)+
−
        else (tya, tye) end+
−
    | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>+
−
        let+
−
          val (tya, tye) = findallex_all rty qty s+
−
        in if needs_lift rty T then+
−
          (tya, (T :: tye))+
−
        else (tya, tye) end+
−
    | Abs(_, T, b) =>+
−
        findallex_all rty qty (subst_bound ((Free ("x", T)), b))+
−
    | f $ a =>+
−
        let+
−
          val (a1, e1) = findallex_all rty qty f;+
−
          val (a2, e2) = findallex_all rty qty a;+
−
        in (a1 @ a2, e1 @ e2) end+
−
    | _ => ([], []);+
−
*}+
−
ML {*+
−
  fun findallex rty qty tm =+
−
    let+
−
      val (a, e) = findallex_all rty qty tm;+
−
      val (ad, ed) = (map domain_type a, map domain_type e);+
−
      val (au, eu) = (distinct (op =) ad, distinct (op =) ed)+
−
    in+
−
      (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu)+
−
    end+
−
*}+
−
+
−
ML {*+
−
fun make_allex_prs_thm lthy quot_thm thm typ =+
−
  let+
−
    val (_, [lty, rty]) = dest_Type typ;+
−
    val thy = ProofContext.theory_of lthy;+
−
    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)+
−
    val inst = [NONE, SOME lcty];+
−
    val lpi = Drule.instantiate' inst [] thm;+
−
    val tac =+
−
      (compose_tac (false, lpi, 1)) THEN_ALL_NEW+
−
      (quotient_tac quot_thm);+
−
    val gc = Drule.strip_imp_concl (cprop_of lpi);+
−
    val t = Goal.prove_internal [] gc (fn _ => tac 1)+
−
    val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t;+
−
    val t_sym = @{thm "HOL.sym"} OF [t_noid];+
−
    val t_eq = @{thm "eq_reflection"} OF [t_sym]+
−
  in+
−
    t_eq+
−
  end+
−
*}+
−
+
−
ML {*+
−
fun applic_prs lthy rty qty absrep ty =+
−
 let+
−
  fun absty ty =+
−
    old_exchange_ty rty qty ty+
−
  fun mk_rep tm =+
−
    let+
−
      val ty = old_exchange_ty rty qty (fastype_of tm)+
−
    in fst (old_get_fun repF rty qty lthy ty) $ tm end;+
−
  fun mk_abs tm =+
−
      let+
−
        val ty = old_exchange_ty rty qty (fastype_of tm) in+
−
      fst (old_get_fun absF rty qty lthy ty) $ tm end;+
−
  val (l, ltl) = Term.strip_type ty;+
−
  val nl = map absty l;+
−
  val vs = map (fn _ => "x") l;+
−
  val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;+
−
  val args = map Free (vfs ~~ nl);+
−
  val lhs = list_comb((Free (fname, nl ---> ltl)), args);+
−
  val rargs = map mk_rep args;+
−
  val f = Free (fname, nl ---> ltl);+
−
  val rhs = mk_abs (list_comb((mk_rep f), rargs));+
−
  val eq = Logic.mk_equals (rhs, lhs);+
−
  val ceq = cterm_of (ProofContext.theory_of lthy') eq;+
−
  val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps});+
−
  val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)+
−
  val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;+
−
 in+
−
  singleton (ProofContext.export lthy' lthy) t_id+
−
 end+
−
*}+
−
+
−
ML {*+
−
fun lookup_quot_data lthy qty =+
−
  let+
−
    val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)+
−
    val rty = Logic.unvarifyT (#rtyp quotdata)+
−
    val rel = #rel quotdata+
−
    val rel_eqv = #equiv_thm quotdata+
−
    val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]+
−
    val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]+
−
  in+
−
    (rty, rel, rel_refl, rel_eqv)+
−
  end+
−
*}+
−
+
−
ML {*+
−
fun lookup_quot_thms lthy qty_name =+
−
  let+
−
    val thy = ProofContext.theory_of lthy;+
−
    val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")+
−
    val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")+
−
    val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")+
−
    val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)+
−
  in+
−
    (trans2, reps_same, absrep, quot)+
−
  end+
−
*}+
−
+
−
ML {*+
−
fun lookup_quot_consts defs =+
−
  let+
−
    fun dest_term (a $ b) = (a, b);+
−
    val def_terms = map (snd o Logic.dest_equals o concl_of) defs;+
−
  in+
−
    map (fst o dest_Const o snd o dest_term) def_terms+
−
  end+
−
*}+
−
+
−
ML {*+
−
fun lift_thm lthy qty qty_name rsp_thms defs t = let+
−
  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;+
−
  val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;+
−
  val consts = lookup_quot_consts defs;+
−
  val t_a = atomize_thm t;+
−
  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;+
−
  val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;+
−
  val (alls, exs) = findallex rty qty (prop_of t_a);+
−
  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls+
−
  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs+
−
  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t+
−
  val abs = findabs rty (prop_of t_a);+
−
  val aps = findaps rty (prop_of t_a);+
−
  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;+
−
  val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;+
−
  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;+
−
  val defs_sym = add_lower_defs lthy defs;+
−
  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;+
−
  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;+
−
  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;+
−
  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;+
−
in+
−
  ObjectLogic.rulify t_r+
−
end+
−
*}+
−
+
−
+
−
end+
−
+
−