1.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Aug 04 01:01:23 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Aug 04 08:34:56 2009 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val to_set_att: thm list -> attribute
     1.6    val to_pred_att: thm list -> attribute
     1.7 +  val to_pred : thm list -> Context.generic -> thm -> thm
     1.8    val pred_set_conv_att: attribute
     1.9    val add_inductive_i:
    1.10      Inductive.inductive_flags ->

     2.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Aug 04 01:01:23 2009 +0200
     2.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    val predfun_name_of: theory -> string -> mode -> string
     2.5    val all_preds_of : theory -> string list
     2.6    val modes_of: theory -> string -> mode list
     2.7 +  val string_of_mode : mode -> string
     2.8    val intros_of: theory -> string -> thm list
     2.9    val nparams_of: theory -> string -> int
    2.10    val add_intro: thm -> theory -> theory
    2.11 @@ -25,12 +26,17 @@
    2.12    val code_pred: string -> Proof.context -> Proof.state
    2.13    val code_pred_cmd: string -> Proof.context -> Proof.state
    2.14    val print_stored_rules: theory -> unit
    2.15 +  val print_all_modes: theory -> unit
    2.16    val do_proofs: bool ref
    2.17    val mk_casesrule : Proof.context -> int -> thm list -> term
    2.18    val analyze_compr: theory -> term -> term
    2.19    val eval_ref: (unit -> term Predicate.pred) option ref
    2.20    val add_equations : string -> theory -> theory
    2.21    val code_pred_intros_attrib : attribute
    2.22 +  (* used by Quickcheck_Generator *) 
    2.23 +  val funT_of : mode -> typ -> typ
    2.24 +  val mk_if_pred : term -> term
    2.25 +  val mk_Eval : term * term -> term
    2.26  end;
    2.27  
    2.28  structure Predicate_Compile : PREDICATE_COMPILE =
    2.29 @@ -43,8 +49,7 @@
    2.30  fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
    2.31  
    2.32  fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);
    2.33 -fun new_print_tac s = Tactical.print_tac s
    2.34 -fun debug_tac msg = (fn st => (Output.tracing msg; Seq.single st));
    2.35 +fun debug_tac msg = (fn st => (tracing msg; Seq.single st));
    2.36  
    2.37  val do_proofs = ref true;
    2.38  
    2.39 @@ -113,7 +118,7 @@
    2.40  
    2.41  val mk_sup = HOLogic.mk_binop @{const_name sup};
    2.42  
    2.43 -fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred},
    2.44 +fun mk_if_pred cond = Const (@{const_name Predicate.if_pred},
    2.45    HOLogic.boolT --> mk_pred_enumT HOLogic.unitT) $ cond;
    2.46  
    2.47  fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT
    2.48 @@ -248,6 +253,18 @@
    2.49      fold print preds ()
    2.50    end;
    2.51  
    2.52 +fun print_all_modes thy =
    2.53 +  let
    2.54 +    val _ = writeln ("Inferred modes:")
    2.55 +    fun print (pred, modes) u =
    2.56 +      let
    2.57 +        val _ = writeln ("predicate: " ^ pred)
    2.58 +        val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
    2.59 +      in u end  
    2.60 +  in
    2.61 +    fold print (all_modes_of thy) ()
    2.62 +  end
    2.63 +
    2.64  (** preprocessing rules **)  
    2.65  
    2.66  fun imp_prems_conv cv ct =
    2.67 @@ -465,12 +482,13 @@
    2.68            end
    2.69          end)) (AList.lookup op = modes name)
    2.70  
    2.71 -  in (case strip_comb t of
    2.72 +  in
    2.73 +    case strip_comb (Envir.eta_contract t) of
    2.74        (Const (name, _), args) => the_default default (mk_modes name args)
    2.75      | (Var ((name, _), _), args) => the (mk_modes name args)
    2.76      | (Free (name, _), args) => the (mk_modes name args)
    2.77 -    | (Abs _, []) => modes_of_param default modes t 
    2.78 -    | _ => default)
    2.79 +    | (Abs _, []) => error "Abs at param position" (* modes_of_param default modes t *)
    2.80 +    | _ => default
    2.81    end
    2.82  
    2.83  datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term;
    2.84 @@ -529,7 +547,7 @@
    2.85    in (p, List.filter (fn m => case find_index
    2.86      (not o check_mode_clause thy param_vs modes m) rs of
    2.87        ~1 => true
    2.88 -    | i => (tracing ("Clause " ^ string_of_int (i+1) ^ " of " ^
    2.89 +    | i => (Output.tracing ("Clause " ^ string_of_int (i+1) ^ " of " ^
    2.90        p ^ " violates mode " ^ string_of_mode m); false)) ms)
    2.91    end;
    2.92  
    2.93 @@ -547,18 +565,18 @@
    2.94  
    2.95  (* term construction *)
    2.96  
    2.97 -(* for simple modes (e.g. parameters) only: better call it param_funT *)
    2.98 -(* or even better: remove it and only use funT'_of - some modifications to funT'_of necessary *) 
    2.99 -fun funT_of T NONE = T
   2.100 -  | funT_of T (SOME mode) = let
   2.101 +(* Remark: types of param_funT_of and funT_of are swapped - which is the more
   2.102 +canonical order? *)
   2.103 +fun param_funT_of T NONE = T
   2.104 +  | param_funT_of T (SOME mode) = let
   2.105       val Ts = binder_types T;
   2.106       val (Us1, Us2) = get_args mode Ts
   2.107     in Us1 ---> (mk_pred_enumT (mk_tupleT Us2)) end;
   2.108  
   2.109 -fun funT'_of (iss, is) T = let
   2.110 +fun funT_of (iss, is) T = let
   2.111      val Ts = binder_types T
   2.112      val (paramTs, argTs) = chop (length iss) Ts
   2.113 -    val paramTs' = map2 (fn SOME is => funT'_of ([], is) | NONE => I) iss paramTs 
   2.114 +    val paramTs' = map2 (fn SOME is => funT_of ([], is) | NONE => I) iss paramTs 
   2.115      val (inargTs, outargTs) = get_args is argTs
   2.116    in
   2.117      (paramTs' @ inargTs) ---> (mk_pred_enumT (mk_tupleT outargTs))
   2.118 @@ -636,9 +654,9 @@
   2.119          val f' = case f of
   2.120              Const (name, T) =>
   2.121                if AList.defined op = modes name then
   2.122 -                Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
   2.123 +                Const (predfun_name_of thy name (iss, is'), funT_of (iss, is') T)
   2.124                else error "compile param: Not an inductive predicate with correct mode"
   2.125 -          | Free (name, T) => Free (name, funT_of T (SOME is'))
   2.126 +          | Free (name, T) => Free (name, param_funT_of T (SOME is'))
   2.127          val outTs = dest_tupleT (dest_pred_enumT (body_type (fastype_of f')))
   2.128          val out_vs = map Free (out_names ~~ outTs)
   2.129          val params' = map (compile_param thy modes) (ms ~~ params)
   2.130 @@ -662,9 +680,9 @@
   2.131       val f' = case f of
   2.132          Const (name, T) =>
   2.133            if AList.defined op = modes name then
   2.134 -             Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
   2.135 +             Const (predfun_name_of thy name (iss, is'), funT_of (iss, is') T)
   2.136            else error "compile param: Not an inductive predicate with correct mode"
   2.137 -      | Free (name, T) => Free (name, funT_of T (SOME is'))
   2.138 +      | Free (name, T) => Free (name, param_funT_of T (SOME is'))
   2.139     in list_comb (f', params' @ args') end
   2.140   | compile_param _ _ _ = error "compile params"
   2.141    
   2.142 @@ -684,7 +702,7 @@
   2.143         | (Free (name, T), args) =>
   2.144           (*if name mem param_vs then *)
   2.145           (* Higher order mode call *)
   2.146 -         let val r = Free (name, funT_of T (SOME is))
   2.147 +         let val r = Free (name, param_funT_of T (SOME is))
   2.148           in list_comb (r, args) end)
   2.149    | compile_expr _ _ _ = error "not a valid inductive expression"
   2.150  
   2.151 @@ -746,7 +764,7 @@
   2.152                   let
   2.153                     val rest = compile_prems [] vs' names'' ps';
   2.154                   in
   2.155 -                   (mk_if_predenum t, rest)
   2.156 +                   (mk_if_pred t, rest)
   2.157                   end
   2.158            in
   2.159              compile_match thy constr_vs' eqs out_ts'' 
   2.160 @@ -761,7 +779,7 @@
   2.161    let
   2.162      val Ts = binder_types T;
   2.163      val (Ts1, Ts2) = chop (length param_vs) Ts;
   2.164 -    val Ts1' = map2 funT_of Ts1 (fst mode)
   2.165 +    val Ts1' = map2 param_funT_of Ts1 (fst mode)
   2.166      val (Us1, Us2) = get_args (snd mode) Ts2;
   2.167      val xnames = Name.variant_list param_vs
   2.168        (map (fn i => "x" ^ string_of_int i) (snd mode));
   2.169 @@ -817,7 +835,7 @@
   2.170    val argnames = Name.variant_list []
   2.171          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   2.172    val (Ts1, Ts2) = chop nparams Ts;
   2.173 -  val Ts1' = map2 funT_of Ts1 (fst mode)
   2.174 +  val Ts1' = map2 param_funT_of Ts1 (fst mode)
   2.175    val args = map Free (argnames ~~ (Ts1' @ Ts2))
   2.176    val (params, io_args) = chop nparams args
   2.177    val (inargs, outargs) = get_args (snd mode) io_args
   2.178 @@ -834,7 +852,7 @@
   2.179    val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
   2.180                     mk_tuple outargs))
   2.181    val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   2.182 -  val _ = Output.tracing (Syntax.string_of_term_global thy introtrm) 
   2.183 +  val _ = tracing (Syntax.string_of_term_global thy introtrm) 
   2.184    val simprules = [defthm, @{thm eval_pred},
   2.185                     @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}]
   2.186    val unfolddef_tac = (Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1)
   2.187 @@ -860,7 +878,7 @@
   2.188          ^ (string_of_mode (snd mode))
   2.189        val Ts = binder_types T;
   2.190        val (Ts1, Ts2) = chop nparams Ts;
   2.191 -      val Ts1' = map2 funT_of Ts1 (fst mode)
   2.192 +      val Ts1' = map2 param_funT_of Ts1 (fst mode)
   2.193        val (Us1, Us2) = get_args (snd mode) Ts2;
   2.194        val names = Name.variant_list []
   2.195          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   2.196 @@ -921,12 +939,12 @@
   2.197    REPEAT_DETERM (etac @{thm thin_rl} 1)
   2.198    THEN REPEAT_DETERM (rtac @{thm ext} 1)
   2.199    THEN (rtac @{thm iffI} 1)
   2.200 -  THEN new_print_tac "prove_param"
   2.201 +  THEN print_tac "prove_param"
   2.202    (* proof in one direction *)
   2.203    THEN (atac 1)
   2.204    (* proof in the other direction *)
   2.205    THEN (atac 1)
   2.206 -  THEN new_print_tac "after prove_param"
   2.207 +  THEN print_tac "after prove_param"
   2.208  (*  let
   2.209      val  (f, args) = strip_comb t
   2.210      val (params, _) = chop (length ms) args
   2.211 @@ -964,10 +982,10 @@
   2.212          (* for the right assumption in first position *)
   2.213          THEN rotate_tac premposition 1
   2.214          THEN rtac introrule 1
   2.215 -        THEN new_print_tac "after intro rule"
   2.216 +        THEN print_tac "after intro rule"
   2.217          (* work with parameter arguments *)
   2.218          THEN (atac 1)
   2.219 -        THEN (new_print_tac "parameter goal")
   2.220 +        THEN (print_tac "parameter goal")
   2.221          THEN (EVERY (map (prove_param thy modes) (ms ~~ args1)))
   2.222          THEN (REPEAT_DETERM (atac 1)) end)
   2.223        else error "Prove expr if case not implemented"
   2.224 @@ -1110,7 +1128,7 @@
   2.225           (fn i => EVERY' (select_sup (length clauses) i) i) 
   2.226             (1 upto (length clauses))))
   2.227    THEN (EVERY (map (prove_clause thy nargs all_vs param_vs modes mode) clauses))
   2.228 -  THEN new_print_tac "proved one direction"
   2.229 +  THEN print_tac "proved one direction"
   2.230  end;
   2.231  
   2.232  (*******************************************************************************************************)
   2.233 @@ -1168,15 +1186,15 @@
   2.234        if AList.defined op = modes name then
   2.235          etac @{thm bindE} 1
   2.236          THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
   2.237 -        THEN new_print_tac "prove_expr2-before"
   2.238 +        THEN print_tac "prove_expr2-before"
   2.239          THEN (debug_tac (Syntax.string_of_term_global thy
   2.240            (prop_of (predfun_elim_of thy name mode))))
   2.241          THEN (etac (predfun_elim_of thy name mode) 1)
   2.242 -        THEN new_print_tac "prove_expr2"
   2.243 +        THEN print_tac "prove_expr2"
   2.244          (* TODO -- FIXME: replace remove_last_goal*)
   2.245          (* THEN (EVERY (replicate (length args) (remove_last_goal thy))) *)
   2.246          THEN (EVERY (map (prove_param thy modes) (ms ~~ args)))
   2.247 -        THEN new_print_tac "finished prove_expr2"
   2.248 +        THEN print_tac "finished prove_expr2"
   2.249        
   2.250        else error "Prove expr2 if case not implemented"
   2.251      | _ => etac @{thm bindE} 1)
   2.252 @@ -1273,7 +1291,7 @@
   2.253      end;
   2.254    val prems_tac = prove_prems2 in_ts' param_vs ps 
   2.255  in
   2.256 -  new_print_tac "starting prove_clause2"
   2.257 +  print_tac "starting prove_clause2"
   2.258    THEN etac @{thm bindE} 1
   2.259    THEN (etac @{thm singleE'} 1)
   2.260    THEN (TRY (etac @{thm Pair_inject} 1))
   2.261 @@ -1401,10 +1419,10 @@
   2.262    val clauses' = map (fn (s, cls) => (s, (the (AList.lookup (op =) preds s), cls))) clauses
   2.263    val _ = tracing "Compiling equations..."
   2.264    val ts = compile_preds thy' all_vs param_vs (extra_modes @ modes) clauses'
   2.265 -  val _ = map (Output.tracing o (Syntax.string_of_term_global thy')) (flat ts)
   2.266 +(*  val _ = map (tracing o (Syntax.string_of_term_global thy')) (flat ts) *)
   2.267    val pred_mode =
   2.268      maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses' 
   2.269 -  val _ = Output.tracing "Proving equations..."
   2.270 +  val _ = tracing "Proving equations..."
   2.271    val result_thms =
   2.272      prove_preds thy' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
   2.273    val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
   2.274 @@ -1486,7 +1504,6 @@
   2.275          assumes = [("", Logic.strip_imp_prems case_rule)],
   2.276          binds = [], cases = []}) cases_rules
   2.277      val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
   2.278 -    val _ = Output.tracing (commas (map fst case_env))
   2.279      val lthy'' = ProofContext.add_cases true case_env lthy'
   2.280      
   2.281      fun after_qed thms =