src/ZF/Inductive_ZF.thy
author wenzelm
Sat Mar 01 14:10:15 2008 +0100 (2008-03-01 ago)
changeset 26189 9808cca5c54d
parent 26056 6a0801279f4c
child 26190 cf51a23c0cd0
permissions -rw-r--r--
misc cleanup of embedded ML code;
use more antiquotations;
tuned;
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
krauss@26056
    44
ML_setup {*
krauss@26056
    45
val iT = Ind_Syntax.iT
krauss@26056
    46
and oT = FOLogic.oT;
krauss@26056
    47
krauss@26056
    48
structure Lfp =
krauss@26056
    49
  struct
wenzelm@26189
    50
  val oper      = @{const lfp}
wenzelm@26189
    51
  val bnd_mono  = @{const bnd_mono}
krauss@26056
    52
  val bnd_monoI = @{thm bnd_monoI}
krauss@26056
    53
  val subs      = @{thm def_lfp_subset}
krauss@26056
    54
  val Tarski    = @{thm def_lfp_unfold}
krauss@26056
    55
  val induct    = @{thm def_induct}
krauss@26056
    56
  end;
krauss@26056
    57
krauss@26056
    58
structure Standard_Prod =
krauss@26056
    59
  struct
wenzelm@26189
    60
  val sigma     = @{const Sigma}
wenzelm@26189
    61
  val pair      = @{const Pair}
wenzelm@26189
    62
  val split_name = @{const_name split}
krauss@26056
    63
  val pair_iff  = @{thm Pair_iff}
krauss@26056
    64
  val split_eq  = @{thm split}
krauss@26056
    65
  val fsplitI   = @{thm splitI}
krauss@26056
    66
  val fsplitD   = @{thm splitD}
krauss@26056
    67
  val fsplitE   = @{thm splitE}
krauss@26056
    68
  end;
krauss@26056
    69
krauss@26056
    70
structure Standard_CP = CartProd_Fun (Standard_Prod);
krauss@26056
    71
krauss@26056
    72
structure Standard_Sum =
krauss@26056
    73
  struct
wenzelm@26189
    74
  val sum       = @{const sum}
wenzelm@26189
    75
  val inl       = @{const Inl}
wenzelm@26189
    76
  val inr       = @{const Inr}
wenzelm@26189
    77
  val elim      = @{const case}
krauss@26056
    78
  val case_inl  = @{thm case_Inl}
krauss@26056
    79
  val case_inr  = @{thm case_Inr}
krauss@26056
    80
  val inl_iff   = @{thm Inl_iff}
krauss@26056
    81
  val inr_iff   = @{thm Inr_iff}
krauss@26056
    82
  val distinct  = @{thm Inl_Inr_iff}
krauss@26056
    83
  val distinct' = @{thm Inr_Inl_iff}
krauss@26056
    84
  val free_SEs  = Ind_Syntax.mk_free_SEs
krauss@26056
    85
            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
krauss@26056
    86
  end;
krauss@26056
    87
krauss@26056
    88
krauss@26056
    89
structure Ind_Package =
krauss@26056
    90
    Add_inductive_def_Fun
krauss@26056
    91
      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
krauss@26056
    92
       and Su=Standard_Sum val coind = false);
krauss@26056
    93
krauss@26056
    94
krauss@26056
    95
structure Gfp =
krauss@26056
    96
  struct
wenzelm@26189
    97
  val oper      = @{const gfp}
wenzelm@26189
    98
  val bnd_mono  = @{const bnd_mono}
krauss@26056
    99
  val bnd_monoI = @{thm bnd_monoI}
krauss@26056
   100
  val subs      = @{thm def_gfp_subset}
krauss@26056
   101
  val Tarski    = @{thm def_gfp_unfold}
krauss@26056
   102
  val induct    = @{thm def_Collect_coinduct}
krauss@26056
   103
  end;
krauss@26056
   104
krauss@26056
   105
structure Quine_Prod =
krauss@26056
   106
  struct
wenzelm@26189
   107
  val sigma     = @{const QSigma}
wenzelm@26189
   108
  val pair      = @{const QPair}
wenzelm@26189
   109
  val split_name = @{const_name qsplit}
krauss@26056
   110
  val pair_iff  = @{thm QPair_iff}
krauss@26056
   111
  val split_eq  = @{thm qsplit}
krauss@26056
   112
  val fsplitI   = @{thm qsplitI}
krauss@26056
   113
  val fsplitD   = @{thm qsplitD}
krauss@26056
   114
  val fsplitE   = @{thm qsplitE}
krauss@26056
   115
  end;
krauss@26056
   116
krauss@26056
   117
structure Quine_CP = CartProd_Fun (Quine_Prod);
krauss@26056
   118
krauss@26056
   119
structure Quine_Sum =
krauss@26056
   120
  struct
wenzelm@26189
   121
  val sum       = @{const qsum}
wenzelm@26189
   122
  val inl       = @{const QInl}
wenzelm@26189
   123
  val inr       = @{const QInr}
wenzelm@26189
   124
  val elim      = @{const qcase}
krauss@26056
   125
  val case_inl  = @{thm qcase_QInl}
krauss@26056
   126
  val case_inr  = @{thm qcase_QInr}
krauss@26056
   127
  val inl_iff   = @{thm QInl_iff}
krauss@26056
   128
  val inr_iff   = @{thm QInr_iff}
krauss@26056
   129
  val distinct  = @{thm QInl_QInr_iff}
krauss@26056
   130
  val distinct' = @{thm QInr_QInl_iff}
krauss@26056
   131
  val free_SEs  = Ind_Syntax.mk_free_SEs
krauss@26056
   132
            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
krauss@26056
   133
  end;
krauss@26056
   134
krauss@26056
   135
krauss@26056
   136
structure CoInd_Package =
krauss@26056
   137
  Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
krauss@26056
   138
    and Su=Quine_Sum val coind = true);
krauss@26056
   139
krauss@26056
   140
*}
krauss@26056
   141
krauss@26056
   142
end