--- a/src/ZF/Datatype.ML Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/Datatype.ML Tue Nov 13 22:20:51 2001 +0100
@@ -59,6 +59,7 @@
fold_bal FOLogic.mk_conj
(map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
+ val datatype_ss = simpset_of (the_context ());
fun proc sg _ old =
let val _ = if !trace then writeln ("data_free: OLD = " ^
@@ -82,7 +83,7 @@
else ();
val goal = Logic.mk_equals (old, new)
val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
- simp_tac (simpset_of Datatype.thy addsimps #free_iffs lcon_info) 1)
+ simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
handle ERROR =>
error ("data_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal)
in Some thm end
--- a/src/ZF/Datatype.thy Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/Datatype.thy Tue Nov 13 22:20:51 2001 +0100
@@ -1,11 +1,13 @@
-(* Title: ZF/Datatype
+(* Title: ZF/Datatype.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations
-
- "Datatype" must be capital to avoid conflicts with ML's "datatype"
+(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
*)
-Datatype = Inductive + Univ + QUniv
+theory Datatype = Inductive + Univ + QUniv
+ files "Tools/datatype_package.ML":
+
+end
+
--- a/src/ZF/Finite.thy Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/Finite.thy Tue Nov 13 22:20:51 2001 +0100
@@ -8,8 +8,6 @@
Finite = Inductive + Nat +
-setup setup_datatypes
-
(*The natural numbers as a datatype*)
rep_datatype
elim natE
--- a/src/ZF/Inductive.thy Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/Inductive.thy Tue Nov 13 22:20:51 2001 +0100
@@ -1,5 +1,20 @@
-(*Dummy theory to document dependencies *)
+(* Title: ZF/Inductive.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
+*)
-Inductive = Fixedpt + mono +
+theory Inductive = Fixedpt + mono
+ files
+ "Tools/cartprod.ML"
+ "Tools/ind_cases.ML"
+ "Tools/inductive_package.ML"
+ "Tools/induct_tacs.ML"
+ "Tools/primrec_package.ML":
+
+setup IndCases.setup
+setup induct_tacs_setup
end
--- a/src/ZF/IsaMakefile Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/IsaMakefile Tue Nov 13 22:20:51 2001 +0100
@@ -43,8 +43,8 @@
OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \
Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML \
Rel.ML Rel.thy Sum.ML Sum.thy \
- Tools/numeral_syntax.ML Tools/cartprod.ML \
- Tools/datatype_package.ML Tools/induct_tacs.ML \
+ Tools/numeral_syntax.ML Tools/cartprod.ML \
+ Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \
Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML \
Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML \
WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy \
@@ -126,13 +126,14 @@
$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
Induct/Comb.ML Induct/Comb.thy Induct/FoldSet.ML Induct/FoldSet.thy \
- Induct/ListN.ML Induct/ListN.thy\
- Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.ML Induct/Mutil.thy\
- Induct/Primrec_defs.ML Induct/Primrec_defs.thy\
- Induct/Primrec.ML Induct/Primrec.thy\
+ Induct/ListN.ML Induct/ListN.thy \
+ Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
+ Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
+ Induct/Primrec.ML Induct/Primrec.thy \
Induct/PropLog.ML Induct/PropLog.thy Induct/Rmap.ML Induct/Rmap.thy
@$(ISATOOL) usedir $(OUT)/ZF Induct
+
## ZF-ex
ZF-ex: ZF $(LOG)/ZF-ex.gz
--- a/src/ZF/ROOT.ML Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/ROOT.ML Tue Nov 13 22:20:51 2001 +0100
@@ -1,35 +1,29 @@
-(* Title: ZF/ROOT
+(* Title: ZF/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
-
-This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
+Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
+This theory is the work of Martin Coen, Philippe Noel and Lawrence
+Paulson.
*)
val banner = "ZF Set Theory (in FOL)";
writeln banner;
-eta_contract:=false;
+reset eta_contract;
print_depth 1;
-(*Add user sections for inductive/datatype definitions*)
-use "thy_syntax";
+(*syntax for old-style theory sections*)
+use "thy_syntax";
use "~~/src/Provers/Arith/cancel_numerals.ML";
use "~~/src/Provers/Arith/combine_numerals.ML";
use_thy "mono";
-use "ind_syntax.ML";
-use "Tools/cartprod.ML";
-use_thy "Fixedpt";
-use "Tools/inductive_package.ML";
-use "Tools/induct_tacs.ML";
-use "Tools/primrec_package.ML";
-use_thy "QUniv";
-use "Tools/datatype_package.ML";
+use "ind_syntax.ML";
+use_thy "Datatype";
use "Tools/numeral_syntax.ML";
(*the all-in-one theory*)
--- 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!)")]];
--- a/src/ZF/Tools/inductive_package.ML Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/Tools/inductive_package.ML Tue Nov 13 22:20:51 2001 +0100
@@ -56,9 +56,6 @@
fun mk_frees a [] = []
| mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
-(*read an assumption in the given theory*)
-fun assume_read thy a = Thm.assume (read_cterm (Theory.sign_of thy) (a,propT));
-
(* add_inductive(_i) *)
@@ -277,16 +274,14 @@
(*Applies freeness of the given constructors, which *must* be unfolded by
the given defs. Cannot simply use the local con_defs because
con_defs=[] for inference systems.
- String s should have the form t:Si where Si is an inductive set*)
- fun mk_cases s =
- rule_by_tactic (basic_elim_tac THEN
- ALLGOALS Asm_full_simp_tac THEN
- basic_elim_tac)
- (assume_read (theory_of_thm elim) s
- (*Don't use thy1: it will be stale*)
- RS elim)
- |> standard;
-
+ Proposition A should have the form t:Si where Si is an inductive set*)
+ fun make_cases ss A =
+ rule_by_tactic
+ (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
+ (Thm.assume A RS elim)
+ |> Drule.standard';
+ fun mk_cases a = make_cases (*delayed evaluation of body!*)
+ (simpset ()) (read_cterm (Thm.sign_of_thm elim) (a, propT));
fun induction_rules raw_induct thy =
let
@@ -527,8 +522,10 @@
|> standard
and mutual_induct = CP.remove_split mutual_induct_fsplit
+ val induct_att =
+ (case rec_names of [name] => [InductAttrib.induct_set_global name] | _ => []);
val (thy', [induct', mutual_induct']) =
- thy |> PureThy.add_thms [(("induct", induct), [InductAttrib.induct_set_global ""]),
+ thy |> PureThy.add_thms [(("induct", induct), induct_att),
(("mutual_induct", mutual_induct), [])];
in (thy', induct', mutual_induct')
end; (*of induction_rules*)
@@ -549,11 +546,11 @@
(("cases", elim), [InductAttrib.cases_set_global ""])]
|>>> (PureThy.add_thmss o map Thm.no_attributes)
[("defs", defs),
- ("intros", intrs)]
- |>> Theory.parent_path;
+ ("intros", intrs)];
val (thy4, intrs'') =
thy3 |> PureThy.add_thms
- (map2 (fn (((bname, _), atts), th) => ((bname, th), atts)) (intr_specs, intrs'));
+ (map2 (fn (((bname, _), atts), th) => ((bname, th), atts)) (intr_specs, intrs'))
+ |>> Theory.parent_path;
in
(thy4,
{defs = defs',