# HG changeset patch # User wenzelm # Date 1723410663 -7200 # Node ID 81da5938a7bebc40c551e209cc9a4e040ea1f021 # Parent daa604a0049196dd90a9faf5d2f8b5f1cfba35cc# Parent 3b6d84c32bfd6fef74da70f239c22d44634b5082 merged diff -r daa604a00491 -r 81da5938a7be src/HOL/Eisbach/match_method.ML --- 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) = diff -r daa604a00491 -r 81da5938a7be src/HOL/Lifting.thy --- 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 \Quotient Predicate\ -definition - "Quotient R Abs Rep T \ - (\a. Abs (Rep a) = a) \ - (\a. R (Rep a) (Rep a)) \ - (\r s. R r s \ R r r \ R s s \ Abs r = Abs s) \ - T = (\x y. R x x \ Abs x = y)" +definition Quotient :: "('a \ 'a \ bool) \ ('a \ 'b) \ ('b \ 'a) \ ('a \ 'b \ bool) \ bool" + where + "Quotient R Abs Rep T \ + (\a. Abs (Rep a) = a) \ + (\a. R (Rep a) (Rep a)) \ + (\r s. R r s \ R r r \ R s s \ Abs r = Abs s) \ + T = (\x y. R x x \ Abs x = y)" lemma QuotientI: assumes "\a. Abs (Rep a) = a" diff -r daa604a00491 -r 81da5938a7be src/HOL/Quotient.thy --- 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)) (\f. P (f x)) = Ex (\f. P (f x)))" proof - - { fix f - assume "P (f x)" - have "(\y. f x) \ 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 "(\y. f x) \ 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 \ 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 "(\!x\Respects R. P x) \ (Bex1_rel R (\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 \ 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 \ Rep a) (SOME x. x \ 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 \ Rep a) x" using r rep some_collect by metis - then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast - then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" - using part_equivp_transp[OF equivp] by (metis \R (SOME x. x \ Rep a) x\) - qed - have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) - then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto - have "R r r \ R s s \ Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" - proof - - assume "R r r" and "R s s" - then have "Abs (Collect (R r)) = Abs (Collect (R s)) \ Collect (R r) = Collect (R s)" - by (metis abs_inverse) - also have "Collect (R r) = Collect (R s) \ (\A x. x \ A) (Collect (R r)) = (\A x. x \ A) (Collect (R s))" - by (rule iffI) simp_all - finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" by simp - qed - then show "R r s \ R r r \ R s s \ (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 \ Rep a) (SOME x. x \ 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 \ Rep a) x" using r rep some_collect by metis + then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast + then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" + using part_equivp_transp[OF equivp] by (metis \R (SOME x. x \ Rep a) x\) + qed + have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) + then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto + have "R r r \ R s s \ Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" + proof - + assume "R r r" and "R s s" + then have "Abs (Collect (R r)) = Abs (Collect (R s)) \ Collect (R r) = Collect (R s)" + by (metis abs_inverse) + also have "Collect (R r) = Collect (R s) \ (\A x. x \ A) (Collect (R r)) = (\A x. x \ A) (Collect (R s))" + by (rule iffI) simp_all + finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" by simp + qed + then show "R r s \ R r r \ R s s \ (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 \Quotient3 to Quotient\ lemma Quotient3_to_Quotient: -assumes "Quotient3 R Abs Rep" -and "T \ \x y. R x x \ 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 \ \x y. R x x \ 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 \ \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 \ \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 \ R s s \ Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) -next - show "T = (\x y. R x x \ 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 \ R s s \ Abs r = Abs s)" for r s + using q by(rule Quotient3_rel[symmetric]) + show "T = (\x y. R x x \ Abs x = y)" + using T_def equivp_reflp[OF eR] by simp qed subsection \ML setup\ diff -r daa604a00491 -r 81da5938a7be src/HOL/Quotient_Examples/Quotient_FSet.thy --- 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 \ -fun dest_fsetT (Type (\<^type_name>\fset\, [T])) = T +fun dest_fsetT \<^Type>\fset T\ = T | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); \ diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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 (); diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/Lifting/lifting_bnf.ML --- 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>\Quotient\, 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 diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/Lifting/lifting_def.ML --- 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>\less_eq\, T --> T --> HOLogic.boolT) $ - (Const (\<^const_name>\HOL.eq\, T)) $ x - end; - val goal = HOLogic.mk_Trueprop (mk_ge_eq rel); - in - mono_eq_prover ctxt goal - end; + val T as \<^Type>\fun A _\ = fastype_of rel + val ge_eq = \<^Const>\less_eq T for \<^Const>\HOL.eq A\ rel\ + 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>\POS\, ty --> ty --> HOLogic.boolT) + fun mk_POS ty = + let val \<^Type>\fun A \<^Type>\fun B bool\\ = ty + in \<^Const>\POS A B\ 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>\fun _ U\, \<^Type>\fun _ V\) = 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>\fun T U\, \<^Type>\fun V W\) = (T, V) :: get_binder_types (U, W) | get_binder_types _ = [] -fun get_binder_types_by_rel (Const (\<^const_name>\rel_fun\, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = +fun get_binder_types_by_rel \<^Const_>\rel_fun _ _ _ _ for _ S\ (\<^Type>\fun T U\, \<^Type>\fun V W\) = (T, V) :: get_binder_types_by_rel S (U, W) | get_binder_types_by_rel _ _ = [] -fun get_body_type_by_rel (Const (\<^const_name>\rel_fun\, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = +fun get_body_type_by_rel \<^Const_>\rel_fun _ _ _ _ for _ S\ (\<^Type>\fun _ U\, \<^Type>\fun _ V\) = get_body_type_by_rel S (U, V) | get_body_type_by_rel _ (U, V) = (U, V) -fun get_binder_rels (Const (\<^const_name>\rel_fun\, _) $ R $ S) = R :: get_binder_rels S +fun get_binder_rels \<^Const_>\rel_fun _ _ _ _ for R S\ = 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>\map_fun\, _) $ _ $ _ => + \<^Const_>\map_fun _ _ _ _ for _ _\ => (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>\HOL.eq\, _) => true - | Const (\<^const_name>\eq_onp\, _) $ _ => true - | _ => false + \<^Const_>\HOL.eq _\ => true + | \<^Const_>\eq_onp _ for _\ => 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 diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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>\undefined\, 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>\undefined \quot_thm_rty_qty quot_thm |> snd\\ 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>\rel_fun\, _) $ _ $ _ => - binop_conv2 Conv.all_conv conv ctm - | _ => conv ctm + \<^Const_>\rel_fun _ _ _ _ for _ _\ => 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>\undefined T\, 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>\type_definition\, - (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>\type_definition qty_isom qty for rep_isom abs_isom \HOLogic.mk_UNIV qty\\ |> 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>\rel_fun\, _) $ _ $ _ => + \<^Const_>\rel_fun _ _ _ _ for _ _\ => (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>\Pure.all\, _) $ Abs (_, T, t)) = T :: all_typs t + fun all_typs \<^Const_>\Pure.all _ for \Abs (_, T, t)\\ = T :: all_typs t | all_typs _ = [] - fun rename (Const (\<^const_name>\Pure.all\, T1) $ Abs (_, T2, t)) (new_name :: names) = - (Const (\<^const_name>\Pure.all\, T1) $ Abs (new_name, T2, rename t names)) + fun rename \<^Const_>\Pure.all T1 for \Abs (_, T2, t)\\ (new_name :: names) = + \<^Const>\Pure.all T1 for \Abs (new_name, T2, rename t names)\\ | rename t _ = t val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/Lifting/lifting_info.ML --- 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>\less_eq\, _) $ (lhs as Const (\<^const_name>\relcompp\,_) $ _ $ _) $ rhs => - (lhs, rhs) - | Const (\<^const_name>\less_eq\, _) $ rhs $ (lhs as Const (\<^const_name>\relcompp\,_) $ _ $ _) => - (lhs, rhs) - | Const (\<^const_name>\HOL.eq\, _) $ (lhs as Const (\<^const_name>\relcompp\,_) $ _ $ _) $ rhs => - (lhs, rhs) + \<^Const_>\less_eq _ for \lhs as \<^Const_>\relcompp _ _ _ for _ _\\ rhs\ => (lhs, rhs) + | \<^Const_>\less_eq _ for rhs \lhs as \<^Const_>\relcompp _ _ _ for _ _\\\ => (lhs, rhs) + | \<^Const_>\HOL.eq _ for \lhs as \<^Const_>\relcompp _ _ _ for _ _\\ rhs\ => (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>\relcompp\, _) $ Var _ $ Var _ => () + \<^Const_>\relcompp _ _ _ for \Var _\ \Var _\\ => () | _ => 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>\less_eq\, _) $ (Const (\<^const_name>\relcompp\,_) $ _ $ _) $ _ => + \<^Const_>\less_eq _ for \<^Const_>\relcompp _ _ _ for _ _\ _\ => add_pos_distr_rule distr_rule context - | Const (\<^const_name>\less_eq\, _) $ _ $ (Const (\<^const_name>\relcompp\,_) $ _ $ _) => + | \<^Const_>\less_eq _ for _ \<^Const_>\relcompp _ _ _ for _ _\\ => add_neg_distr_rule distr_rule context - | Const (\<^const_name>\HOL.eq\, _) $ (Const (\<^const_name>\relcompp\,_) $ _ $ _) $ _ => + | \<^Const_>\HOL.eq _ for \<^Const_>\relcompp _ _ _ for _ _\ _\ => add_eq_distr_rule distr_rule context) end end diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/Lifting/lifting_setup.ML --- 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>\relcompp\, - (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>\relcompp rty rty' qty for param_rel_fixed fixed_crel\ 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>\relcompp\, _) $ Const (\<^const_name>\HOL.eq\, _) $ _ => + \<^Const_>\relcompp _ _ _ for \<^Const_>\HOL.eq _\ _\ => let val thm = pcr_cr_eq @@ -164,8 +160,8 @@ in (thm, lthy') end - | Const (\<^const_name>\relcompp\, _) $ t $ _ => print_generate_pcr_cr_eq_error args_ctxt t - | _ => error "generate_pcr_cr_eq: implementation error" + | \<^Const_>\relcompp _ _ _ for t _\ => 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>\top\, _) => - [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient} - | Const (\<^const_name>\Collect\, _) $ 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_>\top _\ => [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient} + | \<^Const_>\Collect _ for \Abs _\\ => [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>\top\, _) => + \<^Const_>\top _\ => 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>\Quotient\, _) $ _ $ _ $ _ $ _) => setup_quotient () - | (Const (\<^const_name>\type_definition\, _) $ _ $ _ $ _) => setup_typedef () - | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." + \<^Const_>\Quotient _ _ for _ _ _ _\ => setup_quotient () + | \<^Const_>\type_definition _ _ for _ _ _\ => 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>\HOL.eq\, _)) = true + fun is_eq \<^Const_>\HOL.eq _\ = 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>\right_unique\, \<^const_name>\left_unique\, \<^const_name>\right_total\, - \<^const_name>\left_total\, \<^const_name>\bi_unique\, \<^const_name>\bi_total\] - -fun fold_transfer_rel f (Const (\<^const_name>\Transfer.Rel\, _) $ rel $ _ $ _) = f rel - | fold_transfer_rel f (Const (\<^const_name>\HOL.eq\, _) $ - (Const (\<^const_name>\Domainp\, _) $ rel) $ _) = f rel - | fold_transfer_rel f (Const (name, _) $ rel) = - if member op= monotonicity_names name then f rel else f \<^term>\undefined\ +fun fold_transfer_rel f \<^Const_>\Transfer.Rel _ _ for rel _ _\ = f rel + | fold_transfer_rel f \<^Const_>\HOL.eq _ for \<^Const_>\Domainp _ _ for rel\ _\ = f rel + | fold_transfer_rel f \<^Const_>\right_unique _ _ for rel\ = f rel + | fold_transfer_rel f \<^Const_>\left_unique _ _ for rel\ = f rel + | fold_transfer_rel f \<^Const_>\right_total _ _ for rel\ = f rel + | fold_transfer_rel f \<^Const_>\left_total _ _ for rel\ = f rel + | fold_transfer_rel f \<^Const_>\bi_unique _ _ for rel\ = f rel + | fold_transfer_rel f \<^Const_>\bi_total _ _ for rel\ = f rel | fold_transfer_rel f _ = f \<^term>\undefined\ fun filter_transfer_rules_by_rel transfer_rel transfer_rules = diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/Lifting/lifting_term.ML --- 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>\POS\, _) => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm) - | Const (\<^const_name>\NEG\, _) => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm)) + \<^Const_>\POS _ _\ => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm) + | \<^Const_>\NEG _ _\ => 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>\POS\, _) => true - | Const (\<^const_name>\NEG\, _) => true + \<^Const_>\POS _ _\ => true + | \<^Const_>\NEG _ _\ => 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>\HOL.eq\, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm - | [_, Const (\<^const_name>\HOL.eq\, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm + [\<^Const_>\HOL.eq _\, _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm + | [_, \<^Const_>\HOL.eq _\] => 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 diff -r daa604a00491 -r 81da5938a7be src/HOL/Tools/Lifting/lifting_util.ML --- 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>\Quotient\, _) $ rel $ abs $ rep $ cr) - = (rel, abs, rep, cr) +fun mk_Quotient (rel, abs, rep, cr) = + let val \<^Type>\fun A B\ = fastype_of abs + in \<^Const>\Quotient A B for rel abs rep cr\ end + +fun dest_Quotient \<^Const_>\Quotient _ _ for rel abs rep cr\