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 {* infrastructure about id *}+
−
+
−
(* 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}) *}+
−
+
−
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 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+
−
*}+
−
+
−
section {* Does the same as 'subst' in a given 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+
−
*}+
−
+
−
section {*  Infrastructure about definitions *}+
−
+
−
text {* expects atomized definition *}+
−
ML {*+
−
fun add_lower_defs_aux lthy thm =+
−
  let+
−
    val e1 = @{thm fun_cong} OF [thm];+
−
    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;+
−
    val g = simp_ids lthy f+
−
  in+
−
    (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)+
−
  end+
−
  handle _ => [simp_ids lthy thm]+
−
*}+
−
+
−
ML {*+
−
fun add_lower_defs lthy def =+
−
  let+
−
    val def_pre_sym = symmetric def+
−
    val def_atom = atomize_thm def_pre_sym+
−
    val defs_all = add_lower_defs_aux lthy def_atom+
−
  in+
−
    map Thm.varifyT defs_all+
−
  end+
−
*}+
−
+
−
section {* infrastructure about collecting theorems for calling lifting *}+
−
+
−
ML {*+
−
fun lookup_quot_data lthy qty =+
−
  let+
−
    val qty_name = fst (dest_Type qty)+
−
    val SOME quotdata = quotdata_lookup lthy qty_name+
−
                  (* cu: Changed the lookup\<dots>not sure whether this works *)+
−
    (* TODO: Should no longer be needed *)+
−
    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+
−
*}+
−
+
−
+
−
+
−
(******************************************)+
−
(******************************************)+
−
(* version with explicit qtrm             *)+
−
(******************************************)+
−
(******************************************)+
−
+
−
+
−
ML {*+
−
(*+
−
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+
−
*)+
−
+
−
+
−
(* 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 *) +
−
            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 rtm      *)+
−
(* - the result is still not completely typed *)+
−
(* - 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 = REGULARIZE_trm lthy t t'+
−
       in     +
−
         if ty = ty'+
−
         then Abs (x, ty, 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+
−
    (* FIXME: Should = only be replaced, when fully applied? *) +
−
    (* Then there must be a 2nd argument                     *)+
−
  | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>+
−
       let+
−
         val subtrm = REGULARIZE_trm lthy t t'+
−
       in+
−
         if ty = ty'+
−
         then Const (@{const_name "op ="}, ty) $ subtrm+
−
         else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm+
−
       end +
−
  | (t1 $ t2, t1' $ t2') =>+
−
       (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')+
−
  | (Free (x, ty), Free (x', ty')) =>+
−
       if x = x' +
−
       then rtrm     (* FIXME: check whether types corresponds *)+
−
       else raise (LIFT_MATCH "regularize (frees)")+
−
  | (Bound i, Bound i') =>+
−
       if i = i' +
−
       then rtrm +
−
       else raise (LIFT_MATCH "regularize (bounds)")+
−
  | (Const (s, ty), Const (s', ty')) =>+
−
       if s = s' andalso ty = ty'+
−
       then rtrm+
−
       else rtrm (* FIXME: check correspondence according to definitions *) +
−
  | (rt, qt) => +
−
       raise (LIFT_MATCH "regularize (default)")+
−
*}+
−
+
−
ML {*+
−
fun mk_REGULARIZE_goal lthy rtrm qtrm =+
−
  Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))+
−
*}+
−
+
−
(*+
−
To prove that the raw theorem implies the regularised one, +
−
we try in order:+
−
+
−
 - 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+
−
+
−
*)+
−
+
−
lemma my_equiv_res_forallR:+
−
  fixes P::"'a \<Rightarrow> bool"+
−
  fixes Q::"'b \<Rightarrow> bool"+
−
  assumes b: "(All Q) \<longrightarrow> (All P)"+
−
  shows "(All Q) \<longrightarrow> Ball (Respects E) P"+
−
using b by auto+
−
+
−
lemma my_equiv_res_forallL:+
−
  fixes P::"'a \<Rightarrow> bool"+
−
  fixes Q::"'b \<Rightarrow> bool"+
−
  assumes a: "EQUIV E"+
−
  assumes b: "(All Q) \<longrightarrow> (All P)"+
−
  shows "Ball (Respects E) P \<longrightarrow> (All P)"+
−
using a b+
−
unfolding EQUIV_def+
−
by (metis IN_RESPECTS)+
−
+
−
lemma my_equiv_res_existsR:+
−
  fixes P::"'a \<Rightarrow> bool"+
−
  fixes Q::"'b \<Rightarrow> bool"+
−
  assumes a: "EQUIV E"+
−
  and     b: "(Ex Q) \<longrightarrow> (Ex P)"+
−
  shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"+
−
using a b+
−
unfolding EQUIV_def+
−
by (metis IN_RESPECTS)+
−
+
−
lemma my_equiv_res_existsL:+
−
  fixes P::"'a \<Rightarrow> bool"+
−
  fixes Q::"'b \<Rightarrow> bool"+
−
  assumes b: "(Ex Q) \<longrightarrow> (Ex P)"+
−
  shows "Bex (Respects E) Q \<longrightarrow> (Ex P)"+
−
using b+
−
by (auto)+
−
+
−
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: "b \<longrightarrow> d"+
−
  shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"+
−
using a b by auto+
−
+
−
(* version of REGULARIZE_tac including debugging information *)+
−
ML {*+
−
fun my_print_tac ctxt s thm =+
−
let+
−
  val prems_str = prems_of thm+
−
                  |> map (Syntax.string_of_term ctxt)+
−
                  |> cat_lines+
−
  val _ = tracing (s ^ "\n" ^ prems_str)+
−
in+
−
  Seq.single thm+
−
end+
−
 +
−
fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]+
−
*}+
−
+
−
ML {*+
−
fun REGULARIZE_tac' lthy rel_refl rel_eqv =+
−
   (REPEAT1 o FIRST1) +
−
     [(K (print_tac "start")) THEN' (K no_tac), +
−
      DT lthy "1" (rtac rel_refl),+
−
      DT lthy "2" atac,+
−
      DT lthy "3" (rtac @{thm universal_twice}),+
−
      DT lthy "4" (rtac @{thm impI} THEN' atac),+
−
      DT lthy "5" (rtac @{thm implication_twice}),+
−
      DT lthy "6" (rtac @{thm my_equiv_res_forallR}),+
−
      DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})),+
