# HG changeset patch
# User berghofe
# Date 1049787630 -7200
# Node ID c13e6e218a69b4df069fe8ceaaf466f47e834685
# Parent  ad1c28671a936ede44a09057d01b9db8de345cc5
try_param_tac now precomputes substitution for rule, in order to avoid
problems with higher order unification.

diff -r ad1c28671a93 -r c13e6e218a69 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Apr 08 09:05:39 2003 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Apr 08 09:40:30 2003 +0200
@@ -92,8 +92,30 @@
 
 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
 
-fun try_param_tac x s rule i st =
-  res_inst_tac [(x, (case Tactic.innermost_params i st of [] => s | (p, _) :: _ => p))] rule i st;
+(* do case analysis / induction on last parameter of ith subgoal (or s) *)
+
+fun try_param_tac s rule i st =
+  let
+    val cert = cterm_of (#sign (rep_thm st));
+    val g = nth_elem (i - 1, prems_of st);
+    val params = Logic.strip_params g;
+    val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
+    val rule' = Thm.lift_rule (st, i) rule;
+    val (P, ys) = strip_comb (HOLogic.dest_Trueprop
+      (Logic.strip_assums_concl (prop_of rule')));
+    val (x, ca) = (case rev (drop (length params, ys)) of
+        [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
+          (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
+      | [x] => (head_of x, false));
+    val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
+        [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
+          None => sys_error "try_param_tac: no such variable"
+        | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl),
+            (x, Free (s, T))])
+      | (_, T) :: _ => [(P, list_abs (params, if ca then concl
+          else incr_boundvars 1 (Abs (s, T, concl)))),
+        (x, list_abs (params, Bound 0))])) rule'
+  in compose_tac (false, rule'', nprems_of rule) i st end;
 
 
 
@@ -859,13 +881,13 @@
     fun induct_scheme n =
       let val (assm, concl) = induct_scheme_prop n in
         prove_standard [] [assm] concl (fn prems =>
-          EVERY (map (fn rule => try_param_tac "p" rN rule 1) (prune n all_field_inducts))
+          EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_inducts))
           THEN resolve_tac prems 1)
       end;
 
     fun cases_scheme n =
       prove_standard [] [] (cases_scheme_prop n) (fn _ =>
-        EVERY (map (fn rule => try_param_tac "p" rN rule 1) (prune n all_field_cases))
+        EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases))
         THEN simp_all_tac HOL_basic_ss []);
 
     val induct_scheme0 = induct_scheme 0;
@@ -898,7 +920,7 @@
       let val (assm, concl) = induct_prop n in
         prove_standard [] [assm] concl (fn prems =>
           res_inst_tac [(rN, rN)] scheme 1
-          THEN try_param_tac "x" "more" unit_induct 1
+          THEN try_param_tac "more" unit_induct 1
           THEN resolve_tac prems 1)
       end;