src/ZF/Inductive_ZF.thy
author wenzelm
Sat Mar 29 19:14:00 2008 +0100 (2008-03-29 ago)
changeset 26480 544cef16045b
parent 26190 cf51a23c0cd0
child 29580 117b88da143c
permissions -rw-r--r--
replaced 'ML_setup' by 'ML';
wenzelm@26189
     1
(*  Title:      ZF/Inductive_ZF.thy
krauss@26056
     2
    ID:         $Id$
krauss@26056
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
krauss@26056
     4
    Copyright   1993  University of Cambridge
krauss@26056
     5
krauss@26056
     6
Inductive definitions use least fixedpoints with standard products and sums
krauss@26056
     7
Coinductive definitions use greatest fixedpoints with Quine products and sums
krauss@26056
     8
krauss@26056
     9
Sums are used only for mutual recursion;
krauss@26056
    10
Products are used only to derive "streamlined" induction rules for relations
krauss@26056
    11
*)
krauss@26056
    12
krauss@26056
    13
header{*Inductive and Coinductive Definitions*}
krauss@26056
    14
wenzelm@26189
    15
theory Inductive_ZF
wenzelm@26189
    16
imports Fixedpt QPair Nat_ZF
wenzelm@26189
    17
uses
wenzelm@26189
    18
  ("ind_syntax.ML")
wenzelm@26189
    19
  ("Tools/cartprod.ML")
wenzelm@26189
    20
  ("Tools/ind_cases.ML")
wenzelm@26189
    21
  ("Tools/inductive_package.ML")
wenzelm@26189
    22
  ("Tools/induct_tacs.ML")
wenzelm@26189
    23
  ("Tools/primrec_package.ML")
wenzelm@26189
    24
begin
wenzelm@26189
    25
wenzelm@26189
    26
lemma def_swap_iff: "a == b ==> a = c <-> c = b"
wenzelm@26189
    27
  by blast
wenzelm@26189
    28
wenzelm@26189
    29
lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
wenzelm@26189
    30
  by simp
wenzelm@26189
    31
wenzelm@26189
    32
lemma refl_thin: "!!P. a = a ==> P ==> P" .
wenzelm@26189
    33
wenzelm@26189
    34
use "ind_syntax.ML"
wenzelm@26189
    35
use "Tools/cartprod.ML"
wenzelm@26189
    36
use "Tools/ind_cases.ML"
wenzelm@26189
    37
use "Tools/inductive_package.ML"
wenzelm@26189
    38
use "Tools/induct_tacs.ML"
wenzelm@26189
    39
use "Tools/primrec_package.ML"
krauss@26056
    40
krauss@26056
    41
setup IndCases.setup
krauss@26056
    42
setup DatatypeTactics.setup
krauss@26056
    43
wenzelm@26480
    44
ML {*
krauss@26056
    45
structure Lfp =
krauss@26056
    46
  struct
wenzelm@26189
    47
  val oper      = @{const lfp}
wenzelm@26189
    48
  val bnd_mono  = @{const bnd_mono}
krauss@26056
    49
  val bnd_monoI = @{thm bnd_monoI}
krauss@26056
    50
  val subs      = @{thm def_lfp_subset}
krauss@26056
    51
  val Tarski    = @{thm def_lfp_unfold}
krauss@26056
    52
  val induct    = @{thm def_induct}
krauss@26056
    53
  end;
krauss@26056
    54
krauss@26056
    55
structure Standard_Prod =
krauss@26056
    56
  struct
wenzelm@26189
    57
  val sigma     = @{const Sigma}
wenzelm@26189
    58
  val pair      = @{const Pair}
wenzelm@26189
    59
  val split_name = @{const_name split}
krauss@26056
    60
  val pair_iff  = @{thm Pair_iff}
krauss@26056
    61
  val split_eq  = @{thm split}
krauss@26056
    62
  val fsplitI   = @{thm splitI}
krauss@26056
    63
  val fsplitD   = @{thm splitD}
krauss@26056
    64
  val fsplitE   = @{thm splitE}
krauss@26056
    65
  end;
krauss@26056
    66
krauss@26056
    67
structure Standard_CP = CartProd_Fun (Standard_Prod);
krauss@26056
    68
krauss@26056
    69
structure Standard_Sum =
krauss@26056
    70
  struct
wenzelm@26189
    71
  val sum       = @{const sum}
wenzelm@26189
    72
  val inl       = @{const Inl}
wenzelm@26189
    73
  val inr       = @{const Inr}
wenzelm@26189
    74
  val elim      = @{const case}
krauss@26056
    75
  val case_inl  = @{thm case_Inl}
krauss@26056
    76
  val case_inr  = @{thm case_Inr}
krauss@26056
    77
  val inl_iff   = @{thm Inl_iff}
krauss@26056
    78
  val inr_iff   = @{thm Inr_iff}
krauss@26056
    79
  val distinct  = @{thm Inl_Inr_iff}
krauss@26056
    80
  val distinct' = @{thm Inr_Inl_iff}
krauss@26056
    81
  val free_SEs  = Ind_Syntax.mk_free_SEs
krauss@26056
    82
            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
krauss@26056
    83
  end;
krauss@26056
    84
krauss@26056
    85
krauss@26056
    86
structure Ind_Package =
krauss@26056
    87
    Add_inductive_def_Fun
krauss@26056
    88
      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
krauss@26056
    89
       and Su=Standard_Sum val coind = false);
