# HG changeset patch
# User wenzelm
# Date 973547906 -3600
# Node ID 10a1b95ce642ec80abd60c5e802139cc55a03949
# Parent  d8b3613158b162fa3979426a7fd104929c81bbcb
method 'induct' now handles non-atomic goals;
improved error message;
option 'stripped' deprecated;

diff -r d8b3613158b1 -r 10a1b95ce642 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Mon Nov 06 22:56:07 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Mon Nov 06 22:58:26 2000 +0100
@@ -18,6 +18,13 @@
 struct
 
 
+(** theory context references **)
+
+val inductive_atomize = thms "inductive_atomize";
+val inductive_rulify = thms "inductive_rulify";
+
+
+
 (** misc utils **)
 
 (* align lists *)
@@ -43,9 +50,21 @@
   #1 (Term.dest_Type (Term.type_of t))
     handle TYPE _ => raise TERM ("Type of term argument is too general", [t]);
 
-fun prep_inst align cert (tm, ts) =
+fun prep_inst align cert f (tm, ts) =
   let
-    fun prep_var (x, Some t) = Some (cert x, cert t)
+    fun prep_var (x, Some t) =
+          let
+            val cx = cert x;
+            val {T = xT, sign, ...} = Thm.rep_cterm cx;
+            val orig_ct = cert t;
+            val ct = f orig_ct;
+          in
+            if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
+            else error (Pretty.string_of (Pretty.block
+              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
+                Display.pretty_cterm orig_ct, Pretty.str " ::", Pretty.brk 1,
+                Display.pretty_ctyp (#T (Thm.crep_cterm orig_ct))]))
+          end
       | prep_var (_, None) = None;
   in
     align "Rule has fewer variables than instantiations given" (vars_of tm) ts
@@ -58,11 +77,8 @@
 local
 
 (*delete needless equality assumptions*)
-val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
-     (fn _ => [assume_tac 1]);
-
+val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
-
 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
 
 in
@@ -112,7 +128,7 @@
 
     fun inst_rule insts thm =
       (align_left "Rule has fewer premises than arguments given" (Thm.prems_of thm) insts
-        |> (flat o map (prep_inst align_left cert))
+        |> (flat o map (prep_inst align_left cert I))
         |> Drule.cterm_instantiate) thm;
 
     fun find_cases th =
@@ -143,7 +159,10 @@
 
     fun prep_rule (thm, cases) =
       Seq.map (cond_simp cases) (Method.multi_resolves facts [thm]);
-  in Method.resolveq_cases_tac open_parms (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end;
+  in
+    Method.resolveq_cases_tac (RuleCases.make open_parms)
+      (Seq.flat (Seq.map prep_rule (Seq.of_list rules)))
+  end;
 
 in
 
@@ -157,7 +176,6 @@
 
 (*
   rule selection:
-        induct         - mathematical induction
         induct x       - datatype induction
   <x:A> induct ...     - set induction
   ...   induct ... R   - explicit rule
@@ -165,6 +183,25 @@
 
 local
 
+fun rewrite_cterm rews =
+  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
+
+fun drop_Trueprop ct =
+  let
+    fun drop (Abs (x, T, t)) = Abs (x, T, drop t)
+      | drop t = HOLogic.dest_Trueprop t;
+    val {sign, t, ...} = Thm.rep_cterm ct;
+  in Thm.cterm_of sign (drop t) handle TERM _ => ct end;
+
+val atomize_cterm = drop_Trueprop o rewrite_cterm inductive_atomize;
+val atomize_tac = Method.rewrite_goal_tac inductive_atomize;
+val rulify_cterm = rewrite_cterm inductive_rulify;
+val rulify_tac = Method.rewrite_goal_tac inductive_rulify;
+
+fun rulify_cases cert =
+  map (apsnd (apsnd (map (Thm.term_of o rulify_cterm o cert)))) ooo RuleCases.make;
+
+
 infix 1 THEN_ALL_NEW_CASES;
 
 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
@@ -209,7 +246,7 @@
 
     fun inst_rule insts thm =
       (align_right "Rule has fewer conclusions than arguments given" (concls_of thm) insts
-        |> (flat o map (prep_inst align_right cert))
+        |> (flat o map (prep_inst align_right cert atomize_cterm))
         |> Drule.cterm_instantiate) thm;
 
     fun find_induct th =
@@ -233,11 +270,13 @@
 
     fun prep_rule (thm, cases) =
       Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
-    val tac = Method.resolveq_cases_tac open_parms
+    val tac = Method.resolveq_cases_tac (rulify_cases cert open_parms)
       (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   in
-    if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI])
-    else tac
+    if stripped then
+      (warning "induct method: encountered deprecated 'stripped' option";
+        tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI]))
+    else (fn i => Seq.THEN (atomize_tac i, tac i)) THEN_ALL_NEW_CASES rulify_tac
   end;
 
 in