added skip_proof option; playing with compilation of depth-limited predicates

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -138,6 +138,8 @@
   show_mode_inference : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
+  show_compilation : bool,
+  skip_proof : bool,
 
   inductify : bool,
   rpred : bool,
@@ -149,6 +151,8 @@
 fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
 fun show_proof_trace (Options opt) = #show_proof_trace opt
+fun show_compilation (Options opt) = #show_compilation opt
+fun skip_proof (Options opt) = #skip_proof opt
 
 fun is_inductify (Options opt) = #inductify opt
 fun is_rpred (Options opt) = #rpred opt
@@ -160,6 +164,9 @@
   show_intermediate_results = false,
   show_proof_trace = false,
   show_mode_inference = false,
+  show_compilation = false,
+  skip_proof = false,
+  
   inductify = false,
   rpred = false,
   depth_limited = false
@@ -169,7 +176,6 @@
 fun print_step options s =
   if show_steps options then tracing s else ()
 
-
 (* tuple processing *)
 
 fun expand_tuples thy intro =

--- 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
@@ -65,7 +65,7 @@
       |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
       |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
       |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]
-      |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]
+      (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
       |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname]
     val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
     val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -11,7 +11,7 @@
 struct
 
 (* options *)
-val fail_safe_mode = false
+val fail_safe_mode = true
 
 open Predicate_Compile_Aux;
 
@@ -111,6 +111,8 @@
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
       show_mode_inference = chk "show_mode_inference",
+      show_compilation = chk "show_compilation",
+      skip_proof = chk "skip_proof",
       inductify = chk "inductify",
       rpred = chk "rpred",
       depth_limited = chk "depth_limited"
@@ -141,7 +143,7 @@
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
-  "show_mode_inference", "inductify", "rpred", "depth_limited"]
+  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"]
 
 val _ = List.app OuterKeyword.keyword ("mode" :: bool_options)
 

--- 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
@@ -73,10 +73,6 @@
   val rpred_create_definitions :(string * typ) list -> string * mode list
     -> theory -> theory 
   val split_smode : int list -> term list -> (term list * term list) *)
-  val print_moded_clauses :
-    theory -> (moded_clause list) pred_mode_table -> unit
-  val print_compiled_terms : theory -> term pred_mode_table -> unit
-  (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*)
   val pred_compfuns : compilation_funs
   val rpred_compfuns : compilation_funs
   val dest_funT : typ -> typ * typ
@@ -111,6 +107,7 @@
 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
 
 fun print_tac s = Seq.single;
+
 fun print_tac' options s = 
   if show_proof_trace options then Tactical.print_tac s else Seq.single;
 
@@ -438,9 +435,11 @@
   (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " "
    ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))
 
-fun print_compiled_terms thy =
-  print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
-    
+fun print_compiled_terms options thy =
+  if show_compilation options then
+    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
+  else K ()
+
 fun print_stored_rules thy =
   let
     val preds = (Graph.keys o PredData.get) thy
