# HG changeset patch
# User wenzelm
# Date 1133307968 -3600
# Node ID feb79a6b274b7c873d7627782985b0a226030e27
# Parent  28efcdae34dc971f4280fd7d9fc993c827201ed9
proper treatment of tuple/tuple_fun -- nest to the left!

diff -r 28efcdae34dc -r feb79a6b274b src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Tue Nov 29 23:00:20 2005 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Nov 30 00:46:08 2005 +0100
@@ -1,7 +1,7 @@
 (*  ID:         $Id$
-    Author:     Christian Urban
+    Author:     Christian Urban and Makarius
 
-The nominal induct proof method (cf. ~~/src/Provers/induct_method.ML).
+The nominal induct proof method.
 *)
 
 structure NominalInduct:
@@ -13,82 +13,64 @@
 struct
 
 
-(** misc tools **)
+(* proper tuples -- nested left *)
 
-fun nth_list xss i = nth xss i handle Subscript => [];
+fun tupleT Ts = HOLogic.unitT |> fold (fn T => fn U => HOLogic.mk_prodT (U, T)) Ts;
+fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
+
+fun tuple_fun Ts (xi, T) =
+  Library.funpow (length Ts) HOLogic.mk_split
+    (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
 
-fun align_right msg xs ys =
-  let val m = length xs and n = length ys
-  in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
+val split_all_tuples =
+  Simplifier.full_simplify (HOL_basic_ss addsimps
+    [split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]);
 
-fun prep_inst thy tune (tm, ts) =
+
+(* inst_rule conclusion: ?P fresh_struct ... insts *)
+
+fun inst_rule thy insts fresh rule =
   let
-    val cert = Thm.cterm_of thy;
-    fun prep_var (x, SOME t) =
-          let
-            val cx = cert x;
-            val {T = xT, thy, ...} = Thm.rep_cterm cx;
-            val ct = cert (tune t);
-          in
-            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
-            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
-             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
-              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
-              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
-          end
-      | prep_var (_, NONE) = NONE;
-    val xs = InductAttrib.vars_of tm;
+    val vars = InductAttrib.vars_of (Thm.concl_of rule);
+    val m = length vars and n = length insts;
+    val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
+    val P :: x :: ys = vars;
+    val zs = Library.drop (m - n - 2, ys);
+
+    val subst =
+      (P, tuple_fun (map Term.fastype_of fresh) (Term.dest_Var P)) ::
+      (x, tuple fresh) ::
+      List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ insts);
   in
-    align_right "Rule has fewer variables than instantiations given" xs ts
-    |> List.mapPartial prep_var
+    rule
+    |> Drule.cterm_instantiate (PolyML.print (map (pairself (Thm.cterm_of thy)) subst))
+    |> PolyML.print
   end;
 
-fun add_defs def_insts =
-  let
-    fun add (SOME (SOME x, t)) ctxt =
-          let val ((lhs, def), ctxt') = ProofContext.add_def (x, t) ctxt
-          in ((SOME (Free lhs), [def]), ctxt') end
-      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
-      | add NONE ctxt = ((NONE, []), ctxt);
-  in fold_map add def_insts #> apfst (split_list #> apsnd List.concat) end;
 
-
-
-(** nominal_induct_tac **)
-
-fun make_fresh [] = HOLogic.unit
-  | make_fresh [t] = t
-  | make_fresh ts = foldr1 HOLogic.mk_prod ts;
-
-val split_fresh =
-  Simplifier.full_simplify (HOL_basic_ss addsimps [split_paired_all, unit_all_eq1]);
+(* nominal_induct_tac *)
 
 fun nominal_induct_tac ctxt def_insts fresh fixing rule facts =
   let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
-    val ((insts, defs), defs_ctxt) = add_defs def_insts ctxt;
+    val ((insts, defs), defs_ctxt) = InductMethod.add_defs def_insts ctxt;
     val atomized_defs = map ObjectLogic.atomize_thm defs;
 
-    fun inst_rule r =
-      Drule.cterm_instantiate
-        (prep_inst thy (InductMethod.atomize_term thy)
-          (Thm.concl_of r, insts @ [SOME (make_fresh fresh)])) r;
-
     fun rule_cases r = RuleCases.make false (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
   in
     SUBGOAL_CASES (fn (goal, i) => fn st =>
       rule
-      |> inst_rule
       |> `RuleCases.get
+      ||> inst_rule thy insts fresh
       |> RuleCases.consume defs facts
       |> Seq.maps (fn ((cases, (k, more_facts)), r) =>
         (CONJUNCTS (ALLGOALS (fn j =>
             Method.insert_tac (more_facts @ atomized_defs) j
-            THEN InductMethod.fix_tac defs_ctxt k (nth_list fixing (j - 1)) j))
+            THEN InductMethod.fix_tac defs_ctxt k (Library.nth_list fixing (j - 1)) j))
           THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
-            InductMethod.guess_instance (split_fresh r) i st'
+            InductMethod.guess_instance (split_all_tuples r) i st'
             |> Seq.maps (fn r' =>
               CASES (rule_cases r' cases)
                 (Tactic.rtac r' i THEN
@@ -97,8 +79,7 @@
   end;
 
 
-
-(** concrete syntax **)
+(* concrete syntax *)
 
 local