src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML

 
 fun mk_randompredT T =
   @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed})
 
 fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
-  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
+  [Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = T
   | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
 
-fun mk_empty T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
+fun mk_empty T = Const(@{const_name Random_Pred.empty}, mk_randompredT T)
 
 fun mk_single t =
   let               
     val T = fastype_of t
   in
-    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
+    Const (@{const_name Random_Pred.single}, T --> mk_randompredT T) $ t
   end;
 
 fun mk_bind (x, f) =
   let
     val T as (Type ("fun", [_, U])) = fastype_of f
   in
-    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Random_Pred.bind}, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck.union}
-
-fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
+val mk_plus = HOLogic.mk_binop @{const_name Random_Pred.union}
+
+fun mk_if cond = Const (@{const_name Random_Pred.if_randompred},
   HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name Quickcheck.iterate_upto},
+  list_comb (Const (@{const_name Random_Pred.iterate_upto},
       [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T),
     [f, from, to])
 
 fun mk_not t =
   let
     val T = mk_randompredT HOLogic.unitT
-  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
+  in Const (@{const_name Random_Pred.not_randompred}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map},
   (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_randompredT, dest_monadT = dest_randompredT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,

 
 fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
   Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name DSequence.empty}, mk_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.empty}, mk_dseqT T);
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
+  in Const(@{const_name Limited_Sequence.single}, T --> mk_dseqT T) $ t end;
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
-  end;
-
-val mk_plus = HOLogic.mk_binop @{const_name DSequence.union};
-
-fun mk_if cond = Const (@{const_name DSequence.if_seq},
+    Const (@{const_name Limited_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.union};
+
+fun mk_if cond = Const (@{const_name Limited_Sequence.if_seq},
   HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t = let val T = mk_dseqT HOLogic.unitT
-  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
+  in Const (@{const_name Limited_Sequence.not_seq}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map},
   (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_dseqT, dest_monadT = dest_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,

 
 fun dest_pos_dseqT (Type ("fun", [@{typ code_numeral},
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
   | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T);
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name New_DSequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
-  let
-    val T as Type ("fun", [_, U]) = fastype_of f
-  in
-    Const (@{const_name New_DSequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+  in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Limited_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   end;
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
-
-val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
-
-fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
+    Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union};
+
+fun mk_if cond = Const (@{const_name Limited_Sequence.pos_if_seq},
   HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t =
   let
     val pT = mk_pos_dseqT HOLogic.unitT
     val nT =
       @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
         [Type (@{type_name Option.option}, [@{typ unit}])])
-  in Const (@{const_name New_DSequence.pos_not_seq}, nT --> pT) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.pos_map},
+  in Const (@{const_name Limited_Sequence.pos_not_seq}, nT --> pT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.pos_map},
   (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,

 
 fun dest_neg_dseqT (Type ("fun", [@{typ code_numeral},
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
   | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T);
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name New_DSequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
-  let
-    val T as Type ("fun", [_, U]) = fastype_of f
-  in
-    Const (@{const_name New_DSequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+  in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Limited_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
   end;
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
-
-val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
-
-fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
+    Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union};
+
+fun mk_if cond = Const (@{const_name Limited_Sequence.neg_if_seq},
   HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t =
   let
     val nT = mk_neg_dseqT HOLogic.unitT
     val pT =
       @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
         [@{typ unit}])
-  in Const (@{const_name New_DSequence.neg_not_seq}, pT --> nT) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.neg_map},
+  in Const (@{const_name Limited_Sequence.neg_not_seq}, pT --> nT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.neg_map},
   (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,

 fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
     Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
   | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
-  let
-    val T as Type ("fun", [_, U]) = fastype_of f
-  in
-    Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+  in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
-
-val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
-
-fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
+    Const (@{const_name Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union};
+
+fun mk_if cond = Const (@{const_name Random_Sequence.pos_if_random_dseq},
   HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto},
+  list_comb (Const (@{const_name Random_Sequence.pos_iterate_upto},
       [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
         ---> mk_pos_random_dseqT T),
     [f, from, to])
 
 fun mk_not t =

     val pT = mk_pos_random_dseqT HOLogic.unitT
     val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
       @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
         [Type (@{type_name Option.option}, [@{typ unit}])])
 
-  in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
+  in Const (@{const_name Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.pos_map},
   (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,

     Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
       Type (@{type_name Lazy_Sequence.lazy_sequence},
         [Type (@{type_name Option.option}, [T])])])])])])) = T
   | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
-  let
-    val T as Type ("fun", [_, U]) = fastype_of f
-  in
-    Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+  in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
-
-val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
-
-fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
+    Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union};
+
+fun mk_if cond = Const (@{const_name Random_Sequence.neg_if_random_dseq},
   HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto},
+  list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto},
       [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
         ---> mk_neg_random_dseqT T),
     [f, from, to])
 
 fun mk_not t =
   let
     val nT = mk_neg_random_dseqT HOLogic.unitT
     val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
     @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
-  in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
+  in Const (@{const_name Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.neg_map},
   (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,