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+
−
+
−
lemma equiv_trans2:+
−
  assumes e: "EQUIV R"+
−
  and     ac: "R a c"+
−
  and     bd: "R b d"+
−
  shows "R a b = R c d"+
−
using ac bd e+
−
unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def+
−
by (blast)+
−
+
−
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 equal_elim_rule1} OF [thm'', thm']+
−
end+
−
*}+
−
+
−
section {* infrastructure about id *}+
−
+
−
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+
−
+
−
lemmas id_simps =+
−
  FUN_MAP_I[THEN eq_reflection]+
−
  id_apply[THEN eq_reflection]+
−
  id_def[THEN eq_reflection,symmetric]+
−
  prod_fun_id map_id+
−
+
−
ML {*+
−
fun simp_ids thm =+
−
  MetaSimplifier.rewrite_rule @{thms id_simps} thm+
−
*}+
−
+
−
section {* Debugging infrastructure for testing tactics *}+
−
+
−
ML {*+
−
fun my_print_tac ctxt s i thm =+
−
let+
−
  val prem_str = nth (prems_of thm) (i - 1)+
−
                 |> Syntax.string_of_term ctxt+
−
                 handle Subscript => "no subgoal"+
−
  val _ = tracing (s ^ "\n" ^ prem_str)+
−
in+
−
  Seq.single thm+
−
end *}+
−
+
−
+
−
ML {*+
−
fun DT ctxt s tac i thm =+
−
let+
−
  val before_goal = nth (prems_of thm) (i - 1)+
−
                    |> Syntax.string_of_term ctxt+
−
  val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]+
−
                   |> cat_lines+
−
in +
−
  EVERY [tac i, my_print_tac ctxt before_msg i] thm+
−
end+
−
+
−
fun NDT ctxt s tac thm = tac thm  +
−
*}+
−
+
−
+
−
section {*  Infrastructure about definitions *}+
−
+
−
(* 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 equal_elim_rule1} OF [rt, thm]+
−
  end+
−
*}+
−
+
−
(* expects atomized definitions *)+
−
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 f+
−
  in+
−
    (simp_ids thm) :: (add_lower_defs_aux lthy g)+
−
  end+
−
  handle _ => [simp_ids 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 for collecting theorems for starting the 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 = @{thm EQUIV_REFL} OF [rel_eqv]+
−
  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+
−
*}+
−
+
−
section {* Infrastructure for special quotient identity *}+
−
+
−
definition+
−
  "qid TYPE('a) TYPE('b) x \<equiv> x"+
−
+
−
ML {*+
−
fun get_typ_aux (Type ("itself", [T])) = T +
−
fun get_typ (Const ("TYPE", T)) = get_typ_aux T+
−
fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =+
−
  (get_typ ty1, get_typ ty2)+
−
+
−
fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true+
−
  | is_qid _ = false+
−
+
−
+
−
fun mk_itself ty = Type ("itself", [ty])+
−
fun mk_TYPE ty = Const ("TYPE", mk_itself ty)+
−
fun mk_qid (rty, qty, trm) = +
−
  Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) +
−
    $ mk_TYPE rty $ mk_TYPE qty $ trm+
