# HG changeset patch
# User berghofe
# Date 1161071464 -7200
# Node ID e57e91f728314b8d3046cf9bf9a8bd970a0e872f
# Parent  0cf1800ff7cf65dc705517f27ad7caeeb6d89c58
Restructured and repaired code dealing with case names
in induction and elimination rules.

diff -r 0cf1800ff7cf -r e57e91f72831 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Oct 17 02:40:21 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 17 09:51:04 2006 +0200
@@ -277,37 +277,6 @@
 
 
 
-(** properties of (co)inductive predicates **)
-
-(* prepare cases and induct rules *)
-
-fun add_cases_induct no_elim no_induct coind rec_name names elims induct =
-  let
-    fun cases_spec name elim =
-      LocalTheory.note ((NameSpace.append (Sign.base_name name) "cases",
-        [Attrib.internal (InductAttrib.cases_set name)]), [elim]) #> snd;
-    val cases_specs = if no_elim then [] else map2 cases_spec names elims;
-
-    val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
-    fun induct_specs ctxt =
-      if no_induct then ctxt
-      else
-        let
-          val rules = names ~~ ProjectRule.projects ctxt (1 upto length names) induct;
-          val inducts = map (RuleCases.save induct o standard o #2) rules;
-        in
-          ctxt |>
-          LocalTheory.notes (rules |> map (fn (name, th) =>
-            (("", [Attrib.internal (RuleCases.consumes 1),
-                Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |>
-          LocalTheory.note ((NameSpace.append rec_name
-              (coind_prefix coind ^ "inducts"),
-            [Attrib.internal (RuleCases.consumes 1)]), inducts) |> snd
-        end;
-  in Library.apply cases_specs #> induct_specs end;
-
-
-
 (** proofs for (co)inductive predicates **)
 
 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
@@ -386,7 +355,7 @@
         val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
            map mk_elim_prem (map #1 c_intrs)
       in
-        SkipProof.prove ctxt'' [] prems P
+        (SkipProof.prove ctxt'' [] prems P
           (fn {prems, ...} => EVERY
             [cut_facts_tac [hd prems] 1,
              rewrite_goals_tac rec_preds_defs,
@@ -396,8 +365,8 @@
              EVERY (map (fn prem =>
                DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
           |> rulify
-          |> singleton (ProofContext.export ctxt'' ctxt)
-          |> RuleCases.name (map #2 c_intrs)
+          |> singleton (ProofContext.export ctxt'' ctxt),
+         map #2 c_intrs)
       end
 
    in map prove_elim cs end;
@@ -620,14 +589,14 @@
     fun transform_rule r =
       let
         val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params
-          (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
-
+          (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
+        val ps = make_bool_args HOLogic.mk_not I bs i @
+          map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
+          map (subst o HOLogic.dest_Trueprop)
+            (Logic.strip_assums_hyp r)
       in foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
-        (foldr1 HOLogic.mk_conj
-          (make_bool_args HOLogic.mk_not I bs i @
-           map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
-           map (subst o HOLogic.dest_Trueprop)
-             (Logic.strip_assums_hyp r))) (Logic.strip_params r)
+        (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
+        (Logic.strip_params r)
       end
 
     (* make a disjunction of all introduction rules *)
@@ -671,12 +640,13 @@
   end;
 
 fun add_ind_def verbose alt_name coind no_elim no_ind cs
-    intros monos params cnames_syn induct_cases ctxt =
+    intros monos params cnames_syn ctxt =
   let
     val _ =
       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
         commas_quote (map fst cnames_syn)) else ();
 
+    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;
     val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list intros);
 
     val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
@@ -685,8 +655,9 @@
 
     val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs)
       intr_ts rec_preds_defs ctxt1;
-    val elims = ProofContext.export ctxt1 ctxt (if no_elim then [] else
-      prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1);
+    val elims = if no_elim then [] else
+      cnames ~~ map (apfst (singleton (ProofContext.export ctxt1 ctxt)))
+        (prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1);
     val raw_induct = singleton (ProofContext.export ctxt1 ctxt)
       (if no_ind then Drule.asm_rl else
        if coind then ObjectLogic.rulify (rule_by_tactic
@@ -695,37 +666,65 @@
        else
          prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def
            rec_preds_defs ctxt1);
+    val induct_cases = map (#1 o #1) intros;
+    val ind_case_names = RuleCases.case_names induct_cases;
     val induct =
       if coind then
         (raw_induct, [RuleCases.case_names [rec_name],
           RuleCases.case_conclusion (rec_name, induct_cases),
           RuleCases.consumes 1])
       else if no_ind orelse length cs > 1 then
-        (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
-      else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
+        (raw_induct, [ind_case_names, RuleCases.consumes 0])
+      else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
 
     val (intrs', ctxt2) =
       ctxt1 |>
-      LocalTheory.notes (map (NameSpace.append rec_name) intr_names ~~ intr_atts ~~
-        map (single o rpair [] o single) (ProofContext.export ctxt1 ctxt intrs)) |>>
+      LocalTheory.notes
+        (map (fn "" => "" | name => NameSpace.append rec_name name) intr_names ~~
+         intr_atts ~~
+         map (single o rpair [] o single) (ProofContext.export ctxt1 ctxt intrs)) |>>
       map (hd o snd); (* FIXME? *)
-    val (((_, (_, elims')), (_, [induct'])), ctxt3) =
+    val (((_, elims'), (_, [induct'])), ctxt3) =
       ctxt2 |>
       LocalTheory.note ((NameSpace.append rec_name "intros", []), intrs') ||>>
-      LocalTheory.note ((NameSpace.append rec_name "elims",
-        [Attrib.internal (RuleCases.consumes 1)]), elims) ||>>
+      fold_map (fn (name, (elim, cases)) =>
+        LocalTheory.note ((NameSpace.append (Sign.base_name name) "cases",
+          [Attrib.internal (RuleCases.case_names cases),
+           Attrib.internal (RuleCases.consumes 1),
+           Attrib.internal (InductAttrib.cases_set name)]), [elim]) #>
+        apfst (hd o snd)) elims ||>>
       LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "induct"),
-        map Attrib.internal (#2 induct)), [rulify (#1 induct)])
-  in (ctxt3, rec_name,
-    {preds = preds,
-     defs = fp_def :: rec_preds_defs,
-     mono = singleton (ProofContext.export ctxt1 ctxt) mono,
-     unfold = singleton (ProofContext.export ctxt1 ctxt) unfold,
-     intrs = intrs',
-     elims = elims',
-     mk_cases = mk_cases elims',
-     raw_induct = rulify raw_induct,
-     induct = induct'})
+        map Attrib.internal (#2 induct)), [rulify (#1 induct)]);
+
+    val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
+    val ctxt4 = if no_ind then ctxt3 else
+      let val inducts = cnames ~~ ProjectRule.projects ctxt (1 upto length cnames) induct'
+      in
+        ctxt3 |>
+        LocalTheory.notes (inducts |> map (fn (name, th) => (("",
+          [Attrib.internal ind_case_names,
+           Attrib.internal (RuleCases.consumes 1),
+           Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |>
+        LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "inducts"),
+          [Attrib.internal ind_case_names,
+           Attrib.internal (RuleCases.consumes 1)]), map snd inducts) |> snd
+      end;
+
+    val result =
+      {preds = preds,
+       defs = fp_def :: rec_preds_defs,
+       mono = singleton (ProofContext.export ctxt1 ctxt) mono,
+       unfold = singleton (ProofContext.export ctxt1 ctxt) unfold,
+       intrs = intrs',
+       elims = elims',
+       mk_cases = mk_cases elims',
+       raw_induct = rulify raw_induct,
+       induct = induct'}
+      
+  in
+    (LocalTheory.declaration
+       (put_inductives cnames ({names = cnames, coind = coind}, result)) ctxt4,
+     result)
   end;
 
 
@@ -745,7 +744,6 @@
     val cs = map
       (fn (s, SOME T, _) => Free (s, T) | (s, NONE, _) => Free (s, type_of s)) cnames_syn;
     val cnames_syn' = map (fn (s, _, mx) => (s, mx)) cnames_syn;
-    val cnames = map (Sign.full_name thy o #1) cnames_syn;
 
     fun close_rule (x, r) = (x, list_all_free (rev (fold_aterms
       (fn t as Free (v as (s, _)) =>
@@ -754,16 +752,10 @@
         | _ => I) r []), r));
 
     val intros = map (close_rule o check_rule thy cs params) pre_intros;
-    val induct_cases = map (#1 o #1) intros;
-
-    val (ctxt1, rec_name, result as {elims, induct, ...}) =
-      add_ind_def verbose alt_name coind no_elim no_ind cs intros monos
-        params cnames_syn' induct_cases ctxt;
-    val ctxt2 = ctxt1
-      |> LocalTheory.declaration
-        (put_inductives cnames ({names = cnames, coind = coind}, result))
-      |> add_cases_induct no_elim no_ind coind rec_name cnames elims induct;
-  in (ctxt2, result) end;
+  in
+    add_ind_def verbose alt_name coind no_elim no_ind cs intros monos
+      params cnames_syn' ctxt
+  end;
 
 fun add_inductive verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt =
   let