−
      (* For a = b \<longrightarrow> a \<approx> b *)+
−
      DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),+
−
      DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]+
−
*}+
−
+
−
ML {*+
−
fun regularize_tac ctxt rel_eqv rel_refl =+
−
  (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},+
−
    EqSubst.eqsubst_tac ctxt [0]+
−
      [(@{thm equiv_res_forall} OF [rel_eqv]),+
−
       (@{thm equiv_res_exists} OF [rel_eqv])],+
−
    (* For a = b \<longrightarrow> a \<approx> b *)+
−
    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),+
−
    (rtac @{thm RIGHT_RES_FORALL_REGULAR})+
−
  ]);+
−
*}+
−
+
−
ML {*+
−
fun regularize_tac ctxt rel_eqv rel_refl =+
−
  (ObjectLogic.full_atomize_tac) THEN'+
−
  REPEAT_ALL_NEW (FIRST' +
−
   [(K (print_tac "start")) THEN' (K no_tac), +
−
    DT ctxt "1" (rtac rel_refl),+
−
    DT ctxt "2" atac,+
−
    DT ctxt "3" (rtac @{thm universal_twice}),+
−
    DT ctxt "4" (rtac @{thm impI} THEN' atac),+
−
    DT ctxt "5" (rtac @{thm implication_twice}),+
−
    DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]+
−
      [(@{thm equiv_res_forall} OF [rel_eqv]),+
−
       (@{thm equiv_res_exists} OF [rel_eqv])]),+
−
    (* For a = b \<longrightarrow> a \<approx> b *)+
−
    DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),+
−
    DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})+
−
  ]);+
−
*}+
−
+
−
thm RIGHT_RES_FORALL_REGULAR+
−
+
−
section {* Injections of REP and ABSes *}+
−
+
−
(*+
−
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 *)+
−
+
−
fun inj_REPABS lthy (rtrm, qtrm) =+
−
let+
−
  val rty = fastype_of rtrm+
−
  val qty = fastype_of qtrm+
−
in+
−
  case (rtrm, qtrm) of+
−
    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>+
−
       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))+
−
  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>+
−
       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))+
