# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID e2e23987c59ac17aaf4f56606b8a66a3ff7a683c # Parent 0d16c07f8d2450efde016f5c7032390ff107349a reinvestigating the compilation of the random computation in the predicate compiler diff -r 0d16c07f8d24 -r e2e23987c59a src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200 @@ -147,7 +147,7 @@ val vars = map Var (Term.add_vars abs_arg []) val abs_arg' = Logic.unvarify abs_arg val frees = map Free (Term.add_frees abs_arg' []) - val constname = Name.variant [] + val constname = Name.variant (map (Long_Name.base_name o fst) new_defs) ((Long_Name.base_name constname) ^ "_hoaux") val full_constname = Sign.full_bname thy constname val constT = map fastype_of frees ---> (fastype_of abs_arg') diff -r 0d16c07f8d24 -r e2e23987c59a src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200 @@ -73,8 +73,8 @@ if member (op =) modes ([], []) then let val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], []) - val T = @{typ code_numeral} --> (mk_rpredT (HOLogic.mk_tupleT (map snd vs'))) - in Const (name, T) $ Bound 0 end + val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs'))) + in Const (name, T) $ @{term True} $ Bound 0 end else if member (op =) depth_limited_modes ([], []) then let val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) diff -r 0d16c07f8d24 -r e2e23987c59a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 @@ -388,7 +388,7 @@ (* diagnostic display functions *) fun print_modes modes = - tracing ("Inferred modes:\n" ^ + Output.tracing ("Inferred modes:\n" ^ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_mode ms)) modes)); @@ -398,7 +398,7 @@ ^ (string_of_entry pred mode entry) fun print_pred (pred, modes) = "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes) - val _ = tracing (cat_lines (map print_pred pred_mode_table)) + val _ = Output.tracing (cat_lines (map print_pred pred_mode_table)) in () end; fun string_of_prem thy (Prem (ts, p)) = @@ -774,8 +774,6 @@ mk_sup : term * term -> term, mk_if : term -> term, mk_not : term -> term, -(* funT_of : mode -> typ -> typ, *) -(* mk_fun_of : theory -> (string * typ) -> mode -> term, *) mk_map : typ -> typ -> term -> term -> term, lift_pred : term -> term }; @@ -788,8 +786,6 @@ fun mk_sup (CompilationFuns funs) = #mk_sup funs fun mk_if (CompilationFuns funs) = #mk_if funs fun mk_not (CompilationFuns funs) = #mk_not funs -(*fun funT_of (CompilationFuns funs) = #funT_of funs*) -(*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*) fun mk_map (CompilationFuns funs) = #mk_map funs fun lift_pred (CompilationFuns funs) = #lift_pred funs @@ -889,7 +885,8 @@ fun mk_if cond = Const (@{const_name RPred.if_rpred}, HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond; -fun mk_not t = error "Negation is not defined for RPred" +fun mk_not t = let val T = mk_rpredT HOLogic.unitT + in Const (@{const_name RPred.not_rpred}, T --> T) $ t end fun mk_map T1 T2 tf tp = Const (@{const_name RPred.map}, (T1 --> T2) --> mk_rpredT T1 --> mk_rpredT T2) $ tf $ tp @@ -924,7 +921,7 @@ let val Ts = binder_types T val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => depth_limited_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs + val paramTs' = map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs in (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs)) end; @@ -963,16 +960,16 @@ fun term_vTs tm = fold_aterms (fn Free xT => cons xT | _ => I) tm []; -(*FIXME this function should not be named merge... make it local instead*) -fun merge xs [] = xs - | merge [] ys = ys - | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) - else y::merge (x::xs) ys; - -fun subsets i j = if i <= j then - let val is = subsets (i+1) j - in merge (map (fn ks => i::ks) is) is end - else [[]]; +fun subsets i j = + if i <= j then + let + fun merge xs [] = xs + | merge [] ys = ys + | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) + else y::merge (x::xs) ys; + val is = subsets (i+1) j + in merge (map (fn ks => i::ks) is) is end + else [[]]; (* FIXME: should be in library - cprod = map_prod I *) fun cprod ([], ys) = [] @@ -1025,7 +1022,7 @@ *) fun modes_of_term modes t = let - val ks = map_index (fn (i, T) => (i, NONE)) (binder_types (fastype_of t)); + val ks = map_index (fn (i, T) => (i + 1, NONE)) (binder_types (fastype_of t)); val default = [Mode (([], ks), ks, [])]; fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => let @@ -1205,16 +1202,21 @@ fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses = let val prednames = map fst clauses - val extra_modes = all_modes_of thy + val extra_modes' = all_modes_of thy val gen_modes = all_generator_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) - val starting_modes = remove_from extra_modes all_modes + val starting_modes = remove_from extra_modes' all_modes + fun eq_mode (m1, m2) = (m1 = m2) val modes = fixp (fn modes => - map (check_modes_pred options true thy param_vs clauses extra_modes (gen_modes @ modes)) modes) - starting_modes + map (check_modes_pred options true thy param_vs clauses extra_modes' (gen_modes @ modes)) modes) + starting_modes in - map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes + AList.join (op =) + (fn _ => fn ((mps1, mps2)) => + merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2)) + (infer_modes options thy extra_modes all_modes param_vs clauses, + map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes) end; (* term construction *) @@ -1270,13 +1272,12 @@ fold_rev lambda vs (f (list_comb (t, vs))) end; -fun compile_param depth_limited thy compfuns (NONE, t) = t - | compile_param depth_limited thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = +fun compile_param depth_limited thy compfuns mk_fun_of (NONE, t) = t + | compile_param depth_limited thy compfuns mk_fun_of (m as SOME (Mode ((iss, is'), is, ms)), t) = let val (f, args) = strip_comb (Envir.eta_contract t) val (params, args') = chop (length ms) args - val params' = map (compile_param depth_limited thy compfuns) (ms ~~ params) - val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of + val params' = map (compile_param depth_limited thy compfuns mk_fun_of) (ms ~~ params) val funT_of = if depth_limited then depth_limited_funT_of else funT_of val f' = case f of @@ -1287,34 +1288,36 @@ list_comb (f', params' @ args') end -fun compile_expr depth_limited thy ((Mode (mode, is, ms)), t) inargs = +fun compile_expr depth_limited thy compfuns mk_fun_of ((Mode (mode, is, ms)), t) inargs = case strip_comb t of (Const (name, T), params) => let - val params' = map (compile_param depth_limited thy PredicateCompFuns.compfuns) (ms ~~ params) - val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of + val params' = map (compile_param depth_limited thy compfuns mk_fun_of) (ms ~~ params) + (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*) + val _ = if mode = ([], [(0, NONE)]) then error "something is wrong" else () + val _ = Output.tracing ("compile_expr mode: " ^ string_of_mode mode) in - list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params' @ inargs) + (*lift_pred compfuns*)(list_comb (mk_fun_of compfuns thy (name, T) mode, params' @ inargs)) end | (Free (name, T), params) => let val funT_of = if depth_limited then depth_limited_funT_of else funT_of in - list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), params @ inargs) + list_comb (Free (name, funT_of compfuns ([], is) T), params @ inargs) end; - -fun compile_gen_expr depth thy ((Mode (mode, is, ms)), t) inargs = + +fun compile_gen_expr depth_limited thy compfuns mk_fun_of ((Mode (mode, is, ms)), t) inargs = case strip_comb t of (Const (name, T), params) => let - val params' = map (compile_param depth thy RPredCompFuns.compfuns) (ms ~~ params) + val params' = map (compile_param depth_limited thy RPredCompFuns.compfuns mk_fun_of) (ms ~~ params) in list_comb (mk_generator_of RPredCompFuns.compfuns thy (name, T) mode, params' @ inargs) end | (Free (name, T), params) => - lift_pred RPredCompFuns.compfuns - (list_comb (Free (name, depth_limited_funT_of RPredCompFuns.compfuns ([], is) T), params @ inargs)) - + (*lift_pred RPredCompFuns.compfuns*) + (list_comb (Free (name, depth_limited_funT_of RPredCompFuns.compfuns ([], is) T), params @ inargs)) + (** specific rpred functions -- move them to the correct place in this file *) fun mk_Eval_of depth ((x, T), NONE) names = (x, names) @@ -1383,7 +1386,7 @@ | map_params t = t in map_aterms map_params arg end -fun compile_clause compfuns depth thy all_vs param_vs (iss, is) inp (ts, moded_ps) = +fun compile_clause compfuns mk_fun_of depth thy all_vs param_vs (iss, is) inp (ts, moded_ps) = let fun check_constrt t (names, eqs) = if is_constrt thy t then (t, (names, eqs)) else @@ -1421,8 +1424,8 @@ val args = case depth of NONE => in_ts | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t] - val u = lift_pred compfuns - (compile_expr (is_some depth) thy (mode, t) args) + val u = + (compile_expr (is_some depth) thy compfuns mk_fun_of (mode, t) args) val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1433,8 +1436,8 @@ val args = case depth of NONE => in_ts | SOME (polarity, depth_t) => in_ts @ [HOLogic.mk_not polarity, depth_t] - val u = lift_pred compfuns (mk_not PredicateCompFuns.compfuns - (compile_expr (is_some depth) thy (mode, t) args)) + val u = (*lift_pred compfuns*) (mk_not compfuns + (compile_expr (is_some depth) thy compfuns mk_fun_of (mode, t) args)) val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1449,9 +1452,9 @@ let val (in_ts, out_ts''') = split_smode is us; val args = case depth of - NONE => in_ts + NONE => in_ts | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t] - val u = compile_gen_expr (is_some depth) thy (mode, t) args + val u = compile_gen_expr (is_some depth) thy compfuns mk_fun_of (mode, t) args val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1477,7 +1480,7 @@ val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) val (Us1, Us2) = split_smodeT (snd mode) Ts2 val funT_of = if depth_limited then depth_limited_funT_of else funT_of - val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1 + val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1 fun mk_input_term (i, NONE) = [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of @@ -1501,7 +1504,7 @@ else NONE val cl_ts = - map (compile_clause compfuns decr_depth + map (compile_clause compfuns mk_fun_of decr_depth thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls; val compilation = foldr1 (mk_sup compfuns) cl_ts val T' = mk_predT compfuns (mk_tupleT Us2) @@ -1730,11 +1733,12 @@ val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = let + val _ = Output.tracing ("mode: " ^ string_of_mode mode) val mode_cname = create_constname_of_mode thy "gen_" name mode val funT = generator_funT_of mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_generator_name name mode mode_cname + |> set_generator_name name mode mode_cname end; in fold create_definition modes thy @@ -2409,7 +2413,7 @@ goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> (if is_rpred options then (add_equations options [const] #> - add_depth_limited_equations options [const] #> add_quickcheck_equations options [const]) + (*add_depth_limited_equations options [const] #> *)add_quickcheck_equations options [const]) else if is_depth_limited options then add_depth_limited_equations options [const] else @@ -2454,7 +2458,9 @@ case depth_limit of NONE => inargs | SOME d => inargs @ [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d] - val t_pred = compile_expr (is_some depth_limit) thy + val mk_fun_of = if random then mk_generator_of else + if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of + val t_pred = compile_expr (is_some depth_limit) thy compfuns mk_fun_of (m, list_comb (pred, params)) inargs'; val t_eval = if null outargs then t_pred else let diff -r 0d16c07f8d24 -r e2e23987c59a src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 @@ -92,9 +92,7 @@ values "{zs. append [0, Suc 0, 2] [17, 8] zs}" values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" -ML {* Random_Engine.run *} -term "Predicate.map" -values [depth_limit = 5 random] "{(ys, zs). append [1::nat, 2] ys zs}" +values [depth_limit = 10 random] 15 "{(ys, zs). append [1::nat, 2] ys zs}" value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (append_3 ([]::int list))" @@ -119,13 +117,20 @@ subsection {* Tricky cases with tuples *} +inductive zerozero :: "nat * nat => bool" +where + "zerozero (0, 0)" + +code_pred zerozero . +code_pred [rpred] zerozero . + inductive tupled_append :: "'a list \ 'a list \ 'a list \ bool" where "tupled_append ([], xs, xs)" | "tupled_append (xs, ys, zs) \ tupled_append (x # xs, ys, x # zs)" code_pred tupled_append . - +code_pred [rpred] tupled_append . thm tupled_append.equation (* TODO: values with tupled modes @@ -136,22 +141,20 @@ where "tupled_append' ([], xs, xs)" | "[| ys = fst (xa, y); x # zs = snd (xa, y); - tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)" -ML {* aconv *} + tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)" + code_pred tupled_append' . thm tupled_append'.equation -(* TODO: Modeanalysis returns mode [2] ?? *) inductive tupled_append'' :: "'a list \ 'a list \ 'a list \ bool" where "tupled_append'' ([], xs, xs)" -| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, x # zs) \ tupled_append'' (x # xs, yszs)" +| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \ tupled_append'' (x # xs, yszs)" thm tupled_append''.cases code_pred [inductify] tupled_append'' . thm tupled_append''.equation -(* TODO: Modeanalysis returns mode [2] ?? *) inductive tupled_append''' :: "'a list \ 'a list \ 'a list \ bool" where @@ -255,8 +258,9 @@ | "succ m n \ succ (Suc m) (Suc n)" code_pred succ . - +code_pred [rpred] succ . thm succ.equation +thm succ.rpred_equation values 10 "{(m, n). succ n m}" values "{m. succ 0 m}" @@ -378,13 +382,36 @@ code_pred (inductify_all) (rpred) filterP . thm filterP.rpred_equation *) - +thm lexord_def code_pred [inductify] lexord . +code_pred [inductify, rpred] lexord . +thm lexord.equation +inductive less_than_nat :: "nat * nat => bool" +where + "less_than_nat (0, x)" +| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)" + +code_pred less_than_nat . +code_pred [depth_limited] less_than_nat . +code_pred [rpred] less_than_nat . -thm lexord.equation +inductive test_lexord :: "nat list * nat list => bool" +where + "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)" + +code_pred [rpred] test_lexord . +code_pred [depth_limited] test_lexord . +thm test_lexord.depth_limited_equation +thm test_lexord.rpred_equation + +values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" + +values [depth_limit = 25 random] "{xys. test_lexord xys}" + +values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}" lemma "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" -(*quickcheck[generator=pred_compile]*) +quickcheck[generator=pred_compile] oops lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv @@ -415,16 +442,19 @@ "avl ET = True" "avl (MKT x l r h) = ((height l = height r \ height l = 1 + height r \ height r = 1+height l) \ h = max (height l) (height r) + 1 \ avl l \ avl r)" - +(* code_pred [inductify] avl . thm avl.equation - +*) +code_pred [inductify, rpred] avl . +find_theorems "avl_aux" +thm avl.rpred_equation +values [depth_limit = 50 random] 10 "{t. avl (t::int tree)}" fun set_of where "set_of ET = {}" | "set_of (MKT n l r h) = insert n (set_of l \ set_of r)" - fun is_ord :: "nat tree => bool" where "is_ord ET = True" @@ -453,6 +483,10 @@ code_pred [inductify] length . thm size_listP.equation +code_pred [inductify, rpred] length . +thm size_listP.rpred_equation +values [depth_limit = 10 random] 20 "{xs. size_listP (xs::nat list) (5::nat)}" + code_pred [inductify] concat . thm concatP.equation @@ -473,17 +507,20 @@ code_pred [inductify] replicate . code_pred [inductify] splice . code_pred [inductify] List.rev . -thm map.simps code_pred [inductify] map . code_pred [inductify] foldr . code_pred [inductify] foldl . code_pred [inductify] filter . - +(* +code_pred [inductify, rpred] filter . +thm filterP.equation +*) definition test where "test xs = filter (\x. x = (1::nat)) xs" -(* -TODO: implement higher-order replacement correctly + +(* TODO: implement higher-order replacement correctly *) code_pred [inductify] test . thm testP.equation +(* code_pred [inductify, rpred] test . *) section {* Handling set operations *} @@ -502,15 +539,19 @@ | "w \ S\<^isub>1 \ b # w \ S\<^isub>1" | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" -code_pred [inductify] S\<^isub>1p . +code_pred [inductify, rpred] S\<^isub>1p . thm S\<^isub>1p.equation -(* +thm S\<^isub>1p.rpred_equation + +values [depth_limit = 5 random] "{x. S\<^isub>1p x}" + + theorem S\<^isub>1_sound: "w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=pred_compile] +(*quickcheck[generator=pred_compile]*) oops -*) + inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where "[] \ S\<^isub>2" | "w \ A\<^isub>2 \ b # w \ S\<^isub>2" @@ -518,12 +559,14 @@ | "w \ S\<^isub>2 \ a # w \ A\<^isub>2" | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" -(* + code_pred [inductify, rpred] S\<^isub>2 . thm S\<^isub>2.rpred_equation thm A\<^isub>2.rpred_equation thm B\<^isub>2.rpred_equation -*) + +values [depth_limit = 10 random] "{x. S\<^isub>2 x}" + theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" (*quickcheck[generator=SML]*) @@ -539,6 +582,9 @@ | "\v \ B\<^isub>3; w \ B\<^isub>3\ \ a # v @ w \ B\<^isub>3" code_pred [inductify] S\<^isub>3 . +thm S\<^isub>3.equation + +values 10 "{x. S\<^isub>3 x}" theorem S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" @@ -564,6 +610,7 @@ quickcheck[generator=pred_compile, size=10, iterations=100] oops *) + inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where "[] \ S\<^isub>4" | "w \ A\<^isub>4 \ b # w \ S\<^isub>4" diff -r 0d16c07f8d24 -r e2e23987c59a src/HOL/ex/RPred.thy --- a/src/HOL/ex/RPred.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/RPred.thy Sat Oct 24 16:55:42 2009 +0200 @@ -33,9 +33,9 @@ (* Missing a good definition for negation: not_rpred *) -definition not_rpred :: "unit Predicate.pred \ unit rpred" +definition not_rpred :: "unit rpred \ unit rpred" where - "not_rpred = Pair o Predicate.not_pred" + "not_rpred P = (\s. let (P', s') = P s in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" definition lift_pred :: "'a Predicate.pred \ 'a rpred" where