src/ZF/inductive.ML
 changeset 516 1957113f0d7d parent 0 a5a9c433f639
```--- a/src/ZF/inductive.ML	Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/inductive.ML	Fri Aug 12 12:51:34 1994 +0200
@@ -3,15 +3,17 @@
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

-Inductive Definitions for Zermelo-Fraenkel Set Theory
+(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory

-Uses least fixedpoints with standard products and sums
+Inductive definitions use least fixedpoints with standard products and sums
+Coinductive definitions use greatest fixedpoints with Quine products and sums

Sums are used only for mutual recursion;
Products are used only to derive "streamlined" induction rules for relations
*)

-
+local open Ind_Syntax
+in
structure Lfp =
struct
val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
@@ -48,16 +50,179 @@
val distinct	= Inl_Inr_iff
val distinct' = Inr_Inl_iff
end;
+end;

-functor Inductive_Fun (Ind: INDUCTIVE) : sig include INTR_ELIM INDRULE end =
+functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
+  : sig include INTR_ELIM INDRULE end =
struct
structure Intr_elim =
-    Intr_elim_Fun(structure Ind=Ind and Fp=Lfp and
+    Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and
Pr=Standard_Prod and Su=Standard_Sum);

-structure Indrule = Indrule_Fun (structure Ind=Ind and
+structure Indrule = Indrule_Fun (structure Inductive=Inductive and
Pr=Standard_Prod and Intr_elim=Intr_elim);

open Intr_elim Indrule
end;

+
+    (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
+
+
+signature INDUCTIVE_STRING =
+  sig
+  val thy_name   : string 		(*name of the new theory*)
+  val rec_doms   : (string*string) list	(*recursion terms and their domains*)
+  val sintrs     : string list		(*desired introduction rules*)
+  end;
+
+
+(*For upwards compatibility: can be called directly from ML*)
+functor Inductive_Fun
+ (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
+   : sig include INTR_ELIM INDRULE end =
+Ind_section_Fun
+   (open Inductive Ind_Syntax
+    val sign = sign_of thy;
+    val rec_tms = map (readtm sign iT o #1) rec_doms
+    and domts   = map (readtm sign iT o #2) rec_doms
+    and intr_tms = map (readtm sign propT) sintrs;
+    val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms)
+
+
+
+local open Ind_Syntax
+in
+structure Gfp =
+  struct
+  val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
+  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
+  val bnd_monoI	= bnd_monoI
+  val subs	= def_gfp_subset
+  val Tarski	= def_gfp_Tarski
+  val induct	= def_Collect_coinduct
+  end;
+
+structure Quine_Prod =
+  struct
+  val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
+  val pair	= Const("QPair", [iT,iT]--->iT)
+  val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
+  val fsplit_const	= Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
+  val pair_iff	= QPair_iff
+  val split_eq	= qsplit
+  val fsplitI	= qfsplitI
+  val fsplitD	= qfsplitD
+  val fsplitE	= qfsplitE
+  end;
+
+structure Quine_Sum =
+  struct
+  val sum	= Const("op <+>", [iT,iT]--->iT)
+  val inl	= Const("QInl", iT-->iT)
+  val inr	= Const("QInr", iT-->iT)
+  val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
+  val case_inl	= qcase_QInl
+  val case_inr	= qcase_QInr
+  val inl_iff	= QInl_iff
+  val inr_iff	= QInr_iff
+  val distinct	= QInl_QInr_iff
+  val distinct' = QInr_QInl_iff
+  end;
+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 =
+struct
+structure Intr_elim =
+    Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and
+		  Pr=Quine_Prod and Su=Quine_Sum);
+
+open Intr_elim
+val coinduct = raw_induct
+end;
+
+
+structure CoInd =
+    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
+
+
+(*For upwards compatibility: can be called directly from ML*)
+functor CoInductive_Fun
+ (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
+   : sig include INTR_ELIM COINDRULE end =
+CoInd_section_Fun
+   (open Inductive Ind_Syntax
+    val sign = sign_of thy;
+    val rec_tms = map (readtm sign iT o #1) rec_doms
+    and domts   = map (readtm sign iT o #2) rec_doms
+    and intr_tms = map (readtm sign propT) sintrs;
+    val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms)
+
+
+
+(*For installing the theory section.   co is either "" or "Co"*)
+fun inductive_decl co =
+  let open ThyParse Ind_Syntax
+      fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
+	  if Syntax.is_identifier s then "op " ^ s  else "_"
+      fun mk_params (((((domains: (string*string) list, ipairs),
+			monos), con_defs), type_intrs), type_elims) =
+        let val big_rec_name = space_implode "_"
+		             (map (scan_to_id o trim o #1) domains)
+	    and srec_tms = mk_list (map #1 domains)
+            and sdoms    = mk_list (map #2 domains)
+	    and sintrs   = mk_big_list (map snd ipairs)
+            val stri_name = big_rec_name ^ "_Intrnl"
+        in
+	   (";\n\n\
+            \structure " ^ stri_name ^ " =\n\
+            \ let open Ind_Syntax in\n\
+            \  struct\n\
+            \  val rec_tms\t= map (readtm (sign_of thy) iT) "
+	                     ^ srec_tms ^ "\n\
+            \  and domts\t= map (readtm (sign_of thy) iT) "
+	                     ^ sdoms ^ "\n\
+            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
+	                     ^ sintrs ^ "\n\
+            \  end\n\
+            \ end;\n\n\
+            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
+	       stri_name ^ ".rec_tms, " ^
+               stri_name ^ ".domts, " ^
+               stri_name ^ ".intr_tms)"
+           ,
+	    "structure " ^ big_rec_name ^ " =\n\
+            \  struct\n\
+            \  val _ = writeln \"" ^ co ^
+	               "Inductive definition " ^ big_rec_name ^ "\"\n\
+            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
+            \  (open " ^ stri_name ^ "\n\
+            \   val thy\t\t= thy\n\
+            \   val monos\t\t= " ^ monos ^ "\n\
+            \   val con_defs\t\t= " ^ con_defs ^ "\n\
+            \   val type_intrs\t= " ^ type_intrs ^ "\n\
+            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
+            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
+            \  open Result\n\
+            \  end\n"
+	   )
+	end
+      val domains = "domains" \$\$-- repeat1 (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"
+     >> mk_params
+  end;```