--- a/FIXME-TODO Fri Dec 04 15:19:39 2009 +0100
+++ b/FIXME-TODO Fri Dec 04 15:20:06 2009 +0100
@@ -48,3 +48,5 @@
- Check all the places where we do "handle _"
+- We shouldn't use the command 'quotient' as this shadows Larry's quotient.
+ Call it 'quotient_type'
--- a/FSet.thy Fri Dec 04 15:19:39 2009 +0100
+++ b/FSet.thy Fri Dec 04 15:20:06 2009 +0100
@@ -16,14 +16,14 @@
shows "xs \<approx> xs"
by (induct xs) (auto intro: list_eq.intros)
-lemma equiv_list_eq:
- shows "EQUIV list_eq"
- unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+lemma equivp_list_eq:
+ shows "equivp list_eq"
+ unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
apply(auto intro: list_eq.intros list_eq_refl)
done
quotient fset = "'a list" / "list_eq"
- apply(rule equiv_list_eq)
+ apply(rule equivp_list_eq)
done
print_theorems
@@ -59,7 +59,7 @@
term FUNION
thm FUNION_def
-thm QUOTIENT_fset
+thm Quotient_fset
thm QUOT_TYPE_I_fset.thm11
@@ -418,7 +418,7 @@
done
quotient fset2 = "'a list" / "list_eq"
- apply(rule equiv_list_eq)
+ apply(rule equivp_list_eq)
done
quotient_def
@@ -431,7 +431,7 @@
where
"INSERT2 \<equiv> op #"
-ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
+ML {* val quot = @{thms Quotient_fset Quotient_fset2} *}
ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
--- a/IntEx.thy Fri Dec 04 15:19:39 2009 +0100
+++ b/IntEx.thy Fri Dec 04 15:20:06 2009 +0100
@@ -9,13 +9,13 @@
"intrel (x, y) (u, v) = (x + v = u + y)"
quotient my_int = "nat \<times> nat" / intrel
- apply(unfold EQUIV_def)
+ apply(unfold equivp_def)
apply(auto simp add: mem_def expand_fun_eq)
done
thm quotient_thm
-thm my_int_equiv
+thm my_int_equivp
print_theorems
print_quotients
@@ -198,30 +198,30 @@
lemma foldr_prs:
- assumes a: "QUOTIENT R1 abs1 rep1"
- and b: "QUOTIENT R2 abs2 rep2"
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient R2 abs2 rep2"
shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
apply (induct l)
-apply (simp add: QUOTIENT_ABS_REP[OF b])
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
done
lemma foldl_prs:
- assumes a: "QUOTIENT R1 abs1 rep1"
- and b: "QUOTIENT R2 abs2 rep2"
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient R2 abs2 rep2"
shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
apply (induct l arbitrary:e)
-apply (simp add: QUOTIENT_ABS_REP[OF a])
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
done
lemma map_prs:
- assumes a: "QUOTIENT R1 abs1 rep1"
- and b: "QUOTIENT R2 abs2 rep2"
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient R2 abs2 rep2"
shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
apply (induct l)
apply (simp)
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
done
@@ -231,10 +231,10 @@
by simp
lemma cons_prs:
- assumes a: "QUOTIENT R1 abs1 rep1"
+ assumes a: "Quotient R1 abs1 rep1"
shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t"
apply (induct t)
-by (simp_all add: QUOTIENT_ABS_REP[OF a])
+by (simp_all add: Quotient_ABS_REP[OF a])
lemma cons_rsp[quotient_rsp]:
"(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
@@ -264,7 +264,7 @@
apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
apply(simp only: nil_prs)
apply(tactic {* clean_tac @{context} 1 *})
done
@@ -276,8 +276,8 @@
apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
-apply(simp only: cons_prs[OF QUOTIENT_my_int])
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
+apply(simp only: cons_prs[OF Quotient_my_int])
apply(tactic {* clean_tac @{context} 1 *})
done
--- a/QuotList.thy Fri Dec 04 15:19:39 2009 +0100
+++ b/QuotList.thy Fri Dec 04 15:20:06 2009 +0100
@@ -2,7 +2,7 @@
imports QuotScript
begin
-lemma LIST_map_I:
+lemma LIST_map_id:
shows "map (\<lambda>x. x) = (\<lambda>x. x)"
by simp
@@ -28,10 +28,10 @@
shows "LIST_REL R x x"
by (induct x) (auto simp add: a)
-lemma LIST_EQUIV:
- assumes a: "EQUIV R"
- shows "EQUIV (LIST_REL R)"
-unfolding EQUIV_def
+lemma LIST_equivp:
+ assumes a: "equivp R"
+ shows "equivp (LIST_REL R)"
+unfolding equivp_def
apply(rule allI)+
apply(induct_tac x y rule: list_induct2')
apply(simp)
@@ -46,70 +46,70 @@
apply(simp)
apply(simp)
using a
-apply(unfold EQUIV_def)
+apply(unfold equivp_def)
apply(auto)[1]
apply(metis LIST_REL.simps(4))
done
lemma LIST_REL_REL:
- assumes q: "QUOTIENT R Abs Rep"
+ assumes q: "Quotient R Abs Rep"
shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))"
apply(induct r s rule: list_induct2')
apply(simp_all)
-using QUOTIENT_REL[OF q]
+using Quotient_REL[OF q]
apply(metis)
done
-lemma LIST_QUOTIENT:
- assumes q: "QUOTIENT R Abs Rep"
- shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)"
-unfolding QUOTIENT_def
+lemma LIST_Quotient:
+ assumes q: "Quotient R Abs Rep"
+ shows "Quotient (LIST_REL R) (map Abs) (map Rep)"
+unfolding Quotient_def
apply(rule conjI)
apply(rule allI)
apply(induct_tac a)
apply(simp)
-apply(simp add: QUOTIENT_ABS_REP[OF q])
+apply(simp add: Quotient_ABS_REP[OF q])
apply(rule conjI)
apply(rule allI)
apply(induct_tac a)
apply(simp)
apply(simp)
-apply(simp add: QUOTIENT_REP_REFL[OF q])
+apply(simp add: Quotient_REP_reflp[OF q])
apply(rule allI)+
apply(rule LIST_REL_REL[OF q])
done
lemma CONS_PRS:
- assumes q: "QUOTIENT R Abs Rep"
+ assumes q: "Quotient R Abs Rep"
shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))"
-by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q])
+by (induct t) (simp_all add: Quotient_ABS_REP[OF q])
lemma CONS_RSP:
- assumes q: "QUOTIENT R Abs Rep"
+ assumes q: "Quotient R Abs Rep"
and a: "R h1 h2" "LIST_REL R t1 t2"
shows "LIST_REL R (h1#t1) (h2#t2)"
using a by (auto)
lemma NIL_PRS:
- assumes q: "QUOTIENT R Abs Rep"
+ assumes q: "Quotient R Abs Rep"
shows "[] = (map Abs [])"
by (simp)
lemma NIL_RSP:
- assumes q: "QUOTIENT R Abs Rep"
+ assumes q: "Quotient R Abs Rep"
shows "LIST_REL R [] []"
by simp
lemma MAP_PRS:
- assumes q1: "QUOTIENT R1 Abs1 Rep1"
- and q2: "QUOTIENT R2 Abs2 Rep2"
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))"
by (induct l)
- (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2])
+ (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2])
lemma MAP_RSP:
- assumes q1: "QUOTIENT R1 Abs1 Rep1"
- and q2: "QUOTIENT R2 Abs2 Rep2"
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
and a: "(R1 ===> R2) f1 f2"
and b: "LIST_REL R1 l1 l2"
shows "LIST_REL R2 (map f1 l1) (map f2 l2)"
--- a/QuotMain.thy Fri Dec 04 15:19:39 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 15:20:06 2009 +0100
@@ -9,7 +9,7 @@
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"
+ assumes equiv: "equivp R"
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
and rep_inverse: "\<And>x. Abs (Rep x) = x"
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
@@ -29,10 +29,10 @@
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)
+ have a: "R x x" using equiv by (simp add: equivp_reflp_symp_transp reflp_def)
then have "R x (Eps (R x))" by (rule someI)
then show "R (Eps (R x)) = R x"
- using equiv unfolding EQUIV_def by simp
+ using equiv unfolding equivp_def by simp
qed
theorem thm10:
@@ -53,7 +53,7 @@
lemma REP_refl:
shows "R (REP a) (REP a)"
unfolding REP_def
-by (simp add: equiv[simplified EQUIV_def])
+by (simp add: equiv[simplified equivp_def])
lemma lem7:
shows "(R x = R y) = (Abs (R x) = Abs (R y))"
@@ -66,7 +66,7 @@
theorem thm11:
shows "R r r' = (ABS r = ABS r')"
unfolding ABS_def
-by (simp only: equiv[simplified EQUIV_def] lem7)
+by (simp only: equiv[simplified equivp_def] lem7)
lemma REP_ABS_rsp:
@@ -74,13 +74,13 @@
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)
+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])
+apply(simp add: equiv[simplified equivp_def])
done
lemma R_trans:
@@ -88,18 +88,18 @@
and bc: "R b c"
shows "R a c"
proof -
- have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ have tr: "transp R" using equiv 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 TRANS_def by blast
+ ultimately show "R a c" unfolding transp_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
+ have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp
+ then show "R b a" using ab unfolding symp_def by blast
qed
lemma R_trans2:
@@ -128,8 +128,8 @@
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
+ have "reflp R" using equiv 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 simp
qed
@@ -146,7 +146,7 @@
declare [[map "fun" = (fun_map, FUN_REL)]]
lemmas [quotient_thm] =
- FUN_QUOTIENT LIST_QUOTIENT
+ FUN_Quotient LIST_Quotient
ML {* maps_lookup @{theory} "List.list" *}
ML {* maps_lookup @{theory} "*" *}
@@ -265,7 +265,7 @@
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]
+ val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
in
(rty, rel, rel_refl, rel_eqv)
end
@@ -278,7 +278,7 @@
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)
+ val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
in
(trans2, reps_same, absrep, quot)
end
@@ -455,13 +455,13 @@
lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
by auto
-(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
+(* FIXME: OPTION_equivp, PAIR_equivp, ... *)
ML {*
fun equiv_tac rel_eqvs =
REPEAT_ALL_NEW (FIRST'
[resolve_tac rel_eqvs,
- rtac @{thm IDENTITY_EQUIV},
- rtac @{thm LIST_EQUIV}])
+ rtac @{thm IDENTITY_equivp},
+ rtac @{thm LIST_equivp}])
*}
ML {*
@@ -474,7 +474,7 @@
(ogl as ((Const (@{const_name "Ball"}, _)) $
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
(let
- val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+ val gl = Const (@{const_name "equivp"}, 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]]);
@@ -498,7 +498,7 @@
(ogl as ((Const (@{const_name "Bex"}, _)) $
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
(let
- val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+ val gl = Const (@{const_name "equivp"}, 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]]);
@@ -542,7 +542,7 @@
(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 gl = Const (@{const_name "equivp"}, 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);
@@ -573,7 +573,7 @@
(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 gl = Const (@{const_name "equivp"}, 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);
@@ -594,8 +594,8 @@
end
*}
-lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
-by (simp add: EQUIV_REFL)
+lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+by (simp add: equivp_reflp)
ML {*
fun regularize_tac ctxt rel_eqvs =
@@ -724,7 +724,7 @@
ML {*
fun quotient_tac ctxt =
REPEAT_ALL_NEW (FIRST'
- [rtac @{thm IDENTITY_QUOTIENT},
+ [rtac @{thm IDENTITY_Quotient},
resolve_tac (quotient_rules_get ctxt)])
*}
@@ -776,7 +776,7 @@
end
*}
-(* It proves the QUOTIENT assumptions by calling quotient_tac *)
+(* It proves the Quotient assumptions by calling quotient_tac *)
ML {*
fun solve_quotient_assum i ctxt thm =
let
@@ -1088,7 +1088,7 @@
- Rewriting with definitions from the argument defs
NewConst ----> (rep ---> abs) oldConst
- - QUOTIENT_REL_REP:
+ - Quotient_REL_REP:
Rel (Rep x) (Rep y) ----> x = y
- ABS_REP
@@ -1107,9 +1107,9 @@
val thy = ProofContext.theory_of lthy;
val quotients = quotient_rules_get lthy
val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
- val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients
+ val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients
val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
- val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients
+ val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients
val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
(@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
@@ -1237,7 +1237,7 @@
let
val rthm' = atomize_thm rthm
val rule = procedure_inst context (prop_of rthm') (term_of concl)
- val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
+ val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv
val quotients = quotient_rules_get lthy
val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
--- a/quotient.ML Fri Dec 04 15:19:39 2009 +0100
+++ b/quotient.ML Fri Dec 04 15:20:06 2009 +0100
@@ -102,13 +102,13 @@
(* proves the quotient theorem *)
fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
let
- val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
+ val quotient_const = Const (@{const_name "Quotient"}, dummyT)
val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
|> Syntax.check_term lthy
val typedef_quotient_thm_tac =
EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
- rtac @{thm QUOT_TYPE.QUOTIENT},
+ rtac @{thm QUOT_TYPE.Quotient},
rtac quot_type_thm]
in
Goal.prove lthy [] [] goal
@@ -146,7 +146,7 @@
(* quotient theorem *)
val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
- val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
+ val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
(* storing the quot-info *)
val qty_str = fst (Term.dest_Type abs_ty)
@@ -157,7 +157,7 @@
(* FIXME: to recalculated in for example REGULARIZE *)
(* storing of the equiv_thm under a name *)
- val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3
+ val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3
(* interpretation *)
val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -205,9 +205,9 @@
let
fun mk_goal (rty, rel) =
let
- val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+ val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
in
- HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel)
+ HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
end
val goals = map (mk_goal o snd) quot_list