changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned

--- a/src/HOL/MicroJava/J/Eval.thy	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Sat Oct 24 16:55:42 2009 +0200
@@ -40,7 +40,7 @@
           ("_ \<turnstile> _ -_[\<succ>]_-> _" [51,82,60,51,82] 81)
   and exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
           ("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
-  (*for G :: "java_mb prog"*)
+  for G :: "java_mb prog"
 where
 
   -- "evaluation of expressions"

--- 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
@@ -132,7 +132,7 @@
     val th = th
       |> inline_equations thy
       |> Pred_Compile_Set.unfold_set_notation
-      |> AxClass.unoverload thy
+      (*  |> AxClass.unoverload thy *)
     val (const, th) =
       if is_equationlike th then
         let

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -102,9 +102,11 @@
       (Free (Long_Name.base_name name ^ "P", pred_type T))
   end
 
-fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t
-  | mk_param lookup_pred t =
-  if Predicate_Compile_Aux.is_predT (fastype_of t) then
+fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
+  | mk_param thy lookup_pred t =
+  let
+  val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
+  in if Predicate_Compile_Aux.is_predT (fastype_of t) then
     t
   else
     let
@@ -116,11 +118,13 @@
       val (f, args) = strip_comb body'
       val resname = Name.variant (vs_names @ names) "res"
       val resvar = Free (resname, body_type (fastype_of body'))
-      val P = lookup_pred f
+      (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param"
       val pred_body = list_comb (P, args @ [resvar])
+      *)
+      val pred_body = HOLogic.mk_eq (body', resvar)
       val param = fold_rev lambda (vs' @ [resvar]) pred_body
-    in param end;
-
+    in param end
+  end
 (* creates the list of premises for every intro rule *)
 (* theory -> term -> (string list, term list list) *)
 
@@ -272,7 +276,7 @@
                   val pred = lookup_pred t
                   val nparams = get_nparams pred
                   val (params, args) = chop nparams args
-                  val params' = map (mk_param lookup_pred) params
+                  val params' = map (mk_param thy lookup_pred) params
                 in
                   folds_map mk_prems' args (names', prems)
                   |> map (fn (argvs, (names'', prems')) =>
@@ -318,16 +322,14 @@
     val funnames = map (fst o dest_Const) funs
     val fun_pred_names = (funnames ~~ prednames)  
       (* mapping from term (Free or Const) to term *)
-    fun lookup_pred (Const (@{const_name Cons}, T)) =
-      Const ("Preprocessing.ConsP", pred_type T) (* FIXME: temporary - Cons lookup *)
-      | lookup_pred (Const (name, T)) =
+    fun lookup_pred (Const (name, T)) =
       (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
           SOME c => Const (c, pred_type T)
         | NONE =>
           (case AList.lookup op = fun_pred_names name of
             SOME f => Free (f, pred_type T)
           | NONE => Const (name, T)))
-      | lookup_pred  (Free (name, T)) =
+      | lookup_pred (Free (name, T)) =
         if member op = (map fst pnames) name then
           Free (name, transform_ho_typ T)
         else

--- 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
@@ -44,7 +44,7 @@
       (fn th => if is_equationlike th then Pred_Compile_Data.normalize_equation thy' th else th))) specs
     val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy')
     val _ = print_intross options thy'' "Flattened introduction rules: " intross1
-    val _ =  "Replacing functions in introrules..."
+    val _ = print_step options "Replacing functions in introrules..."
     val intross2 =
       if fail_safe_mode then
         case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of

--- 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
@@ -259,82 +259,6 @@
   (if null param_modes then "" else
     "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
 
-fun unify_consts thy cs intr_ts =
-  (let
-     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
-     fun varify (t, (i, ts)) =
-       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t))
-       in (maxidx_of_term t', t'::ts) end;
-     val (i, cs') = foldr varify (~1, []) cs;
-     val (i', intr_ts') = foldr varify (i, []) intr_ts;
-     val rec_consts = fold add_term_consts_2 cs' [];
-     val intr_consts = fold add_term_consts_2 intr_ts' [];
-     fun unify (cname, cT) =
-       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
-       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
-     val (env, _) = fold unify rec_consts (Vartab.empty, i');
-     val subst = map_types (Envir.norm_type env)
-   in (map subst cs', map subst intr_ts')
-   end) handle Type.TUNIFY =>
-     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
-
-(* how to detect polymorphic type dependencies in mutual recursive inductive predicates? *)
-fun import_intros [] ctxt = ([], ctxt)
-  | import_intros (th :: ths) ctxt =
-    let
-      val ((_, [th']), ctxt') = Variable.import false [th] ctxt
-      val thy = ProofContext.theory_of ctxt'
-      val (pred, ([], args)) = strip_intro_concl 0 (prop_of th')
-      val ho_args = filter (is_predT o fastype_of) args
-      fun instantiate_typ th =
-        let
-          val (pred', _) = strip_intro_concl 0 (prop_of th)
-          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
-            error "Trying to instantiate another predicate" else ()
-          val subst = Sign.typ_match thy
-            (fastype_of pred', fastype_of pred) Vartab.empty
-          val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T))
-            (Vartab.dest subst)
-        in Thm.certify_instantiate (subst', []) th end;
-      fun instantiate_ho_args th =
-        let
-          val (_, (_, args')) = strip_intro_concl 0 (prop_of th)
-          val ho_args' = map dest_Var (filter (is_predT o fastype_of) args')
-        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
-      val ((_, ths'), ctxt1) =
-        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
-    in
-      (th' :: ths', ctxt1)
-    end
-
-
-(* generation of case rules from user-given introduction rules *)
-
-fun mk_casesrule ctxt nparams introrules =
-  let
-    val (intros_th, ctxt1) = import_intros introrules ctxt
-    val intros = map prop_of intros_th
-    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
-    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
-    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
-    val (argnames, ctxt3) = Variable.variant_fixes
-      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt2
-    val argvs = map2 (curry Free) argnames (map fastype_of args)
-    fun mk_case intro =
-      let
-        val (_, (_, args)) = strip_intro_concl nparams intro
-        val prems = Logic.strip_imp_prems intro
-        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
-        val frees = (fold o fold_aterms)
-          (fn t as Free _ =>
-              if member (op aconv) params t then I else insert (op aconv) t
-           | _ => I) (args @ prems) []
-      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
-    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
-    val cases = map mk_case intros
-  in Logic.list_implies (assm :: cases, prop) end;
-    
-
 datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
   GeneratorPrem of term list * term | Generator of (string * typ);
 
@@ -544,7 +468,82 @@
   in
     fold print (all_modes_of thy) ()
   end
-  
+
+(* importing introduction rules *)   
+
+fun unify_consts thy cs intr_ts =
+  (let
+     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
+     fun varify (t, (i, ts)) =
+       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t))
+       in (maxidx_of_term t', t'::ts) end;
+     val (i, cs') = foldr varify (~1, []) cs;
+     val (i', intr_ts') = foldr varify (i, []) intr_ts;
+     val rec_consts = fold add_term_consts_2 cs' [];
+     val intr_consts = fold add_term_consts_2 intr_ts' [];
+     fun unify (cname, cT) =
+       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
+       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
+     val (env, _) = fold unify rec_consts (Vartab.empty, i');
+     val subst = map_types (Envir.norm_type env)
+   in (map subst cs', map subst intr_ts')
+   end) handle Type.TUNIFY =>
+     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
+
+fun import_intros _ [] ctxt = ([], ctxt)
+  | import_intros nparams (th :: ths) ctxt =
+    let
+      val ((_, [th']), ctxt') = Variable.import false [th] ctxt
+      val thy = ProofContext.theory_of ctxt'
+      val (pred, (params, args)) = strip_intro_concl nparams (prop_of th')
+      val ho_args = filter (is_predT o fastype_of) args
+      fun instantiate_typ th =
+        let
+          val (pred', _) = strip_intro_concl 0 (prop_of th)
+          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+            error "Trying to instantiate another predicate" else ()
+          val subst = Sign.typ_match thy
+            (fastype_of pred', fastype_of pred) Vartab.empty
+          val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T))
+            (Vartab.dest subst)
+        in Thm.certify_instantiate (subst', []) th end;
+      fun instantiate_ho_args th =
+        let
+          val (_, (params', args')) = strip_intro_concl nparams (prop_of th)
+          val ho_args' = map dest_Var (filter (is_predT o fastype_of) args')
+        in Thm.certify_instantiate ([], map dest_Var params' ~~ params) th end
+      val ((_, ths'), ctxt1) =
+        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
+    in
+      (th' :: ths', ctxt1)
+    end
+
+(* generation of case rules from user-given introduction rules *)
+
+fun mk_casesrule ctxt nparams introrules =
+  let
+    val (intros_th, ctxt1) = import_intros nparams introrules ctxt
+    val intros = map prop_of intros_th
+    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
+    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
+    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
+    val (argnames, ctxt3) = Variable.variant_fixes
+      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt2
+    val argvs = map2 (curry Free) argnames (map fastype_of args)
+    fun mk_case intro =
+      let
+        val (_, (_, args)) = strip_intro_concl nparams intro
+        val prems = Logic.strip_imp_prems intro
+        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+        val frees = (fold o fold_aterms)
+          (fn t as Free _ =>
+              if member (op aconv) params t then I else insert (op aconv) t
+           | _ => I) (args @ prems) []
+      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
+    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
+    val cases = map mk_case intros
+  in Logic.list_implies (assm :: cases, prop) end;
+
 (** preprocessing rules **)  
 
 fun imp_prems_conv cv ct =

--- 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
@@ -7,7 +7,7 @@
   | "even n \<Longrightarrow> odd (Suc n)"
   | "odd n \<Longrightarrow> even (Suc n)"
 
-code_pred (mode: [], [1]) [show_steps, inductify] even .
+code_pred (mode: [], [1]) [show_steps] even .
 
 thm odd.equation
 thm even.equation
@@ -425,7 +425,7 @@
 code_pred [inductify] splice .
 code_pred [inductify] List.rev .
 thm map.simps
-code_pred [inductify, show_steps, show_intermediate_results] map .
+code_pred [inductify] map .
 code_pred [inductify] foldr .
 code_pred [inductify] foldl .
 code_pred [inductify] filter .