−
  | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>+
−
       Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))+
−
  | (Abs (x, T, t), Abs (x', T', t')) =>+
−
      let+
−
        val (y, s) = Term.dest_abs (x, T, t)+
−
        val (_, s') = Term.dest_abs (x', T', t')+
−
        val yvar = Free (y, T)+
−
        val result = lambda yvar (inj_REPABS lthy (s, s'))+
−
      in+
−
        if rty = qty +
−
        then result+
−
        else mk_repabs lthy (rty, qty) result+
−
      end+
−
  | _ =>+
−
      (* FIXME / TODO: this is a case that needs to be looked at          *)+
−
      (* - variables get a rep-abs insde and outside an application       *)+
−
      (* - constants only get a rep-abs on the outside of the application *)+
−
      (* - applications get a rep-abs insde and outside an application    *)+
−
      let+
−
        val (rhead, rargs) = strip_comb rtrm+
−
        val (qhead, qargs) = strip_comb qtrm+
−
        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)+
−
      in+
−
        if rty = qty+
−
        then+
−
          case (rhead, qhead) of+
−
            (Free (_, T), Free (_, T')) =>+
−
              if T = T' then list_comb (rhead, rargs')+
−
              else list_comb (mk_repabs lthy (T, T') rhead, rargs')+
−
          | _ => list_comb (rhead, rargs')+
−
        else+
−
          case (rhead, qhead, length rargs') of+
−
            (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead+
−
          | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead+
−
          | (Const _, Const _, _) =>  mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) +
−
          | (Free (x, T), Free (x', T'), _) => +
−
               mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))+
−
          | (Abs _, Abs _, _ ) =>+
−
               mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) +
−
          | _ => raise (LIFT_MATCH "injection")+
−
      end+
−
end+
−
*}+
−
+
−
ML {*+
−
fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =+
−
  Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))+
−
*}+
−
+
−
section {* RepAbs injection tactic *}+
−
(*+
−
To prove that the regularised theorem implies the abs/rep injected, 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+
−
+
−
*)+
−
+
−
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))+
−
*}+
−
+
−
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,+
−
    rtac @{thm RES_FORALL_RSP},+
−
    ball_rsp_tac ctxt,+
−
    rtac @{thm RES_EXISTS_RSP},+
−
    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}))+
−
    ])+
−
*}+
−
+
−
(*+
−
To prove that the regularised theorem implies the abs/rep injected, +
−
we 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 respectfulness+
−
+
−
*)+
−
+
−
ML {*+
−
fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms =+
−
  REPEAT_ALL_NEW (FIRST' [+
−
    (K (print_tac "start")) THEN' (K no_tac), +
−
    DT ctxt "1" (rtac trans_thm),+
−
    DT ctxt "2" (LAMBDA_RES_TAC ctxt),+
−
    DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),+
−
    DT ctxt "4" (ball_rsp_tac ctxt),+
−
    DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),+
−
    DT ctxt "6" (bex_rsp_tac ctxt),+
−
    DT ctxt "7" (FIRST' (map rtac rsp_thms)),+
−
    DT ctxt "8" (rtac refl),+
−
    DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt +
−
                  THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))),+
−
    DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' +
−
                (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))),+
−
    DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),+
−
    DT ctxt "C" (rtac @{thm ext}),+
−
    DT ctxt "D" (rtac reflex_thm),+
−
    DT ctxt "E" (atac),+
−
    DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),+
−
    DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),+
−
    DT ctxt "H" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))+
−
    ])+
