new inductive, datatype and primrec packages, etc.
--- a/src/ZF/AC.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/AC.thy Mon Dec 28 16:59:28 1998 +0100
@@ -9,6 +9,12 @@
*)
AC = func +
+
+constdefs
+ (*Needs to be visible for Zorn.thy*)
+ increasing :: i=>i
+ "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
+
rules
AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
end
--- a/src/ZF/Bool.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Bool.ML Mon Dec 28 16:59:28 1998 +0100
@@ -24,6 +24,8 @@
by (rtac consI1 1);
qed "bool_0I";
+Addsimps [bool_1I, bool_0I];
+
Goalw bool_defs "1~=0";
by (rtac succ_not_0 1);
qed "one_not_0";
@@ -54,10 +56,16 @@
fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
-Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
+Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
by (bool_tac 1);
qed "cond_type";
+(*For Simp_tac and Blast_tac*)
+Goal "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A";
+by (bool_tac 1);
+qed "cond_simple_type";
+Addsimps [cond_simple_type];
+
val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
by (rewtac rew);
by (rtac cond_1 1);
@@ -89,10 +97,14 @@
"[| a:bool; b:bool |] ==> a or b : bool"
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
+Addsimps [not_type, and_type, or_type];
+
qed_goalw "xor_type" Bool.thy [xor_def]
"[| a:bool; b:bool |] ==> a xor b : bool"
(fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
+Addsimps [xor_type];
+
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type,
or_type, xor_type];
--- a/src/ZF/Datatype.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Datatype.ML Mon Dec 28 16:59:28 1998 +0100
@@ -7,63 +7,41 @@
*)
-(*For most datatypes involving univ*)
-val datatype_intrs =
- [SigmaI, InlI, InrI,
- Pair_in_univ, Inl_in_univ, Inr_in_univ,
- zero_in_univ, A_into_univ, nat_into_univ, UnCI];
-
-(*Needed for mutual recursion*)
-val datatype_elims = [make_elim InlD, make_elim InrD];
+(*Typechecking rules for most datatypes involving univ*)
+structure Data_Arg =
+ struct
+ val intrs =
+ [SigmaI, InlI, InrI,
+ Pair_in_univ, Inl_in_univ, Inr_in_univ,
+ zero_in_univ, A_into_univ, nat_into_univ, UnCI];
-(*For most codatatypes involving quniv*)
-val codatatype_intrs =
- [QSigmaI, QInlI, QInrI,
- QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
- zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
-
-val codatatype_elims = [make_elim QInlD, make_elim QInrD];
-
-signature INDUCTIVE_THMS =
- sig
- val monos : thm list (*monotonicity of each M operator*)
- val type_intrs : thm list (*type-checking intro rules*)
- val type_elims : thm list (*type-checking elim rules*)
+ (*Needed for mutual recursion*)
+ val elims = [make_elim InlD, make_elim InrD];
end;
-functor Data_section_Fun
- (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)
- : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
-struct
-structure Con = Constructor_Fun
- (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
-
-structure Inductive = Ind_section_Fun
- (open Arg;
- val con_defs = Con.con_defs
- val type_intrs = Arg.type_intrs @ datatype_intrs
- val type_elims = Arg.type_elims @ datatype_elims);
-
-open Inductive Con
-end;
+structure Data_Package =
+ Add_datatype_def_Fun
+ (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+ and Su=Standard_Sum
+ and Ind_Package = Ind_Package
+ and Datatype_Arg = Data_Arg);
-functor CoData_section_Fun
- (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)
- : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
-struct
-
-structure Con = Constructor_Fun
- (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
+(*Typechecking rules for most codatatypes involving quniv*)
+structure CoData_Arg =
+ struct
+ val intrs =
+ [QSigmaI, QInlI, QInrI,
+ QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
+ zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
-structure CoInductive = CoInd_section_Fun
- (open Arg;
- val con_defs = Con.con_defs
- val type_intrs = Arg.type_intrs @ codatatype_intrs
- val type_elims = Arg.type_elims @ codatatype_elims);
+ val elims = [make_elim QInlD, make_elim QInrD];
+ end;
-open CoInductive Con
-end;
+structure CoData_Package =
+ Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+ and Su=Quine_Sum
+ and Ind_Package = CoInd_Package
+ and Datatype_Arg = CoData_Arg);
-
--- a/src/ZF/Datatype.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Datatype.thy Mon Dec 28 16:59:28 1998 +0100
@@ -8,7 +8,9 @@
"Datatype" must be capital to avoid conflicts with ML's "datatype"
*)
-Datatype = "constructor" + Inductive + Univ + QUniv +
+Datatype = Inductive + Univ + QUniv +
+
+setup setup_datatypes
end
--- a/src/ZF/Finite.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Finite.thy Mon Dec 28 16:59:28 1998 +0100
@@ -16,7 +16,7 @@
intrs
emptyI "0 : Fin(A)"
consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
- type_intrs "[empty_subsetI, cons_subsetI, PowI]"
+ type_intrs empty_subsetI, cons_subsetI, PowI
type_elims "[make_elim PowD]"
inductive
--- a/src/ZF/Inductive.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Inductive.ML Mon Dec 28 16:59:28 1998 +0100
@@ -56,35 +56,10 @@
end;
-functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
- : sig include INTR_ELIM INDRULE end =
-let
- structure Intr_elim =
- Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and
- Pr=Standard_Prod and Su=Standard_Sum);
-
- structure Indrule =
- Indrule_Fun (structure Inductive=Inductive and
- Pr=Standard_Prod and CP=Standard_CP and
- Su=Standard_Sum and
- Intr_elim=Intr_elim)
-in
- struct
- val thy = Intr_elim.thy
- val defs = Intr_elim.defs
- val bnd_mono = Intr_elim.bnd_mono
- val dom_subset = Intr_elim.dom_subset
- val intrs = Intr_elim.intrs
- val elim = Intr_elim.elim
- val mk_cases = Intr_elim.mk_cases
- open Indrule
- end
-end;
-
-
-structure Ind = Add_inductive_def_Fun
- (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
- and Su=Standard_Sum);
+structure Ind_Package =
+ Add_inductive_def_Fun
+ (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+ and Su=Standard_Sum);
structure Gfp =
@@ -128,34 +103,7 @@
end;
-signature COINDRULE =
- sig
- val coinduct : thm
- end;
-
-
-functor CoInd_section_Fun
- (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
- : sig include INTR_ELIM COINDRULE end =
-let
- structure Intr_elim =
- Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and
- Pr=Quine_Prod and CP=Standard_CP and
- Su=Quine_Sum);
-in
- struct
- val thy = Intr_elim.thy
- val defs = Intr_elim.defs
- val bnd_mono = Intr_elim.bnd_mono
- val dom_subset = Intr_elim.dom_subset
- val intrs = Intr_elim.intrs
- val elim = Intr_elim.elim
- val mk_cases = Intr_elim.mk_cases
- val coinduct = Intr_elim.raw_induct
- end
-end;
-
-structure CoInd =
+structure CoInd_Package =
Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
and Su=Quine_Sum);
--- a/src/ZF/Inductive.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Inductive.thy Mon Dec 28 16:59:28 1998 +0100
@@ -1,5 +1,5 @@
(*Dummy theory to document dependencies *)
-Inductive = Fixedpt + Sum + QPair + "indrule" +
+Inductive = Fixedpt + Sum + QPair +
end
--- a/src/ZF/InfDatatype.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/InfDatatype.ML Mon Dec 28 16:59:28 1998 +0100
@@ -97,4 +97,4 @@
[InfCard_nat, InfCard_nat_Un_cardinal,
Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc,
zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
- Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs;
+ Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs;
--- a/src/ZF/IsaMakefile Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/IsaMakefile Mon Dec 28 16:59:28 1998 +0100
@@ -38,12 +38,12 @@
Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \
Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \
- ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \
- cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \
+ ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML \
domrange.thy equalities.ML equalities.thy func.ML func.thy \
- ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
- intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
- subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \
+ ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
+ subset.thy thy_syntax.ML upair.ML upair.thy \
+ Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \
+ Tools/primrec_package.ML Tools/typechk.ML \
Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy
@$(ISATOOL) usedir -b $(OUT)/FOL ZF
@@ -96,7 +96,7 @@
Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
- Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \
+ Resid/Substitution.ML \
Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
@$(ISATOOL) usedir $(OUT)/ZF Resid
@@ -111,6 +111,7 @@
ex/Enum.thy ex/LList.ML ex/LList.thy \
ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
+ ex/Primrec_defs.ML ex/Primrec_defs.thy \
ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
ex/Term.ML ex/Term.thy ex/misc.ML
--- a/src/ZF/List.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/List.ML Mon Dec 28 16:59:28 1998 +0100
@@ -6,13 +6,8 @@
Datatype definition of Lists
*)
-open List;
-
(*** Aspects of the datatype definition ***)
-Addsimps list.case_eqns;
-
-
(*An elimination rule, for type-checking*)
val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
@@ -61,39 +56,12 @@
\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \
\ |] ==> list_case(c,h,l) : C(l)";
by (rtac (major RS list.induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps list.case_eqns @ prems)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "list_case_type";
-(** For recursion **)
-
-Goalw list.con_defs "rank(a) < rank(Cons(a,l))";
-by (simp_tac rank_ss 1);
-qed "rank_Cons1";
-
-Goalw list.con_defs "rank(l) < rank(Cons(a,l))";
-by (simp_tac rank_ss 1);
-qed "rank_Cons2";
-
-
(*** List functions ***)
-(** hd and tl **)
-
-Goalw [hd_def] "hd(Cons(a,l)) = a";
-by (resolve_tac list.case_eqns 1);
-qed "hd_Cons";
-
-Goalw [tl_def] "tl(Nil) = Nil";
-by (resolve_tac list.case_eqns 1);
-qed "tl_Nil";
-
-Goalw [tl_def] "tl(Cons(a,l)) = l";
-by (resolve_tac list.case_eqns 1);
-qed "tl_Cons";
-
-Addsimps [hd_Cons, tl_Nil, tl_Cons];
-
Goal "l: list(A) ==> tl(l) : list(A)";
by (etac list.elim 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
@@ -126,52 +94,21 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
qed "drop_type";
-(** list_rec -- by Vset recursion **)
-
-Goal "list_rec(Nil,c,h) = c";
-by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (simpset() addsimps list.case_eqns) 1);
-qed "list_rec_Nil";
-Goal "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
-by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps rank_Cons2::list.case_eqns) 1);
-qed "list_rec_Cons";
+(** Type checking -- proved by induction, as usual **)
-Addsimps [list_rec_Nil, list_rec_Cons];
-
-
-(*Type checking -- proved by induction, as usual*)
val prems = Goal
"[| l: list(A); \
\ c: C(Nil); \
\ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
-\ |] ==> list_rec(l,c,h) : C(l)";
+\ |] ==> list_rec(c,h,l) : C(l)";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "list_rec_type";
-(** Versions for use with definitions **)
-
-val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
-by (rewtac rew);
-by (rtac list_rec_Nil 1);
-qed "def_list_rec_Nil";
-
-val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
-by (rewtac rew);
-by (rtac list_rec_Cons 1);
-qed "def_list_rec_Cons";
-
-fun list_recs def = map standard
- ([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
-
(** map **)
-val [map_Nil,map_Cons] = list_recs map_def;
-Addsimps [map_Nil, map_Cons];
-
-val prems = Goalw [map_def]
+val prems = Goalw [get_def thy "map_list"]
"[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
qed "map_type";
@@ -183,30 +120,21 @@
(** length **)
-val [length_Nil,length_Cons] = list_recs length_def;
-Addsimps [length_Nil,length_Cons];
-
-Goalw [length_def]
+Goalw [get_def thy "length_list"]
"l: list(A) ==> length(l) : nat";
by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
qed "length_type";
(** app **)
-val [app_Nil,app_Cons] = list_recs app_def;
-Addsimps [app_Nil, app_Cons];
-
-Goalw [app_def]
+Goalw [get_def thy "op @_list"]
"[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)";
by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
qed "app_type";
(** rev **)
-val [rev_Nil,rev_Cons] = list_recs rev_def;
-Addsimps [rev_Nil,rev_Cons] ;
-
-Goalw [rev_def]
+Goalw [get_def thy "rev_list"]
"xs: list(A) ==> rev(xs) : list(A)";
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
qed "rev_type";
@@ -214,10 +142,7 @@
(** flat **)
-val [flat_Nil,flat_Cons] = list_recs flat_def;
-Addsimps [flat_Nil,flat_Cons];
-
-Goalw [flat_def]
+Goalw [get_def thy "flat_list"]
"ls: list(list(A)) ==> flat(ls) : list(A)";
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
qed "flat_type";
@@ -225,10 +150,7 @@
(** set_of_list **)
-val [set_of_list_Nil,set_of_list_Cons] = list_recs set_of_list_def;
-Addsimps [set_of_list_Nil,set_of_list_Cons];
-
-Goalw [set_of_list_def]
+Goalw [get_def thy "set_of_list_list"]
"l: list(A) ==> set_of_list(l) : Pow(A)";
by (etac list_rec_type 1);
by (ALLGOALS (Blast_tac));
@@ -243,10 +165,7 @@
(** list_add **)
-val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
-Addsimps [list_add_Nil,list_add_Cons];
-
-Goalw [list_add_def]
+Goalw [get_def thy "list_add_list"]
"xs: list(nat) ==> list_add(xs) : nat";
by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
qed "list_add_type";
@@ -256,6 +175,8 @@
[list_rec_type, map_type, map_type2, app_type, length_type,
rev_type, flat_type, list_add_type];
+Addsimps list_typechecks;
+
simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks);
@@ -282,8 +203,8 @@
qed "map_flat";
Goal "l: list(A) ==> \
-\ list_rec(map(h,l), c, d) = \
-\ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
+\ list_rec(c, d, map(h,l)) = \
+\ list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)";
by (list_ind_tac "l" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "list_rec_map";
--- a/src/ZF/List.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/List.thy Mon Dec 28 16:59:28 1998 +0100
@@ -29,42 +29,54 @@
"[]" == "Nil"
-constdefs
+consts
+ length :: i=>i
hd :: i=>i
- "hd(l) == list_case(0, %x xs. x, l)"
+ tl :: i=>i
+ map :: [i=>i, i] => i
+ set_of_list :: i=>i
+ "@" :: [i,i]=>i (infixr 60)
+ rev :: i=>i
+ flat :: i=>i
+ list_add :: i=>i
+
+primrec
+ "length([]) = 0"
+ "length(Cons(a,l)) = succ(length(l))"
- tl :: i=>i
- "tl(l) == list_case(Nil, %x xs. xs, l)"
+primrec
+ "hd(Cons(a,l)) = a"
+
+primrec
+ "tl([]) = []"
+ "tl(Cons(a,l)) = l"
+
+primrec
+ "map(f,[]) = []"
+ "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
+
+primrec
+ "set_of_list([]) = 0"
+ "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
+
+primrec
+ "[] @ ys = ys"
+ "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
+primrec
+ "rev([]) = []"
+ "rev(Cons(a,l)) = rev(l) @ [a]"
+
+primrec
+ "flat([]) = []"
+ "flat(Cons(l,ls)) = l @ flat(ls)"
+
+primrec
+ "list_add([]) = 0"
+ "list_add(Cons(a,l)) = a #+ list_add(l)"
+
+constdefs
drop :: [i,i]=>i
"drop(i,l) == rec(i, l, %j r. tl(r))"
- list_rec :: [i, i, [i,i,i]=>i] => i
- "list_rec(l,c,h) == Vrec(l, %l g. list_case(c, %x xs. h(x, xs, g`xs), l))"
-
- map :: [i=>i, i] => i
- "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))"
-
- length :: i=>i
- "length(l) == list_rec(l, 0, %x xs r. succ(r))"
-
- set_of_list :: i=>i
- "set_of_list(l) == list_rec(l, 0, %x xs r. cons(x,r))"
-
-consts (*Cannot use constdefs because @ is not an identifier*)
- "@" :: [i,i]=>i (infixr 60)
-defs
- app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))"
-
-
-constdefs
- rev :: i=>i
- "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])"
-
- flat :: i=>i
- "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)"
-
- list_add :: i=>i
- "list_add(l) == list_rec(l, 0, %x xs r. x#+r)"
-
end
--- a/src/ZF/Perm.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Perm.ML Mon Dec 28 16:59:28 1998 +0100
@@ -71,7 +71,7 @@
Goal "[| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
by (asm_simp_tac (simpset() addsimps [inj_def]) 1);
-by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1);
+by (blast_tac (claset() addIs [subst_context RS box_equals]) 1);
bind_thm ("f_imp_injective", ballI RSN (2,result()));
val prems = Goal
--- a/src/ZF/ROOT.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/ROOT.ML Mon Dec 28 16:59:28 1998 +0100
@@ -30,12 +30,22 @@
print_depth 1;
(*Add user sections for inductive/datatype definitions*)
-use "$ISABELLE_HOME/src/Pure/section_utils.ML";
-use "thy_syntax.ML";
+use "$ISABELLE_HOME/src/Pure/section_utils";
+use "thy_syntax";
use_thy "Let";
use_thy "func";
-use "typechk.ML";
+use "Tools/typechk";
+use_thy "mono";
+use "ind_syntax";
+use "Tools/cartprod";
+use_thy "Fixedpt";
+use "Tools/inductive_package";
+use_thy "Inductive";
+use_thy "QUniv";
+use "Tools/datatype_package";
+use "Tools/primrec_package";
+use_thy "Datatype";
use_thy "InfDatatype";
use_thy "List";
--- a/src/ZF/Univ.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Univ.ML Mon Dec 28 16:59:28 1998 +0100
@@ -513,6 +513,20 @@
by (rtac Vrec 1);
qed "def_Vrec";
+(*NOT SUITABLE FOR REWRITING: recursive!*)
+Goalw [Vrecursor_def]
+ "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x), a)";
+by (stac transrec 1);
+by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta,
+ VsetI RS beta, le_refl]) 1);
+qed "Vrecursor";
+
+(*This form avoids giant explosions in proofs. NOTE USE OF == *)
+Goal "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x), a)";
+by (Asm_simp_tac 1);
+by (rtac Vrecursor 1);
+qed "def_Vrecursor";
+
(*** univ(A) ***)
--- a/src/ZF/Univ.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Univ.thy Mon Dec 28 16:59:28 1998 +0100
@@ -19,6 +19,7 @@
Vfrom :: [i,i]=>i
Vset :: i=>i
Vrec :: [i, [i,i]=>i] =>i
+ Vrecursor :: [[i,i]=>i, i] =>i
univ :: i=>i
translations
@@ -33,6 +34,10 @@
"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
+ Vrecursor_def
+ "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
+ H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
+
univ_def "univ(A) == Vfrom(A,nat)"
end
--- a/src/ZF/Zorn.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Zorn.ML Mon Dec 28 16:59:28 1998 +0100
@@ -9,8 +9,6 @@
Classical Theorems of Set Theory.
*)
-open Zorn;
-
(*** Section 1. Mathematical Preamble ***)
Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
--- a/src/ZF/Zorn.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Zorn.thy Mon Dec 28 16:59:28 1998 +0100
@@ -15,13 +15,11 @@
consts
Subset_rel :: i=>i
- increasing :: i=>i
chain, maxchain :: i=>i
super :: [i,i]=>i
defs
Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
- increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
chain_def "chain(A) == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
super_def "super(A,c) == {d: chain(A). c<=d & c~=d}"
@@ -44,8 +42,8 @@
Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
- monos "[Pow_mono]"
- con_defs "[increasing_def]"
+ monos Pow_mono
+ con_defs increasing_def
type_intrs "[CollectD1 RS apply_funtype, Union_in_Pow]"
end
--- a/src/ZF/add_ind_def.ML Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,270 +0,0 @@
-(* Title: ZF/add_ind_def.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Fixedpoint definition module -- for Inductive/Coinductive Definitions
-
-Features:
-* least or greatest fixedpoints
-* user-specified product and sum constructions
-* mutually recursive definitions
-* definitions involving arbitrary monotone operators
-* automatically proves introduction and elimination rules
-
-The recursive sets must *already* be declared as constants in parent theory!
-
- Introduction rules have the form
- [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
- where M is some monotone operator (usually the identity)
- P(x) is any (non-conjunctive) side condition on the free variables
- ti, t are any terms
- Sj, Sk are two of the sets being defined in mutual recursion
-
-Sums are used only for mutual recursion;
-Products are used only to derive "streamlined" induction rules for relations
-*)
-
-signature FP = (** Description of a fixed point operator **)
- sig
- val oper : term (*fixed point operator*)
- val bnd_mono : term (*monotonicity predicate*)
- val bnd_monoI : thm (*intro rule for bnd_mono*)
- val subs : thm (*subset theorem for fp*)
- val Tarski : thm (*Tarski's fixed point theorem*)
- val induct : thm (*induction/coinduction rule*)
- end;
-
-signature SU = (** Description of a disjoint sum **)
- sig
- val sum : term (*disjoint sum operator*)
- val inl : term (*left injection*)
- val inr : term (*right injection*)
- val elim : term (*case operator*)
- val case_inl : thm (*inl equality rule for case*)
- val case_inr : thm (*inr equality rule for case*)
- val inl_iff : thm (*injectivity of inl, using <->*)
- val inr_iff : thm (*injectivity of inr, using <->*)
- val distinct : thm (*distinctness of inl, inr using <->*)
- val distinct' : thm (*distinctness of inr, inl using <->*)
- val free_SEs : thm list (*elim rules for SU, and pair_iff!*)
- end;
-
-signature ADD_INDUCTIVE_DEF =
- sig
- val add_fp_def_i : term list * term * term list -> theory -> theory
- val add_constructs_def :
- string list * ((string*typ*mixfix) *
- string * term list * term list) list list ->
- theory -> theory
- end;
-
-
-
-(*Declares functions to add fixedpoint/constructor defs to a theory*)
-functor Add_inductive_def_Fun
- (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)
- : ADD_INDUCTIVE_DEF =
-struct
-open Logic Ind_Syntax;
-
-(*internal version*)
-fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy =
- let
- val dummy = (*has essential ancestors?*)
- Theory.requires thy "Inductive" "(co)inductive definitions"
-
- val sign = sign_of thy;
-
- (*recT and rec_params should agree for all mutually recursive components*)
- val rec_hds = map head_of rec_tms;
-
- val dummy = assert_all is_Const rec_hds
- (fn t => "Recursive set not previously declared as constant: " ^
- Sign.string_of_term sign t);
-
- (*Now we know they are all Consts, so get their names, type and params*)
- val rec_names = map (#1 o dest_Const) rec_hds
- and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
-
- val rec_base_names = map Sign.base_name rec_names;
- val dummy = assert_all Syntax.is_identifier rec_base_names
- (fn a => "Base name of recursive set not an identifier: " ^ a);
-
- local (*Checking the introduction rules*)
- val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
- fun intr_ok set =
- case head_of set of Const(a,recT) => a mem rec_names | _ => false;
- in
- val dummy = assert_all intr_ok intr_sets
- (fn t => "Conclusion of rule does not name a recursive set: " ^
- Sign.string_of_term sign t);
- end;
-
- val dummy = assert_all is_Free rec_params
- (fn t => "Param in recursion term not a free variable: " ^
- Sign.string_of_term sign t);
-
- (*** Construct the lfp definition ***)
- val mk_variant = variant (foldr add_term_names (intr_tms,[]));
-
- val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
-
- fun dest_tprop (Const("Trueprop",_) $ P) = P
- | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
- Sign.string_of_term sign Q);
-
- (*Makes a disjunct from an introduction rule*)
- fun lfp_part intr = (*quantify over rule's free vars except parameters*)
- let val prems = map dest_tprop (strip_imp_prems intr)
- val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
- val exfrees = term_frees intr \\ rec_params
- val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
- in foldr FOLogic.mk_exists
- (exfrees, fold_bal (app FOLogic.conj) (zeq::prems))
- end;
-
- (*The Part(A,h) terms -- compose injections to make h*)
- fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
- | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);
-
- (*Access to balanced disjoint sums via injections*)
- val parts =
- map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
- (length rec_tms));
-
- (*replace each set by the corresponding Part(A,h)*)
- val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
-
- val lfp_abs = absfree(X', iT,
- mk_Collect(z', dom_sum,
- fold_bal (app FOLogic.disj) part_intrs));
-
- val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
-
- val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
- "Illegal occurrence of recursion operator")
- rec_hds;
-
- (*** Make the new theory ***)
-
- (*A key definition:
- If no mutual recursion then it equals the one recursive set.
- If mutual recursion then it differs from all the recursive sets. *)
- val big_rec_base_name = space_implode "_" rec_base_names;
- val big_rec_name = Sign.intern_const sign big_rec_base_name;
-
- (*Big_rec... is the union of the mutually recursive sets*)
- val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
-
- (*The individual sets must already be declared*)
- val axpairs = map Logic.mk_defpair
- ((big_rec_tm, lfp_rhs) ::
- (case parts of
- [_] => [] (*no mutual recursion*)
- | _ => rec_tms ~~ (*define the sets as Parts*)
- map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
-
- (*tracing: print the fixedpoint definition*)
- val _ = if !Ind_Syntax.trace then
- seq (writeln o Sign.string_of_term sign o #2) axpairs
- else ()
-
- in thy |> PureThy.add_defs_i (map Attribute.none axpairs) end
-
-
-(*Expects the recursive sets to have been defined already.
- con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
-fun add_constructs_def (rec_base_names, con_ty_lists) thy =
- let
- val dummy = (*has essential ancestors?*)
- Theory.requires thy "Datatype" "(co)datatype definitions";
-
- val sign = sign_of thy;
- val full_name = Sign.full_name sign;
-
- val dummy = writeln" Defining the constructor functions...";
- val case_name = "f"; (*name for case variables*)
-
-
- (** Define the constructors **)
-
- (*The empty tuple is 0*)
- fun mk_tuple [] = Const("0",iT)
- | mk_tuple args = foldr1 (app Pr.pair) args;
-
- fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
-
- val npart = length rec_base_names; (*total # of mutually recursive parts*)
-
- (*Make constructor definition; kpart is # of this mutually recursive part*)
- fun mk_con_defs (kpart, con_ty_list) =
- let val ncon = length con_ty_list (*number of constructors*)
- fun mk_def (((id,T,syn), name, args, prems), kcon) =
- (*kcon is index of constructor*)
- mk_defpair (list_comb (Const (full_name name, T), args),
- mk_inject npart kpart
- (mk_inject ncon kcon (mk_tuple args)))
- in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
-
- (** Define the case operator **)
-
- (*Combine split terms using case; yields the case operator for one part*)
- fun call_case case_list =
- let fun call_f (free,[]) = Abs("null", iT, free)
- | call_f (free,args) =
- CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
- Ind_Syntax.iT
- free
- in fold_bal (app Su.elim) (map call_f case_list) end;
-
- (** Generating function variables for the case definition
- Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
-
- (*Treatment of a single constructor*)
- fun add_case (((_, T, _), name, args, prems), (opno, cases)) =
- if Syntax.is_identifier name then
- (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases)
- else
- (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
-
- (*Treatment of a list of constructors, for one part*)
- fun add_case_list (con_ty_list, (opno, case_lists)) =
- let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
- in (opno', case_list :: case_lists) end;
-
- (*Treatment of all parts*)
- val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
-
- val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
-
- val big_rec_base_name = space_implode "_" rec_base_names;
- val big_case_base_name = big_rec_base_name ^ "_case";
- val big_case_name = full_name big_case_base_name;
-
- (*The list of all the function variables*)
- val big_case_args = flat (map (map #1) case_lists);
-
- val big_case_tm =
- list_comb (Const (big_case_name, big_case_typ), big_case_args);
-
- val big_case_def = mk_defpair
- (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
-
-
- (* Build the new theory *)
-
- val const_decs =
- (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
-
- val axpairs =
- big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists));
-
- in
- thy
- |> Theory.add_consts_i const_decs
- |> PureThy.add_defs_i (map Attribute.none axpairs)
- end;
-
-
-end;
--- a/src/ZF/add_ind_def.thy Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-add_ind_def = Fixedpt + "ind_syntax" + "cartprod"
--- a/src/ZF/cartprod.ML Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(* Title: ZF/cartprod.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Syntactic operations for Cartesian Products
-*)
-
-signature PR = (** Description of a Cartesian product **)
- sig
- val sigma : term (*Cartesian product operator*)
- val pair : term (*pairing operator*)
- val split_name : string (*name of polymorphic split*)
- val pair_iff : thm (*injectivity of pairing, using <->*)
- val split_eq : thm (*equality rule for split*)
- val fsplitI : thm (*intro rule for fsplit*)
- val fsplitD : thm (*destruct rule for fsplit*)
- val fsplitE : thm (*elim rule; apparently never used*)
- end;
-
-signature CARTPROD = (** Derived syntactic functions for produts **)
- sig
- val ap_split : typ -> typ -> term -> term
- val factors : typ -> typ list
- val mk_prod : typ * typ -> typ
- val mk_tuple : term -> typ -> term list -> term
- val pseudo_type : term -> typ
- val remove_split : thm -> thm
- val split_const : typ -> term
- val split_rule_var : term * typ * thm -> thm
- end;
-
-
-functor CartProd_Fun (Pr: PR) : CARTPROD =
-struct
-
-(* Some of these functions expect "pseudo-types" containing products,
- as in HOL; the true ZF types would just be "i" *)
-
-fun mk_prod (T1,T2) = Type("*", [T1,T2]);
-
-(*Bogus product type underlying a (possibly nested) Sigma.
- Lets us share HOL code*)
-fun pseudo_type (t $ A $ Abs(_,_,B)) =
- if t = Pr.sigma then mk_prod(pseudo_type A, pseudo_type B)
- else Ind_Syntax.iT
- | pseudo_type _ = Ind_Syntax.iT;
-
-(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
-fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
- | factors T = [T];
-
-(*Make a well-typed instance of "split"*)
-fun split_const T = Const(Pr.split_name,
- [[Ind_Syntax.iT, Ind_Syntax.iT]--->T,
- Ind_Syntax.iT] ---> T);
-
-(*In ap_split S T u, term u expects separate arguments for the factors of S,
- with result type T. The call creates a new term expecting one argument
- of type S.*)
-fun ap_split (Type("*", [T1,T2])) T3 u =
- split_const T3 $
- Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
- ap_split T2 T3
- ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
- Bound 0))
- | ap_split T T3 u = u;
-
-(*Makes a nested tuple from a list, following the product type structure*)
-fun mk_tuple pair (Type("*", [T1,T2])) tms =
- pair $ (mk_tuple pair T1 tms)
- $ (mk_tuple pair T2 (drop (length (factors T1), tms)))
- | mk_tuple pair T (t::_) = t;
-
-(*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [Pr.split_eq];
-
-(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
-fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
- let val T' = factors T1 ---> T2
- val newt = ap_split T1 T2 (Var(v,T'))
- val cterm = Thm.cterm_of (#sign(rep_thm rl))
- in
- remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
- cterm newt)]) rl)
- end
- | split_rule_var (t,T,rl) = rl;
-
-end;
-
--- a/src/ZF/cartprod.thy Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-cartprod = "ind_syntax"
--- a/src/ZF/constructor.ML Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-(* Title: ZF/constructor.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Constructor function module -- for (Co)Datatype Definitions
-*)
-
-signature CONSTRUCTOR_ARG =
- sig
- val thy : theory (*parent containing constructor defs*)
- val big_rec_name : string (*name of mutually recursive set*)
- val con_ty_lists : ((string*typ*mixfix) *
- string * term list * term list) list list
- (*description of constructors*)
- end;
-
-signature CONSTRUCTOR_RESULT =
- sig
- val con_defs : thm list (*definitions made in thy*)
- val case_eqns : thm list (*equations for case operator*)
- val free_iffs : thm list (*freeness rewrite rules*)
- val free_SEs : thm list (*freeness destruct rules*)
- val mk_free : string -> thm (*makes freeness theorems*)
- end;
-
-
-(*Proves theorems relating to constructors*)
-functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
- Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
-let
-
-(*1st element is the case definition; others are the constructors*)
-val big_case_name = Const.big_rec_name ^ "_case";
-
-val con_defs = get_def Const.thy big_case_name ::
- map (get_def Const.thy o #2) (flat Const.con_ty_lists);
-
-(** Prove the case theorem **)
-
-(*Get the case term from its definition*)
-val Const("==",_) $ big_case_tm $ _ =
- hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
-
-val (_, big_case_args) = strip_comb big_case_tm;
-
-(*Each equation has the form
- rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
-fun mk_case_equation (((id,T,syn), name, args, prems), case_free) =
- FOLogic.mk_Trueprop
- (FOLogic.mk_eq
- (big_case_tm $
- (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T),
- args)),
- list_comb (case_free, args)));
-
-val case_trans = hd con_defs RS Ind_Syntax.def_trans
-and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
-
-(*Proves a single case equation. Could use simp_tac, but it's slower!*)
-fun case_tacsf con_def _ =
- [rewtac con_def,
- rtac case_trans 1,
- REPEAT (resolve_tac [refl, split_trans,
- Su.case_inl RS trans,
- Su.case_inr RS trans] 1)];
-
-fun prove_case_equation (arg,con_def) =
- prove_goalw_cterm []
- (cterm_of (sign_of Const.thy) (mk_case_equation arg))
- (case_tacsf con_def);
-
-val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
-
-in
- struct
- val con_defs = con_defs
-
- val free_iffs = con_iffs @
- [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
-
- val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
-
- (*Typical theorems have the form ~con1=con2, con1=con2==>False,
- con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
- fun mk_free s =
- prove_goalw Const.thy con_defs s
- (fn prems => [cut_facts_tac prems 1,
- fast_tac (ZF_cs addSEs free_SEs) 1]);
-
- val case_eqns = map prove_case_equation
- (flat Const.con_ty_lists ~~ big_case_args ~~ tl con_defs);
- end
-end;
-
-
--- a/src/ZF/constructor.thy Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-constructor = "intr_elim"
--- a/src/ZF/ind_syntax.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/ind_syntax.ML Mon Dec 28 16:59:28 1998 +0100
@@ -15,6 +15,10 @@
(*Print tracing messages during processing of "inductive" theory sections*)
val trace = ref false;
+fun traceIt msg ct =
+ if !trace then (writeln (msg ^ string_of_cterm ct); ct)
+ else ct;
+
(** Abstract syntax definitions for ZF **)
val iT = Type("i",[]);
@@ -29,6 +33,10 @@
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
+val apply_const = Const("op `", [iT,iT]--->iT);
+
+val Vrecursor_const = Const("Vrecursor", [[iT,iT]--->iT, iT]--->iT);
+
val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
@@ -60,6 +68,11 @@
(** For datatype definitions **)
+(*Constructor name, type, mixfix info;
+ internal name from mixfix, datatype sets, full premises*)
+type constructor_spec =
+ ((string * typ * mixfix) * string * term list * term list);
+
fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
| dest_mem _ = error "Constructor specifications must have the form x:A";
@@ -103,8 +116,8 @@
(*Previously these both did replicate (length rec_tms); however now
[q]univ itself constitutes the sum domain for mutual recursion!*)
-fun data_domain rec_tms = univ $ union_params (hd rec_tms);
-fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
+fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
+ | data_domain true rec_tms = quniv $ union_params (hd rec_tms);
(*Could go to FOL, but it's hardly general*)
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
@@ -128,5 +141,3 @@
end;
-
-val trace_induct = Ind_Syntax.trace;
--- a/src/ZF/ind_syntax.thy Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-ind_syntax = "mono"
--- a/src/ZF/indrule.ML Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-(* Title: ZF/indrule.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Induction rule module -- for Inductive/Coinductive Definitions
-
-Proves a strong induction rule and a mutual induction rule
-*)
-
-signature INDRULE =
- sig
- val induct : thm (*main induction rule*)
- val mutual_induct : thm (*mutual induction rule*)
- end;
-
-
-functor Indrule_Fun
- (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
- and Pr: PR and CP: CARTPROD and Su : SU and
- Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE =
-let
-
-val sign = sign_of Inductive.thy;
-
-val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
-
-val big_rec_name =
- Sign.intern_const sign (space_implode "_" (map Sign.base_name Intr_elim.rec_names));
-
-val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
-
-val _ = writeln " Proving the induction rule...";
-
-(*** Prove the main induction rule ***)
-
-val pred_name = "P"; (*name for predicate variables*)
-
-val big_rec_def::part_rec_defs = Intr_elim.defs;
-
-(*Used to make induction rules;
- ind_alist = [(rec_tm1,pred1),...] -- associates predicates with rec ops
- prem is a premise of an intr rule*)
-fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
- (Const("op :",_)$t$X), iprems) =
- (case gen_assoc (op aconv) (ind_alist, X) of
- Some pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
- | None => (*possibly membership in M(rec_tm), for M monotone*)
- let fun mk_sb (rec_tm,pred) =
- (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
- in subst_free (map mk_sb ind_alist) prem :: iprems end)
- | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
-
-(*Make a premise of the induction rule.*)
-fun induct_prem ind_alist intr =
- let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
- val iprems = foldr (add_induct_prem ind_alist)
- (Logic.strip_imp_prems intr,[])
- val (t,X) = Ind_Syntax.rule_concl intr
- val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
- val concl = FOLogic.mk_Trueprop (pred $ t)
- in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
- handle Bind => error"Recursion term not found in conclusion";
-
-(*Minimizes backtracking by delivering the correct premise to each goal.
- Intro rules with extra Vars in premises still cause some backtracking *)
-fun ind_tac [] 0 = all_tac
- | ind_tac(prem::prems) i =
- DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
- ind_tac prems (i-1);
-
-val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
-
-val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms))
- Inductive.intr_tms;
-
-val _ = if !Ind_Syntax.trace then
- (writeln "ind_prems = ";
- seq (writeln o Sign.string_of_term sign) ind_prems;
- writeln "raw_induct = "; print_thm Intr_elim.raw_induct)
- else ();
-
-
-(*We use a MINIMAL simpset because others (such as FOL_ss) contain too many
- simplifications. If the premises get simplified, then the proofs could
- fail. *)
-val min_ss = empty_ss
- setmksimps (map mk_eq o ZF_atomize o gen_all)
- setSolver (fn prems => resolve_tac (triv_rls@prems)
- ORELSE' assume_tac
- ORELSE' etac FalseE);
-
-val quant_induct =
- prove_goalw_cterm part_rec_defs
- (cterm_of sign
- (Logic.list_implies (ind_prems,
- FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
- (fn prems =>
- [rtac (impI RS allI) 1,
- DETERM (etac Intr_elim.raw_induct 1),
- (*Push Part inside Collect*)
- full_simp_tac (min_ss addsimps [Part_Collect]) 1,
- (*This CollectE and disjE separates out the introduction rules*)
- REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
- (*Now break down the individual cases. No disjE here in case
- some premise involves disjunction.*)
- REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]
- ORELSE' hyp_subst_tac)),
- ind_tac (rev prems) (length prems) ]);
-
-val _ = if !Ind_Syntax.trace then
- (writeln "quant_induct = "; print_thm quant_induct)
- else ();
-
-
-(*** Prove the simultaneous induction rule ***)
-
-(*Make distinct predicates for each inductive set*)
-
-(*The components of the element type, several if it is a product*)
-val elem_type = CP.pseudo_type Inductive.dom_sum;
-val elem_factors = CP.factors elem_type;
-val elem_frees = mk_frees "za" elem_factors;
-val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
-
-(*Given a recursive set and its domain, return the "fsplit" predicate
- and a conclusion for the simultaneous induction rule.
- NOTE. This will not work for mutually recursive predicates. Previously
- a summand 'domt' was also an argument, but this required the domain of
- mutual recursion to invariably be a disjoint sum.*)
-fun mk_predpair rec_tm =
- let val rec_name = (#1 o dest_Const o head_of) rec_tm
- val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
- elem_factors ---> FOLogic.oT)
- val qconcl =
- foldr FOLogic.mk_all
- (elem_frees,
- FOLogic.imp $
- (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
- $ (list_comb (pfree, elem_frees)))
- in (CP.ap_split elem_type FOLogic.oT pfree,
- qconcl)
- end;
-
-val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
-
-(*Used to form simultaneous induction lemma*)
-fun mk_rec_imp (rec_tm,pred) =
- FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $
- (pred $ Bound 0);
-
-(*To instantiate the main induction rule*)
-val induct_concl =
- FOLogic.mk_Trueprop
- (Ind_Syntax.mk_all_imp
- (big_rec_tm,
- Abs("z", Ind_Syntax.iT,
- fold_bal (app FOLogic.conj)
- (ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
-and mutual_induct_concl =
- FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls);
-
-val _ = if !Ind_Syntax.trace then
- (writeln ("induct_concl = " ^
- Sign.string_of_term sign induct_concl);
- writeln ("mutual_induct_concl = " ^
- Sign.string_of_term sign mutual_induct_concl))
- else ();
-
-
-val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
- resolve_tac [allI, impI, conjI, Part_eqI],
- dresolve_tac [spec, mp, Pr.fsplitD]];
-
-val need_mutual = length Intr_elim.rec_names > 1;
-
-val lemma = (*makes the link between the two induction rules*)
- if need_mutual then
- (writeln " Proving the mutual induction rule...";
- prove_goalw_cterm part_rec_defs
- (cterm_of sign (Logic.mk_implies (induct_concl,
- mutual_induct_concl)))
- (fn prems =>
- [cut_facts_tac prems 1,
- REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
- lemma_tac 1)]))
- else (writeln " [ No mutual induction rule needed ]";
- TrueI);
-
-val _ = if !Ind_Syntax.trace then
- (writeln "lemma = "; print_thm lemma)
- else ();
-
-
-(*Mutual induction follows by freeness of Inl/Inr.*)
-
-(*Simplification largely reduces the mutual induction rule to the
- standard rule*)
-val mut_ss =
- min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
-
-val all_defs = Inductive.con_defs @ part_rec_defs;
-
-(*Removes Collects caused by M-operators in the intro rules. It is very
- hard to simplify
- list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))})
- where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}).
- Instead the following rules extract the relevant conjunct.
-*)
-val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos
- RLN (2,[rev_subsetD]);
-
-(*Minimizes backtracking by delivering the correct premise to each goal*)
-fun mutual_ind_tac [] 0 = all_tac
- | mutual_ind_tac(prem::prems) i =
- DETERM
- (SELECT_GOAL
- (
- (*Simplify the assumptions and goal by unfolding Part and
- using freeness of the Sum constructors; proves all but one
- conjunct by contradiction*)
- rewrite_goals_tac all_defs THEN
- simp_tac (mut_ss addsimps [Part_iff]) 1 THEN
- IF_UNSOLVED (*simp_tac may have finished it off!*)
- ((*simplify assumptions*)
- (*some risk of excessive simplification here -- might have
- to identify the bare minimum set of rewrites*)
- full_simp_tac
- (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1
- THEN
- (*unpackage and use "prem" in the corresponding place*)
- REPEAT (rtac impI 1) THEN
- rtac (rewrite_rule all_defs prem) 1 THEN
- (*prem must not be REPEATed below: could loop!*)
- DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE'
- eresolve_tac (conjE::mp::cmonos))))
- ) i)
- THEN mutual_ind_tac prems (i-1);
-
-val mutual_induct_fsplit =
- if need_mutual then
- prove_goalw_cterm []
- (cterm_of sign
- (Logic.list_implies
- (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms,
- mutual_induct_concl)))
- (fn prems =>
- [rtac (quant_induct RS lemma) 1,
- mutual_ind_tac (rev prems) (length prems)])
- else TrueI;
-
-(** Uncurrying the predicate in the ordinary induction rule **)
-
-(*instantiate the variable to a tuple, if it is non-trivial, in order to
- allow the predicate to be "opened up".
- The name "x.1" comes from the "RS spec" !*)
-val inst =
- case elem_frees of [_] => I
- | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)),
- cterm_of sign elem_tuple)]);
-
-(*strip quantifier and the implication*)
-val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
-
-val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0
-
-in
- struct
- (*strip quantifier*)
- val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
- |> standard;
-
- (*Just "True" unless there's true mutual recursion. This saves storage.*)
- val mutual_induct = CP.remove_split mutual_induct_fsplit
- end
-end;
--- a/src/ZF/indrule.thy Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-indrule = "ind_syntax" + "cartprod" + "intr_elim"
--- a/src/ZF/intr_elim.ML Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,165 +0,0 @@
-(* Title: ZF/intr_elim.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Introduction/elimination rule module -- for Inductive/Coinductive Definitions
-*)
-
-signature INDUCTIVE_ARG = (** Description of a (co)inductive def **)
- sig
- val thy : theory (*new theory with inductive defs*)
- val monos : thm list (*monotonicity of each M operator*)
- val con_defs : thm list (*definitions of the constructors*)
- val type_intrs : thm list (*type-checking intro rules*)
- val type_elims : thm list (*type-checking elim rules*)
- end;
-
-
-signature INDUCTIVE_I = (** Terms read from the theory section **)
- sig
- val rec_tms : term list (*the recursive sets*)
- val dom_sum : term (*their common domain*)
- val intr_tms : term list (*terms for the introduction rules*)
- end;
-
-signature INTR_ELIM =
- sig
- val thy : theory (*copy of input theory*)
- val defs : thm list (*definitions made in thy*)
- val bnd_mono : thm (*monotonicity for the lfp definition*)
- val dom_subset : thm (*inclusion of recursive set in dom*)
- val intrs : thm list (*introduction rules*)
- val elim : thm (*case analysis theorem*)
- val mk_cases : thm list -> string -> thm (*generates case theorems*)
- end;
-
-signature INTR_ELIM_AUX = (** Used to make induction rules **)
- sig
- val raw_induct : thm (*raw induction rule from Fp.induct*)
- val rec_names : string list (*names of recursive sets*)
- end;
-
-(*prove intr/elim rules for a fixedpoint definition*)
-functor Intr_elim_Fun
- (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
- and Fp: FP and Pr : PR and Su : SU)
- : sig include INTR_ELIM INTR_ELIM_AUX end =
-let
-
-val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
-val big_rec_base_name = space_implode "_" (map Sign.base_name rec_names);
-
-val _ = deny (big_rec_base_name mem (Sign.stamp_names_of (sign_of Inductive.thy)))
- ("Definition " ^ big_rec_base_name ^
- " would clash with the theory of the same name!");
-
-(*fetch fp definitions from the theory*)
-val big_rec_def::part_rec_defs =
- map (get_def Inductive.thy)
- (case rec_names of [_] => rec_names | _ => big_rec_base_name::rec_names);
-
-
-val sign = sign_of Inductive.thy;
-
-(********)
-val _ = writeln " Proving monotonicity...";
-
-val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
- big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
-
-val bnd_mono =
- prove_goalw_cterm []
- (cterm_of sign (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
- (fn _ =>
- [rtac (Collect_subset RS bnd_monoI) 1,
- REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
-
-val dom_subset = standard (big_rec_def RS Fp.subs);
-
-val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
-
-(********)
-val _ = writeln " Proving the introduction rules...";
-
-(*Mutual recursion? Helps to derive subset rules for the individual sets.*)
-val Part_trans =
- case rec_names of
- [_] => asm_rl
- | _ => standard (Part_subset RS subset_trans);
-
-(*To type-check recursive occurrences of the inductive sets, possibly
- enclosed in some monotonic operator M.*)
-val rec_typechecks =
- [dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD];
-
-(*Type-checking is hardest aspect of proof;
- disjIn selects the correct disjunct after unfolding*)
-fun intro_tacsf disjIn prems =
- [(*insert prems and underlying sets*)
- cut_facts_tac prems 1,
- DETERM (stac unfold 1),
- REPEAT (resolve_tac [Part_eqI,CollectI] 1),
- (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
- rtac disjIn 2,
- (*Not ares_tac, since refl must be tried before any equality assumptions;
- backtracking may occur if the premises have extra variables!*)
- DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),
- (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
- rewrite_goals_tac Inductive.con_defs,
- REPEAT (rtac refl 2),
- (*Typechecking; this can fail*)
- REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
- ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::
- Inductive.type_elims)
- ORELSE' hyp_subst_tac)),
- DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)];
-
-(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
-val mk_disj_rls =
- let fun f rl = rl RS disjI1
- and g rl = rl RS disjI2
- in accesses_bal(f, g, asm_rl) end;
-
-val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs))
- (map (cterm_of sign) Inductive.intr_tms,
- map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
-
-(********)
-val _ = writeln " Proving the elimination rule...";
-
-(*Breaks down logical connectives in the monotonic function*)
-val basic_elim_tac =
- REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
- ORELSE' bound_hyp_subst_tac))
- THEN prune_params_tac
- (*Mutual recursion: collapse references to Part(D,h)*)
- THEN fold_tac part_rec_defs;
-
-in
- struct
- val thy = Inductive.thy
- and defs = big_rec_def :: part_rec_defs
- and bnd_mono = bnd_mono
- and dom_subset = dom_subset
- and intrs = intrs;
-
- val elim = rule_by_tactic basic_elim_tac
- (unfold RS Ind_Syntax.equals_CollectD);
-
- (*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 defs s =
- rule_by_tactic (rewrite_goals_tac defs THEN
- basic_elim_tac THEN
- fold_tac defs)
- (assume_read Inductive.thy s RS elim)
- |> standard;
-
- val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
- and rec_names = rec_names
- end
-end;
-
--- a/src/ZF/intr_elim.thy Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-intr_elim = "add_ind_def"
--- a/src/ZF/mono.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/mono.ML Mon Dec 28 16:59:28 1998 +0100
@@ -6,8 +6,6 @@
Monotonicity of various operations (for lattice properties see subset.ML)
*)
-open mono;
-
(** Replacement, in its various formulations **)
(*Not easy to express monotonicity in P, since any "bigger" predicate
--- a/src/ZF/thy_syntax.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/thy_syntax.ML Mon Dec 28 16:59:28 1998 +0100
@@ -9,134 +9,144 @@
local
-(*Inductive definitions theory section. co is either "" or "Co"*)
-fun inductive_decl co =
- let open ThyParse
- fun mk_intr_name (s,_) = (*the "op" cancels any infix status*)
- if Syntax.is_identifier s then "op " ^ s else "_"
- fun mk_params ((((((rec_tms, sdom_sum), ipairs),
+
+open ThyParse;
+
+(*ML identifiers for introduction rules.*)
+fun mk_intr_name suffix s =
+ if Syntax.is_identifier s then
+ "op " ^ s ^ suffix (*the "op" cancels any infix status*)
+ else "_"; (*bad name, don't try to bind*)
+
+
+(*For lists of theorems. Either a string (an ML list expression) or else
+ a list of identifiers.*)
+fun optlist s =
+ optional (s $$--
+ (string >> strip_quotes
+ || list1 (name>>strip_quotes) >> mk_list))
+ "[]";
+
+
+(*(Co)Inductive definitions theory section."*)
+fun inductive_decl coind =
+ let
+ fun mk_params ((((((recs, sdom_sum), ipairs),
monos), con_defs), type_intrs), type_elims) =
let val big_rec_name = space_implode "_"
- (map (scan_to_id o trim) rec_tms)
- and srec_tms = mk_list rec_tms
+ (map (scan_to_id o strip_quotes) recs)
+ and srec_tms = mk_list recs
and sintrs = mk_big_list (map snd ipairs)
- val stri_name = big_rec_name ^ "_Intrnl"
+ and inames = mk_list (map (mk_intr_name "" o fst) ipairs)
in
- (";\n\n\
- \structure " ^ stri_name ^ " =\n\
- \ struct\n\
- \ val _ = writeln \"" ^ co ^
- "Inductive definition " ^ big_rec_name ^ "\"\n\
- \ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) "
- ^ srec_tms ^ "\n\
- \ and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\
- \ and intr_tms\t= map (readtm (sign_of thy) propT)\n"
- ^ sintrs ^ "\n\
- \ end;\n\n\
- \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^
- stri_name ^ ".rec_tms, " ^
- stri_name ^ ".dom_sum, " ^
- stri_name ^ ".intr_tms)"
- ,
- "structure " ^ big_rec_name ^ " =\n\
- \ let\n\
- \ val _ = writeln \"Proofs for " ^ co ^
- "Inductive definition " ^ big_rec_name ^ "\"\n\
- \ structure Result = " ^ co ^ "Ind_section_Fun\n\
- \\t (open " ^ stri_name ^ "\n\
- \\t val thy\t\t= thy\n\
- \\t val monos\t\t= " ^ monos ^ "\n\
- \\t val con_defs\t\t= " ^ con_defs ^ "\n\
- \\t val type_intrs\t= " ^ type_intrs ^ "\n\
- \\t val type_elims\t= " ^ type_elims ^ ")\n\
- \ in\n\
- \ struct\n\
- \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
- \ open Result\n\
- \ end\n\
- \ end;\n\n\
- \structure " ^ stri_name ^ " = struct end;\n\n"
- )
+ ";\n\n\
+ \local\n\
+ \val (thy, {defs, intrs, elim, mk_cases, \
+ \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
+ \ " ^
+ (if coind then "Co" else "") ^
+ "Ind_Package.add_inductive (" ^ srec_tms ^ ", " ^ sdom_sum ^ ", " ^
+ sintrs ^ ", " ^ monos ^ ", " ^ con_defs ^ ", " ^
+ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
+ \in\n\
+ \structure " ^ big_rec_name ^ " =\n\
+ \struct\n\
+ \ val defs = defs\n\
+ \ val bnd_mono = bnd_mono\n\
+ \ val dom_subset = dom_subset\n\
+ \ val intrs = intrs\n\
+ \ val elim = elim\n\
+ \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\
+ \ val mutual_induct = mutual_induct\n\
+ \ val mk_cases = mk_cases\n\
+ \ val " ^ inames ^ " = intrs\n\
+ \end;\n\
+ \val thy = thy;\nend;\n\
+ \val thy = thy\n"
end
val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
- fun optstring s = optional (s $$-- string >> trim) "[]"
- in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
- -- optstring "type_intrs" -- optstring "type_elims"
+ in domains -- ipairs -- optlist "monos" -- optlist "con_defs"
+ -- optlist "type_intrs" -- optlist "type_elims"
>> mk_params
end;
-(*Datatype definitions theory section. co is either "" or "Co"*)
-fun datatype_decl co =
- let open ThyParse
- (*generate strings*)
- fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
- val mk_data = mk_list o map mk_const o snd
- val mk_scons = mk_big_list o map mk_data
- fun mk_intr_name s = (*the "op" cancels any infix status*)
- if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
- fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
- let val rec_names = map (scan_to_id o trim o fst) rec_pairs
- val big_rec_name = space_implode "_" rec_names
- and srec_tms = mk_list (map fst rec_pairs)
- and scons = mk_scons rec_pairs
- and sdom_sum =
- if dom = "" then (*default domain: univ or quniv*)
- "Ind_Syntax." ^ co ^ "data_domain rec_tms"
- else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom
- val stri_name = big_rec_name ^ "_Intrnl"
- val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
- in
- (";\n\n\
- \structure " ^ stri_name ^ " =\n\
- \ struct\n\
- \ val _ = writeln \"" ^ co ^
- "Datatype definition " ^ big_rec_name ^ "\"\n\
- \ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\
- \ val dom_sum\t= " ^ sdom_sum ^ "\n\
- \ and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n"
- ^ scons ^ "\n\
- \ val intr_tms\t= Ind_Syntax.mk_all_intr_tms (sign_of thy) (rec_tms, con_ty_lists)\n\
- \ end;\n\n\
- \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^
- mk_list (map quote rec_names) ^ ", " ^
- stri_name ^ ".con_ty_lists) \n\
- \ |> " ^ co ^ "Ind.add_fp_def_i \n (" ^
- stri_name ^ ".rec_tms, " ^
- stri_name ^ ".dom_sum, " ^
- stri_name ^ ".intr_tms)"
- ,
- "structure " ^ big_rec_name ^ " =\n\
- \ let\n\
- \ val _ = writeln \"Proofs for " ^ co ^
- "Datatype definition " ^ big_rec_name ^ "\"\n\
- \ structure Result = " ^ co ^ "Data_section_Fun\n\
- \\t (open " ^ stri_name ^ "\n\
- \\t val thy\t\t= thy\n\
- \\t val big_rec_name\t= Sign.intern_const (sign_of thy) \"" ^ big_rec_name ^ "\"\n\
- \\t val monos\t\t= " ^ monos ^ "\n\
- \\t val type_intrs\t= " ^ type_intrs ^ "\n\
- \\t val type_elims\t= " ^ type_elims ^ ");\n\
- \ in\n\
- \ struct\n\
- \ val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
- \ open Result\n\
- \ end\n\
- \ end;\n\n\
- \structure " ^ stri_name ^ " = struct end;\n\n"
- )
- end
- fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
- val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
- val construct = name -- string_list -- opt_mixfix;
- in optional ("<=" $$-- string) "" --
+(*Datatype definitions theory section. co is true for codatatypes*)
+fun datatype_decl coind =
+ let
+ (*generate strings*)
+ fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
+ val mk_data = mk_list o map mk_const o snd
+ val mk_scons = mk_big_list o map mk_data
+ fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
+ let val rec_names = map (scan_to_id o strip_quotes o fst) rec_pairs
+ val big_rec_name = space_implode "_" rec_names
+ and srec_tms = mk_list (map fst rec_pairs)
+ and scons = mk_scons rec_pairs
+ val con_names = flat (map (map (strip_quotes o #1 o #1) o snd)
+ rec_pairs)
+ val inames = mk_list (map (mk_intr_name "_I") con_names)
+ in
+ ";\n\n\
+ \local\n\
+ \val (thy,\n\
+ \ {defs, intrs, elim, mk_cases, \
+ \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
+ \ {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
+ \ " ^
+ (if coind then "Co" else "") ^
+ "Data_Package.add_datatype (" ^ sdom ^ ", " ^ srec_tms ^ ", " ^
+ scons ^ ", " ^ monos ^ ", " ^
+ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
+ \in\n\
+ \structure " ^ big_rec_name ^ " =\n\
+ \struct\n\
+ \ val defs = defs\n\
+ \ val bnd_mono = bnd_mono\n\
+ \ val dom_subset = dom_subset\n\
+ \ val intrs = intrs\n\
+ \ val elim = elim\n\
+ \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\
+ \ val mutual_induct = mutual_induct\n\
+ \ val mk_cases = mk_cases\n\
+ \ val con_defs = con_defs\n\
+ \ val case_eqns = case_eqns\n\
+ \ val recursor_eqns = recursor_eqns\n\
+ \ val free_iffs = free_iffs\n\
+ \ val free_SEs = free_SEs\n\
+ \ val mk_free = mk_free\n\
+ \ val " ^ inames ^ " = intrs;\n\
+ \end;\n\
+ \val thy = thy;\nend;\n\
+ \val thy = thy\n"
+ end
+ val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
+ val construct = name -- string_list -- opt_mixfix;
+ in optional ("<=" $$-- string) "\"\"" --
enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
- optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
+ optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
>> mk_params
end;
+(** primrec **)
+
+fun mk_primrec_decl eqns =
+ let val names = map fst eqns
+ in
+ ";\nval (thy, " ^ mk_list names ^
+ ") = PrimrecPackage.add_primrec " ^
+ mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
+ \val thy = thy\n"
+ end;
+
+(* either names and axioms or just axioms *)
+val primrec_decl =
+ ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl;
+
+
+
(** augment thy syntax **)
@@ -146,9 +156,10 @@
["inductive", "coinductive", "datatype", "codatatype", "and", "|",
"<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
"type_elims"]
- [("inductive", inductive_decl ""),
- ("coinductive", inductive_decl "Co"),
- ("datatype", datatype_decl ""),
- ("codatatype", datatype_decl "Co")];
+ [section "inductive" "" (inductive_decl false),
+ section "coinductive" "" (inductive_decl true),
+ section "datatype" "" (datatype_decl false),
+ section "codatatype" "" (datatype_decl true),
+ section "primrec" "" primrec_decl];
end;
--- a/src/ZF/typechk.ML Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: ZF/typechk
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Tactics for type checking -- from CTT
-*)
-
-fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
- not (is_Var (head_of a))
- | is_rigid_elem _ = false;
-
-(*Try solving a:A by assumption provided a is rigid!*)
-val test_assume_tac = SUBGOAL(fn (prem,i) =>
- if is_rigid_elem (Logic.strip_assums_concl prem)
- then assume_tac i else eq_assume_tac i);
-
-(*Type checking solves a:?A (a rigid, ?A maybe flexible).
- match_tac is too strict; would refuse to instantiate ?A*)
-fun typechk_step_tac tyrls =
- FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
-
-fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
-
-val ZF_typechecks =
- [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
-
-(*Instantiates variables in typing conditions.
- drawback: does not simplify conjunctions*)
-fun type_auto_tac tyrls hyps = SELECT_GOAL
- (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
- ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
-