# HG changeset patch # User huffman # Date 1291673855 28800 # Node ID 4acbacd6c5bcfa302c7612d6042865078e6bbe8f # Parent 22a57175df202046c36f50dba3d50f7768be03ca add set-union-like syntax for powerdomain bind operators diff -r 22a57175df20 -r 4acbacd6c5bc src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Mon Dec 06 13:43:05 2010 -0800 +++ b/src/HOL/HOLCF/ConvexPD.thy Mon Dec 06 14:17:35 2010 -0800 @@ -342,6 +342,13 @@ convex_bind :: "'a convex_pd \ ('a \ 'b convex_pd) \ 'b convex_pd" where "convex_bind = convex_pd.basis_fun convex_bind_basis" +syntax + "_convex_bind" :: "[logic, logic, logic] \ logic" + ("(3\\_\_./ _)" [0, 0, 10] 10) + +translations + "\\x\xs. e" == "CONST convex_bind\xs\(\ x. e)" + lemma convex_bind_principal [simp]: "convex_bind\(convex_principal t) = convex_bind_basis t" unfolding convex_bind_def diff -r 22a57175df20 -r 4acbacd6c5bc src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Mon Dec 06 13:43:05 2010 -0800 +++ b/src/HOL/HOLCF/LowerPD.thy Mon Dec 06 14:17:35 2010 -0800 @@ -335,6 +335,13 @@ lower_bind :: "'a lower_pd \ ('a \ 'b lower_pd) \ 'b lower_pd" where "lower_bind = lower_pd.basis_fun lower_bind_basis" +syntax + "_lower_bind" :: "[logic, logic, logic] \ logic" + ("(3\\_\_./ _)" [0, 0, 10] 10) + +translations + "\\x\xs. e" == "CONST lower_bind\xs\(\ x. e)" + lemma lower_bind_principal [simp]: "lower_bind\(lower_principal t) = lower_bind_basis t" unfolding lower_bind_def diff -r 22a57175df20 -r 4acbacd6c5bc src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Mon Dec 06 13:43:05 2010 -0800 +++ b/src/HOL/HOLCF/UpperPD.thy Mon Dec 06 14:17:35 2010 -0800 @@ -330,6 +330,13 @@ upper_bind :: "'a upper_pd \ ('a \ 'b upper_pd) \ 'b upper_pd" where "upper_bind = upper_pd.basis_fun upper_bind_basis" +syntax + "_upper_bind" :: "[logic, logic, logic] \ logic" + ("(3\\_\_./ _)" [0, 0, 10] 10) + +translations + "\\x\xs. e" == "CONST upper_bind\xs\(\ x. e)" + lemma upper_bind_principal [simp]: "upper_bind\(upper_principal t) = upper_bind_basis t" unfolding upper_bind_def