# HG changeset patch
# User wenzelm
# Date 955576317 -7200
# Node ID 850e845267454c5016362a7f2d2ee9ebf5e2c89e
# Parent  c1d0cc81f06c4bc95f383535ce950f3d522d79db
export concl_of;
induct method: admit "_";

diff -r c1d0cc81f06c -r 850e84526745 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Wed Apr 12 23:49:10 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Wed Apr 12 23:51:57 2000 +0200
@@ -16,6 +16,7 @@
       type_induct: (string * thm) list, set_induct: (string * thm) list}
   val print_local_rules: Proof.context -> unit
   val vars_of: term -> term list
+  val concls_of: thm -> term list
   val cases_type_global: string -> theory attribute
   val cases_set_global: string -> theory attribute
   val cases_type_local: string -> Proof.context attribute
@@ -141,7 +142,9 @@
 
 (** misc utils **)
 
-(* terms *)
+(* thms and terms *)
+
+val concls_of = HOLogic.dest_conj o HOLogic.dest_Trueprop o Thm.concl_of;
 
 fun vars_of tm =        (*ordered left-to-right, preferring right!*)
   Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
@@ -295,15 +298,21 @@
     val sg = ProofContext.sign_of ctxt;
     val cert = Thm.cterm_of sg;
 
+    fun prep_var (x, Some t) = Some (cert x, cert t)
+      | prep_var (_, None) = None;
+
     fun prep_inst (concl, ts) =
       let val xs = vars_of concl; val n = length xs - length ts in
-        if n < 0 then error "More arguments given than in induction rule"
-        else map cert (Library.drop (n, xs)) ~~ map cert ts
+        if n < 0 then error "More variables than given than in induction rule"
+        else mapfilter prep_var (Library.drop (n, xs) ~~ ts)
       end;
 
     fun inst_rule insts thm =
-      Drule.cterm_instantiate (flat (map2 prep_inst
-        (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of thm)), insts))) thm;
+      let val concls = concls_of thm in
+        if length concls < length insts then
+          error "More arguments than given than in induction rule"
+        else Drule.cterm_instantiate (flat (map prep_inst (concls ~~ insts))) thm
+      end;
 
     fun find_induct th =
       NetRules.may_unify (#2 (get_induct ctxt))
@@ -313,7 +322,8 @@
       (case (args, facts) of
         (([], None), []) => []
       | ((insts, None), []) =>
-          let val thms = map (induct_rule ctxt o last_elem) insts
+          let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts
+            handle Library.LIST _ => error "Unable to figure out type induction rule"
           in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end
       | (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th)
       | ((insts, None), th :: _) =>
@@ -392,16 +402,17 @@
 
 val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.$$$ ":";
 val term = Scan.unless (Scan.lift kind) Args.local_term;
+val term_dummy = Scan.unless (Scan.lift kind)
+  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
 
 fun mode name =
   Scan.lift (Scan.optional (Args.$$$ name -- Args.$$$ ":" >> K true) false);
 
 in
 
-val cases_args =
-  Method.syntax (mode simplifiedN -- (Scan.option term -- Scan.option cases_rule));
-val induct_args =
-  Method.syntax (mode strippedN -- (Args.and_list (Scan.repeat1 term) -- Scan.option induct_rule));
+val cases_args = Method.syntax (mode simplifiedN -- (Scan.option term -- Scan.option cases_rule));
+val induct_args = Method.syntax
+  (mode strippedN -- (Args.and_list (Scan.repeat term_dummy) -- Scan.option induct_rule));
 
 end;