−
*}+
−
+
−
ML {*+
−
fun insertion_aux rtrm qtrm =+
−
  case (rtrm, qtrm) of+
−
    (Abs (x, ty, t), Abs (x', ty', t')) =>+
−
       let+
−
         val (y, s) = Term.dest_abs (x, ty, t)+
−
         val (_, s') = Term.dest_abs (x', ty', t')+
−
         val yvar = Free (y, ty)+
−
         val result = Term.lambda_name (y, yvar) (insertion_aux s s')+
−
       in     +
−
         if ty = ty'+
−
         then result+
−
         else mk_qid (ty, ty', result)+
−
       end+
−
  | (t1 $ t2, t1' $ t2') =>+
−
       let +
−
         val rty = fastype_of rtrm+
−
         val qty = fastype_of qtrm +
−
         val subtrm1 = insertion_aux t1 t1' +
−
         val subtrm2 = insertion_aux t2 t2'+
−
       in+
−
         if rty = qty+
−
         then subtrm1 $ subtrm2+
−
         else mk_qid (rty, qty, subtrm1 $ subtrm2)+
−
       end+
−
  | (Free (_, ty), Free (_, ty')) =>+
−
       if ty = ty'+
−
       then rtrm +
−
       else mk_qid (ty, ty', rtrm)+
−
  | (Const (s, ty), Const (s', ty')) =>+
−
       if s = s' andalso ty = ty'+
−
       then rtrm+
−
       else mk_qid (ty, ty', rtrm) +
−
  | (_, _) => raise (LIFT_MATCH "insertion")+
−
*}+
−
+
−
section {* Regularization *} +
−
+
−
(*+
−
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 trm =+
−
  case trm of+
−
    (Abs (x, T, t)) => Abs (x, T, f t)+
−
  | _ => f trm+
−
+
−
(* the major type of All and Ex quantifiers *)+
−
fun qnt_typ ty = domain_type (domain_type ty)  +
−
*}+
−
+
−
ML {*+
−
(* produces a regularized version of trm      *)+
−
(* - the result is still not completely typed *)+
−
(* - does not need any special treatment of   *)+
−
(*   bound variables                          *)+
−
+
−
fun regularize_trm lthy trm =+
−
  case trm of+
−
    (Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) =>+
−
       let+
−
         val rty = get_typ rty'+
−
         val qty = get_typ qty'+
−
         val subtrm = regularize_trm lthy t+
−
       in     +
−
         mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm)+
−
       end+
−
  | (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) => +
−
       let+
−
         val subtrm = apply_subt (regularize_trm lthy) 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')) => +
−
       (* 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)")+
−
  | (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)")+
−
*}+
−
+
−
(*+
−
FIXME / TODO: needs to be adapted+
−
+
−
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+
−
+
−
*)+
−
+
−
(* FIXME: they should be in in the new Isabelle *)+
−
lemma [mono]: +
−
  "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"+
−
by blast+
−
+
−
lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"+
−
by auto+
−
+
−
(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)+
−
ML {*+
−
fun equiv_tac rel_eqvs =+
−
  REPEAT_ALL_NEW (FIRST' +
−
    [resolve_tac rel_eqvs,+
−
     rtac @{thm IDENTITY_EQUIV},+
−
     rtac @{thm LIST_EQUIV}])+
−
*}+
−
+
−
ML {*+
−
fun ball_reg_eqv_simproc rel_eqvs ss redex =+
−
  let+
−
    val ctxt = Simplifier.the_context ss+
−
    val thy = ProofContext.theory_of ctxt+
−
  in+
−
  case redex of+
−
      (ogl as ((Const (@{const_name "Ball"}, _)) $+
−
        ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>+
−
      (let+
−
        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;+
−
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);+
−
        val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);+
−
        val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);+
−
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)+
−
      in+
−
        SOME thm+
−
      end+
−
      handle _ => NONE+
−
      )+
−
  | _ => NONE+
−
  end+
−
*}+
−
+
−
ML {*+
−
fun bex_reg_eqv_simproc rel_eqvs ss redex =+
−
  let+
−
    val ctxt = Simplifier.the_context ss+
−
    val thy = ProofContext.theory_of ctxt+
−
  in+
−
  case redex of+
−
      (ogl as ((Const (@{const_name "Bex"}, _)) $+
−
        ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>+
−
      (let+
−
        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;+
−
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);+
−
        val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);+
−
        val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);+
−
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)+
−
      in+
−
        SOME thm+
−
      end+
−
      handle _ => NONE+
−
      )+
−
  | _ => NONE+
−
  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 ball_reg_eqv_range_simproc rel_eqvs ss redex =+
−
  let+
−
    val ctxt = Simplifier.the_context ss+
−
    val thy = ProofContext.theory_of ctxt+
−
  in+
−
  case redex of+
−
      (ogl as ((Const (@{const_name "Ball"}, _)) $+
−
        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>+
−
      (let+
−
        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;+
−
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);+
−
        val _ = tracing (Syntax.string_of_term ctxt glc);+
−
        val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);+
−
        val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);+
−
        val R1c = cterm_of thy R1;+
−
        val thmi = Drule.instantiate' [] [SOME R1c] thm;+
−
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)+
−
        val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl+
−
        val _ = tracing "AAA";+
−
        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);+
−
        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));+
