merged

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 02 09:01:18 2009 +0100
@@ -18,8 +18,6 @@
 
 open Predicate_Compile_Aux;
 
-val priority = tracing;
-
 (* Some last processing *)
 
 fun remove_pointless_clauses intro =
@@ -27,14 +25,12 @@
     []
   else [intro]
 
-fun tracing s = ()
-
 fun print_intross options thy msg intross =
   if show_intermediate_results options then
-   Output.tracing (msg ^ 
-    (space_implode "\n" (map 
-      (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
-         commas (map (Display.string_of_thm_global thy) intros)) intross)))
+    tracing (msg ^ 
+      (space_implode "\n" (map 
+        (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
+           commas (map (Display.string_of_thm_global thy) intros)) intross)))
   else ()
       
 fun print_specs thy specs =
@@ -122,7 +118,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 +147,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	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Nov 02 09:01:18 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	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Nov 02 09:01:18 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 =
@@ -2020,6 +2018,8 @@
   map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
     compiled_terms
 
+(* preparation of introduction rules into special datastructures *)
+
 fun dest_prem thy params t =
   (case strip_comb t of
     (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
@@ -2093,6 +2093,8 @@
     val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds
   in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
 
+(* sanity check of introduction rules *)
+
 fun check_format_of_intro_rule thy intro =
   let
     val concl = Logic.strip_imp_concl (prop_of intro)
@@ -2134,6 +2136,40 @@
   in forall check prednames end
 *)
 
+(* create code equation *)
+
+fun add_code_equations thy nparams preds result_thmss =
+  let
+    fun add_code_equation ((predname, T), (pred, result_thms)) =
+      let
+        val full_mode = (replicate nparams NONE,
+          map (rpair NONE) (1 upto (length (binder_types T) - nparams)))
+      in
+        if member (op =) (modes_of thy predname) full_mode then
+          let
+            val Ts = binder_types T
+            val arg_names = Name.variant_list []
+              (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
+            val args = map Free (arg_names ~~ Ts)
+            val predfun = Const (predfun_name_of thy predname full_mode,
+              Ts ---> PredicateCompFuns.mk_predT @{typ unit})
+            val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"})
+            val eq_term = HOLogic.mk_Trueprop
+              (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
+            val def = predfun_definition_of thy predname full_mode
+            val tac = fn {...} => Simplifier.simp_tac
+              (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
+            val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
+          in
+            (pred, result_thms @ [eq])
+          end
+        else
+          (pred, result_thms)
+      end
+  in
+    map add_code_equation (preds ~~ result_thmss)
+  end
+
 (** main function of predicate compiler **)
 
 datatype steps = Steps of
@@ -2147,6 +2183,8 @@
   prove : options -> theory -> (string * (term list * indprem list) list) list
     -> (string * typ) list -> (string * mode list) list
     -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
+  add_code_equations : theory -> int -> (string * typ) list
+    -> (string * thm list) list -> (string * thm list) list,
   are_not_defined : theory -> string list -> bool,
   qname : bstring
   }
@@ -2176,14 +2214,15 @@
     val _ = print_step options "Proving equations..."
     val result_thms = #prove (dest_steps steps) options thy' clauses preds (extra_modes @ modes)
       moded_clauses compiled_terms
+    val result_thms' = #add_code_equations (dest_steps steps) thy' nparams preds
+      (maps_modes result_thms)
     val qname = #qname (dest_steps steps)
     val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
       (fn thm => Context.mapping (Code.add_eqn thm) I))))
     val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
         [attrib thy ])] thy))
-      (maps_modes result_thms) thy'
-      |> Theory.checkpoint
+      result_thms' thy' |> Theory.checkpoint
   in
     thy''
   end
@@ -2260,7 +2299,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})],
@@ -2274,6 +2313,7 @@
   create_definitions = create_definitions,
   compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove,
+  add_code_equations = add_code_equations,
   are_not_defined = fn thy => forall (null o modes_of thy),
   qname = "equation"})
 
@@ -2282,16 +2322,18 @@
   create_definitions = create_definitions_of_depth_limited_functions,
   compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove_by_skip,
+  add_code_equations = K (K (K I)),
   are_not_defined = fn thy => forall (null o depth_limited_modes_of thy),
   qname = "depth_limited_equation"})
 
 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"})
+  add_code_equations = K (K (K I)),
+  are_not_defined = fn thy => forall (null o random_modes_of thy),
+  qname = "random_equation"})
 
 (** user interface **)
 
@@ -2345,7 +2387,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 +2437,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_data.ML	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Nov 02 09:01:18 2009 +0100
@@ -126,8 +126,9 @@
   |> split_all_pairs thy
   |> tap check_equation_format
 
-fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
-((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
+fun inline_equations thy th = Conv.fconv_rule
+  (Simplifier.rewrite ((Simplifier.theory_context thy Simplifier.empty_ss)
+    addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
 
 fun store_thm_in_table ignore_consts thy th=
   let

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 02 09:01:18 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	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Nov 02 09:01:18 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	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy	Mon Nov 02 09:01:18 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	Sun Nov 01 21:42:27 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Mon Nov 02 09:01:18 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}"