--- a/src/ZF/Tools/induct_tacs.ML Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Tue Nov 13 22:20:51 2001 +0100
@@ -23,7 +23,7 @@
(** Datatype information, e.g. associated theorems **)
type datatype_info =
- {inductive: bool, (*true if inductive, not coinductive*)
+ {inductive: bool, (*true if inductive, not coinductive*)
constructors : term list, (*the constructors, as Consts*)
rec_rewrites : thm list, (*recursor equations*)
case_rewrites : thm list, (*case equations*)
@@ -75,9 +75,6 @@
structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
-val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
-
-
structure DatatypeTactics : DATATYPE_TACTICS =
struct
@@ -90,18 +87,18 @@
(*Given a variable, find the inductive set associated it in the assumptions*)
fun find_tname var Bi =
- let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
+ let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
(v, #1 (dest_Const (head_of A)))
- | mk_pair _ = raise Match
+ | mk_pair _ = raise Match
val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
- (#2 (strip_context Bi))
+ (#2 (strip_context Bi))
in case assoc (pairs, var) of
None => error ("Cannot determine datatype of " ^ quote var)
| Some t => t
end;
-(** generic exhaustion and induction tactic for datatypes
- Differences from HOL:
+(** generic exhaustion and induction tactic for datatypes
+ Differences from HOL:
(1) no checking if the induction var occurs in premises, since it always
appears in one of them, and it's hard to check for other occurrences
(2) exhaustion works for VARIABLES in the premises, not general terms
@@ -112,16 +109,16 @@
val (_, _, Bi, _) = dest_state (state, i)
val {sign, ...} = rep_thm state
val tn = find_tname var Bi
- val rule =
- if exh then #exhaustion (datatype_info_sg sign tn)
- else #induct (datatype_info_sg sign tn)
- val (Const("op :",_) $ Var(ixn,_) $ _) =
+ val rule =
+ if exh then #exhaustion (datatype_info_sg sign tn)
+ else #induct (datatype_info_sg sign tn)
+ val (Const("op :",_) $ Var(ixn,_) $ _) =
(case prems_of rule of
- [] => error "induction is not available for this datatype"
- | major::_ => FOLogic.dest_Trueprop major)
+ [] => error "induction is not available for this datatype"
+ | major::_ => FOLogic.dest_Trueprop major)
val ind_vname = Syntax.string_of_vname ixn
val vname' = (*delete leading question mark*)
- String.substring (ind_vname, 1, size ind_vname-1)
+ String.substring (ind_vname, 1, size ind_vname-1)
in
eres_inst_tac [(vname',var)] rule i state
end;
@@ -140,55 +137,63 @@
(*analyze the LHS of a case equation to get a constructor*)
fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
- Sign.string_of_term sign eqn);
+ Sign.string_of_term sign eqn);
val constructors =
- map (head_of o const_of o FOLogic.dest_Trueprop o
- #prop o rep_thm) case_eqns;
+ map (head_of o const_of o FOLogic.dest_Trueprop o
+ #prop o rep_thm) case_eqns;
val Const ("op :", _) $ _ $ data =
- FOLogic.dest_Trueprop (hd (prems_of elim));
-
+ FOLogic.dest_Trueprop (hd (prems_of elim));
+
val Const(big_rec_name, _) = head_of data;
val simps = case_eqns @ recursor_eqns;
val dt_info =
- {inductive = true,
- constructors = constructors,
- rec_rewrites = recursor_eqns,
- case_rewrites = case_eqns,
- induct = induct,
- mutual_induct = TrueI, (*No need for mutual induction*)
- exhaustion = elim};
+ {inductive = true,
+ constructors = constructors,
+ rec_rewrites = recursor_eqns,
+ case_rewrites = case_eqns,
+ induct = induct,
+ mutual_induct = TrueI, (*No need for mutual induction*)
+ exhaustion = elim};
val con_info =
- {big_rec_name = big_rec_name,
- constructors = constructors,
- (*let primrec handle definition by cases*)
- free_iffs = [], (*thus we expect the necessary freeness rewrites
- to be in the simpset already, as is the case for
- Nat and disjoint sum*)
- rec_rewrites = (case recursor_eqns of
- [] => case_eqns | _ => recursor_eqns)};
+ {big_rec_name = big_rec_name,
+ constructors = constructors,
+ (*let primrec handle definition by cases*)
+ free_iffs = [], (*thus we expect the necessary freeness rewrites
+ to be in the simpset already, as is the case for
+ Nat and disjoint sum*)
+ rec_rewrites = (case recursor_eqns of
+ [] => case_eqns | _ => recursor_eqns)};
(*associate with each constructor the datatype name and rewrites*)
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
in
thy |> Theory.add_path (Sign.base_name big_rec_name)
- |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
- |> DatatypesData.put
- (Symtab.update
- ((big_rec_name, dt_info), DatatypesData.get thy))
- |> ConstructorsData.put
- (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
- |> Theory.parent_path
+ |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
+ |> DatatypesData.put
+ (Symtab.update
+ ((big_rec_name, dt_info), DatatypesData.get thy))
+ |> ConstructorsData.put
+ (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
+ |> Theory.parent_path
end
handle exn => (writeln "Failure in rep_datatype"; raise exn);
end;
-
val exhaust_tac = DatatypeTactics.exhaust_tac;
val induct_tac = DatatypeTactics.induct_tac;
+
+val induct_tacs_setup =
+ [DatatypesData.init,
+ ConstructorsData.init,
+ Method.add_methods
+ [("induct_tac", Method.goal_args Args.name induct_tac,
+ "induct_tac emulation (dynamic instantiation!)"),
+ ("case_tac", Method.goal_args Args.name case_tac,
+ "case_tac emulation (dynamic instantiation!)")]];