krauss@26056
    90
krauss@26056
    91
krauss@26056
    92
structure Gfp =
krauss@26056
    93
  struct
wenzelm@26189
    94
  val oper      = @{const gfp}
wenzelm@26189
    95
  val bnd_mono  = @{const bnd_mono}
krauss@26056
    96
  val bnd_monoI = @{thm bnd_monoI}
krauss@26056
    97
  val subs      = @{thm def_gfp_subset}
krauss@26056
    98
  val Tarski    = @{thm def_gfp_unfold}
krauss@26056
    99
  val induct    = @{thm def_Collect_coinduct}
krauss@26056
   100
  end;
krauss@26056
   101
krauss@26056
   102
structure Quine_Prod =
krauss@26056
   103
  struct
wenzelm@26189
   104
  val sigma     = @{const QSigma}
wenzelm@26189
   105
  val pair      = @{const QPair}
wenzelm@26189
   106
  val split_name = @{const_name qsplit}
krauss@26056
   107
  val pair_iff  = @{thm QPair_iff}
krauss@26056
   108
  val split_eq  = @{thm qsplit}
krauss@26056
   109
  val fsplitI   = @{thm qsplitI}
krauss@26056
   110
  val fsplitD   = @{thm qsplitD}
krauss@26056
   111
  val fsplitE   = @{thm qsplitE}
krauss@26056
   112
  end;
krauss@26056
   113
krauss@26056
   114
structure Quine_CP = CartProd_Fun (Quine_Prod);
krauss@26056
   115
krauss@26056
   116
structure Quine_Sum =
krauss@26056
   117
  struct
wenzelm@26189
   118
  val sum       = @{const qsum}
wenzelm@26189
   119
  val inl       = @{const QInl}
wenzelm@26189
   120
  val inr       = @{const QInr}
wenzelm@26189
   121
  val elim      = @{const qcase}
krauss@26056
   122
  val case_inl  = @{thm qcase_QInl}
krauss@26056
   123
  val case_inr  = @{thm qcase_QInr}
krauss@26056
   124
  val inl_iff   = @{thm QInl_iff}
krauss@26056
   125
  val inr_iff   = @{thm QInr_iff}
krauss@26056
   126
  val distinct  = @{thm QInl_QInr_iff}
krauss@26056
   127
  val distinct' = @{thm QInr_QInl_iff}
krauss@26056
   128
  val free_SEs  = Ind_Syntax.mk_free_SEs
krauss@26056
   129
            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
krauss@26056
   130
  end;
krauss@26056
   131
krauss@26056
   132
krauss@26056
   133
structure CoInd_Package =
krauss@26056
   134
  Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
krauss@26056
   135
    and Su=Quine_Sum val coind = true);
krauss@26056
   136
krauss@26056
   137
*}
krauss@26056
   138
krauss@26056
   139
end