--- a/src/HOL/Eisbach/match_method.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Eisbach/match_method.ML Sun Aug 11 23:11:03 2024 +0200
@@ -480,7 +480,7 @@
val tenv = Envir.term_env env;
val tyenv = Envir.type_env env;
in
- forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
+ Vartab.forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) tenv
end;
fun term_eq_wrt (env1, env2) (t1, t2) =
--- a/src/HOL/Lifting.thy Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Lifting.thy Sun Aug 11 23:11:03 2024 +0200
@@ -25,12 +25,13 @@
subsection \<open>Quotient Predicate\<close>
-definition
- "Quotient R Abs Rep T \<longleftrightarrow>
- (\<forall>a. Abs (Rep a) = a) \<and>
- (\<forall>a. R (Rep a) (Rep a)) \<and>
- (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
- T = (\<lambda>x y. R x x \<and> Abs x = y)"
+definition Quotient :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ (\<forall>a. Abs (Rep a) = a) \<and>
+ (\<forall>a. R (Rep a) (Rep a)) \<and>
+ (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
+ T = (\<lambda>x y. R x x \<and> Abs x = y)"
lemma QuotientI:
assumes "\<And>a. Abs (Rep a) = a"
--- a/src/HOL/Quotient.thy Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Quotient.thy Sun Aug 11 23:11:03 2024 +0200
@@ -268,11 +268,9 @@
assumes a: "equivp R2"
shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
proof -
- { fix f
- assume "P (f x)"
- have "(\<lambda>y. f x) \<in> Respects (R1 ===> R2)"
- using a equivp_reflp_symp_transp[of "R2"]
- by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE) }
+ have "(\<lambda>y. f x) \<in> Respects (R1 ===> R2)" for f
+ using a equivp_reflp_symp_transp[of "R2"]
+ by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE)
then show ?thesis
by auto
qed
@@ -338,12 +336,13 @@
and q2: "Quotient3 R2 Abs2 Rep2"
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
proof -
- { fix x
+ have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x" for x
+ proof -
have "Rep1 x \<in> Respects R1"
by (simp add: in_respects Quotient3_rel_rep[OF q1])
- then have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x"
+ then show ?thesis
by (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
- }
+ qed
then show ?thesis
by force
qed
@@ -422,8 +421,7 @@
shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
(is "?lhs = ?rhs")
using assms
- apply (auto simp add: Bex1_rel_def Respects_def)
- by (metis (full_types) Quotient3_def)+
+ by (auto simp add: Bex1_rel_def Respects_def) (metis (full_types) Quotient3_def)+
lemma bex1_bexeq_reg:
shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
@@ -440,8 +438,7 @@
lemma quot_rel_rsp:
assumes a: "Quotient3 R Abs Rep"
shows "(R ===> R ===> (=)) R R"
- apply(rule rel_funI)+
- by (meson assms equals_rsp)
+ by (rule rel_funI)+ (meson assms equals_rsp)
lemma o_prs:
assumes q1: "Quotient3 R1 Abs1 Rep1"
@@ -519,35 +516,33 @@
lemma some_collect:
assumes "R r r"
shows "R (SOME x. x \<in> Collect (R r)) = R r"
- apply simp
- by (metis assms exE_some equivp[simplified part_equivp_def])
+ by simp (metis assms exE_some equivp[simplified part_equivp_def])
-lemma Quotient:
- shows "Quotient3 R abs rep"
+lemma Quotient: "Quotient3 R abs rep"
unfolding Quotient3_def abs_def rep_def
- proof (intro conjI allI)
- fix a r s
- show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
- obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
- have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis
- then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
- then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
- using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>)
- qed
- have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
- then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
- have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
- proof -
- assume "R r r" and "R s s"
- then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
- by (metis abs_inverse)
- also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
- by (rule iffI) simp_all
- finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
- qed
- then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
- using equivp[simplified part_equivp_def] by metis
- qed
+proof (intro conjI allI)
+ fix a r s
+ show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
+ obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
+ have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis
+ then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
+ then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
+ using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>)
+ qed
+ have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
+ then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
+ have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
+ proof -
+ assume "R r r" and "R s s"
+ then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
+ by (metis abs_inverse)
+ also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
+ by (rule iffI) simp_all
+ finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
+ qed
+ then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
+ using equivp[simplified part_equivp_def] by metis
+qed
end
@@ -576,9 +571,8 @@
using r Quotient3_refl1 R1 rep_abs_rsp by fastforce
moreover have "R2' (Rep1 (Abs1 r)) (Rep1 (Abs1 s))"
using that
- apply simp
- apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1])
- done
+ by simp (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1]
+ Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1])
moreover have "R1 (Rep1 (Abs1 s)) s"
by (metis s Quotient3_rel R1 rep_abs_rsp_left)
ultimately show ?thesis
@@ -616,27 +610,25 @@
subsection \<open>Quotient3 to Quotient\<close>
lemma Quotient3_to_Quotient:
-assumes "Quotient3 R Abs Rep"
-and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
-shows "Quotient R Abs Rep T"
-using assms unfolding Quotient3_def by (intro QuotientI) blast+
+ assumes "Quotient3 R Abs Rep"
+ and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
+ shows "Quotient R Abs Rep T"
+ using assms unfolding Quotient3_def by (intro QuotientI) blast+
lemma Quotient3_to_Quotient_equivp:
-assumes q: "Quotient3 R Abs Rep"
-and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
-and eR: "equivp R"
-shows "Quotient R Abs Rep T"
+ assumes q: "Quotient3 R Abs Rep"
+ and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
+ and eR: "equivp R"
+ shows "Quotient R Abs Rep T"
proof (intro QuotientI)
- fix a
- show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep)
-next
- fix a
- show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp)
-next
- fix r s
- show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric])
-next
- show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
+ show "Abs (Rep a) = a" for a
+ using q by(rule Quotient3_abs_rep)
+ show "R (Rep a) (Rep a)" for a
+ using q by(rule Quotient3_rep_reflp)
+ show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" for r s
+ using q by(rule Quotient3_rel[symmetric])
+ show "T = (\<lambda>x y. R x x \<and> Abs x = y)"
+ using T_def equivp_reflp[OF eR] by simp
qed
subsection \<open>ML setup\<close>
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Sun Aug 11 23:11:03 2024 +0200
@@ -1147,7 +1147,7 @@
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
ML \<open>
-fun dest_fsetT (Type (\<^type_name>\<open>fset\<close>, [T])) = T
+fun dest_fsetT \<^Type>\<open>fset T\<close> = T
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
\<close>
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Aug 11 23:11:03 2024 +0200
@@ -998,9 +998,6 @@
val is_valid_case_argumentT = not o member (op =) [Y, ssig_T];
- fun is_same_type_constr (Type (s, _)) (Type (s', _)) = (s = s')
- | is_same_type_constr _ _ = false;
-
exception NO_ENCAPSULATION of unit;
val parametric_consts = Unsynchronized.ref [];
@@ -1064,7 +1061,7 @@
CLeaf $ t
else if T = YpreT then
it $ t
- else if is_nested_type T andalso is_same_type_constr T U then
+ else if is_nested_type T andalso eq_Type_name (T, U) then
explore_nested lthy encapsulate params t
else
raise NO_ENCAPSULATION ();
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Aug 11 23:11:03 2024 +0200
@@ -11,6 +11,7 @@
structure Lifting_BNF : LIFTING_BNF =
struct
+open Lifting_Util
open BNF_Util
open BNF_Def
open Transfer_BNF
@@ -38,13 +39,6 @@
hyp_subst_tac ctxt, rtac ctxt refl] i
end
-fun mk_Quotient args =
- let
- val argTs = map fastype_of args
- in
- list_comb (Const (\<^const_name>\<open>Quotient\<close>, argTs ---> HOLogic.boolT), args)
- end
-
fun prove_Quotient_map bnf ctxt =
let
val live = live_of_bnf bnf
@@ -57,12 +51,13 @@
|> @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss)
|>> `transpose
- val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
+ val assms = argss |> map (fn [rel, abs, rep, cr] =>
+ HOLogic.mk_Trueprop (mk_Quotient (rel, abs, rep, cr)))
val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0)
val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1)
val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2)
val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
- val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
+ val concl = HOLogic.mk_Trueprop (mk_Quotient (R_rel, Abs_map, Rep_map, T_rel))
val goal = Logic.list_implies (assms, concl)
in
Goal.prove_sorry ctxt'' [] [] goal
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Sun Aug 11 23:11:03 2024 +0200
@@ -145,17 +145,9 @@
fun try_prove_refl_rel ctxt rel =
let
- fun mk_ge_eq x =
- let
- val T = fastype_of x
- in
- Const (\<^const_name>\<open>less_eq\<close>, T --> T --> HOLogic.boolT) $
- (Const (\<^const_name>\<open>HOL.eq\<close>, T)) $ x
- end;
- val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
- in
- mono_eq_prover ctxt goal
- end;
+ val T as \<^Type>\<open>fun A _\<close> = fastype_of rel
+ val ge_eq = \<^Const>\<open>less_eq T for \<^Const>\<open>HOL.eq A\<close> rel\<close>
+ in mono_eq_prover ctxt (HOLogic.mk_Trueprop ge_eq) end;
fun try_prove_reflexivity ctxt prop =
let
@@ -223,7 +215,9 @@
fun zip_transfer_rules ctxt thm =
let
- fun mk_POS ty = Const (\<^const_name>\<open>POS\<close>, ty --> ty --> HOLogic.boolT)
+ fun mk_POS ty =
+ let val \<^Type>\<open>fun A \<^Type>\<open>fun B bool\<close>\<close> = ty
+ in \<^Const>\<open>POS A B\<close> end
val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
val typ = Thm.typ_of_cterm rel
val POS_const = Thm.cterm_of ctxt (mk_POS typ)
@@ -279,21 +273,21 @@
(* Generation of the code certificate from the rsp theorem *)
-fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+fun get_body_types (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) = get_body_types (U, V)
| get_body_types (U, V) = (U, V)
-fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+fun get_binder_types (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) = (T, V) :: get_binder_types (U, W)
| get_binder_types _ = []
-fun get_binder_types_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
+fun get_binder_types_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) =
(T, V) :: get_binder_types_by_rel S (U, W)
| get_binder_types_by_rel _ _ = []
-fun get_body_type_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
+fun get_body_type_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) =
get_body_type_by_rel S (U, V)
| get_body_type_by_rel _ (U, V) = (U, V)
-fun get_binder_rels (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R $ S) = R :: get_binder_rels S
+fun get_binder_rels \<^Const_>\<open>rel_fun _ _ _ _ for R S\<close> = R :: get_binder_rels S
| get_binder_rels _ = []
fun force_rty_type ctxt rty rhs =
@@ -337,7 +331,7 @@
let
fun unfold_conv ctm =
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _ =>
+ \<^Const_>\<open>map_fun _ _ _ _ for _ _\<close> =>
(Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
| _ => Conv.all_conv ctm
in
@@ -376,9 +370,9 @@
fun can_generate_code_cert quot_thm =
case quot_thm_rel quot_thm of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) => true
- | Const (\<^const_name>\<open>eq_onp\<close>, _) $ _ => true
- | _ => false
+ \<^Const_>\<open>HOL.eq _\<close> => true
+ | \<^Const_>\<open>eq_onp _ for _\<close> => true
+ | _ => false
fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
let
@@ -475,7 +469,7 @@
local
fun no_no_code ctxt (rty, qty) =
- if same_type_constrs (rty, qty) then
+ if eq_Type_name (rty, qty) then
forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
else
if Term.is_Type qty then
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Aug 11 23:11:03 2024 +0200
@@ -179,12 +179,10 @@
(** witnesses **)
-fun mk_undefined T = Const (\<^const_name>\<open>undefined\<close>, T);
-
fun mk_witness quot_thm =
let
val wit_thm = quot_thm RS @{thm type_definition_Quotient_not_empty_witness}
- val wit = quot_thm_rep quot_thm $ mk_undefined (quot_thm_rty_qty quot_thm |> snd)
+ val wit = quot_thm_rep quot_thm $ \<^Const>\<open>undefined \<open>quot_thm_rty_qty quot_thm |> snd\<close>\<close>
in
(wit, wit_thm)
end
@@ -238,9 +236,8 @@
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
fun ret_rel_conv conv ctm =
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
- binop_conv2 Conv.all_conv conv ctm
- | _ => conv ctm
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> => binop_conv2 Conv.all_conv conv ctm
+ | _ => conv ctm
fun R_conv rel_eq_onps ctxt =
Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} ctxt
then_conv Conv.bottom_rewrs_conv rel_eq_onps ctxt
@@ -392,7 +389,7 @@
SOME code_dt =>
(fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_witness_of_code_dt qty_ret code_dt),
wit_thm_of_code_dt code_dt :: wits)
- | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T), wits)
+ | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts \<^Const>\<open>undefined T\<close>, wits)
in
@{fold_map 2} (fn Ts => fn k' => fn wits =>
(if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks []
@@ -434,13 +431,8 @@
|>> mk_lift_const_of_lift_def (qty_isom --> qty_ret))) sel_names sel_rhs lthy5
(* now we can execute the qty qty_isom isomorphism *)
- fun mk_type_definition newT oldT RepC AbsC A =
- let
- val typedefC =
- Const (\<^const_name>\<open>type_definition\<close>,
- (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
- in typedefC $ RepC $ AbsC $ A end;
- val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
+ val typedef_goal =
+ \<^Const>\<open>type_definition qty_isom qty for rep_isom abs_isom \<open>HOLogic.mk_UNIV qty\<close>\<close> |>
HOLogic.mk_Trueprop;
fun typ_isom_tac ctxt i =
EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}),
@@ -700,7 +692,7 @@
(K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq ctxt)))) ctxt
in
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> =>
(binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
| _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
end
@@ -723,11 +715,11 @@
fun rename_to_tnames ctxt term =
let
- fun all_typs (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) = T :: all_typs t
+ fun all_typs \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T, t)\<close>\<close> = T :: all_typs t
| all_typs _ = []
- fun rename (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (_, T2, t)) (new_name :: names) =
- (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (new_name, T2, rename t names))
+ fun rename \<^Const_>\<open>Pure.all T1 for \<open>Abs (_, T2, t)\<close>\<close> (new_name :: names) =
+ \<^Const>\<open>Pure.all T1 for \<open>Abs (new_name, T2, rename t names)\<close>\<close>
| rename t _ = t
val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
--- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Sun Aug 11 23:11:03 2024 +0200
@@ -478,12 +478,9 @@
val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of rule);
val (lhs, rhs) =
(case concl of
- Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
- (lhs, rhs)
- | Const (\<^const_name>\<open>less_eq\<close>, _) $ rhs $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
- (lhs, rhs)
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
- (lhs, rhs)
+ \<^Const_>\<open>less_eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
+ | \<^Const_>\<open>less_eq _ for rhs \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close>\<close> => (lhs, rhs)
+ | \<^Const_>\<open>HOL.eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
| _ => error "The rule has a wrong format.")
val lhs_vars = Term.add_vars lhs []
@@ -501,10 +498,9 @@
val rhs_args = (snd o strip_comb) rhs;
fun check_comp t =
(case t of
- Const (\<^const_name>\<open>relcompp\<close>, _) $ Var _ $ Var _ => ()
+ \<^Const_>\<open>relcompp _ _ _ for \<open>Var _\<close> \<open>Var _\<close>\<close> => ()
| _ => error "There is an argument on the rhs that is not a composition.")
- val _ = map check_comp rhs_args
- in () end
+ in List.app check_comp rhs_args end
in
fun add_distr_rule distr_rule context =
@@ -513,11 +509,11 @@
val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of distr_rule)
in
(case concl of
- Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+ \<^Const_>\<open>less_eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
add_pos_distr_rule distr_rule context
- | Const (\<^const_name>\<open>less_eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
+ | \<^Const_>\<open>less_eq _ for _ \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> =>
add_neg_distr_rule distr_rule context
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+ | \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
add_eq_distr_rule distr_rule context)
end
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun Aug 11 23:11:03 2024 +0200
@@ -81,15 +81,11 @@
val args_fixed = (map (Term_Subst.instantiate (instT, Vars.empty))) args_subst
val param_rel_fixed = Term_Subst.instantiate (instT, Vars.empty) param_rel_subst
val rty = (domain_type o fastype_of) param_rel_fixed
- val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>,
- (rty --> rty' --> HOLogic.boolT) -->
- (rty' --> qty --> HOLogic.boolT) -->
- rty --> qty --> HOLogic.boolT)
val qty_name = dest_Type_name qty
val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
- val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
+ val rhs = \<^Const>\<open>relcompp rty rty' qty for param_rel_fixed fixed_crel\<close>
val definition_term = Logic.mk_equals (lhs, rhs)
fun note_def lthy =
Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
@@ -151,7 +147,7 @@
(Conv.bottom_rewrs_conv (Transfer.get_relator_eq args_ctxt) args_ctxt)))
in
case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of
- Const (\<^const_name>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ =>
+ \<^Const_>\<open>relcompp _ _ _ for \<^Const_>\<open>HOL.eq _\<close> _\<close> =>
let
val thm =
pcr_cr_eq
@@ -164,8 +160,8 @@
in
(thm, lthy')
end
- | Const (\<^const_name>\<open>relcompp\<close>, _) $ t $ _ => print_generate_pcr_cr_eq_error args_ctxt t
- | _ => error "generate_pcr_cr_eq: implementation error"
+ | \<^Const_>\<open>relcompp _ _ _ for t _\<close> => print_generate_pcr_cr_eq_error args_ctxt t
+ | _ => error "generate_pcr_cr_eq: implementation error"
end
end
@@ -217,13 +213,12 @@
Pretty.brk 1] @
((Pretty.commas o map (Pretty.str o quote)) extras) @
[Pretty.str "."])]
- val not_type_constr =
- case qty of
- Type _ => []
- | _ => [Pretty.block [Pretty.str "The quotient type ",
- Pretty.quote (Syntax.pretty_typ ctxt' qty),
- Pretty.brk 1,
- Pretty.str "is not a type constructor."]]
+ val not_type_constr =
+ if is_Type qty then []
+ else [Pretty.block [Pretty.str "The quotient type ",
+ Pretty.quote (Syntax.pretty_typ ctxt' qty),
+ Pretty.brk 1,
+ Pretty.str "is not a type constructor."]]
val errs = extra_rty_tfrees @ not_type_constr
in
if null errs then () else raise QUOT_ERROR errs
@@ -641,22 +636,20 @@
(**)
val T_def = Morphism.thm (Local_Theory.target_morphism lthy1) T_def
(**)
- val quot_thm = case typedef_set of
- Const (\<^const_name>\<open>top\<close>, _) =>
- [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
- | Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, _) =>
- [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
- | _ =>
- [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
+ val quot_thm =
+ case typedef_set of
+ \<^Const_>\<open>top _\<close> => [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
+ | \<^Const_>\<open>Collect _ for \<open>Abs _\<close>\<close> => [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
+ | _ => [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
val (rty, qty) = quot_thm_rty_qty quot_thm
val qty_full_name = dest_Type_name qty
val qty_name = Binding.name (Long_Name.base_name qty_full_name)
val qualify = Binding.qualify_name true qty_name
val opt_reflp_thm =
case typedef_set of
- Const (\<^const_name>\<open>top\<close>, _) =>
+ \<^Const_>\<open>top _\<close> =>
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
- | _ => NONE
+ | _ => NONE
val dom_thm = get_Domainp_thm quot_thm
fun setup_transfer_rules_nonpar notes =
@@ -789,9 +782,9 @@
end
in
case input_term of
- (Const (\<^const_name>\<open>Quotient\<close>, _) $ _ $ _ $ _ $ _) => setup_quotient ()
- | (Const (\<^const_name>\<open>type_definition\<close>, _) $ _ $ _ $ _) => setup_typedef ()
- | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
+ \<^Const_>\<open>Quotient _ _ for _ _ _ _\<close> => setup_quotient ()
+ | \<^Const_>\<open>type_definition _ _ for _ _ _\<close> => setup_typedef ()
+ | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
end
val _ =
@@ -830,7 +823,7 @@
Pretty.brk 1,
Thm.pretty_thm ctxt pcr_cr_eq]]
val (pcr_const_eq, eqs) = strip_comb eq_lhs
- fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+ fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
| is_eq _ = false
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
| eq_Const _ _ = false
@@ -929,14 +922,14 @@
(* lifting_forget *)
-val monotonicity_names = [\<^const_name>\<open>right_unique\<close>, \<^const_name>\<open>left_unique\<close>, \<^const_name>\<open>right_total\<close>,
- \<^const_name>\<open>left_total\<close>, \<^const_name>\<open>bi_unique\<close>, \<^const_name>\<open>bi_total\<close>]
-
-fun fold_transfer_rel f (Const (\<^const_name>\<open>Transfer.Rel\<close>, _) $ rel $ _ $ _) = f rel
- | fold_transfer_rel f (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
- (Const (\<^const_name>\<open>Domainp\<close>, _) $ rel) $ _) = f rel
- | fold_transfer_rel f (Const (name, _) $ rel) =
- if member op= monotonicity_names name then f rel else f \<^term>\<open>undefined\<close>
+fun fold_transfer_rel f \<^Const_>\<open>Transfer.Rel _ _ for rel _ _\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>Domainp _ _ for rel\<close> _\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>right_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>left_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>right_total _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>left_total _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>bi_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>bi_total _ _ for rel\<close> = f rel
| fold_transfer_rel f _ = f \<^term>\<open>undefined\<close>
fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
--- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Sun Aug 11 23:11:03 2024 +0200
@@ -108,8 +108,8 @@
(case Lifting_Info.lookup_relator_distr_data ctxt s of
SOME rel_distr_thm =>
(case tm of
- Const (\<^const_name>\<open>POS\<close>, _) => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
- | Const (\<^const_name>\<open>NEG\<close>, _) => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
+ \<^Const_>\<open>POS _ _\<close> => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
+ | \<^Const_>\<open>NEG _ _\<close> => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
| NONE => raise QUOT_THM_INTERNAL (Pretty.block
[Pretty.str ("No relator distr. data for the type " ^ quote s),
Pretty.brk 1,
@@ -450,9 +450,6 @@
val tm = Thm.term_of ctm
val rel = (hd o get_args 2) tm
- fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
- | same_constants _ _ = false
-
fun prove_extra_assms ctxt ctm distr_rule =
let
fun prove_assm assm =
@@ -461,8 +458,8 @@
fun is_POS_or_NEG ctm =
case (head_of o Thm.term_of o Thm.dest_arg) ctm of
- Const (\<^const_name>\<open>POS\<close>, _) => true
- | Const (\<^const_name>\<open>NEG\<close>, _) => true
+ \<^Const_>\<open>POS _ _\<close> => true
+ | \<^Const_>\<open>NEG _ _\<close> => true
| _ => false
val inst_distr_rule = rewr_imp distr_rule ctm
@@ -480,13 +477,13 @@
in
case get_args 2 rel of
- [Const (\<^const_name>\<open>HOL.eq\<close>, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
- | [_, Const (\<^const_name>\<open>HOL.eq\<close>, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
+ [\<^Const_>\<open>HOL.eq _\<close>, _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
+ | [_, \<^Const_>\<open>HOL.eq _\<close>] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
| [_, trans_rel] =>
let
val (rty', qty) = (relation_types o fastype_of) trans_rel
in
- if same_type_constrs (rty', qty) then
+ if eq_Type_name (rty', qty) then
let
val distr_rules = get_rel_distr_rules ctxt0 (dest_Type_name rty') (head_of tm)
val distr_rule = get_first (prove_extra_assms ctxt0 ctm) distr_rules
@@ -502,7 +499,7 @@
val pcrel_def = get_pcrel_def quotients ctxt0 (dest_Type_name qty)
val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def
in
- if same_constants pcrel_const (head_of trans_rel) then
+ if eq_Const_name (pcrel_const, head_of trans_rel) then
let
val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
@@ -540,7 +537,7 @@
let
val (rty, qty) = (relation_types o fastype_of) (Thm.term_of ctm)
in
- if same_type_constrs (rty, qty) then
+ if eq_Type_name (rty, qty) then
if forall op= (Targs rty ~~ Targs qty) then
Conv.all_conv ctm
else
--- a/src/HOL/Tools/Lifting/lifting_util.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Sun Aug 11 23:11:03 2024 +0200
@@ -7,6 +7,7 @@
signature LIFTING_UTIL =
sig
val MRSL: thm list * thm -> thm
+ val mk_Quotient: term * term * term * term -> term
val dest_Quotient: term -> term * term * term * term
val quot_thm_rel: thm -> term
@@ -19,20 +20,16 @@
val undisch: thm -> thm
val undisch_all: thm -> thm
- val is_fun_type: typ -> bool
val get_args: int -> term -> term list
val strip_args: int -> term -> term
val all_args_conv: conv -> conv
- val same_type_constrs: typ * typ -> bool
val Targs: typ -> typ list
val Tname: typ -> string
- val is_rel_fun: term -> bool
val relation_types: typ -> typ * typ
val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory
end
-
structure Lifting_Util: LIFTING_UTIL =
struct
@@ -40,90 +37,62 @@
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
-fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr)
- = (rel, abs, rep, cr)
+fun mk_Quotient (rel, abs, rep, cr) =
+ let val \<^Type>\<open>fun A B\<close> = fastype_of abs
+ in \<^Const>\<open>Quotient A B for rel abs rep cr\<close> end
+
+fun dest_Quotient \<^Const_>\<open>Quotient _ _ for rel abs rep cr\<close> = (rel, abs, rep, cr)
| dest_Quotient t = raise TERM ("dest_Quotient", [t])
-(*
- quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
- for destructing quotient theorems (Quotient R Abs Rep T).
-*)
-
-fun quot_thm_rel quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (rel, _, _, _) => rel
+val dest_Quotient_thm = dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of
-fun quot_thm_abs quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (_, abs, _, _) => abs
-
-fun quot_thm_rep quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (_, _, rep, _) => rep
-
-fun quot_thm_crel quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (_, _, _, crel) => crel
+val quot_thm_rel = #1 o dest_Quotient_thm
+val quot_thm_abs = #2 o dest_Quotient_thm
+val quot_thm_rep = #3 o dest_Quotient_thm
+val quot_thm_crel = #4 o dest_Quotient_thm
fun quot_thm_rty_qty quot_thm =
- let
- val abs = quot_thm_abs quot_thm
- val abs_type = fastype_of abs
- in
- (domain_type abs_type, range_type abs_type)
- end
+ let val \<^Type>\<open>fun A B\<close> = fastype_of (quot_thm_abs quot_thm)
+ in (A, B) end
-fun Quotient_conv R_conv Abs_conv Rep_conv T_conv = Conv.combination_conv (Conv.combination_conv
- (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv;
-
-fun Quotient_R_conv R_conv = Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv;
+fun Quotient_conv R_conv Abs_conv Rep_conv T_conv =
+ Conv.combination_conv (Conv.combination_conv
+ (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv
+
+fun Quotient_R_conv R_conv =
+ Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv
fun undisch thm =
- let
- val assm = Thm.cprem_of thm 1
- in
- Thm.implies_elim thm (Thm.assume assm)
- end
+ let val assm = Thm.cprem_of thm 1
+ in Thm.implies_elim thm (Thm.assume assm) end
fun undisch_all thm = funpow (Thm.nprems_of thm) undisch thm
-fun is_fun_type (Type (\<^type_name>\<open>fun\<close>, _)) = true
- | is_fun_type _ = false
-
fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
fun strip_args n = funpow n (fst o dest_comb)
-fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
-
-fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q)
- | same_type_constrs _ = false
-
-fun Targs (Type (_, args)) = args
- | Targs _ = []
+fun all_args_conv conv ctm =
+ Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
-fun Tname (Type (name, _)) = name
- | Tname _ = ""
+fun Targs T = if is_Type T then dest_Type_args T else []
+fun Tname T = if is_Type T then dest_Type_name T else ""
-fun is_rel_fun (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) = true
- | is_rel_fun _ = false
-
-fun relation_types typ =
- case strip_type typ of
- ([typ1, typ2], \<^typ>\<open>bool\<close>) => (typ1, typ2)
- | _ => error "relation_types: not a relation"
+fun relation_types typ =
+ (case strip_type typ of
+ ([typ1, typ2], \<^Type>\<open>bool\<close>) => (typ1, typ2)
+ | _ => error "relation_types: not a relation")
fun map_interrupt f l =
let
fun map_interrupt' _ [] l = SOME (rev l)
- | map_interrupt' f (x::xs) l = (case f x of
- NONE => NONE
- | SOME v => map_interrupt' f xs (v::l))
- in
- map_interrupt' f l []
- end
+ | map_interrupt' f (x::xs) l =
+ (case f x of
+ NONE => NONE
+ | SOME v => map_interrupt' f xs (v::l))
+ in map_interrupt' f l [] end
-fun conceal_naming_result f lthy =
- lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy;
+fun conceal_naming_result f lthy =
+ lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy
end
--- a/src/HOL/Tools/Qelim/qelim.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Sun Aug 11 23:11:03 2024 +0200
@@ -6,51 +6,50 @@
signature QELIM =
sig
- val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
- ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
- val standard_qelim_conv: Proof.context ->
- (cterm list -> conv) -> (cterm list -> conv) ->
- (cterm list -> conv) -> conv
+ val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
+ ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
+ val standard_qelim_conv: Proof.context ->
+ (cterm list -> conv) -> (cterm list -> conv) ->
+ (cterm list -> conv) -> conv
end;
structure Qelim: QELIM =
struct
-val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
+fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
+ let
+ fun conv env p =
+ (case Thm.term_of p of
+ \<^Const_>\<open>conj for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>disj for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>implies for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>HOL.eq _ for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>Not for _\<close> => Conv.arg_conv (conv env) p
+ | \<^Const_>\<open>Ex _ for \<open>Abs (s, _, _)\<close>\<close> =>
+ let
+ val (e,p0) = Thm.dest_comb p
+ val (x,p') = Thm.dest_abs_global p0
+ val env' = ins x env
+ val th =
+ Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
+ |> Drule.arg_cong_rule e
+ val th' = simpex_conv (Thm.rhs_of th)
+ val (_, r) = Thm.dest_equals (Thm.cprop_of th')
+ in
+ if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
+ else Thm.transitive (Thm.transitive th th') (conv env r)
+ end
+ | \<^Const_>\<open>Ex _ for _\<close> => (Thm.eta_long_conversion then_conv conv env) p
+ | \<^Const_>\<open>All _ for _\<close> =>
+ let
+ val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
+ val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT)
+ val P = Thm.dest_arg p
+ val th = \<^instantiate>\<open>'a = T and P in lemma "\<forall>x::'a. P x \<equiv> \<nexists>x. \<not> P x" by simp\<close>
+ in Thm.transitive th (conv env (Thm.rhs_of th)) end
+ | _ => atcv env p)
+ in precv then_conv (conv env) then_conv postcv end
-fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
- let
- fun conv env p =
- case Thm.term_of p of
- Const(s,T)$_$_ =>
- if domain_type T = HOLogic.boolT
- andalso member (op =) [\<^const_name>\<open>HOL.conj\<close>, \<^const_name>\<open>HOL.disj\<close>,
- \<^const_name>\<open>HOL.implies\<close>, \<^const_name>\<open>HOL.eq\<close>] s
- then Conv.binop_conv (conv env) p
- else atcv env p
- | Const(\<^const_name>\<open>Not\<close>,_)$_ => Conv.arg_conv (conv env) p
- | Const(\<^const_name>\<open>Ex\<close>,_)$Abs (s, _, _) =>
- let
- val (e,p0) = Thm.dest_comb p
- val (x,p') = Thm.dest_abs_global p0
- val env' = ins x env
- val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
- |> Drule.arg_cong_rule e
- val th' = simpex_conv (Thm.rhs_of th)
- val (_, r) = Thm.dest_equals (Thm.cprop_of th')
- in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
- else Thm.transitive (Thm.transitive th th') (conv env r) end
- | Const(\<^const_name>\<open>Ex\<close>,_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const(\<^const_name>\<open>All\<close>, _)$_ =>
- let
- val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
- val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT)
- val p = Thm.dest_arg p
- val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
- in Thm.transitive th (conv env (Thm.rhs_of th))
- end
- | _ => atcv env p
- in precv then_conv (conv env) then_conv postcv end
(* Instantiation of some parameter for most common cases *)
@@ -60,6 +59,7 @@
simpset_of
(put_simpset HOL_basic_ss \<^context>
addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib});
+
fun pcv ctxt = Simplifier.rewrite (put_simpset ss ctxt)
in
--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Aug 11 23:11:03 2024 +0200
@@ -55,8 +55,7 @@
let
val rty = fastype_of rhs
val qty = fastype_of lhs
- val absrep_trm =
- Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
+ val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
val (_, prop') = Local_Defs.cert_def lthy (K []) prop
val (_, newrhs) = Local_Defs.abs_def prop'
@@ -80,8 +79,7 @@
qcinfo as {qconst = Const (c, _), ...} =>
Quotient_Info.update_quotconsts (c, qcinfo)
| _ => I))
- |> (snd oo Local_Theory.note)
- ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
+ |> (snd oo Local_Theory.note) ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
in
(qconst_data Morphism.identity, lthy'')
end
@@ -92,10 +90,11 @@
fun abs_conv2 cv = Conv.abs_conv (Conv.abs_conv (cv o #2) o #2) ctxt
fun erase_quants ctxt' ctm' =
- case (Thm.term_of ctm') of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
- | _ => (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
- Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+ (case Thm.term_of ctm' of
+ \<^Const_>\<open>HOL.eq _ for _ _\<close> => Conv.all_conv ctm'
+ | _ =>
+ (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
+ Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm')
val norm_fun_eq = abs_conv2 erase_quants then_conv Thm.eta_conversion
fun simp_arrows_conv ctm =
@@ -106,10 +105,10 @@
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
- case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
+ (case Thm.term_of ctm of
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> =>
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
- | _ => Conv.all_conv ctm
+ | _ => Conv.all_conv ctm)
end
val unfold_ret_val_invs = Conv.bottom_conv
@@ -151,48 +150,41 @@
fun try_to_prove_refl thm =
let
val lhs_eq =
- thm
- |> Thm.prop_of
- |> Logic.dest_implies
- |> fst
+ #1 (Logic.dest_implies (Thm.prop_of thm))
|> strip_all_body
|> try HOLogic.dest_Trueprop
in
- case lhs_eq of
- SOME (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => SOME (@{thm refl} RS thm)
- | SOME _ => (case body_type (fastype_of lhs) of
- Type (typ_name, _) =>
- \<^try>\<open>
- #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
- RS @{thm Equiv_Relations.equivp_reflp} RS thm\<close>
- | _ => NONE
- )
- | _ => NONE
+ (case lhs_eq of
+ SOME \<^Const_>\<open>HOL.eq _ for _ _\<close> => SOME (@{thm refl} RS thm)
+ | SOME _ =>
+ (case body_type (fastype_of lhs) of
+ Type (typ_name, _) =>
+ \<^try>\<open>
+ #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
+ RS @{thm Equiv_Relations.equivp_reflp} RS thm\<close>
+ | _ => NONE)
+ | _ => NONE)
end
val rsp_rel = Quotient_Term.equiv_relation lthy (fastype_of rhs, lhs_ty)
val internal_rsp_tm = HOLogic.mk_Trueprop (Syntax.check_term lthy (rsp_rel $ rhs $ rhs))
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
- val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
fun after_qed thm_list lthy =
let
val internal_rsp_thm =
- case thm_list of
+ (case thm_list of
[] => the maybe_proven_rsp_thm
| [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
- (fn _ =>
- resolve_tac ctxt [readable_rsp_thm_eq] 1 THEN
- Proof_Context.fact_tac ctxt [thm] 1)
- in
- snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
- end
- in
- case maybe_proven_rsp_thm of
- SOME _ => Proof.theorem NONE after_qed [] lthy
- | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
- end
+ (fn _ =>
+ resolve_tac ctxt [readable_rsp_thm_eq] 1 THEN
+ Proof_Context.fact_tac ctxt [thm] 1))
+ in snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy) end
+ val goal =
+ if is_some maybe_proven_rsp_thm then []
+ else [[(#1 (Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)), [])]]
+ in Proof.theorem NONE after_qed goal lthy end
val quotient_def = gen_quotient_def Proof_Context.cert_var (K I)
val quotient_def_cmd = gen_quotient_def Proof_Context.read_var Syntax.parse_term
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Aug 11 23:11:03 2024 +0200
@@ -37,9 +37,6 @@
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps [])
-(* composition of two theorems, used in maps *)
-fun OF1 thm1 thm2 = thm2 RS thm1
-
fun atomize_thm ctxt thm =
let
val thm' = Thm.legacy_freezeT (Thm.forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
@@ -72,17 +69,19 @@
| _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
-fun get_match_inst thy pat trm =
- let
- val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
- val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *)
- val tenv = Vartab.dest (Envir.term_env env)
- val tyenv = Vartab.dest (Envir.type_env env)
- fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty)
- fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t)
- in
- (TVars.make (map prep_ty tyenv), Vars.make (map prep_trm tenv))
- end
+fun get_match_inst ctxt pat trm =
+ (case Unify.matcher (Context.Proof ctxt) [pat] [trm] of
+ SOME env =>
+ let
+ val instT =
+ TVars.build (Envir.type_env env |> Vartab.fold (fn (x, (S, T)) =>
+ TVars.add ((x, S), Thm.ctyp_of ctxt T)))
+ val inst =
+ Vars.build (Envir.term_env env |> Vartab.fold (fn (x, (T, t)) =>
+ Vars.add ((x, T), Thm.cterm_of ctxt t)))
+ in (instT, inst) end
+ | NONE => raise TERM ("Higher-order match failed", [pat, trm]));
+
(* Calculates the instantiations for the lemmas:
@@ -94,7 +93,6 @@
*)
fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
let
- val thy = Proof_Context.theory_of ctxt
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)]
val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1]
@@ -102,21 +100,17 @@
(case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of
NONE => NONE
| SOME thm' =>
- (case try (get_match_inst thy (get_lhs thm')) (Thm.term_of redex) of
+ (case try (get_match_inst ctxt (get_lhs thm')) (Thm.term_of redex) of
NONE => NONE
| SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
end
fun ball_bex_range_simproc ctxt redex =
(case Thm.term_of redex of
- (Const (\<^const_name>\<open>Ball\<close>, _) $ (Const (\<^const_name>\<open>Respects\<close>, _) $
- (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R1 $ R2)) $ _) =>
- calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
- | (Const (\<^const_name>\<open>Bex\<close>, _) $ (Const (\<^const_name>\<open>Respects\<close>, _) $
- (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R1 $ R2)) $ _) =>
- calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
+ \<^Const_>\<open>Ball _ for \<open>\<^Const_>\<open>Respects _ for \<^Const_>\<open>rel_fun _ _ _ _ for R1 R2\<close>\<close>\<close> _\<close> =>
+ calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+ | \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for \<^Const_>\<open>rel_fun _ _ _ _ for R1 R2\<close>\<close> _\<close> =>
+ calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
| _ => NONE)
(* Regularize works as follows:
@@ -139,13 +133,13 @@
*)
fun reflp_get ctxt =
- map_filter (fn th => if Thm.no_prems th then SOME (OF1 @{thm equivp_reflp} th) else NONE
+ map_filter (fn th => if Thm.no_prems th then SOME (th RS @{thm equivp_reflp}) else NONE
handle THM _ => NONE) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
val eq_imp_rel = @{lemma "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" by (simp add: equivp_reflp)}
fun eq_imp_rel_get ctxt =
- map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
+ map (fn th => th RS eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
val regularize_simproc =
\<^simproc_setup>\<open>passive regularize
@@ -179,19 +173,17 @@
*)
fun find_qt_asm asms =
let
- fun find_fun trm =
- (case trm of
- (Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Quot_True\<close>, _) $ _)) => true
- | _ => false)
+ fun find_fun \<^Const_>\<open>Trueprop for \<^Const_>\<open>Quot_True _ for _\<close>\<close> = true
+ | find_fun _ = false
in
- (case find_first find_fun asms of
- SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
- | _ => NONE)
+ (case find_first find_fun asms of
+ SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+ | _ => NONE)
end
fun quot_true_simple_conv ctxt fnctn ctrm =
(case Thm.term_of ctrm of
- (Const (\<^const_name>\<open>Quot_True\<close>, _) $ x) =>
+ \<^Const_>\<open>Quot_True _ for x\<close> =>
let
val fx = fnctn x;
val cx = Thm.cterm_of ctxt x;
@@ -205,7 +197,7 @@
fun quot_true_conv ctxt fnctn ctrm =
(case Thm.term_of ctrm of
- (Const (\<^const_name>\<open>Quot_True\<close>, _) $ _) =>
+ \<^Const_>\<open>Quot_True _ for _\<close> =>
quot_true_simple_conv ctxt fnctn ctrm
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
@@ -259,13 +251,14 @@
complex we rely on instantiation to tell us if it applies
*)
fun equals_rsp_tac R ctxt =
- case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *) (* FIXME fragile *)
- SOME ctm =>
+ case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *)
+ SOME ct =>
let
- val ty = domain_type (fastype_of R)
+ val T = Thm.ctyp_of_cterm ct
+ val A = try Thm.dest_ctyp0 T
+ val try_inst = \<^try>\<open>Thm.instantiate' [SOME (the A)] [SOME ct] @{thm equals_rsp}\<close>
in
- case try (Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
- [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
+ case try_inst of
SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
| NONE => K no_tac
end
@@ -314,54 +307,53 @@
fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
(case bare_concl goal of
(* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
- (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $ (Abs _) $ (Abs _)
- => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _ \<open>Abs _\<close> \<open>Abs _\<close>\<close> =>
+ resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
- | (Const (\<^const_name>\<open>HOL.eq\<close>,_) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _))
- => resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
+ | \<^Const_>\<open>HOL.eq _ for
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
(* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
- | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
- => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+ | \<^Const_>\<open>rel_fun _ _ _ _ for _ _
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
- | Const (\<^const_name>\<open>HOL.eq\<close>,_) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
- => resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
+ | \<^Const_>\<open>HOL.eq _ for
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
(* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
- | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
- => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+ | \<^Const_>\<open>rel_fun _ _ _ _ for _ _
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
- | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
- (Const(\<^const_name>\<open>Bex1_rel\<close>,_) $ _) $ (Const(\<^const_name>\<open>Bex1_rel\<close>,_) $ _)
- => resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
+ | \<^Const_>\<open>rel_fun _ _ _ _ for _ _ \<^Const_>\<open>Bex1_rel _ for _\<close> \<^Const_>\<open>Bex1_rel _ for _\<close>\<close> =>
+ resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
| (_ $
- (Const(\<^const_name>\<open>Babs\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Babs\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _))
- => resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
+ \<^Const_>\<open>Babs _ _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> $
+ \<^Const_>\<open>Babs _ _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>) =>
+ resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
- | Const (\<^const_name>\<open>HOL.eq\<close>,_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
- (resolve_tac ctxt @{thms refl} ORELSE'
+ | \<^Const_>\<open>HOL.eq _ for \<open>R $ _ $ _\<close> \<open>_ $ _ $ _\<close>\<close> =>
+ (resolve_tac ctxt @{thms refl} ORELSE'
(equals_rsp_tac R ctxt THEN' RANGE [
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
(* reflexivity of operators arising from Cong_tac *)
- | Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _ => resolve_tac ctxt @{thms refl}
+ | \<^Const_>\<open>HOL.eq _ for _ _\<close> => resolve_tac ctxt @{thms refl}
(* respectfulness of constants; in particular of a simple relation *)
- | _ $ (Const _) $ (Const _) (* rel_fun, list_rel, etc but not equality *)
- => resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_respect\<close>))
- THEN_ALL_NEW quotient_tac ctxt
+ | _ $ Const _ $ Const _ => (* rel_fun, list_rel, etc but not equality *)
+ resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_respect\<close>))
+ THEN_ALL_NEW quotient_tac ctxt
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
(* observe map_fun *)
@@ -411,10 +403,10 @@
(* expands all map_funs, except in front of the (bound) variables listed in xs *)
fun map_fun_simple_conv xs ctrm =
(case Thm.term_of ctrm of
- ((Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _) $ h $ _) =>
- if member (op=) xs h
- then Conv.all_conv ctrm
- else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
+ \<^Const_>\<open>map_fun _ _ _ _ for _ _ h _\<close> =>
+ if member (op=) xs h
+ then Conv.all_conv ctrm
+ else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
| _ => Conv.all_conv ctrm)
fun map_fun_conv xs ctxt ctrm =
@@ -439,7 +431,7 @@
fun make_inst lhs t =
let
- val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+ val _ $ (Abs (_, _, (_ $ ((f as Var (_, \<^Type>\<open>fun T _\<close>)) $ u)))) = lhs;
val _ $ (Abs (_, _, (_ $ g))) = t;
in
(f, Abs ("x", T, mk_abs u 0 g))
@@ -447,7 +439,7 @@
fun make_inst_id lhs t =
let
- val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ val _ $ (Abs (_, _, (f as Var (_, \<^Type>\<open>fun T _\<close>)) $ u)) = lhs;
val _ $ (Abs (_, _, g)) = t;
in
(f, Abs ("x", T, mk_abs u 0 g))
@@ -462,7 +454,7 @@
*)
fun lambda_prs_simple_conv ctxt ctrm =
(case Thm.term_of ctrm of
- (Const (\<^const_name>\<open>map_fun\<close>, _) $ r1 $ a2) $ (Abs _) =>
+ \<^Const_>\<open>map_fun _ _ _ _ for r1 a2 \<open>Abs _\<close>\<close> =>
let
val (ty_b, ty_a) = dest_funT (fastype_of r1)
val (ty_c, ty_d) = dest_funT (fastype_of a2)
@@ -557,32 +549,9 @@
(** The General Shape 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
-
- - 1st prem is the regularization step
- - 2nd prem is the rep/abs injection step
- - 3rd prem is the cleaning part
-
- the Quot_True premise in 2nd records the lifted theorem
-*)
-val procedure_thm =
- @{lemma "\<lbrakk>A;
- A \<longrightarrow> B;
- Quot_True D \<Longrightarrow> B = C;
- C = D\<rbrakk> \<Longrightarrow> D"
- by (simp add: Quot_True_def)}
-
(* in case of partial equivalence relations, this form of the
procedure theorem results in solvable proof obligations
*)
-val partiality_procedure_thm =
- @{lemma "[|B;
- Quot_True D ==> B = C;
- C = D|] ==> D"
- by (simp add: Quot_True_def)}
fun lift_match_error ctxt msg rtrm qtrm =
let
@@ -603,11 +572,24 @@
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
- Thm.instantiate' []
- [SOME (Thm.cterm_of ctxt rtrm'),
- SOME (Thm.cterm_of ctxt reg_goal),
- NONE,
- SOME (Thm.cterm_of ctxt inj_goal)] procedure_thm
+ (* - 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
+
+ - 1st prem is the regularization step
+ - 2nd prem is the rep/abs injection step
+ - 3rd prem is the cleaning part
+
+ the Quot_True premise in 2nd records the lifted theorem
+ *)
+ \<^instantiate>\<open>
+ A = \<open>Thm.cterm_of ctxt rtrm'\<close> and
+ B = \<open>Thm.cterm_of ctxt reg_goal\<close> and
+ C = \<open>Thm.cterm_of ctxt inj_goal\<close>
+ in
+ lemma (schematic) "A \<Longrightarrow> A \<longrightarrow> B \<Longrightarrow> (Quot_True D \<Longrightarrow> B = C) \<Longrightarrow> C = D \<Longrightarrow> D"
+ by (simp add: Quot_True_def)\<close>
end
@@ -662,10 +644,12 @@
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
- Thm.instantiate' []
- [SOME (Thm.cterm_of ctxt reg_goal),
- NONE,
- SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
+ \<^instantiate>\<open>
+ B = \<open>Thm.cterm_of ctxt reg_goal\<close> and
+ C = \<open>Thm.cterm_of ctxt inj_goal\<close>
+ in
+ lemma (schematic) "B \<Longrightarrow> (Quot_True D \<Longrightarrow> B = C) \<Longrightarrow> C = D \<Longrightarrow> D"
+ by (simp add: Quot_True_def)\<close>
end
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Sun Aug 11 23:11:03 2024 +0200
@@ -55,11 +55,9 @@
fun negF AbsF = RepF
| negF RepF = AbsF
-fun is_identity (Const (\<^const_name>\<open>id\<close>, _)) = true
+fun is_identity \<^Const_>\<open>id _\<close> = true
| is_identity _ = false
-fun mk_identity ty = Const (\<^const_name>\<open>id\<close>, ty --> ty)
-
fun mk_fun_compose flag (trm1, trm2) =
case flag of
AbsF => Const (\<^const_name>\<open>comp\<close>, dummyT) $ trm1 $ trm2
@@ -191,7 +189,7 @@
end
in
if rty = qty
- then mk_identity rty
+ then \<^Const>\<open>id rty\<close>
else
case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
@@ -235,7 +233,7 @@
end
| (TFree x, TFree x') =>
if x = x'
- then mk_identity rty
+ then \<^Const>\<open>id rty\<close>
else raise (LIFT_MATCH "absrep_fun (frees)")
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
| _ => raise (LIFT_MATCH "absrep_fun (default)")
@@ -264,7 +262,7 @@
map_types (Envir.subst_type ty_inst) trm
end
-fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
| is_eq _ = false
fun mk_rel_compose (trm1, trm2) =
@@ -312,7 +310,7 @@
val rtys' = map (Envir.subst_type qtyenv) rtys
val args = map (equiv_relation ctxt) (tys ~~ rtys')
val eqv_rel = get_equiv_rel ctxt s'
- val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> \<^typ>\<open>bool\<close>)
+ val eqv_rel' = force_typ ctxt eqv_rel \<^Type>\<open>fun rty \<^Type>\<open>fun rty \<^Type>\<open>bool\<close>\<close>\<close>
in
if forall is_eq args
then eqv_rel'
@@ -607,8 +605,8 @@
| (_, Const _) =>
let
val thy = Proof_Context.theory_of ctxt
- fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
- | same_const _ _ = false
+ fun same_const t u =
+ eq_Const_name (t, u) andalso matches_typ ctxt (dest_Const_type t) (dest_Const_type u)
in
if same_const rtrm qtrm then rtrm
else
--- a/src/HOL/Tools/Quotient/quotient_type.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sun Aug 11 23:11:03 2024 +0200
@@ -72,11 +72,10 @@
(* proves the quot_type theorem for the new type *)
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
let
- val quot_type_const = Const (\<^const_name>\<open>quot_type\<close>,
- fastype_of rel --> fastype_of abs --> fastype_of rep --> \<^typ>\<open>bool\<close>)
- val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+ val \<^Type>\<open>fun A _\<close> = fastype_of rel
+ val \<^Type>\<open>fun _ B\<close> = fastype_of abs
in
- Goal.prove lthy [] [] goal
+ Goal.prove lthy [] [] (HOLogic.mk_Trueprop (\<^Const>\<open>quot_type A B for rel abs rep\<close>))
(fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info)
end
@@ -97,12 +96,12 @@
val (rty, qty) = (dest_funT o fastype_of) abs_fun
val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
- val Abs_body = (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
- Const (\<^const_name>\<open>equivp\<close>, _) $ _ => abs_fun_graph
- | Const (\<^const_name>\<open>part_equivp\<close>, _) $ rel =>
- HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
- | _ => error "unsupported equivalence theorem"
- )
+ val Abs_body =
+ (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
+ \<^Const_>\<open>equivp _ for _\<close> => abs_fun_graph
+ | \<^Const_>\<open>part_equivp _ for rel\<close> =>
+ HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
+ | _ => error "unsupported equivalence theorem")
val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
val qty_name = Binding.name (Long_Name.base_name (dest_Type_name qty))
val cr_rel_name = Binding.prefix_name "cr_" qty_name
@@ -122,10 +121,10 @@
val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
val (reflp_thm, quot_thm) =
(case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
- Const (\<^const_name>\<open>equivp\<close>, _) $ _ =>
+ \<^Const_>\<open>equivp _ for _\<close> =>
(SOME (equiv_thm RS @{thm equivp_reflp2}),
[quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp})
- | Const (\<^const_name>\<open>part_equivp\<close>, _) $ _ =>
+ | \<^Const_>\<open>part_equivp _ for _\<close> =>
(NONE, [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient})
| _ => error "unsupported equivalence theorem")
val config = { notes = true }
@@ -177,11 +176,8 @@
val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
(* more useful abs and rep definitions *)
- val abs_const = Const (\<^const_name>\<open>quot_type.abs\<close>,
- (rty --> rty --> \<^typ>\<open>bool\<close>) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
- val rep_const = Const (\<^const_name>\<open>quot_type.rep\<close>, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
- val abs_trm = abs_const $ rel $ Abs_const
- val rep_trm = rep_const $ Rep_const
+ val abs_trm = \<^Const>\<open>quot_type.abs rty Abs_ty\<close> $ rel $ Abs_const
+ val rep_trm = \<^Const>\<open>quot_type.rep Abs_ty rty\<close> $ Rep_const
val (rep_name, abs_name) =
(case opt_morphs of
NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
@@ -301,16 +297,9 @@
val _ = sanity_check quot
val _ = map_check lthy quot
- fun mk_goal (rty, rel, partial) =
- let
- val equivp_ty = ([rty, rty] ---> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>
- val const =
- if partial then \<^const_name>\<open>part_equivp\<close> else \<^const_name>\<open>equivp\<close>
- in
- HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
- end
-
- val goal = (mk_goal o #2) quot
+ val (rty, rel, partial) = #2 quot
+ val const = if partial then \<^Const>\<open>part_equivp rty\<close> else \<^Const>\<open>equivp rty\<close>
+ val goal = HOLogic.mk_Trueprop (const $ rel)
fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm)
in
@@ -325,7 +314,7 @@
val tmp_lthy1 = Variable.declare_typ rty lthy
val rel =
Syntax.parse_term tmp_lthy1 rel_str
- |> Type.constraint (rty --> rty --> \<^typ>\<open>bool\<close>)
+ |> Type.constraint \<^Type>\<open>fun rty \<^Type>\<open>fun rty \<^Type>\<open>bool\<close>\<close>\<close>
|> Syntax.check_term tmp_lthy1
val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
--- a/src/HOL/Tools/typedef.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Tools/typedef.ML Sun Aug 11 23:11:03 2024 +0200
@@ -101,7 +101,7 @@
val typedef_overloaded = Attrib.setup_config_bool \<^binding>\<open>typedef_overloaded\<close> (K false);
fun mk_inhabited T A =
- HOLogic.mk_Trueprop (\<^Const>\<open>Ex T for \<open>Abs ("x", T, \<^Const>\<open>Set.member T for \<open>Bound 0\<close> A\<close>)\<close>\<close>);
+ \<^instantiate>\<open>'a = T and A in prop \<open>\<exists>x::'a. x \<in> A\<close>\<close>;
fun mk_typedef newT oldT RepC AbsC A =
let val type_definition = \<^Const>\<open>type_definition newT oldT for RepC AbsC A\<close>
--- a/src/Pure/Isar/generic_target.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/Pure/Isar/generic_target.ML Sun Aug 11 23:11:03 2024 +0200
@@ -122,7 +122,7 @@
fun same_const (Const (c, _), Const (c', _)) = c = c'
| same_const (t $ _, t' $ _) = same_const (t, t')
- | same_const (_, _) = false;
+ | same_const _ = false;
fun const_decl phi_pred prmode ((b, mx), rhs) = Morphism.entity (fn phi => fn context =>
if phi_pred phi then
--- a/src/Pure/more_thm.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/Pure/more_thm.ML Sun Aug 11 23:11:03 2024 +0200
@@ -23,6 +23,8 @@
val aconvc: cterm * cterm -> bool
val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
val add_vars: thm -> cterm Vars.table -> cterm Vars.table
+ val dest_ctyp0: ctyp -> ctyp
+ val dest_ctyp1: ctyp -> ctyp
val dest_funT: ctyp -> ctyp * ctyp
val strip_type: ctyp -> ctyp list * ctyp
val instantiate_ctyp: ctyp TVars.table -> ctyp -> ctyp
@@ -143,6 +145,9 @@
(* ctyp operations *)
+val dest_ctyp0 = Thm.dest_ctypN 0;
+val dest_ctyp1 = Thm.dest_ctypN 1;
+
fun dest_funT cT =
(case Thm.typ_of cT of
Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end
--- a/src/Pure/term.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/Pure/term.ML Sun Aug 11 23:11:03 2024 +0200
@@ -37,6 +37,7 @@
val is_Type: typ -> bool
val is_TFree: typ -> bool
val is_TVar: typ -> bool
+ val eq_Type_name: typ * typ -> bool
val dest_Type: typ -> string * typ list
val dest_Type_name: typ -> string
val dest_Type_args: typ -> typ list
@@ -46,6 +47,7 @@
val is_Const: term -> bool
val is_Free: term -> bool
val is_Var: term -> bool
+ val eq_Const_name: term * term -> bool
val dest_Const: term -> string * typ
val dest_Const_name: term -> string
val dest_Const_type: term -> typ
@@ -280,6 +282,9 @@
fun is_TVar (TVar _) = true
| is_TVar _ = false;
+fun eq_Type_name (Type (a, _), Type (b, _)) = a = b
+ | eq_Type_name _ = false;
+
(** Destructors **)
@@ -310,6 +315,9 @@
fun is_Var (Var _) = true
| is_Var _ = false;
+fun eq_Const_name (Const (a, _), Const (b, _)) = a = b
+ | eq_Const_name _ = false;
+
(** Destructors **)
--- a/src/Pure/thm.ML Thu Aug 08 18:56:14 2024 +0100
+++ b/src/Pure/thm.ML Sun Aug 11 23:11:03 2024 +0200
@@ -30,8 +30,6 @@
val ctyp_of: Proof.context -> typ -> ctyp
val dest_ctyp: ctyp -> ctyp list
val dest_ctypN: int -> ctyp -> ctyp
- val dest_ctyp0: ctyp -> ctyp
- val dest_ctyp1: ctyp -> ctyp
val make_ctyp: ctyp -> ctyp list -> ctyp
(*certified terms*)
val term_of: cterm -> term
@@ -226,9 +224,6 @@
| _ => err ())
end;
-val dest_ctyp0 = dest_ctypN 0;
-val dest_ctyp1 = dest_ctypN 1;
-
fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);