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