@@ -1294,8 +1293,6 @@
        let
          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
          (*lift_pred compfuns*)(list_comb (mk_fun_of compfuns thy (name, T) mode, params' @ inargs))
        end
@@ -1475,7 +1472,7 @@
     mk_bind compfuns (mk_single compfuns inp, prem_t)
   end
 
-fun compile_pred compfuns mk_fun_of depth_limited thy all_vs param_vs s T mode moded_cls =
+fun compile_pred compfuns mk_fun_of' depth_limited thy all_vs param_vs s T mode moded_cls =
   let
 	  val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
     val (Us1, Us2) = split_smodeT (snd mode) Ts2
@@ -1504,20 +1501,30 @@
       else
         NONE
     val cl_ts =
-      map (compile_clause compfuns mk_fun_of 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)
     val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
     val full_mode = null Us2
-    val depth_compilation = 
-      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
-      $ (if full_mode then 
-          if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') $ mk_single compfuns HOLogic.unit
-        else
-          mk_bot compfuns (dest_predT compfuns T'))
-      $ compilation
-    val fun_const = mk_fun_of compfuns thy (s, T) mode
+    val depth_compilation =
+      if full_mode then
+        if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+        $ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') $
+            mk_single compfuns HOLogic.unit)
+        $ compilation
+      else
+        let
+          val compilation_without_depth_limit = foldr1 (mk_sup compfuns)
+            (map (compile_clause compfuns mk_fun_of NONE
+               thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls)
+        in
+          if_const $ polarity $ 
+            (if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) $
+            mk_bot compfuns (dest_predT compfuns T') $ compilation)
+          $ compilation_without_depth_limit
+        end
+    val fun_const = mk_fun_of' compfuns thy (s, T) mode
     val eq = if depth_limited then
       (list_comb (fun_const, params @ in_ts @ [polarity, depth]), depth_compilation)
     else
@@ -1733,7 +1740,6 @@
     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
@@ -2121,7 +2127,7 @@
     val clauses = the (AList.lookup (op =) clauses pred)
   in
     Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
-      (if !do_proofs then
+      (if skip_proof options then
         (fn _ =>
         rtac @{thm pred_iffI} 1
 				THEN print_tac' options "after pred_iffI"
@@ -2284,14 +2290,14 @@
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes options modes
     val _ = print_modes modes
-    val _ = print_moded_clauses thy moded_clauses
+      (*val _ = print_moded_clauses thy moded_clauses*)
     val _ = print_step options "Defining executable functions..."
     val thy' = fold (#create_definitions steps preds) modes thy
       |> Theory.checkpoint
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
       (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
-    val _ = print_compiled_terms thy' compiled_terms
+    val _ = print_compiled_terms options thy' compiled_terms
     val _ = print_step options "Proving equations..."
     val result_thms = #prove steps options thy' clauses preds (extra_modes @ modes)
       moded_clauses compiled_terms

--- 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
@@ -409,15 +409,19 @@
 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"
+ML {* Predicate_Compile_Core.do_proofs := false *}
+lemma "(u, v) : lexord less_than_nat ==> (x @ u, y @ v) : lexord less_than_nat"
 quickcheck[generator=pred_compile]
 oops
 
 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
-
+(*
 code_pred [inductify] lexn .
 thm lexn.equation
+*)
+code_pred [inductify, rpred] lexn .
+
+thm lexn.rpred_equation
 
 code_pred [inductify] lenlex .
 thm lenlex.equation
@@ -447,9 +451,14 @@
 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)}"
+
+lemma "avl t ==> t = ET"
+quickcheck[generator=code]
+quickcheck[generator = pred_compile]
+oops
+
 fun set_of
 where
 "set_of ET = {}"
@@ -546,12 +555,73 @@
 
 values [depth_limit = 5 random] "{x. S\<^isub>1p x}"
 
+inductive is_a where
+"is_a a"
+
+inductive is_b where
+  "is_b b"
+
+code_pred is_a .
+code_pred [depth_limited] is_a .
+code_pred [rpred] is_a .
+
+values [depth_limit=5 random] "{x. is_a x}"
+code_pred [rpred] is_b .
+
+code_pred [rpred] filterP .
+values [depth_limit=5 random] "{x. filterP is_a [a, b] x}"
+values [depth_limit=3 random] "{x. filterP is_b [a, b] x}"
+
+lemma "w \<in> S\<^isub>1 \<Longrightarrow> length (filter (\<lambda>x. x = a) w) = 1"
+quickcheck[generator=pred_compile, size=10]
+oops
+
+inductive test_lemma where
+  "S\<^isub>1p w ==> filterP is_a w r1 ==> size_listP r1 r2 ==> filterP is_b w r3 ==> size_listP r3 r4 ==> r2 \<noteq> r4 ==> test_lemma w"
+
+code_pred [rpred] test_lemma .
+
+definition test_lemma' where
+  "test_lemma' w == (w \<in> S\<^isub>1 \<and> (\<not> length [x <- w. x = a] = length [x <- w. x = b]))"
+
+code_pred [inductify, rpred] test_lemma' .
+thm test_lemma'.rpred_equation
+(*thm test_lemma'.rpred_equation*)
+(*
+values [depth_limit=3 random] "{x. S\<^isub>1 x}"
+*)
+code_pred [depth_limited] is_b .
+code_pred [inductify, depth_limited] filter .
+thm  filterP.intros
+thm filterP.equation
+
+values [depth_limit=3] "{x. filterP is_b [a, b] x}"
+find_theorems "test_lemma'_hoaux"
+code_pred [depth_limited] test_lemma'_hoaux .
+thm test_lemma'_hoaux.depth_limited_equation
+values [depth_limit=2] "{x. test_lemma'_hoaux b}"
+inductive test1 where
+  "\<not> test_lemma'_hoaux x ==> test1 x"
+code_pred test1 .
+code_pred [depth_limited] test1 .
+thm test1.depth_limited_equation
+thm test_lemma'_hoaux.depth_limited_equation
+thm test1.intros
+
+values [depth_limit=2] "{x. test1 b}"
+
+thm filterP.intros
+thm filterP.depth_limited_equation
+values [depth_limit=3] "{x. filterP test_lemma'_hoaux [a, b] x}"
+values [depth_limit=4 random] "{w. test_lemma w}"
+values [depth_limit=4 random] "{w. test_lemma' w}"
 
 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]*)
+"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=pred_compile, size=5]
 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"
@@ -565,12 +635,12 @@
 thm A\<^isub>2.rpred_equation
 thm B\<^isub>2.rpred_equation
 
-values [depth_limit = 10 random] "{x. S\<^isub>2 x}"
+values [depth_limit = 4 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]*)
-(*quickcheck[generator=pred_compile, size=15, iterations=100]*)
+quickcheck[generator=pred_compile, size=4, iterations=1]
 oops
 
 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
@@ -588,7 +658,7 @@
 
 theorem S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-(*quickcheck[generator=pred_compile, size=10, iterations=1]*)
+quickcheck[generator=pred_compile, size=10, iterations=1]
 oops
 
 lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"