changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned

--- 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
@@ -258,9 +258,30 @@
 
 (* generation of case rules from user-given introduction rules *)
 
+fun import_intros [] ctxt = ([], ctxt)
+  | import_intros (th :: ths) ctxt =
+    let
+      val ((_, [th']), ctxt') = Variable.import false [th] ctxt
+      val (pred, _) = strip_intro_concl 0 (prop_of th')
+      fun instantiate_typ th =
+        let
+          val (pred', _) = strip_intro_concl 0 (prop_of th)
+          val subst = Sign.typ_match (ProofContext.theory_of ctxt')
+            (fastype_of pred', fastype_of pred) Vartab.empty
+          val _ = Output.tracing (commas (map (fn ((x, i), (s, T)) => x ^ " instantiate to " ^ (Syntax.string_of_typ ctxt' T))
+          (Vartab.dest subst)))
+          val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T))
+            (Vartab.dest subst)
+        in Thm.certify_instantiate (subst', []) th end;
+      val ((_, ths'), ctxt1) =
+        Variable.import false (map instantiate_typ ths) ctxt'
+    in
+      (th' :: ths', ctxt1)
+    end
+
 fun mk_casesrule ctxt nparams introrules =
   let
-    val ((_, intros_th), ctxt1) = Variable.import false introrules ctxt
+    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
@@ -633,7 +654,7 @@
    fun cons_intro gr =
      case try (Graph.get_node gr) name of
        SOME pred_data => Graph.map_node name (map_pred_data
-         (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr
+         (apfst (fn (intros, elim, nparams) => (thm::intros, elim, nparams)))) gr
      | NONE =>
        let
          val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
@@ -965,7 +986,7 @@
           val prfx = map (rpair NONE) (1 upto k)
         in
           if not (is_prefix op = prfx is) then [] else
-          let val is' = List.drop (is, k)
+          let val is' = map (fn (i, t) => (i - k, t)) (List.drop (is, k))
           in map (fn x => Mode (m, is', x)) (cprods (map
             (fn (NONE, _) => [NONE]
               | (SOME js, arg) => map SOME (filter
@@ -2143,7 +2164,7 @@
     
 fun prepare_intrs thy prednames intros =
   let
-    val ((_, intrs), _) = Variable.import false intros (ProofContext.init thy)
+    val (intrs, _) =  import_intros 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)

--- 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
@@ -53,6 +53,24 @@
 value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
 value [code] "Predicate.the (append_3 ([]::int list))"
 
+subsection {* Tricky case with alternative rules *}
+
+inductive append2
+where
+  "append2 [] xs xs"
+| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
+
+lemma append2_Nil: "append2 [] (xs::'b list) xs"
+  by (simp add: append2.intros(1))
+
+lemmas [code_pred_intros] = append2_Nil append2.intros(2)
+
+code_pred append2
+proof -
+  case append2
+  from append2.cases[OF append2(1)] append2(2-3) show thesis by blast
+qed
+
 subsection {* Tricky cases with tuples *}
 
 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -412,6 +430,7 @@
 thm revP.equation
 
 
+
 section {* Context Free Grammar *}
 
 datatype alphabet = a | b
@@ -475,6 +494,8 @@
   "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] ==> test w"
 ML {* @{term "[x \<leftarrow> w. x = a]"} *}
 code_pred (inductify_all) test .
+
+thm test.equation
 (*
 theorem S\<^isub>3_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"