added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -209,9 +209,11 @@
   let
     fun is_nondefining_constname c = member (op =) logic_operator_names c
     val is_defining_constname = member (op =) (Symtab.keys table)
+    fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c)
     fun defiants_of specs =
       fold (Term.add_const_names o prop_of) specs []
       |> filter is_defining_constname
+      |> filter_out has_code_pred_intros
       |> filter_out (case_consts thy)
       |> filter_out special_cases
     fun extend constname =

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -15,7 +15,7 @@
 structure Pred_Compile_Set : PRED_COMPILE_SET =
 struct
 (*FIXME: unfolding Ball in pretty adhoc here *)
-val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}]
+val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}, @{thm Bex_def}]
 
 val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
 

--- 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
@@ -993,7 +993,7 @@
             (modes_of_term modes t handle Option =>
                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
       | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
-            length us = length is andalso
+        is = map (rpair NONE) (1 upto length us) andalso
             terms_vs us subset vs andalso
             term_vs t subset vs)
             (modes_of_term modes t handle Option =>
@@ -2135,8 +2135,8 @@
     
 fun prepare_intrs thy prednames intros =
   let
-    val intrs = intros
-      |> map (Logic.unvarify o prop_of)
+    val ((_, intrs), _) = Variable.import false intros (ProofContext.init thy)
+    val intrs = map prop_of intrs
     val nparams = nparams_of thy (hd prednames)
     val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
     val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs)

--- a/src/HOL/ex/Predicate_Compile.thy	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Sat Oct 24 16:55:42 2009 +0200
@@ -14,4 +14,50 @@
 setup {* Predicate_Compile.setup *}
 setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *}
 
+section {* Alternative rules for set *}
+
+lemma set_ConsI1 [code_pred_intros]:
+  "set (x # xs) x"
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+lemma set_ConsI2 [code_pred_intros]:
+  "set xs x ==> set (x' # xs) x" 
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+code_pred set
+proof -
+  case set
+  from this show thesis
+    apply (case_tac a1)
+    apply auto
+    unfolding mem_def[symmetric, of _ a2]
+    apply auto
+    unfolding mem_def
+    apply auto
+    done
+qed
+
+section {* Alternative rules for list_all2 *}
+
+lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []"
+by auto
+
+lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
+by auto
+
+code_pred list_all2
+proof -
+  case list_all2
+  from this show thesis
+    apply -
+    apply (case_tac a1)
+    apply (case_tac a2)
+    apply auto
+    apply (case_tac a2)
+    apply auto
+    done
+qed
+
 end
\ No newline at end of file

--- 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
@@ -34,6 +34,8 @@
 value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
 value [code] "Predicate.the (append_3 ([]::int list))"
 
+subsection {* Tricky cases with tuples *}
+
 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
 where
   "tupled_append ([], xs, xs)"
@@ -43,8 +45,40 @@
 
 thm tupled_append.equation
 (*
+TODO: values with tupled modes
 values "{xs. tupled_append ([1,2,3], [4,5], xs)}"
 *)
+
+inductive tupled_append'
+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)"
+
+code_pred tupled_append' .
+thm tupled_append'.equation
+(* TODO: Missing a few modes! *)
+
+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)"
+
+code_pred tupled_append'' .
+thm tupled_append''.equation
+(* TODO: Missing a few modes *)
+
+inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
+where
+  "tupled_append''' ([], xs, xs)"
+| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
+
+code_pred tupled_append''' .
+thm tupled_append'''.equation
+(* TODO: Missing a few modes *)
+
+section {* reverse *}
+
 inductive rev where
     "rev [] []"
   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
@@ -142,6 +176,8 @@
 values 20 "{(n, m). tranclp succ n m}"
 *)
 
+subsection{* *}
+
 subsection{* IMP *}
 
 types