src/ZF/Inductive.ML
author lcp
Thu, 25 Aug 1994 12:09:21 +0200
changeset 578 efc648d29dd0
child 734 a3e0fd3c0f2f
permissions -rw-r--r--
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/Inductive.ML
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     2
    ID:         $Id$
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     5
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     6
(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     7
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     8
Inductive definitions use least fixedpoints with standard products and sums
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     9
Coinductive definitions use greatest fixedpoints with Quine products and sums
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    10
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    11
Sums are used only for mutual recursion;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    12
Products are used only to derive "streamlined" induction rules for relations
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    13
*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    14
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    15
local open Ind_Syntax
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    16
in
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    17
structure Lfp =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    18
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    19
  val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    20
  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    21
  val bnd_monoI	= bnd_monoI
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    22
  val subs	= def_lfp_subset
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    23
  val Tarski	= def_lfp_Tarski
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    24
  val induct	= def_induct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    25
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    26
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    27
structure Standard_Prod =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    28
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    29
  val sigma	= Const("Sigma", [iT, iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    30
  val pair	= Const("Pair", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    31
  val split_const	= Const("split", [[iT,iT]--->iT, iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    32
  val fsplit_const	= Const("fsplit", [[iT,iT]--->oT, iT]--->oT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    33
  val pair_iff	= Pair_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    34
  val split_eq	= split
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    35
  val fsplitI	= fsplitI
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    36
  val fsplitD	= fsplitD
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    37
  val fsplitE	= fsplitE
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    38
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    39
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    40
structure Standard_Sum =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    41
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    42
  val sum	= Const("op +", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    43
  val inl	= Const("Inl", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    44
  val inr	= Const("Inr", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    45
  val elim	= Const("case", [iT-->iT, iT-->iT, iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    46
  val case_inl	= case_Inl
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    47
  val case_inr	= case_Inr
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    48
  val inl_iff	= Inl_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    49
  val inr_iff	= Inr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    50
  val distinct	= Inl_Inr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    51
  val distinct' = Inr_Inl_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    52
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    53
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    54
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    55
functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    56
  : sig include INTR_ELIM INDRULE end =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    57
struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    58
structure Intr_elim = 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    59
    Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    60
		  Pr=Standard_Prod and Su=Standard_Sum);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    61
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    62
structure Indrule = Indrule_Fun (structure Inductive=Inductive and 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    63
		                 Pr=Standard_Prod and Intr_elim=Intr_elim);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    64
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    65
open Intr_elim Indrule
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    66
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    67
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    68
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    69
structure Ind = Add_inductive_def_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    70
    (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    71
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    72
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    73
signature INDUCTIVE_STRING =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    74
  sig
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    75
  val thy_name   : string 		(*name of the new theory*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    76
  val rec_doms   : (string*string) list	(*recursion terms and their domains*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    77
  val sintrs     : string list		(*desired introduction rules*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    78
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    79
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    80
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    81
(*For upwards compatibility: can be called directly from ML*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    82
functor Inductive_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    83
 (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    84
   : sig include INTR_ELIM INDRULE end =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    85
Ind_section_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    86
   (open Inductive Ind_Syntax
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    87
    val sign = sign_of thy;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    88
    val rec_tms = map (readtm sign iT o #1) rec_doms
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    89
    and domts   = map (readtm sign iT o #2) rec_doms
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    90
    and intr_tms = map (readtm sign propT) sintrs;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    91
    val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms) 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    92
                  |> add_thyname thy_name);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    93
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    94
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    95
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    96
local open Ind_Syntax
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    97
in
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    98
structure Gfp =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    99
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   100
  val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   101
  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   102
  val bnd_monoI	= bnd_monoI
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   103
  val subs	= def_gfp_subset
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   104
  val Tarski	= def_gfp_Tarski
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   105
  val induct	= def_Collect_coinduct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   106
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   107
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   108
structure Quine_Prod =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   109
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   110
  val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   111
  val pair	= Const("QPair", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   112
  val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   113
  val fsplit_const	= Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   114
  val pair_iff	= QPair_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   115
  val split_eq	= qsplit
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   116
  val fsplitI	= qfsplitI
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   117
  val fsplitD	= qfsplitD
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   118
  val fsplitE	= qfsplitE
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   119
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   120
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   121
structure Quine_Sum =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   122
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   123
  val sum	= Const("op <+>", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   124
  val inl	= Const("QInl", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   125
  val inr	= Const("QInr", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   126
  val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   127
  val case_inl	= qcase_QInl
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   128
  val case_inr	= qcase_QInr
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   129
  val inl_iff	= QInl_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   130
  val inr_iff	= QInr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   131
  val distinct	= QInl_QInr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   132
  val distinct' = QInr_QInl_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   133
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   134
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   135
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   136
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   137
signature COINDRULE =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   138
  sig
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   139
  val coinduct : thm
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   140
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   141
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   142
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   143
functor CoInd_section_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   144
 (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   145
    : sig include INTR_ELIM COINDRULE end =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   146
struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   147
structure Intr_elim = 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   148
    Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   149
		  Pr=Quine_Prod and Su=Quine_Sum);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   150
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   151
open Intr_elim 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   152
val coinduct = raw_induct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   153
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   154
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   155
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   156
structure CoInd = 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   157
    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   158
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   159
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   160
(*For upwards compatibility: can be called directly from ML*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   161
functor CoInductive_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   162
 (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   163
   : sig include INTR_ELIM COINDRULE end =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   164
CoInd_section_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   165
   (open Inductive Ind_Syntax
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   166
    val sign = sign_of thy;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   167
    val rec_tms = map (readtm sign iT o #1) rec_doms
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   168
    and domts   = map (readtm sign iT o #2) rec_doms
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   169
    and intr_tms = map (readtm sign propT) sintrs;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   170
    val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms) 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   171
                  |> add_thyname thy_name);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   172
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   173
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   174
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   175
(*For installing the theory section.   co is either "" or "Co"*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   176
fun inductive_decl co =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   177
  let open ThyParse Ind_Syntax
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   178
      fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   179
	  if Syntax.is_identifier s then "op " ^ s  else "_"
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   180
      fun mk_params (((((domains: (string*string) list, ipairs), 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   181
			monos), con_defs), type_intrs), type_elims) =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   182
        let val big_rec_name = space_implode "_" 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   183
		             (map (scan_to_id o trim o #1) domains)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   184
	    and srec_tms = mk_list (map #1 domains)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   185
            and sdoms    = mk_list (map #2 domains)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   186
	    and sintrs   = mk_big_list (map snd ipairs)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   187
            val stri_name = big_rec_name ^ "_Intrnl"
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   188
        in
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   189
	   (";\n\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   190
            \structure " ^ stri_name ^ " =\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   191
            \ let open Ind_Syntax in\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   192
            \  struct\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   193
            \  val _ = writeln \"" ^ co ^ 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   194
	               "Inductive definition " ^ big_rec_name ^ "\"\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   195
            \  val rec_tms\t= map (readtm (sign_of thy) iT) "
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   196
	                     ^ srec_tms ^ "\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   197
            \  and domts\t= map (readtm (sign_of thy) iT) "
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   198
	                     ^ sdoms ^ "\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   199
            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   200
	                     ^ sintrs ^ "\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   201
            \  end\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   202
            \ end;\n\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   203
            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   204
	       stri_name ^ ".rec_tms, " ^
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   205
               stri_name ^ ".domts, " ^
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   206
               stri_name ^ ".intr_tms)"
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   207
           ,
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   208
	    "structure " ^ big_rec_name ^ " =\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   209
            \  struct\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   210
            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   211
            \  (open " ^ stri_name ^ "\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   212
            \   val thy\t\t= thy\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   213
            \   val monos\t\t= " ^ monos ^ "\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   214
            \   val con_defs\t\t= " ^ con_defs ^ "\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   215
            \   val type_intrs\t= " ^ type_intrs ^ "\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   216
            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   217
            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   218
            \  open Result\n\
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   219
            \  end\n"
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   220
	   )
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   221
	end
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   222
      val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   223
      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   224
      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   225
  in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   226
             -- optstring "type_intrs" -- optstring "type_elims"
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   227
     >> mk_params
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   228
  end;