--- 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);