tuned auxiliary structures;

--- a/src/Tools/induct.ML	Thu Jun 24 11:28:34 2010 +0200
+++ b/src/Tools/induct.ML	Thu Jun 24 12:16:39 2010 +0200
@@ -4,7 +4,7 @@
 Proof by cases, induction, and coinduction.
 *)
 
-signature INDUCT_DATA =
+signature INDUCT_ARGS =
 sig
   val cases_default: thm
   val atomize: thm list
@@ -82,7 +82,7 @@
   val setup: theory -> theory
 end;
 
-functor Induct(Data: INDUCT_DATA): INDUCT =
+functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
 struct
 
 (** variables -- ordered left-to-right, preferring right **)
@@ -135,7 +135,7 @@
     val l = length (Logic.strip_params t);
     val Hs = Logic.strip_assums_hyp t;
     fun find (i, t) =
-      case Data.dest_def (drop_judgment ctxt t) of
+      case Induct_Args.dest_def (drop_judgment ctxt t) of
         SOME (Bound j, _) => SOME (i, j)
       | SOME (_, Bound j) => SOME (i, j)
       | _ => NONE
@@ -168,13 +168,13 @@
 (* rulify operators around definition *)
 
 fun rulify_defs_conv ctxt ct =
-  if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso
-    not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct))))
+  if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) andalso
+    not (is_some (Induct_Args.dest_def (drop_judgment ctxt (term_of ct))))
   then
     (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
      Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
        (Conv.try_conv (rulify_defs_conv ctxt)) else_conv
-     Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv
+     Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv
        Conv.try_conv (rulify_defs_conv ctxt)) ct
   else Conv.no_conv ct;
 
@@ -203,7 +203,7 @@
 
 (* context data *)
 
-structure InductData = Generic_Data
+structure Data = Generic_Data
 (
   type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset;
   val empty =
@@ -220,7 +220,7 @@
      merge_ss (simpset1, simpset2));
 );
 
-val get_local = InductData.get o Context.Proof;
+val get_local = Data.get o Context.Proof;
 
 fun dest_rules ctxt =
   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
@@ -276,9 +276,9 @@
 local
 
 fun mk_att f g name arg =
-  let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
+  let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
 
-fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
+fun del_att which = Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
   fold Item_Net.remove (filter_rules rs th) rs))));
 
 fun map1 f (x, y, z, s) = (f x, y, z, s);
@@ -310,7 +310,7 @@
 val coinduct_pred = mk_att add_coinductP consumes1;
 val coinduct_del = del_att map3;
 
-fun map_simpset f = InductData.map (map4 f);
+fun map_simpset f = Data.map (map4 f);
 
 fun induct_simp f =
   Thm.declaration_attribute (fn thm => fn context =>
@@ -410,14 +410,14 @@
 
 (* mark equality constraints in cases rule *)
 
-val equal_def' = Thm.symmetric Data.equal_def;
+val equal_def' = Thm.symmetric Induct_Args.equal_def;
 
 fun mark_constraints n ctxt = Conv.fconv_rule
   (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
      (MetaSimplifier.rewrite false [equal_def']))) ctxt));
 
 val unmark_constraints = Conv.fconv_rule
-  (MetaSimplifier.rewrite true [Data.equal_def]);
+  (MetaSimplifier.rewrite true [Induct_Args.equal_def]);
 
 (* simplify *)
 
@@ -425,7 +425,7 @@
   Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)));
 
 fun simplify_conv ctxt ct =
-  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
+  if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then
     (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct
   else Conv.all_conv ct;
 
@@ -437,7 +437,7 @@
 
 fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
 
-val trivial_tac = Data.trivial_tac;
+val trivial_tac = Induct_Args.trivial_tac;
 
 
 
@@ -477,7 +477,7 @@
       (case opt_rule of
         SOME r => Seq.single (inst_rule r)
       | NONE =>
-          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
+          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default])
           |> tap (trace_rules ctxt casesN)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   in
@@ -507,12 +507,12 @@
 (* atomize *)
 
 fun atomize_term thy =
-  MetaSimplifier.rewrite_term thy Data.atomize []
+  MetaSimplifier.rewrite_term thy Induct_Args.atomize []
   #> Object_Logic.drop_judgment thy;
 
-val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
+val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize;
 
-val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
+val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
 
 val inner_atomize_tac =
   Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
@@ -521,8 +521,8 @@
 (* rulify *)
 
 fun rulify_term thy =
-  MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
-  MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
+  MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
+  MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback [];
 
 fun rulified_term thm =
   let
@@ -532,8 +532,8 @@
   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
 
 val rulify_tac =
-  Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
-  Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
+  Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
+  Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN'
   Goal.conjunction_tac THEN_ALL_NEW
   (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);