314 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); |
314 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); |
315 fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
315 fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
316 fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, |
316 fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, |
317 liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; |
317 liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; |
318 fun mk_split T = Sign.mk_const thy |
318 fun mk_split T = Sign.mk_const thy |
319 (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]); |
319 (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]); |
320 fun mk_scomp_split T t t' = |
320 fun mk_scomp_split T t t' = |
321 mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t |
321 mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t |
322 (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t'))); |
322 (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t'))); |
323 fun mk_bindclause (_, _, i, T) = mk_scomp_split T |
323 fun mk_bindclause (_, _, i, T) = mk_scomp_split T |
324 (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i); |
324 (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i); |
360 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); |
360 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); |
361 fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
361 fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
362 fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, |
362 fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, |
363 liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; |
363 liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; |
364 fun mk_split T = Sign.mk_const thy |
364 fun mk_split T = Sign.mk_const thy |
365 (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]); |
365 (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]); |
366 fun mk_scomp_split T t t' = |
366 fun mk_scomp_split T t t' = |
367 mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t |
367 mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t |
368 (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t'))); |
368 (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t'))); |
369 fun mk_bindclause (_, _, i, T) = mk_scomp_split T |
369 fun mk_bindclause (_, _, i, T) = mk_scomp_split T |
370 (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i); |
370 (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i); |