(* Code for getting the goal *)apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}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*}ML {*fun repeat_eqsubst_thm ctxt thms thm = repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) handle _ => thm*}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*}text {* tyRel takes a type and builds a relation that a quantifier over this type needs to respect. *}ML {*fun tyRel ty rty rel lthy = if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty) 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)*}(* ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} *)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 (* FIXME: t should be regularised too *) 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*}(* For polymorphic types we need to find the type of the Relation term. *)(* TODO: we assume that the relation is a Constant. Is this always true? *)ML {*fun my_reg_inst lthy rel rty trm = case rel of Const (n, _) => Syntax.check_term lthy (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)*}(*ML {* val r = Free ("R", dummyT); val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"}); val t2 = Syntax.check_term @{context} t; cterm_of @{theory} t2*}*)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_inst lthy rel rty (prop_of thm)))*}ML {*fun regularize thm rty rel rel_eqv rel_refl lthy = let val goal = 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}, 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}) ]); val cthm = Goal.prove lthy [] [] goal (fn {context, ...} => tac context 1); in cthm OF [thm] end*}(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"axioms Rl_eq: "EQUIV Rl"quotient ql = "'a list" / "Rl" by (rule Rl_eq)ML {* ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}); ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})*}*)ML {*(* returns all subterms where two types differ *)fun diff (T, S) Ds = case (T, S) of (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds | (Type (a, Ts), Type (b, Us)) => if a = b then diffs (Ts, Us) Ds else (T, S)::Ds | _ => (T, S)::Dsand diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) | diffs ([], []) Ds = Ds | diffs _ _ = error "Unequal length of type arguments"*}ML {*fun build_repabs_term lthy thm consts rty qty = let (* TODO: The rty and qty stored in the quotient_info should be varified, so this will soon not be needed *) val rty = Logic.varifyT rty; val qty = Logic.varifyT qty; 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 fun mk_repabs tm = let val ty = fastype_of tm in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end fun is_lifted_const (Const (x, _)) = member (op =) consts x | is_lifted_const _ = 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_repabs ( if not (needs_lift rty vty) then t' else let val v' = mk_repabs v; (* TODO: I believe 'beta' is not needed any more *) val t1 = (* Envir.beta_norm *) (t' $ v') in lambda v t1 end) end | x => case Term.strip_comb tm of (Const(@{const_name Respects}, _), _) => tm | (opp, tms0) => let val tms = map (build_aux lthy) tms0 val ty = fastype_of tm in if (is_lifted_const opp andalso needs_lift rty ty) then mk_repabs (list_comb (opp, tms)) else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then mk_repabs (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 {* Builds provable goals for regularized theorems *}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 repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms = let val rt = build_repabs_term lthy thm consts 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*}(* TODO: Check if it behaves properly with varifyed rty *)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)*}(* Currently useful only for LAMBDA_PRS *)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 lthy 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); val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) in (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy 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 lift_thm lthy qty qty_name rsp_thms defs rthm = let val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm)) 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 rthm; val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t)) val (alls, exs) = findallex lthy 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 _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) 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 _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l)) val defs_sym = flat (map (add_lower_defs lthy) defs); val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; val t_id = simp_ids lthy t_l; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id)) val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0)) val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d)) val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) val t_rv = ObjectLogic.rulify t_r val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))in Thm.varifyT t_rvend*}ML {*fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = let val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; val (_, lthy2) = note (name, lifted_thm) lthy; in lthy2 end*}ML {*fun regularize_goal lthy thm rel_eqv rel_refl qtrm = let val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; fun tac lthy = regularize_tac lthy rel_eqv rel_refl; val cthm = Goal.prove lthy [] [] reg_trm (fn {context, ...} => tac context 1); in cthm OF [thm] end*}ML {*fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = let val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); 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*}ML {*fun atomize_goal thy gl = let val vars = map Free (Term.add_frees gl []); val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all; fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm; val glv = fold lambda_all vars gl val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv)) val glf = Type.legacy_freeze gla in if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf end*}ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}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 lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =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 t_a = atomize_thm rthm; val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a; val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; val (alls, exs) = findallex lthy 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 = flat (map (add_lower_defs lthy) defs); val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; val t_id = simp_ids lthy t_l; val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; val t_rv = ObjectLogic.rulify t_rin Thm.varifyT t_rvend*}ML {*fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal = let val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal; val (_, lthy2) = note (name, lifted_thm) lthy; in lthy2 end*}ML {*fun simp_ids_trm trm = trm |> MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} |> cprop_of |> Thm.dest_equals |> snd*}(* Unused part of the locale *)lemma R_trans: assumes ab: "R a b" and bc: "R b c" shows "R a c"proof - have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp moreover have ab: "R a b" by fact moreover have bc: "R b c" by fact ultimately show "R a c" unfolding transp_def by blastqedlemma R_sym: assumes ab: "R a b" shows "R b a"proof - have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp then show "R b a" using ab unfolding symp_def by blastqedlemma R_trans2: assumes ac: "R a c" and bd: "R b d" shows "R a b = R c d"using ac bdby (blast intro: R_trans R_sym)lemma REPS_same: shows "R (REP a) (REP b) \<equiv> (a = b)"proof - have "R (REP a) (REP b) = (a = b)" proof assume as: "R (REP a) (REP b)" from rep_prop obtain x y where eqs: "Rep a = R x" "Rep b = R y" by blast from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp then have "R x (Eps (R y))" using lem9 by simp then have "R (Eps (R y)) x" using R_sym by blast then have "R y x" using lem9 by simp then have "R x y" using R_sym by blast then have "ABS x = ABS y" using thm11 by simp then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp then show "a = b" using rep_inverse by simp next assume ab: "a = b" have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto qed then show "R (REP a) (REP b) \<equiv> (a = b)" by simpqed