−
      in+
−
        SOME thm2+
−
      end+
−
      handle _ => NONE+
−
+
−
      )+
−
  | _ => NONE+
−
  end+
−
*}+
−
+
−
ML {*+
−
fun bex_reg_eqv_range_simproc rel_eqvs ss redex =+
−
  let+
−
    val ctxt = Simplifier.the_context ss+
−
    val thy = ProofContext.theory_of ctxt+
−
  in+
−
  case redex of+
−
      (ogl as ((Const (@{const_name "Bex"}, _)) $+
−
        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>+
−
      (let+
−
        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;+
−
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);+
−
        val _ = tracing (Syntax.string_of_term ctxt glc);+
−
        val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);+
−
        val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);+
−
        val R1c = cterm_of thy R1;+
−
        val thmi = Drule.instantiate' [] [SOME R1c] thm;+
−
(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)+
−
        val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl+
−
        val _ = tracing "AAA";+
−
        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);+
−
        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));+
−
      in+
−
        SOME thm2+
−
      end+
−
      handle _ => NONE+
−
+
−
      )+
−
  | _ => NONE+
−
  end+
−
*}+
−
+
−
lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"+
−
by (simp add: EQUIV_REFL)+
−
+
−
ML {*+
−
fun regularize_tac ctxt rel_eqvs =+
−
  let+
−
    val pat1 = [@{term "Ball (Respects R) P"}];+
−
    val pat2 = [@{term "Bex (Respects R) P"}];+
−
    val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];+
−
    val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];+
−
    val thy = ProofContext.theory_of ctxt+
−
    val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))+
−
    val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))+
−
    val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))+
−
    val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))+
−
    val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]+
−
    (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)+
−
    val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs+
−
  in+
−
  ObjectLogic.full_atomize_tac THEN'+
−
  simp_tac simp_ctxt THEN'+
−
  REPEAT_ALL_NEW (FIRST' [+
−
    rtac @{thm ball_reg_right},+
−
    rtac @{thm bex_reg_left},+
−
    resolve_tac (Inductive.get_monos ctxt),+
−
    rtac @{thm ball_all_comm},+
−
    rtac @{thm bex_ex_comm},+
−
    resolve_tac eq_eqvs,+
−
    simp_tac simp_ctxt+
−
  ])+
−
  end+
−
*}+
−
+
−
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_trm 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_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') =>+
−
       Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm 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 = 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+
−
  | _ =>+
−
      (* 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_trm 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_trm lthy (rhead, qhead), rargs')) +
−
          | _ => raise (LIFT_MATCH "injection")+
−
      end+
−
end+
−
*}+
−
+
−
section {* RepAbs Injection Tactic *}+
−
+
−
ML {*+
−
fun stripped_term_of ct =+
−
  ct |> term_of |> HOLogic.dest_Trueprop+
−
*}+
−
+
−
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_thms =+
−
  REPEAT_ALL_NEW (FIRST' +
−
    [rtac @{thm FUN_QUOTIENT},+
−
     resolve_tac quot_thms,+
−
     rtac @{thm IDENTITY_QUOTIENT},+
−
     (* For functional identity quotients, (op = ---> op =) *)+
−
     (* TODO: think about the other way around, if we need to shorten the relation *)+
−
     CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])+
−
*}+
−
+
−
lemma FUN_REL_I:+
−
  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"+
−
  shows "(R1 ===> R2) f g"+
