cleaned up

--- a/src/HOL/ex/Predicate_Compile.thy	Thu Jul 30 13:52:17 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Thu Jul 30 13:52:18 2009 +0200
@@ -1,61 +1,8 @@
 theory Predicate_Compile
-imports Complex_Main Lattice_Syntax Code_Eval
+imports Complex_Main
 uses "predicate_compile.ML"
 begin
 
-text {* Package setup *}
-
 setup {* Predicate_Compile.setup *}
 
-text {* Experimental code *}
-
-ML {*
-structure Predicate_Compile =
-struct
-
-open Predicate_Compile;
-
-fun eval thy t_compr =
-  let
-    val t = Predicate_Compile.analyze_compr thy t_compr;
-    val Type (@{type_name Predicate.pred}, [T]) = fastype_of t;
-    fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
-    val T1 = T --> @{typ term};
-    val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
-    val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
-      $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
-  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
-
-fun values ctxt k t_compr =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val (T, t') = eval thy t_compr;
-  in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end;
-
-fun values_cmd modes k raw_t state =
-  let
-    val ctxt = Toplevel.context_of state;
-    val t = Syntax.read_term ctxt raw_t;
-    val t' = values ctxt k t;
-    val ty' = Term.type_of t';
-    val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
-      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
-  in Pretty.writeln p end;
-
-end;
-
-local structure P = OuterParse in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_modes -- Scan.optional P.nat ~1 -- P.term
-    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
-        (Predicate_Compile.values_cmd modes k t)));
-
-end;
-*}
-
 end
\ No newline at end of file

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jul 30 13:52:17 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jul 30 13:52:18 2009 +0200
@@ -17,17 +17,11 @@
 values 10 "{n. even n}"
 values 10 "{n. odd n}"
 
-
 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
-    append_Nil: "append [] xs xs"
-  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
+    "append [] xs xs"
+  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
-inductive rev
-where
-"rev [] []"
-| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-
-code_pred rev .
+code_pred append .
 
 thm append.equation
 
@@ -35,6 +29,16 @@
 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]}"
 
+inductive rev where
+    "rev [] []"
+  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
+
+code_pred rev .
+
+thm rev.equation
+
+values "{xs. rev [0, 1, 2, 3::nat] xs}"
+values "Collect (rev [0, 1, 2, 3::nat])"
 
 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   for f where
@@ -57,9 +61,9 @@
 
 
 lemma [code_pred_intros]:
-"r a b ==> tranclp r a b"
-"r a b ==> tranclp r b c ==> tranclp r a c"
-by auto
+  "r a b \<Longrightarrow> tranclp r a b"
+  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
+  by auto
 
 (* Setup requires quick and dirty proof *)
 (*
@@ -71,6 +75,7 @@
 
 thm tranclp.equation
 *)
+
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
@@ -78,6 +83,11 @@
 code_pred succ .
 
 thm succ.equation
+
+values 10 "{(m, n). succ n m}"
+values "{m. succ 0 m}"
+values "{m. succ m 0}"
+
 (* FIXME: why does this not terminate? *)
 (*
 values 20 "{n. tranclp succ 10 n}"