modernized structure Rule_Cases;
authorwenzelm
Sun Nov 01 15:24:45 2009 +0100 (2009-11-01)
changeset 33368b1cf34f1855c
parent 33367 2912bf1871ba
child 33369 470a7b233ee5
modernized structure Rule_Cases;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/record.ML
src/HOL/Tools/split_rule.ML
src/HOL/Tools/typedef.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/specification.ML
src/Tools/induct.ML
src/Tools/induct_tacs.ML
src/Tools/project_rule.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -62,10 +62,10 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
     1.8 +fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
     1.9  
    1.10  fun mk_case_names_exhausts descr new =
    1.11 -  map (RuleCases.case_names o exhaust_cases descr o #1)
    1.12 +  map (Rule_Cases.case_names o exhaust_cases descr o #1)
    1.13      (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    1.14  
    1.15  end;
    1.16 @@ -153,7 +153,7 @@
    1.17  
    1.18  fun projections rule =
    1.19    Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
    1.20 -  |> map (Drule.standard #> RuleCases.save rule);
    1.21 +  |> map (Drule.standard #> Rule_Cases.save rule);
    1.22  
    1.23  val supp_prod = thm "supp_prod";
    1.24  val fresh_prod = thm "fresh_prod";
     2.1 --- a/src/HOL/Nominal/nominal_induct.ML	Fri Oct 30 18:33:21 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 01 15:24:45 2009 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  sig
     2.5    val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     2.6      (string * typ) list -> (string * typ) list list -> thm list ->
     2.7 -    thm list -> int -> RuleCases.cases_tactic
     2.8 +    thm list -> int -> Rule_Cases.cases_tactic
     2.9    val nominal_induct_method: (Proof.context -> Proof.method) context_parser
    2.10  end =
    2.11  struct
    2.12 @@ -31,9 +31,9 @@
    2.13  
    2.14  fun inst_mutual_rule ctxt insts avoiding rules =
    2.15    let
    2.16 -    val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
    2.17 +    val (nconcls, joined_rule) = Rule_Cases.strict_mutual_rule ctxt rules;
    2.18      val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
    2.19 -    val (cases, consumes) = RuleCases.get joined_rule;
    2.20 +    val (cases, consumes) = Rule_Cases.get joined_rule;
    2.21  
    2.22      val l = length rules;
    2.23      val _ =
    2.24 @@ -93,12 +93,12 @@
    2.25        split_all_tuples
    2.26        #> rename_params_rule true
    2.27          (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    2.28 -    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    2.29 +    fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    2.30    in
    2.31      (fn i => fn st =>
    2.32        rules
    2.33        |> inst_mutual_rule ctxt insts avoiding
    2.34 -      |> RuleCases.consume (flat defs) facts
    2.35 +      |> Rule_Cases.consume (flat defs) facts
    2.36        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    2.37          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    2.38            (CONJUNCTS (ALLGOALS
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Oct 30 18:33:21 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Nov 01 15:24:45 2009 +0100
     3.3 @@ -158,7 +158,7 @@
     3.4          [] => ()
     3.5        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     3.6            commas_quote xs));
     3.7 -    val induct_cases = map fst (fst (RuleCases.get (the
     3.8 +    val induct_cases = map fst (fst (Rule_Cases.get (the
     3.9        (Induct.lookup_inductP ctxt (hd names)))));
    3.10      val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
    3.11      val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
    3.12 @@ -547,7 +547,7 @@
    3.13        let
    3.14          val rec_name = space_implode "_" (map Long_Name.base_name names);
    3.15          val rec_qualified = Binding.qualify false rec_name;
    3.16 -        val ind_case_names = RuleCases.case_names induct_cases;
    3.17 +        val ind_case_names = Rule_Cases.case_names induct_cases;
    3.18          val induct_cases' = Inductive.partition_rules' raw_induct
    3.19            (intrs ~~ induct_cases); 
    3.20          val thss' = map (map atomize_intr) thss;
    3.21 @@ -558,9 +558,9 @@
    3.22            (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
    3.23          val strong_induct =
    3.24            if length names > 1 then
    3.25 -            (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
    3.26 +            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    3.27            else (strong_raw_induct RSN (2, rev_mp),
    3.28 -            [ind_case_names, RuleCases.consumes 1]);
    3.29 +            [ind_case_names, Rule_Cases.consumes 1]);
    3.30          val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
    3.31            ((rec_qualified (Binding.name "strong_induct"),
    3.32              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
    3.33 @@ -572,12 +572,12 @@
    3.34          LocalTheory.note Thm.generatedK
    3.35            ((rec_qualified (Binding.name "strong_inducts"),
    3.36              [Attrib.internal (K ind_case_names),
    3.37 -             Attrib.internal (K (RuleCases.consumes 1))]),
    3.38 +             Attrib.internal (K (Rule_Cases.consumes 1))]),
    3.39             strong_inducts) |> snd |>
    3.40          LocalTheory.notes Thm.generatedK (map (fn ((name, elim), (_, cases)) =>
    3.41              ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    3.42 -              [Attrib.internal (K (RuleCases.case_names (map snd cases))),
    3.43 -               Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
    3.44 +              [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
    3.45 +               Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
    3.46            (strong_cases ~~ induct_cases')) |> snd
    3.47        end)
    3.48        (map (map (rulify_term thy #> rpair [])) vc_compat)
     4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Oct 30 18:33:21 2009 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Nov 01 15:24:45 2009 +0100
     4.3 @@ -164,7 +164,7 @@
     4.4          [] => ()
     4.5        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     4.6            commas_quote xs));
     4.7 -    val induct_cases = map fst (fst (RuleCases.get (the
     4.8 +    val induct_cases = map fst (fst (Rule_Cases.get (the
     4.9        (Induct.lookup_inductP ctxt (hd names)))));
    4.10      val induct_cases' = if null induct_cases then replicate (length intrs) ""
    4.11        else induct_cases;
    4.12 @@ -449,7 +449,7 @@
    4.13        let
    4.14          val rec_name = space_implode "_" (map Long_Name.base_name names);
    4.15          val rec_qualified = Binding.qualify false rec_name;
    4.16 -        val ind_case_names = RuleCases.case_names induct_cases;
    4.17 +        val ind_case_names = Rule_Cases.case_names induct_cases;
    4.18          val induct_cases' = Inductive.partition_rules' raw_induct
    4.19            (intrs ~~ induct_cases); 
    4.20          val thss' = map (map atomize_intr) thss;
    4.21 @@ -458,9 +458,9 @@
    4.22            mk_ind_proof ctxt thss' |> Inductive.rulify;
    4.23          val strong_induct =
    4.24            if length names > 1 then
    4.25 -            (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
    4.26 +            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    4.27            else (strong_raw_induct RSN (2, rev_mp),
    4.28 -            [ind_case_names, RuleCases.consumes 1]);
    4.29 +            [ind_case_names, Rule_Cases.consumes 1]);
    4.30          val (induct_name, inducts_name) =
    4.31            case alt_name of
    4.32              NONE => (rec_qualified (Binding.name "strong_induct"),
    4.33 @@ -477,7 +477,7 @@
    4.34          LocalTheory.note Thm.generatedK
    4.35            ((inducts_name,
    4.36              [Attrib.internal (K ind_case_names),
    4.37 -             Attrib.internal (K (RuleCases.consumes 1))]),
    4.38 +             Attrib.internal (K (Rule_Cases.consumes 1))]),
    4.39             strong_inducts) |> snd
    4.40        end)
    4.41        (map (map (rulify_term thy #> rpair [])) vc_compat)
     5.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 30 18:33:21 2009 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 01 15:24:45 2009 +0100
     5.3 @@ -203,10 +203,10 @@
     5.4  
     5.5  in
     5.6  
     5.7 -fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
     5.8 +fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
     5.9  
    5.10  fun mk_case_names_exhausts descr new =
    5.11 -  map (RuleCases.case_names o exhaust_cases descr o #1)
    5.12 +  map (Rule_Cases.case_names o exhaust_cases descr o #1)
    5.13      (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
    5.14  
    5.15  end;
    5.16 @@ -328,7 +328,7 @@
    5.17        [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
    5.18         ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
    5.19      val unnamed_rules = map (fn induct =>
    5.20 -      ((Binding.empty, [induct]), [RuleCases.inner_rule, Induct.induct_type ""]))
    5.21 +      ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
    5.22          (Library.drop (length dt_names, inducts));
    5.23    in
    5.24      thy9
     6.1 --- a/src/HOL/Tools/Function/function.ML	Fri Oct 30 18:33:21 2009 +0100
     6.2 +++ b/src/HOL/Tools/Function/function.ML	Sun Nov 01 15:24:45 2009 +0100
     6.3 @@ -98,12 +98,12 @@
     6.4                   psimp_attribs psimps
     6.5              ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
     6.6              ||>> note_theorem ((qualify "pinduct",
     6.7 -                   [Attrib.internal (K (RuleCases.case_names cnames)),
     6.8 -                    Attrib.internal (K (RuleCases.consumes 1)),
     6.9 +                   [Attrib.internal (K (Rule_Cases.case_names cnames)),
    6.10 +                    Attrib.internal (K (Rule_Cases.consumes 1)),
    6.11                      Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
    6.12              ||>> note_theorem ((qualify "termination", []), [termination])
    6.13              ||> (snd o note_theorem ((qualify "cases",
    6.14 -                   [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
    6.15 +                   [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
    6.16              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    6.17  
    6.18            val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
    6.19 @@ -153,7 +153,7 @@
    6.20              |> add_simps I "simps" simp_attribs tsimps |> snd
    6.21              |> note_theorem
    6.22                 ((qualify "induct",
    6.23 -                 [Attrib.internal (K (RuleCases.case_names case_names))]),
    6.24 +                 [Attrib.internal (K (Rule_Cases.case_names case_names))]),
    6.25                  tinduct) |> snd
    6.26            end
    6.27      in
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Oct 30 18:33:21 2009 +0100
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 01 15:24:45 2009 +0100
     7.3 @@ -2332,7 +2332,7 @@
     7.4        in mk_casesrule lthy' pred nparams intros end  
     7.5      val cases_rules = map mk_cases preds
     7.6      val cases =
     7.7 -      map (fn case_rule => RuleCases.Case {fixes = [],
     7.8 +      map (fn case_rule => Rule_Cases.Case {fixes = [],
     7.9          assumes = [("", Logic.strip_imp_prems case_rule)],
    7.10          binds = [], cases = []}) cases_rules
    7.11      val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     8.1 --- a/src/HOL/Tools/inductive.ML	Fri Oct 30 18:33:21 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 01 15:24:45 2009 +0100
     8.3 @@ -693,15 +693,15 @@
     8.4      val rec_name = Binding.name_of rec_binding;
     8.5      fun rec_qualified qualified = Binding.qualify qualified rec_name;
     8.6      val intr_names = map Binding.name_of intr_bindings;
     8.7 -    val ind_case_names = RuleCases.case_names intr_names;
     8.8 +    val ind_case_names = Rule_Cases.case_names intr_names;
     8.9      val induct =
    8.10        if coind then
    8.11 -        (raw_induct, [RuleCases.case_names [rec_name],
    8.12 -          RuleCases.case_conclusion (rec_name, intr_names),
    8.13 -          RuleCases.consumes 1, Induct.coinduct_pred (hd cnames)])
    8.14 +        (raw_induct, [Rule_Cases.case_names [rec_name],
    8.15 +          Rule_Cases.case_conclusion (rec_name, intr_names),
    8.16 +          Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
    8.17        else if no_ind orelse length cnames > 1 then
    8.18 -        (raw_induct, [ind_case_names, RuleCases.consumes 0])
    8.19 -      else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
    8.20 +        (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    8.21 +      else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
    8.22  
    8.23      val (intrs', ctxt1) =
    8.24        ctxt |>
    8.25 @@ -716,8 +716,8 @@
    8.26        LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    8.27        fold_map (fn (name, (elim, cases)) =>
    8.28          LocalTheory.note kind ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
    8.29 -          [Attrib.internal (K (RuleCases.case_names cases)),
    8.30 -           Attrib.internal (K (RuleCases.consumes 1)),
    8.31 +          [Attrib.internal (K (Rule_Cases.case_names cases)),
    8.32 +           Attrib.internal (K (Rule_Cases.consumes 1)),
    8.33             Attrib.internal (K (Induct.cases_pred name)),
    8.34             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    8.35          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    8.36 @@ -732,7 +732,7 @@
    8.37          LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
    8.38            inducts |> map (fn (name, th) => ([th],
    8.39              [Attrib.internal (K ind_case_names),
    8.40 -             Attrib.internal (K (RuleCases.consumes 1)),
    8.41 +             Attrib.internal (K (Rule_Cases.consumes 1)),
    8.42               Attrib.internal (K (Induct.induct_pred name))])))] |> snd
    8.43        end
    8.44    in (intrs', elims', induct', ctxt3) end;
     9.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Oct 30 18:33:21 2009 +0100
     9.2 +++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 01 15:24:45 2009 +0100
     9.3 @@ -343,7 +343,7 @@
     9.4      Simplifier.full_simplify (HOL_basic_ss addsimprocs
     9.5        [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
     9.6      eta_contract_thm (is_pred pred_arities) |>
     9.7 -    RuleCases.save thm
     9.8 +    Rule_Cases.save thm
     9.9    end;
    9.10  
    9.11  val to_pred_att = Thm.rule_attribute o to_pred;
    9.12 @@ -374,7 +374,7 @@
    9.13      Thm.instantiate ([], insts) |>
    9.14      Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
    9.15          addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
    9.16 -    RuleCases.save thm
    9.17 +    Rule_Cases.save thm
    9.18    end;
    9.19  
    9.20  val to_set_att = Thm.rule_attribute o to_set;
    9.21 @@ -522,7 +522,7 @@
    9.22        Inductive.declare_rules kind rec_name coind no_ind cnames
    9.23        (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
    9.24        (map (fn th => (to_set [] (Context.Proof ctxt3) th,
    9.25 -         map fst (fst (RuleCases.get th)))) elims)
    9.26 +         map fst (fst (Rule_Cases.get th)))) elims)
    9.27        raw_induct' ctxt3
    9.28    in
    9.29      ({intrs = intrs', elims = elims', induct = induct,
    10.1 --- a/src/HOL/Tools/old_primrec.ML	Fri Oct 30 18:33:21 2009 +0100
    10.2 +++ b/src/HOL/Tools/old_primrec.ML	Sun Nov 01 15:24:45 2009 +0100
    10.3 @@ -237,8 +237,8 @@
    10.4      val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
    10.5    in
    10.6      induct
    10.7 -    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
    10.8 -    |> RuleCases.save induct
    10.9 +    |> Rule_Cases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
   10.10 +    |> Rule_Cases.save induct
   10.11    end;
   10.12  
   10.13  local
    11.1 --- a/src/HOL/Tools/record.ML	Fri Oct 30 18:33:21 2009 +0100
    11.2 +++ b/src/HOL/Tools/record.ML	Sun Nov 01 15:24:45 2009 +0100
    11.3 @@ -1553,7 +1553,7 @@
    11.4  
    11.5  (* attributes *)
    11.6  
    11.7 -fun case_names_fields x = RuleCases.case_names ["fields"] x;
    11.8 +fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
    11.9  fun induct_type_global name = [case_names_fields, Induct.induct_type name];
   11.10  fun cases_type_global name = [case_names_fields, Induct.cases_type name];
   11.11  
    12.1 --- a/src/HOL/Tools/split_rule.ML	Fri Oct 30 18:33:21 2009 +0100
    12.2 +++ b/src/HOL/Tools/split_rule.ML	Sun Nov 01 15:24:45 2009 +0100
    12.3 @@ -118,7 +118,7 @@
    12.4      fst (fold_rev complete_split_rule_var vars (rl, xs))
    12.5      |> remove_internal_split
    12.6      |> Drule.standard
    12.7 -    |> RuleCases.save rl
    12.8 +    |> Rule_Cases.save rl
    12.9    end;
   12.10  
   12.11  
   12.12 @@ -138,7 +138,7 @@
   12.13      |> fold_index one_goal xss
   12.14      |> Simplifier.full_simplify split_rule_ss
   12.15      |> Drule.standard
   12.16 -    |> RuleCases.save rl
   12.17 +    |> Rule_Cases.save rl
   12.18    end;
   12.19  
   12.20  
    13.1 --- a/src/HOL/Tools/typedef.ML	Fri Oct 30 18:33:21 2009 +0100
    13.2 +++ b/src/HOL/Tools/typedef.ML	Sun Nov 01 15:24:45 2009 +0100
    13.3 @@ -152,13 +152,13 @@
    13.4                  ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
    13.5                  ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
    13.6                  ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
    13.7 -                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
    13.8 +                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
    13.9                  ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
   13.10 -                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
   13.11 +                  [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
   13.12                  ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
   13.13 -                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
   13.14 +                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
   13.15                  ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
   13.16 -                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
   13.17 +                  [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
   13.18              ||> Sign.parent_path;
   13.19            val info = {rep_type = oldT, abs_type = newT,
   13.20              Rep_name = full Rep_name, Abs_name = full Abs_name,
    14.1 --- a/src/Pure/Isar/attrib.ML	Fri Oct 30 18:33:21 2009 +0100
    14.2 +++ b/src/Pure/Isar/attrib.ML	Sun Nov 01 15:24:45 2009 +0100
    14.3 @@ -287,15 +287,15 @@
    14.4      "rename bound variables in abstractions" #>
    14.5    setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
    14.6    setup (Binding.name "folded") folded "folded definitions" #>
    14.7 -  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes)
    14.8 +  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
    14.9      "number of consumed facts" #>
   14.10 -  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names)
   14.11 +  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
   14.12      "named rule cases" #>
   14.13    setup (Binding.name "case_conclusion")
   14.14 -    (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion)
   14.15 +    (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
   14.16      "named conclusion of rule cases" #>
   14.17    setup (Binding.name "params")
   14.18 -    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params)
   14.19 +    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
   14.20      "named rule parameters" #>
   14.21    setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
   14.22      "result put into standard form (legacy)" #>
    15.1 --- a/src/Pure/Isar/obtain.ML	Fri Oct 30 18:33:21 2009 +0100
    15.2 +++ b/src/Pure/Isar/obtain.ML	Sun Nov 01 15:24:45 2009 +0100
    15.3 @@ -222,7 +222,7 @@
    15.4      val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
    15.5      val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
    15.6  
    15.7 -    val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
    15.8 +    val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
    15.9      val m = length vars;
   15.10      val n = length params;
   15.11      val _ = m <= n orelse err "More variables than parameters in obtained rule" rule;
    16.1 --- a/src/Pure/Isar/proof.ML	Fri Oct 30 18:33:21 2009 +0100
    16.2 +++ b/src/Pure/Isar/proof.ML	Sun Nov 01 15:24:45 2009 +0100
    16.3 @@ -387,7 +387,7 @@
    16.4  fun no_goal_cases st = map (rpair NONE) (goals st);
    16.5  
    16.6  fun goal_cases st =
    16.7 -  RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
    16.8 +  Rule_Cases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
    16.9  
   16.10  fun apply_method current_context meth state =
   16.11    let
    17.1 --- a/src/Pure/Isar/proof_context.ML	Fri Oct 30 18:33:21 2009 +0100
    17.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 01 15:24:45 2009 +0100
    17.3 @@ -112,9 +112,9 @@
    17.4    val add_assms_i: Assumption.export ->
    17.5      (Thm.binding * (term * term list) list) list ->
    17.6      Proof.context -> (string * thm list) list * Proof.context
    17.7 -  val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
    17.8 -  val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
    17.9 -  val get_case: Proof.context -> string -> string option list -> RuleCases.T
   17.10 +  val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   17.11 +  val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   17.12 +  val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
   17.13    val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   17.14    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
   17.15      Context.generic -> Context.generic
   17.16 @@ -169,7 +169,7 @@
   17.17      syntax: LocalSyntax.T,                            (*local syntax*)
   17.18      consts: Consts.T * Consts.T,                      (*local/global consts*)
   17.19      facts: Facts.T,                                   (*local facts*)
   17.20 -    cases: (string * (RuleCases.T * bool)) list};     (*named case contexts*)
   17.21 +    cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
   17.22  
   17.23  fun make_ctxt (mode, naming, syntax, consts, facts, cases) =
   17.24    Ctxt {mode = mode, naming = naming, syntax = syntax,
   17.25 @@ -1150,13 +1150,13 @@
   17.26      fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
   17.27        | replace [] ys = ys
   17.28        | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
   17.29 -    val RuleCases.Case {fixes, assumes, binds, cases} = c;
   17.30 +    val Rule_Cases.Case {fixes, assumes, binds, cases} = c;
   17.31      val fixes' = replace fxs fixes;
   17.32      val binds' = map drop_schematic binds;
   17.33    in
   17.34      if null (fold (Term.add_tvarsT o snd) fixes []) andalso
   17.35        null (fold (fold Term.add_vars o snd) assumes []) then
   17.36 -        RuleCases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
   17.37 +        Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
   17.38      else error ("Illegal schematic variable(s) in case " ^ quote name)
   17.39    end;
   17.40  
   17.41 @@ -1172,9 +1172,9 @@
   17.42  
   17.43  fun case_result c ctxt =
   17.44    let
   17.45 -    val RuleCases.Case {fixes, ...} = c;
   17.46 +    val Rule_Cases.Case {fixes, ...} = c;
   17.47      val (ts, ctxt') = ctxt |> fold_map fix fixes;
   17.48 -    val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
   17.49 +    val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   17.50    in
   17.51      ctxt'
   17.52      |> bind_terms (map drop_schematic binds)
   17.53 @@ -1292,7 +1292,7 @@
   17.54  fun pretty_cases ctxt =
   17.55    let
   17.56      fun add_case (_, (_, false)) = I
   17.57 -      | add_case (name, (c as RuleCases.Case {fixes, ...}, true)) =
   17.58 +      | add_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
   17.59            cons (name, (fixes, case_result c ctxt));
   17.60      val cases = fold add_case (cases_of ctxt) [];
   17.61    in
    18.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Oct 30 18:33:21 2009 +0100
    18.2 +++ b/src/Pure/Isar/rule_cases.ML	Sun Nov 01 15:24:45 2009 +0100
    18.3 @@ -47,7 +47,7 @@
    18.4    val strict_mutual_rule: Proof.context -> thm list -> int list * thm
    18.5  end;
    18.6  
    18.7 -structure RuleCases: RULE_CASES =
    18.8 +structure Rule_Cases: RULE_CASES =
    18.9  struct
   18.10  
   18.11  (** cases **)
   18.12 @@ -379,5 +379,5 @@
   18.13  
   18.14  end;
   18.15  
   18.16 -structure Basic_Rule_Cases: BASIC_RULE_CASES = RuleCases;
   18.17 +structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
   18.18  open Basic_Rule_Cases;
    19.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Oct 30 18:33:21 2009 +0100
    19.2 +++ b/src/Pure/Isar/rule_insts.ML	Sun Nov 01 15:24:45 2009 +0100
    19.3 @@ -177,7 +177,7 @@
    19.4          else
    19.5            T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
    19.6    in
    19.7 -    Drule.instantiate insts thm |> RuleCases.save thm
    19.8 +    Drule.instantiate insts thm |> Rule_Cases.save thm
    19.9    end;
   19.10  
   19.11  fun read_instantiate_mixed' ctxt (args, concl_args) thm =
    20.1 --- a/src/Pure/Isar/specification.ML	Fri Oct 30 18:33:21 2009 +0100
    20.2 +++ b/src/Pure/Isar/specification.ML	Sun Nov 01 15:24:45 2009 +0100
    20.3 @@ -318,7 +318,7 @@
    20.4            end;
    20.5  
    20.6          val atts = map (Attrib.internal o K)
    20.7 -          [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
    20.8 +          [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];
    20.9          val prems = Assumption.local_prems_of elems_ctxt ctxt;
   20.10          val stmt = [((Binding.empty, atts), [(thesis, [])])];
   20.11  
    21.1 --- a/src/Tools/induct.ML	Fri Oct 30 18:33:21 2009 +0100
    21.2 +++ b/src/Tools/induct.ML	Sun Nov 01 15:24:45 2009 +0100
    21.3 @@ -216,8 +216,8 @@
    21.4  fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
    21.5  fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
    21.6  
    21.7 -val consumes0 = RuleCases.consumes_default 0;
    21.8 -val consumes1 = RuleCases.consumes_default 1;
    21.9 +val consumes0 = Rule_Cases.consumes_default 0;
   21.10 +val consumes1 = Rule_Cases.consumes_default 1;
   21.11  
   21.12  in
   21.13  
   21.14 @@ -344,10 +344,10 @@
   21.15      val thy = ProofContext.theory_of ctxt;
   21.16  
   21.17      fun inst_rule r =
   21.18 -      if null insts then `RuleCases.get r
   21.19 +      if null insts then `Rule_Cases.get r
   21.20        else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
   21.21          |> maps (prep_inst ctxt align_left I)
   21.22 -        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
   21.23 +        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r);
   21.24  
   21.25      val ruleq =
   21.26        (case opt_rule of
   21.27 @@ -359,9 +359,9 @@
   21.28    in
   21.29      fn i => fn st =>
   21.30        ruleq
   21.31 -      |> Seq.maps (RuleCases.consume [] facts)
   21.32 +      |> Seq.maps (Rule_Cases.consume [] facts)
   21.33        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   21.34 -        CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases)
   21.35 +        CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases)
   21.36            (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
   21.37    end;
   21.38  
   21.39 @@ -483,7 +483,7 @@
   21.40            in Logic.list_implies (map rename_asm As, C) end;
   21.41          val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
   21.42          val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
   21.43 -      in [RuleCases.save thm thm'] end
   21.44 +      in [Rule_Cases.save thm thm'] end
   21.45    | special_rename_params _ _ ths = ths;
   21.46  
   21.47  
   21.48 @@ -570,7 +570,7 @@
   21.49        ((fn [] => NONE | ts => List.last ts) #>
   21.50          (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
   21.51          find_inductT ctxt)) [[]]
   21.52 -  |> filter_out (forall RuleCases.is_inner_rule);
   21.53 +  |> filter_out (forall Rule_Cases.is_inner_rule);
   21.54  
   21.55  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   21.56    | get_inductP _ _ = [];
   21.57 @@ -583,29 +583,29 @@
   21.58      val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
   21.59  
   21.60      fun inst_rule (concls, r) =
   21.61 -      (if null insts then `RuleCases.get r
   21.62 +      (if null insts then `Rule_Cases.get r
   21.63         else (align_left "Rule has fewer conclusions than arguments given"
   21.64            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
   21.65          |> maps (prep_inst ctxt align_right (atomize_term thy))
   21.66 -        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
   21.67 +        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
   21.68        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
   21.69  
   21.70      val ruleq =
   21.71        (case opt_rule of
   21.72 -        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
   21.73 +        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
   21.74        | NONE =>
   21.75            (get_inductP ctxt facts @
   21.76              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
   21.77 -          |> map_filter (RuleCases.mutual_rule ctxt)
   21.78 +          |> map_filter (Rule_Cases.mutual_rule ctxt)
   21.79            |> tap (trace_rules ctxt inductN o map #2)
   21.80            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   21.81  
   21.82      fun rule_cases rule =
   21.83 -      RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule);
   21.84 +      Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule);
   21.85    in
   21.86      (fn i => fn st =>
   21.87        ruleq
   21.88 -      |> Seq.maps (RuleCases.consume (flat defs) facts)
   21.89 +      |> Seq.maps (Rule_Cases.consume (flat defs) facts)
   21.90        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   21.91          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   21.92            (CONJUNCTS (ALLGOALS
   21.93 @@ -643,7 +643,7 @@
   21.94  fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
   21.95  
   21.96  fun main_prop_of th =
   21.97 -  if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
   21.98 +  if Rule_Cases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
   21.99  
  21.100  in
  21.101  
  21.102 @@ -652,9 +652,9 @@
  21.103      val thy = ProofContext.theory_of ctxt;
  21.104  
  21.105      fun inst_rule r =
  21.106 -      if null inst then `RuleCases.get r
  21.107 +      if null inst then `Rule_Cases.get r
  21.108        else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
  21.109 -        |> pair (RuleCases.get r);
  21.110 +        |> pair (Rule_Cases.get r);
  21.111  
  21.112      fun ruleq goal =
  21.113        (case opt_rule of
  21.114 @@ -666,12 +666,12 @@
  21.115    in
  21.116      SUBGOAL_CASES (fn (goal, i) => fn st =>
  21.117        ruleq goal
  21.118 -      |> Seq.maps (RuleCases.consume [] facts)
  21.119 +      |> Seq.maps (Rule_Cases.consume [] facts)
  21.120        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  21.121          guess_instance ctxt rule i st
  21.122          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
  21.123          |> Seq.maps (fn rule' =>
  21.124 -          CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
  21.125 +          CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases)
  21.126              (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
  21.127    end;
  21.128  
    22.1 --- a/src/Tools/induct_tacs.ML	Fri Oct 30 18:33:21 2009 +0100
    22.2 +++ b/src/Tools/induct_tacs.ML	Sun Nov 01 15:24:45 2009 +0100
    22.3 @@ -86,9 +86,9 @@
    22.4      val argss = map (map (Option.map induct_var)) varss;
    22.5      val rule =
    22.6        (case opt_rules of
    22.7 -        SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
    22.8 +        SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
    22.9        | NONE =>
   22.10 -          (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
   22.11 +          (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
   22.12              (_, rule) :: _ => rule
   22.13            | [] => raise THM ("No induction rules", 0, [])));
   22.14  
    23.1 --- a/src/Tools/project_rule.ML	Fri Oct 30 18:33:21 2009 +0100
    23.2 +++ b/src/Tools/project_rule.ML	Sun Nov 01 15:24:45 2009 +0100
    23.3 @@ -47,8 +47,8 @@
    23.4          Thm.permute_prems 0 (~ k)
    23.5          #> singleton (Variable.export ctxt' ctxt)
    23.6          #> Drule.zero_var_indexes
    23.7 -        #> RuleCases.save raw_rule
    23.8 -        #> RuleCases.add_consumes k);
    23.9 +        #> Rule_Cases.save raw_rule
   23.10 +        #> Rule_Cases.add_consumes k);
   23.11    in map result is end;
   23.12  
   23.13  fun project ctxt i th = hd (projects ctxt [i] th);
    24.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Oct 30 18:33:21 2009 +0100
    24.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Nov 01 15:24:45 2009 +0100
    24.3 @@ -66,7 +66,7 @@
    24.4  
    24.5    val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
    24.6    val (intr_names, intr_tms) = split_list (map fst intr_specs);
    24.7 -  val case_names = RuleCases.case_names intr_names;
    24.8 +  val case_names = Rule_Cases.case_names intr_names;
    24.9  
   24.10    (*recT and rec_params should agree for all mutually recursive components*)
   24.11    val rec_hds = map head_of rec_tms;