−
*}+
−
+
−
+
−
+
−
+
−
section {* Cleaning of the theorem *}+
−
+
−
(* 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+
−
*}+
−
+
−
ML {*+
−
fun applic_prs_old lthy rty qty absrep ty =+
−
  let+
−
    val rty = Logic.varifyT rty;+
−
    val qty = Logic.varifyT qty;+
−
    fun absty ty =+
−
      exchange_ty lthy rty qty ty+
−
    fun mk_rep tm =+
−
      let+
−
        val ty = exchange_ty lthy qty rty (fastype_of tm)+
−
      in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;+
−
    fun mk_abs tm =+
−
      let+
−
        val ty = fastype_of tm+
−
      in Syntax.check_term lthy ((get_fun_OLD 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 = 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 applic_prs lthy absrep (rty, qty) =+
−
  let+
−
    fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;+
−
    fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;+
−
    val (raty, rgty) = Term.strip_type rty;+
−
    val (qaty, qgty) = Term.strip_type qty;+
−
    val vs = map (fn _ => "x") qaty;+
−
    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;+
−
    val f = Free (fname, qaty ---> qgty);+
−
    val args = map Free (vfs ~~ qaty);+
−
    val rhs = list_comb(f, args);+
−
    val largs = map2 mk_rep (raty ~~ qaty) args;+
−
    val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));+
−
    val llhs = Syntax.check_term lthy lhs;+
−
    val eq = Logic.mk_equals (llhs, rhs);+
−
    val ceq = cterm_of (ProofContext.theory_of lthy') eq;+
−
    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});+
−
    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)+
−
    val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;+
−
  in+
−
    singleton (ProofContext.export lthy' lthy) t_id+
−
  end+
−
*}+
−
+
−
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 find_aps_all rtm qtm =+
−
  case (rtm, qtm) of+
−
    (Abs(_, T1, s1), Abs(_, T2, s2)) =>+
−
      find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))+
−
  | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>+
−
      let+
−
        val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)+
−
      in+
−
        if T1 = T2 then sub else (T1, T2) :: sub+
−
      end+
−
  | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)+
−
  | _ => [];+
−
+
−
fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)+
−
*}+
−
+
−
ML {*+
−
(* FIXME: allex_prs and lambda_prs can be one function *)+
−
fun allex_prs_tac lthy quot =+
−
  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})+
−
  THEN' (quotient_tac quot);+
−
*}+
−
+
−
ML {*+
−
let+
−
   val parser = Args.context -- Scan.lift Args.name_source+
−
   fun term_pat (ctxt, str) =+
−
      str |> ProofContext.read_term_pattern ctxt+
−
          |> ML_Syntax.print_term+
−
          |> ML_Syntax.atomic+
−
in+
−
   ML_Antiquote.inline "term_pat" (parser >> term_pat)+
−
end+
−
*}+
−
+
−
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 lambda_prs_conv1 ctxt quot ctrm =+
−
  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>+
−
  let+
−
    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);+
−
    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);+
−
    val thy = ProofContext.theory_of ctxt;+
−
    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]+
−
    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];+
−
    val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]+
−
    val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};+
−
    val tac =+
−
      (compose_tac (false, lpi, 2)) THEN_ALL_NEW+
−
      (quotient_tac quot);+
−
    val gc = Drule.strip_imp_concl (cprop_of lpi);+
−
    val t = Goal.prove_internal [] gc (fn _ => tac 1)+
−
    val te = @{thm eq_reflection} OF [t]+
−
    val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te+
−
    val tl = Thm.lhs_of ts+
−
(*    val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)+
−
(*    val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)+
−
    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);+
−
    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);+
−
(*    val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)+
−
  in+
−
    Conv.rewr_conv ti ctrm+
−
  end+
−
(* TODO: We can add a proper error message... *)+
−
  handle Bind => Conv.all_conv ctrm+
−
+
−
*}+
−
+
−
(* quot stands for the QUOTIENT theorems: *) +
−
(* could be potentially all of them       *)+
−
ML {*+
−
fun lambda_prs_conv ctxt quot ctrm =+
−
  case (term_of ctrm) of+
−
    (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>+
−
      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)+
−
      then_conv (lambda_prs_conv1 ctxt quot)) ctrm+
−
  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm+
−
  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm+
−
  | _ => Conv.all_conv ctrm+
−
*}+
−
+
−
ML {*+
−
fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>+
−
  CONVERSION+
−
    (Conv.params_conv ~1 (fn ctxt =>+
−
       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv+
−
          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)+
−
*}+
−
+
−
ML {*+
−
fun clean_tac lthy quot defs reps_same absrep aps =+
−
  let+
−
    val lower = flat (map (add_lower_defs lthy) defs)+
−
    val aps_thms = map (applic_prs lthy absrep) aps+
−
  in+
−
    EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), +
−
            lambda_prs_tac lthy quot,+
−
            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),+
−
            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),+
−
            simp_tac (HOL_ss addsimps [reps_same])]+
−
  end+
