reinvestigating the compilation of the random computation in the predicate compiler
--- 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')
--- 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 ([], [])
--- 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
--- 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 \<times> 'a list \<times> 'a list \<Rightarrow> bool"
where
"tupled_append ([], xs, xs)"
| "tupled_append (xs, ys, zs) \<Longrightarrow> 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 \<times> 'a list \<times> 'a list \<Rightarrow> bool"
where
"tupled_append'' ([], xs, xs)"
-| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, x # zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
+| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> 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 \<times> 'a list \<times> 'a list \<Rightarrow> bool"
where
@@ -255,8 +258,9 @@
| "succ m n \<Longrightarrow> 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 \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
h = max (height l) (height r) + 1 \<and> avl l \<and> 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 \<union> 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 (\<lambda>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 \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> 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 \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> 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
"[] \<in> S\<^isub>2"
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
@@ -518,12 +559,14 @@
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> 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 \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
(*quickcheck[generator=SML]*)
@@ -539,6 +582,9 @@
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> 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 \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> 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
"[] \<in> S\<^isub>4"
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
--- 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 \<Rightarrow> unit rpred"
+definition not_rpred :: "unit rpred \<Rightarrow> unit rpred"
where
- "not_rpred = Pair o Predicate.not_pred"
+ "not_rpred P = (\<lambda>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 \<Rightarrow> 'a rpred"
where