# HG changeset patch
# User wenzelm
# Date 952172901 -3600
# Node ID 4417e588d9f7d928e06a0f464a5060794ff6fa47
# Parent  fb604f0e5640f30b32894e7241950c827a100ebd
induct: "stripped" option;

diff -r fb604f0e5640 -r 4417e588d9f7 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Sat Mar 04 13:25:09 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Sat Mar 04 13:28:21 2000 +0100
@@ -126,6 +126,8 @@
 
 (** misc utils **)
 
+(* terms *)
+
 fun vars_of tm =        (*ordered left-to-right, preferring right!*)
   Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
   |> Library.distinct |> rev;
@@ -171,6 +173,8 @@
   ...   cases ... r   - explicit rule
 *)
 
+local
+
 fun cases_var thm =
   (case try (hd o vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of) thm of
     None => raise THM ("Malformed cases rule", 0, [thm])
@@ -179,7 +183,7 @@
 fun simplify_cases ctxt =
   Tactic.rule_by_tactic (con_elim_solved_tac (Simplifier.get_local_simpset ctxt));
 
-fun cases_tac (ctxt, ((simplified, opt_tm), opt_rule)) facts =
+fun cases_tac (ctxt, (simplified, args)) facts =
   let
     val sg = ProofContext.sign_of ctxt;
     val cert = Thm.cterm_of sg;
@@ -188,7 +192,7 @@
       Drule.cterm_instantiate [(cert (cases_var thm), cert t)] thm;
 
     val raw_thms =
-      (case ((opt_tm, opt_rule), facts) of
+      (case (args, facts) of
         ((None, None), []) => [case_split_thm]
       | ((None, None), th :: _) =>
           NetRules.may_unify (#2 (get_cases ctxt))
@@ -207,8 +211,12 @@
       |> (if simplified then Seq.map (simplify_cases ctxt) else I);
   in Method.resolveq_tac thms end;
 
+in
+
 val cases_meth = Method.METHOD o (FINDGOAL oo cases_tac);
 
+end;
+
 
 
 (** induct method **)
@@ -221,6 +229,8 @@
   ...   induct ... r   - explicit rule
 *)
 
+local
+
 fun induct_rule ctxt t =
   let val name = type_name t in
     (case lookup_inductT ctxt name of
@@ -250,7 +260,7 @@
         | bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads)))
       end;
 
-fun induct_tac (ctxt, args) facts =
+fun induct_tac (ctxt, (stripped, args)) facts =
   let
     val sg = ProofContext.sign_of ctxt;
     val cert = Thm.cterm_of sg;
@@ -276,17 +286,28 @@
           [inst_rule insts (join_rules (map (induct_rule ctxt o last_elem) insts))]
       | (([], Some thm), _) => [thm]
       | ((insts, Some thm), _) => [inst_rule insts thm]);
-  in Method.rule_tac thms facts end;
+  in
+    if stripped then
+      Method.rule_tac thms facts THEN_ALL_NEW (REPEAT o resolve_tac [impI, allI, ballI])
+    else Method.rule_tac thms facts
+  end;
+
+in
 
 val induct_meth = Method.METHOD o (FINDGOAL oo induct_tac);
 
+end;
+
 
 
 (** concrete syntax **)
 
 val casesN = "cases";
 val inductN = "induct";
+
 val simplifiedN = "simplified";
+val strippedN = "stripped";
+
 val typeN = "type";
 val setN = "set";
 val ruleN = "rule";
@@ -333,13 +354,15 @@
 val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.$$$ ":";
 val term = Scan.unless (Scan.lift kind) Args.local_term;
 
-val simp_mode =
-  Scan.lift (Scan.optional (Args.$$$ simplifiedN -- Args.$$$ ":" >> K true) false);
+fun mode name =
+  Scan.lift (Scan.optional (Args.$$$ name -- Args.$$$ ":" >> K true) false);
 
 in
 
-val cases_args = Method.syntax (simp_mode -- Scan.option term -- Scan.option cases_rule);
-val induct_args = Method.syntax (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.repeat1 term) -- Scan.option induct_rule));
 
 end;