# HG changeset patch
# User wenzelm
# Date 1003185121 -7200
# Node ID 42393a11642ddafdb4e4ee9e0521c040d1d62278
# Parent  da81334357bae62e06b3a7606da092ecdd50e7c2
simplified resolveq_cases_tac for cases, separate version for induct;
divinate instantiation of induct rules;
tuned;

diff -r da81334357ba -r 42393a11642d src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Tue Oct 16 00:30:53 2001 +0200
+++ b/src/Provers/induct_method.ML	Tue Oct 16 00:32:01 2001 +0200
@@ -63,22 +63,6 @@
   end;
 
 
-(* tactics with cases *)
-
-fun resolveq_cases_tac make tac ruleq i st =
-  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
-    (Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st
-    |> Seq.map (rpair (make rule cases)))
-  |> Seq.flat;
-
-
-infix 1 THEN_ALL_NEW_CASES;
-
-fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
-  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
-    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
-
-
 
 (** cases method **)
 
@@ -92,6 +76,12 @@
 
 local
 
+fun resolveq_cases_tac make ruleq i st =
+  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
+    (Method.insert_tac facts THEN' Tactic.rtac rule) i st
+    |> Seq.map (rpair (make rule cases)))
+  |> Seq.flat;
+
 fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
   | find_casesT _ _ = [];
 
@@ -122,10 +112,7 @@
 
     fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
       (Method.multi_resolves (take (n, facts)) [th]);
-  in
-    resolveq_cases_tac (RuleCases.make open_parms) (K all_tac)
-      (Seq.flat (Seq.map prep_rule ruleq))
-  end;
+  in resolveq_cases_tac (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end;
 
 in
 
@@ -146,6 +133,9 @@
 
 local
 
+
+(* atomize and rulify *)
+
 fun atomize_cterm ct =
   Thm.cterm_fun (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct)))
     (Tactic.rewrite_cterm true Data.atomize ct);
@@ -167,6 +157,8 @@
   in map (apsnd ruly_case) ooo RuleCases.make_raw end;
 
 
+(* join multi-rules *)
+
 val eq_prems = curry (Term.aconvs o pairself Thm.prems_of);
 
 fun join_rules [] = []
@@ -185,6 +177,58 @@
           |> Drule.standard']
         end;
 
+
+(* divinate rule instantiation (cannot handle pending goal parameters) *)
+
+fun dest_env sign (Envir.Envir {asol, iTs, ...}) =
+  let
+    val pairs = Vartab.dest asol;
+    val ts = map (Thm.cterm_of sign o #2) pairs;
+    val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
+  in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end;
+
+fun divinate_inst rule i st =
+  let
+    val {sign, maxidx, ...} = Thm.rep_thm st;
+    val goal = List.nth (Thm.prems_of st, i - 1);  (*exception Subscript*)
+    val params = rev (rename_wrt_term goal (Logic.strip_params goal));  (*as they are printed :-*)
+  in
+    if not (null params) then
+      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
+        commas (map (Sign.string_of_term sign o Syntax.mark_boundT) params));
+      Seq.single rule)
+    else
+      let
+        val rule' = Thm.incr_indexes (maxidx + 1) rule;
+        val concl = Logic.strip_assums_concl goal;
+      in
+        Unify.smash_unifiers (sign, Envir.empty (#maxidx (Thm.rep_thm rule')),
+          [(Thm.concl_of rule', concl)])
+        |> Seq.map (fn env => Thm.instantiate (dest_env sign env) rule')
+      end
+  end handle Subscript => Seq.empty;
+
+
+(* compose tactics with cases *)
+
+fun resolveq_cases_tac' make ruleq i st =
+  ruleq |> Seq.map (fn (rule, (cases, facts)) => st
+    |> (Method.insert_tac facts THEN' atomize_tac) i
+    |> Seq.map (fn st' => divinate_inst rule i st'
+      |> Seq.map (fn rule' => st' |> Tactic.rtac rule' i |> Seq.map (rpair (make rule' cases)))
+      |> Seq.flat)
+    |> Seq.flat)
+  |> Seq.flat;
+
+infix 1 THEN_ALL_NEW_CASES;
+
+fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
+  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
+    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
+
+
+(* find rules *)
+
 fun find_inductT ctxt insts =
   foldr multiply (insts |> mapfilter (fn [] => None | ts => last_elem ts)
     |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
@@ -193,6 +237,9 @@
 fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
   | find_inductS _ _ = [];
 
+
+(* main tactic *)
+
 fun induct_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
   let
     val sg = ProofContext.sign_of ctxt;
@@ -215,11 +262,9 @@
           end
       | Some r => Seq.single (inst_rule r));
 
-    (* FIXME divinate rule_inst *)
-
     fun prep_rule (th, (cases, n)) =
       Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [th]);
-    val tac = resolveq_cases_tac (rulify_cases sg cert open_parms) atomize_tac
+    val tac = resolveq_cases_tac' (rulify_cases sg cert open_parms)
       (Seq.flat (Seq.map prep_rule ruleq));
   in tac THEN_ALL_NEW_CASES rulify_tac end;