−
using a by (simp add: FUN_REL.simps)+
−
+
−
ML {*+
−
val lambda_res_tac =+
−
  Subgoal.FOCUS (fn {concl, ...} =>+
−
    case (stripped_term_of concl) of+
−
       (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1+
−
     | _ => no_tac)+
−
*}+
−
+
−
ML {*+
−
val weak_lambda_res_tac =+
−
  Subgoal.FOCUS (fn {concl, ...} =>+
−
    case (stripped_term_of concl) of+
−
       (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1+
−
     | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1+
−
     | _ => no_tac)+
−
*}+
−
+
−
ML {*+
−
val ball_rsp_tac = +
−
  Subgoal.FOCUS (fn {concl, ...} =>+
−
     case (stripped_term_of concl) of+
−
        (_ $ (Const (@{const_name Ball}, _) $ _) +
−
           $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1+
−
      |_ => no_tac)+
−
*}+
−
+
−
ML {*+
−
val bex_rsp_tac = +
−
  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>+
−
     case (stripped_term_of concl) of+
−
        (_ $ (Const (@{const_name Bex}, _) $ _) +
−
           $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1+
−
      | _ => no_tac)+
−
*}+
−
+
−
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, ...} =>+
−
    case (stripped_term_of concl) of+
−
       (_ $ (f $ _) $ (_ $ _)) =>+
−
          let+
−
            val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});+
−
            val insts = Thm.match (pat, concl)+
−
          in+
−
            if needs_lift rty (fastype_of f) +
−
            then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1+
−
            else no_tac+
−
          end+
−
     | _ => no_tac)+
−
*}+
−
+
−
ML {*+
−
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)+
−
*}+
−
+
−
(*+
−
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+
−
 A) reflexivity of the relation+
−
 B) assumption+
−
    (Lambdas under respects may have left us some assumptions)+
−
 C) proving obvious higher order equalities by simplifying fun_rel+
−
    (not sure if it is still needed?)+
−
 D) unfolding lambda on one side+
−
 E) simplifying (= ===> =) for simpler respectfulness+
−
+
−
*)+
−
+
−
ML {*+
−
fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =+
−
  (FIRST' [+
−
    (* "cong" rule of the of the relation / transitivity*)+
−
    (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)+
−
    NDT ctxt "1" (resolve_tac trans2),+
−
+
−
    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) +
−
    NDT ctxt "2" (lambda_res_tac ctxt),+
−
+
−
    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)+
−
    NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),+
−
+
−
    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)+
−
    NDT ctxt "4" (ball_rsp_tac ctxt),+
−
+
−
    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)+
−
    NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),+
−
+
−
    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)+
−
    NDT ctxt "6" (bex_rsp_tac ctxt),+
−
+
−
    (* respectfulness of constants *)+
−
    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),+
−
+
−
    (* reflexivity of operators arising from Cong_tac *)+
−
    NDT ctxt "8" (rtac @{thm refl}),+
−
+
−
    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)+
−
    (* observe ---> *) +
−
    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt +
−
                  THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),+
−
+
−
    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)+
−
    NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' +
−
                (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),+
−
+
−
    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)+
−
    (* merge with previous tactic *)+
−
    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),+
−
+
−
    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)+
−
    NDT ctxt "C" (rtac @{thm ext}),+
−
    +
−
    (* reflexivity of the basic relations *)+
−
    (* R \<dots> \<dots> *)+
−
    NDT ctxt "D" (resolve_tac rel_refl),+
−
+
−
    (* resolving with R x y assumptions *)+
−
    NDT ctxt "E" (atac),+
−
+
−
    (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)+
−
    +
−
    (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) +
−
    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) +
−
    (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*)+
−
+
−
    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)+
−
    (* global simplification *)+
−
    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])+
−
*}+
−
+
−
ML {*+
−
fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =+
−
  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)+
−
*}+
−
+
−
+
−
section {* Cleaning of the theorem *}+
−
+
−
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 (@{thms fun_map.simps id_simps} @ absrep);+
−
    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)+