−
*}+
−
+
−
(* Genralisation of free variables in a goal *)+
−
+
−
ML {*+
−
fun inst_spec ctrm =+
−
let+
−
   val cty = ctyp_of_term ctrm+
−
in+
−
   Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}+
−
end+
−
+
−
fun inst_spec_tac ctrms =+
−
  EVERY' (map (dtac o inst_spec) ctrms)+
−
+
−
fun abs_list (xs, t) = +
−
  fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t+
−
+
−
fun gen_frees_tac ctxt =+
−
 SUBGOAL (fn (concl, i) =>+
−
  let+
−
    val thy = ProofContext.theory_of ctxt+
−
    val concl' = HOLogic.dest_Trueprop concl+
−
    val vrs = Term.add_frees concl' []+
−
    val cvrs = map (cterm_of thy o Free) vrs+
−
    val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))+
−
    val goal = Logic.mk_implies (concl'', concl)+
−
    val rule = Goal.prove ctxt [] [] goal +
−
      (K ((inst_spec_tac (rev cvrs) THEN' atac) 1))+
−
  in+
−
    rtac rule i+
−
  end)  +
−
*}+
−
+
−
(* General outline of the lifting procedure *)+
−
(* **************************************** *)+
−
(*                                          *)+
−
(* - A is the original raw theorem          *)+
−
(* - B is the regularized theorem           *)+
−
(* - C is the rep/abs injected version of B *) +
−
(* - D is the lifted theorem                *)+
−
(*                                          *)+
−
(* - b is the regularization step           *)+
−
(* - c is the rep/abs injection step        *)+
−
(* - d is the cleaning part                 *)+
−
+
−
lemma procedure:+
−
  assumes a: "A"+
−
  and     b: "A \<Longrightarrow> B"+
−
  and     c: "B = C"+
−
  and     d: "C = D"+
−
  shows   "D"+
−
  using a b c d+
−
  by simp+
−
+
−
ML {*+
−
fun lift_error ctxt fun_str rtrm qtrm =+
−
let+
−
  val rtrm_str = Syntax.string_of_term ctxt rtrm+
−
  val qtrm_str = Syntax.string_of_term ctxt qtrm+
−
  val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, +
−
             "and the lifted theorem\n", rtrm_str, "do not match"]+
−
in+
−
  error (space_implode " " msg)+
−
end+
−
*}+
−
+
−
ML {* +
−
fun procedure_inst ctxt rtrm qtrm =+
−
let+
−
  val thy = ProofContext.theory_of ctxt+
−
  val rtrm' = HOLogic.dest_Trueprop rtrm+
−
  val qtrm' = HOLogic.dest_Trueprop qtrm+
−
  val reg_goal = +
−
        Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')+
−
        handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm+
−
  val inj_goal = +
−
        Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))+
−
        handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm+
−
in+
−
  Drule.instantiate' []+
−
    [SOME (cterm_of thy rtrm'),+
−
     SOME (cterm_of thy reg_goal),+
−
     SOME (cterm_of thy inj_goal)]+
−
  @{thm procedure}+
−
end+
−
*}+
−
+
−
(* Left for debugging *)+
−
ML {*+
−
fun procedure_tac lthy rthm =+
−
  ObjectLogic.full_atomize_tac+
−
  THEN' gen_frees_tac lthy+
−
  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>+
−
    let+
−
      val rthm' = atomize_thm rthm+
−
      val rule = procedure_inst context (prop_of rthm') (term_of concl)+
−
    in+
−
      rtac rule THEN' rtac rthm'+
−
    end 1) lthy+
−
*}+
−
+
−
ML {*+
−
fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =+
−
  ObjectLogic.full_atomize_tac+
−
  THEN' gen_frees_tac lthy+
−
  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>+
−
    let+
−
      val rthm' = atomize_thm rthm+
−
      val rule = procedure_inst context (prop_of rthm') (term_of concl)+
−
      val aps = find_aps (prop_of rthm') (term_of concl)+
−
    in+
−
      rtac rule THEN' RANGE [+
−
        rtac rthm',+
−
        regularize_tac lthy rel_eqv rel_refl,+
−
        REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),+
−
        clean_tac lthy quot defs reps_same absrep aps+
−
      ]+
−
    end 1) lthy+
−
*}+
−
+
−
end+
−
+
−
+
−