--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Oct 30 09:55:15 2009 +0100
@@ -122,7 +122,7 @@
show_compilation = chk "show_compilation",
skip_proof = chk "skip_proof",
inductify = chk "inductify",
- rpred = chk "rpred",
+ random = chk "random",
depth_limited = chk "depth_limited"
}
end
@@ -151,7 +151,7 @@
val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
- "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"]
+ "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited"]
local structure P = OuterParse
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Oct 30 09:55:15 2009 +0100
@@ -169,7 +169,7 @@
skip_proof : bool,
inductify : bool,
- rpred : bool,
+ random : bool,
depth_limited : bool
};
@@ -183,7 +183,7 @@
fun skip_proof (Options opt) = #skip_proof opt
fun is_inductify (Options opt) = #inductify opt
-fun is_rpred (Options opt) = #rpred opt
+fun is_random (Options opt) = #random opt
fun is_depth_limited (Options opt) = #depth_limited opt
val default_options = Options {
@@ -197,7 +197,7 @@
skip_proof = false,
inductify = false,
- rpred = false,
+ random = false,
depth_limited = false
}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Oct 30 09:55:15 2009 +0100
@@ -254,7 +254,7 @@
val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data
-val rpred_modes_of = (map fst) o #generators oo the_pred_data
+val random_modes_of = (map fst) o #generators oo the_pred_data
fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy)
@@ -302,8 +302,6 @@
val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
-(*val generator_modes_of = (map fst) o #generators oo the_pred_data*)
-
(* diagnostic display functions *)
fun print_modes options modes =
@@ -1586,7 +1584,7 @@
(mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
end
-fun rpred_create_definitions preds (name, modes) thy =
+fun random_create_definitions preds (name, modes) thy =
let
val T = AList.lookup (op =) preds name |> the
fun create_definition mode thy =
@@ -2260,7 +2258,7 @@
in [polarity', depth'] end
}
-val rpred_comp_modifiers = Comp_Mod.Comp_Modifiers
+val random_comp_modifiers = Comp_Mod.Comp_Modifiers
{const_name_of = generator_name_of,
funT_of = K generator_funT_of : (compilation_funs -> mode -> typ -> typ),
additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
@@ -2287,11 +2285,11 @@
val add_quickcheck_equations = gen_add_equations
(Steps {infer_modes = infer_modes_with_generator,
- create_definitions = rpred_create_definitions,
- compile_preds = compile_preds rpred_comp_modifiers RandomPredCompFuns.compfuns,
+ create_definitions = random_create_definitions,
+ compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns,
prove = prove_by_skip,
- are_not_defined = fn thy => forall (null o rpred_modes_of thy),
- qname = "rpred_equation"})
+ are_not_defined = fn thy => forall (null o random_modes_of thy),
+ qname = "random_equation"})
(** user interface **)
@@ -2345,7 +2343,7 @@
(ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
in
goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
- (if is_rpred options then
+ (if is_random options then
(add_equations options [const] #>
add_quickcheck_equations options [const])
else if is_depth_limited options then
@@ -2395,7 +2393,7 @@
| SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d]
val comp_modifiers =
case depth_limit of NONE =>
- (if random then rpred_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
+ (if random then random_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
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 comp_modifiers compfuns thy
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Oct 30 09:55:15 2009 +0100
@@ -144,8 +144,6 @@
val abs_args = filter is_Abs args
fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
let
- val _ = tracing ("Introduce new constant for " ^
- Syntax.string_of_term_global thy abs_arg)
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' [])
@@ -156,7 +154,6 @@
val const = Const (full_constname, constT)
val lhs = list_comb (const, frees)
val def = Logic.mk_equals (lhs, abs_arg')
- val _ = tracing (Syntax.string_of_term_global thy def)
val ([definition], thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
|> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 30 09:55:15 2009 +0100
@@ -32,7 +32,7 @@
skip_proof = false,
inductify = false,
- rpred = false,
+ random = false,
depth_limited = false
}
--- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Oct 30 09:55:15 2009 +0100
@@ -32,10 +32,10 @@
| "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
+code_pred [inductify, random] S\<^isub>2 .
+thm S\<^isub>2.random_equation
+thm A\<^isub>2.random_equation
+thm B\<^isub>2.random_equation
values [random] 10 "{x. S\<^isub>2 x}"
--- a/src/HOL/ex/Predicate_Compile_ex.thy Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Oct 30 09:55:15 2009 +0100
@@ -1,5 +1,5 @@
theory Predicate_Compile_ex
-imports "../Main" Predicate_Compile_Alternative_Defs
+imports Main Predicate_Compile_Alternative_Defs
begin
subsection {* Basic predicates *}
@@ -8,7 +8,7 @@
code_pred (mode : []) False' .
code_pred [depth_limited] False' .
-code_pred [rpred] False' .
+code_pred [random] False' .
inductive EmptySet :: "'a \<Rightarrow> bool"
@@ -67,7 +67,7 @@
"zerozero (0, 0)"
code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero .
-code_pred [rpred] zerozero .
+code_pred [random] zerozero .
subsection {* Alternative Rules *}
@@ -188,14 +188,14 @@
code_pred (mode: [], [1]) even .
code_pred [depth_limited] even .
-code_pred [rpred] even .
+code_pred [random] even .
thm odd.equation
thm even.equation
thm odd.depth_limited_equation
thm even.depth_limited_equation
-thm even.rpred_equation
-thm odd.rpred_equation
+thm even.random_equation
+thm odd.random_equation
values "{x. even 2}"
values "{x. odd 2}"
@@ -211,7 +211,7 @@
code_pred (mode: [1]) [inductify] odd' .
code_pred [inductify, depth_limited] odd' .
-code_pred [inductify, rpred] odd' .
+code_pred [inductify, random] odd' .
thm odd'.depth_limited_equation
values [depth_limit = 2] "{x. odd' 7}"
@@ -231,11 +231,11 @@
code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
code_pred [depth_limited] append .
-code_pred [rpred] append .
+code_pred [random] append .
thm append.equation
thm append.depth_limited_equation
-thm append.rpred_equation
+thm append.random_equation
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
@@ -279,7 +279,7 @@
| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append .
-code_pred [rpred] tupled_append .
+code_pred [random] tupled_append .
thm tupled_append.equation
(*
TODO: values with tupled modes
@@ -332,7 +332,7 @@
code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 .
code_pred [depth_limited] filter1 .
-code_pred [rpred] filter1 .
+code_pred [random] filter1 .
thm filter1.equation
@@ -344,9 +344,9 @@
code_pred (mode: [1, 2, 3], [1, 2]) filter2 .
code_pred [depth_limited] filter2 .
-code_pred [rpred] filter2 .
+code_pred [random] filter2 .
thm filter2.equation
-thm filter2.rpred_equation
+thm filter2.random_equation
inductive filter3
for P
@@ -363,7 +363,7 @@
code_pred (mode: [1, 2], [1, 2, 3]) filter4 .
code_pred [depth_limited] filter4 .
-code_pred [rpred] filter4 .
+code_pred [random] filter4 .
subsection {* reverse predicate *}
@@ -394,7 +394,7 @@
code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition .
code_pred [depth_limited] partition .
-code_pred [rpred] partition .
+code_pred [random] partition .
values 10 "{(ys, zs). partition is_even
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
@@ -425,18 +425,18 @@
qed
code_pred [depth_limited] tranclp .
-code_pred [rpred] tranclp .
+code_pred [random] tranclp .
thm tranclp.equation
-thm tranclp.rpred_equation
+thm tranclp.random_equation
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
code_pred succ .
-code_pred [rpred] succ .
+code_pred [random] succ .
thm succ.equation
-thm succ.rpred_equation
+thm succ.random_equation
values 10 "{(m, n). succ n m}"
values "{m. succ 0 m}"
@@ -549,9 +549,9 @@
subsection {* Lexicographic order *}
code_pred [inductify] lexord .
-code_pred [inductify, rpred] lexord .
+code_pred [inductify, random] lexord .
thm lexord.equation
-thm lexord.rpred_equation
+thm lexord.random_equation
inductive less_than_nat :: "nat * nat => bool"
where
@@ -561,16 +561,16 @@
code_pred less_than_nat .
code_pred [depth_limited] less_than_nat .
-code_pred [rpred] less_than_nat .
+code_pred [random] less_than_nat .
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 [random] test_lexord .
code_pred [depth_limited] test_lexord .
thm test_lexord.depth_limited_equation
-thm test_lexord.rpred_equation
+thm test_lexord.random_equation
values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
@@ -580,15 +580,15 @@
code_pred [inductify] lexn .
thm lexn.equation
-code_pred [rpred] lexn .
+code_pred [random] lexn .
-thm lexn.rpred_equation
+thm lexn.random_equation
-code_pred [inductify, show_steps] lenlex .
+code_pred [inductify] lenlex .
thm lenlex.equation
-code_pred [inductify, rpred] lenlex .
-thm lenlex.rpred_equation
+code_pred [inductify, random] lenlex .
+thm lenlex.random_equation
code_pred [inductify] lists .
thm lists.equation
@@ -609,8 +609,8 @@
code_pred [inductify] avl .
thm avl.equation
-code_pred [rpred] avl .
-thm avl.rpred_equation
+code_pred [random] avl .
+thm avl.random_equation
fun set_of
where
@@ -667,9 +667,9 @@
subsection {* Inverting list functions *}
code_pred [inductify] length .
-code_pred [inductify, rpred] length .
+code_pred [inductify, random] length .
thm size_listP.equation
-thm size_listP.rpred_equation
+thm size_listP.random_equation
values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}"
@@ -693,7 +693,7 @@
code_pred [inductify] foldr .
code_pred [inductify] foldl .
code_pred [inductify] filter .
-code_pred [inductify, rpred] filter .
+code_pred [inductify, random] filter .
subsection {* Context Free Grammar *}
@@ -708,9 +708,9 @@
| "\<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 .
+code_pred [inductify, random] S\<^isub>1p .
thm S\<^isub>1p.equation
-thm S\<^isub>1p.rpred_equation
+thm S\<^isub>1p.random_equation
values [random] 5 "{x. S\<^isub>1p x}"
@@ -722,10 +722,10 @@
| "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
+code_pred [inductify, random] S\<^isub>2 .
+thm S\<^isub>2.random_equation
+thm A\<^isub>2.random_equation
+thm B\<^isub>2.random_equation
values [random] 10 "{x. S\<^isub>2 x}"