−
    val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;+
−
  in+
−
    singleton (ProofContext.export lthy' lthy) t_id+
−
  end+
−
*}+
−
+
−
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 {*+
−
fun allex_prs_tac lthy quot =+
−
  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})+
−
  THEN' (quotient_tac quot)+
−
*}+
−
+
−
(* Rewrites the term with LAMBDA_PRS thm.+
−
+
−
Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))+
−
    with: f+
−
+
−
It proves the QUOTIENT assumptions by calling quotient_tac+
−
 *)+
−
ML {*+
−
fun make_inst lhs t =+
−
  let+
−
    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;+
−
    val _ $ (Abs (_, _, g)) = t;+
−
    fun mk_abs i t =+
−
      if incr_boundvars i u aconv t then Bound i+
−
      else (case t of+
−
        t1 $ t2 => mk_abs i t1 $ mk_abs i t2+
−
      | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')+
−
      | Bound j => if i = j then error "make_inst" else t+
−
      | _ => t);+
−
  in (f, Abs ("x", T, mk_abs 0 g)) end;+
−
+
−
fun lambda_prs_conv1 ctxt quot_thms 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_thms);+
−
    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 @{thms id_simps} te+
−
    val tl = Thm.lhs_of ts;+
−
    val (insp, inst) = make_inst (term_of tl) (term_of ctrm);+
−
    val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;+
−
(*    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)+
−
  in+
−
    Conv.rewr_conv ti ctrm+
−
  end+
−
*}+
−
+
−
(* 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 aps =+
−
  let+
−
    val lower = flat (map (add_lower_defs lthy) defs)+
−
    val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower+
−
    val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot+
−
    val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot+
−
    val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same+
−
    val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower)+
−
    val aps_thms = map (applic_prs lthy absrep) aps+
−
  in+
−
    EVERY' [lambda_prs_tac lthy quot,+
−
            TRY o simp_tac simp_ctxt,+
−
            TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),+
−
            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),+
−
            TRY o rtac refl]+
−
  end+
−
*}+
−
+
−
section {* Genralisation of free variables in a goal *}+
−
+
−
ML {*+
−
fun inst_spec ctrm =+
−
   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}+
−
+
−
fun inst_spec_tac ctrms =+
−
  EVERY' (map (dtac o inst_spec) ctrms)+
−
+
−
fun all_list xs trm = +
−
  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm+
−
+
−
fun apply_under_Trueprop f = +
−
  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop+
−
+
−
fun gen_frees_tac ctxt =+
−
 SUBGOAL (fn (concl, i) =>+
−
  let+
−
    val thy = ProofContext.theory_of ctxt+
−
    val vrs = Term.add_frees concl []+
−
    val cvrs = map (cterm_of thy o Free) vrs+
−
    val concl' = apply_under_Trueprop (all_list vrs) concl+
−
    val goal = Logic.mk_implies (concl', concl)+
−
    val rule = Goal.prove ctxt [] [] goal +
−
      (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))+
−
  in+
−
    rtac rule i+
−
  end)  +
−
*}+
−
+
−
section {* 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 lifting_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_match_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_match_error ctxt s rtrm qtrm+
−
  val inj_goal = +
−
        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))+
−
        handle (LIFT_MATCH s) => lift_match_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 lifting_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+
−
      EVERY1 [rtac rule, rtac rthm']+
−
    end) lthy+
−
*}+
−
+
−
ML {*+
−
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)+
−
fun lift_tac lthy rthm rel_eqv rty quot 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)+
−
      val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv+
−
      val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv+
−
    in+
−
      EVERY1+
−
       [rtac rule,+
−
        RANGE [rtac rthm',+
−
               regularize_tac lthy rel_eqv,+
−
               all_inj_repabs_tac lthy rty quot rel_refl trans2,+
−
               clean_tac lthy quot defs aps]]+
−
    end) lthy+
−
*}+
−
+
−
end+
−
+
−
+
−