# HG changeset patch # User wenzelm # Date 1722880643 -7200 # Node ID cc205e40192e8c257db22598a9c460052373bbcf # Parent 3cde955e4e47ea079d8f71b22f2cda90c77fb5c6 tuned: more antiquotations; diff -r 3cde955e4e47 -r cc205e40192e src/HOL/Tools/set_comprehension_pointfree.ML --- a/src/HOL/Tools/set_comprehension_pointfree.ML Sun Aug 04 23:50:44 2024 +0200 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Mon Aug 05 19:57:23 2024 +0200 @@ -18,73 +18,46 @@ (* syntactic operations *) fun mk_inf (t1, t2) = - let - val T = fastype_of t1 - in - Const (\<^const_name>\Lattices.inf_class.inf\, T --> T --> T) $ t1 $ t2 - end + let val T = fastype_of t1 + in \<^Const>\inf T for t1 t2\ end fun mk_sup (t1, t2) = - let - val T = fastype_of t1 - in - Const (\<^const_name>\Lattices.sup_class.sup\, T --> T --> T) $ t1 $ t2 - end + let val T = fastype_of t1 + in \<^Const>\sup T for t1 t2\ end fun mk_Compl t = - let - val T = fastype_of t - in - Const (\<^const_name>\Groups.uminus_class.uminus\, T --> T) $ t - end + let val T = fastype_of t + in \<^Const>\uminus T for t\ end fun mk_image t1 t2 = - let - val T as Type (\<^type_name>\fun\, [_ , R]) = fastype_of t1 - in - Const (\<^const_name>\image\, - T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2 - end; + let val \<^Type>\fun A B\ = fastype_of t1 + in \<^Const>\image A B for t1 t2\ end; fun mk_sigma (t1, t2) = let - val T1 = fastype_of t1 - val T2 = fastype_of t2 - val setT = HOLogic.dest_setT T1 - val resT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2)) - in - Const (\<^const_name>\Sigma\, - T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2 - end; + val \<^Type>\set A\ = fastype_of t1 + val \<^Type>\set B\ = fastype_of t2 + in \<^Const>\Sigma A B for t1 \absdummy A t2\\ end; fun mk_vimage f s = - let - val T as Type (\<^type_name>\fun\, [T1, T2]) = fastype_of f - in - Const (\<^const_name>\vimage\, T --> HOLogic.mk_setT T2 --> HOLogic.mk_setT T1) $ f $ s - end; + let val \<^Type>\fun A B\ = fastype_of f + in \<^Const>\vimage A B for f s\ end; -fun dest_Collect (Const (\<^const_name>\Collect\, _) $ Abs (x, T, t)) = ((x, T), t) +fun dest_Collect \<^Const_>\Collect _ for \Abs (x, T, t)\\ = ((x, T), t) | dest_Collect t = raise TERM ("dest_Collect", [t]) (* Copied from predicate_compile_aux.ML *) -fun strip_ex (Const (\<^const_name>\Ex\, _) $ Abs (x, T, t)) = - let - val (xTs, t') = strip_ex t - in - ((x, T) :: xTs, t') - end +fun strip_ex \<^Const_>\Ex _ for \Abs (x, T, t)\\ = + let val (xTs, t') = strip_ex t + in ((x, T) :: xTs, t') end | strip_ex t = ([], t) fun mk_prod1 Ts (t1, t2) = - let - val (T1, T2) = apply2 (curry fastype_of1 Ts) (t1, t2) - in - HOLogic.pair_const T1 T2 $ t1 $ t2 - end; + let val (A, B) = apply2 (curry fastype_of1 Ts) (t1, t2) + in \<^Const>\Pair A B for t1 t2\ end; fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end - | mk_split_abs vs (Const (\<^const_name>\Product_Type.Pair\, _) $ u $ v) t = + | mk_split_abs vs \<^Const_>\Pair _ _ for u v\ t = HOLogic.mk_case_prod (mk_split_abs vs u (mk_split_abs vs v t)) | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]); @@ -92,7 +65,7 @@ val strip_ptupleabs = let fun strip [] qs vs t = (t, rev vs, qs) - | strip (p :: ps) qs vs (Const (\<^const_name>\case_prod\, _) $ t) = + | strip (p :: ps) qs vs \<^Const_>\case_prod _ _ _ for t\ = strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t | strip (_ :: ps) qs vs t = strip ps qs @@ -114,8 +87,8 @@ fun term_of_pattern Ts (Pattern bs) = let fun mk [b] = Bound b - | mk (b :: bs) = HOLogic.pair_const (nth Ts b) (type_of_pattern Ts (Pattern bs)) - $ Bound b $ mk bs + | mk (b :: bs) = + \<^Const>\Pair \nth Ts b\ \type_of_pattern Ts (Pattern bs)\ for \Bound b\ \mk bs\\ in mk bs end; (* formulas *) @@ -125,8 +98,8 @@ fun map_atom f (Atom a) = Atom (f a) | map_atom _ x = x -fun is_collect_atom (Atom (_, Const(\<^const_name>\Collect\, _) $ _)) = true - | is_collect_atom (Atom (_, Const (\<^const_name>\Groups.uminus_class.uminus\, _) $ (Const(\<^const_name>\Collect\, _) $ _))) = true +fun is_collect_atom (Atom (_, \<^Const_>\Collect _ for _\)) = true + | is_collect_atom (Atom (_, \<^Const_>\uminus _ for \<^Const_>\Collect _ for _\\)) = true | is_collect_atom _ = false fun mk_case_prod _ [(x, T)] t = (T, Abs (x, T, t)) @@ -151,12 +124,12 @@ let val (tuple, (vs', t')) = mk_term vs t val T = HOLogic.mk_tupleT (map snd vs') - val s = HOLogic.Collect_const T $ (snd (mk_case_prod \<^typ>\bool\ vs' t')) + val s = \<^Const>\Collect T for \snd (mk_case_prod \<^Type>\bool\ vs' t')\\ in (tuple, Atom (tuple, s)) end -fun mk_atom vs (t as Const (\<^const_name>\Set.member\, _) $ x $ s) = +fun mk_atom vs (t as \<^Const_>\Set.member _ for x s\) = if not (null (loose_bnos s)) then default_atom vs t else @@ -165,10 +138,10 @@ | NONE => let val (tuple, (vs', x')) = mk_term vs x - val rT = HOLogic.dest_setT (fastype_of s) + val \<^Type>\set rT\ = fastype_of s val s = mk_vimage (snd (mk_case_prod rT vs' x')) s in (tuple, Atom (tuple, s)) end) - | mk_atom vs (Const (\<^const_name>\HOL.Not\, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t) + | mk_atom vs \<^Const_>\Not for t\ = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t) | mk_atom vs t = default_atom vs t fun merge' [] (pats1, pats2) = ([], (pats1, pats2)) @@ -305,14 +278,14 @@ (* proof tactic *) -val case_prod_beta = - @{lemma "case_prod g x z = case_prod (\x y. (g x y) z) x" by (simp add: case_prod_beta)} +val case_prod_beta = @{lemma "case_prod g x z = case_prod (\x y. (g x y) z) x" by (simp add: case_prod_beta)} -val vimageI2' = @{lemma "f a \ A \ a \ f -` A" by simp} -val vimageE' = @{lemma "a \ f -` B \ (\ x. f a = x ==> x \ B \ P) \ P" by simp} +val vimageI2' = @{lemma "f a \ A ==> a \ f -` A" by simp} +val vimageE' = + @{lemma "a \ f -` B ==> (\ x. f a = x ==> x \ B ==> P) ==> P" by simp} -val collectI' = @{lemma "\ P a \ a \ {x. P x}" by auto} -val collectE' = @{lemma "a \ {x. P x} \ (\ P a \ Q) \ Q" by auto} +val collectI' = @{lemma "\ P a ==> a \ {x. P x}" by auto} +val collectE' = @{lemma "a \ {x. P x} ==> (\ P a ==> Q) ==> Q" by auto} fun elim_Collect_tac ctxt = dresolve_tac ctxt @{thms iffD1 [OF mem_Collect_eq]} @@ -415,7 +388,7 @@ fun comprehension_conv ctxt ct = let - fun dest_Collect (Const (\<^const_name>\Collect\, T) $ t) = (HOLogic.dest_setT (body_type T), t) + fun dest_Collect \<^Const_>\Collect A for t\ = (A, t) | dest_Collect t = raise TERM ("dest_Collect", [t]) fun list_ex vs t = fold_rev (fn (x, T) => fn t => HOLogic.exists_const T $ Abs (x, T, t)) vs t fun mk_term t = @@ -428,7 +401,7 @@ val eq = HOLogic.eq_const T $ Bound (length Ts) $ (HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts))) in - HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t''))) + \<^Const>\Collect T for \absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))\\ end; fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (Thm.prop_of th)) val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}