src/ZF/Inductive_ZF.thy
author wenzelm
Tue Sep 01 22:32:58 2015 +0200 (2015-09-01)
changeset 61076 bdc1e2f0a86a
parent 60770 240563fbf41d
child 63435 7743df69a6b4
permissions -rw-r--r--
eliminated \<Colon>;
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
wenzelm@60770
    12
section\<open>Inductive and Coinductive Definitions\<close>
krauss@26056
    13
wenzelm@26189
    14
theory Inductive_ZF
wenzelm@26189
    15
imports Fixedpt QPair Nat_ZF
wenzelm@46947
    16
keywords
wenzelm@56146
    17
  "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
wenzelm@46950
    18
  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
wenzelm@46947
    19
  "elimination" "induction" "case_eqns" "recursor_eqns"
wenzelm@26189
    20
begin
wenzelm@26189
    21
paulson@46821
    22
lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
wenzelm@26189
    23
  by blast
wenzelm@26189
    24
wenzelm@26189
    25
lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
wenzelm@26189
    26
  by simp
wenzelm@26189
    27
wenzelm@26189
    28
lemma refl_thin: "!!P. a = a ==> P ==> P" .
wenzelm@26189
    29
wenzelm@48891
    30
ML_file "ind_syntax.ML"
wenzelm@48891
    31
ML_file "Tools/ind_cases.ML"
wenzelm@48891
    32
ML_file "Tools/cartprod.ML"
wenzelm@48891
    33
ML_file "Tools/inductive_package.ML"
wenzelm@48891
    34
ML_file "Tools/induct_tacs.ML"
wenzelm@48891
    35
ML_file "Tools/primrec_package.ML"
krauss@26056
    36
wenzelm@60770
    37
ML \<open>
krauss@26056
    38
structure Lfp =
krauss@26056
    39
  struct
wenzelm@26189
    40
  val oper      = @{const lfp}
wenzelm@26189
    41
  val bnd_mono  = @{const bnd_mono}
krauss@26056
    42
  val bnd_monoI = @{thm bnd_monoI}
krauss@26056
    43
  val subs      = @{thm def_lfp_subset}
krauss@26056
    44
  val Tarski    = @{thm def_lfp_unfold}
krauss@26056
    45
  val induct    = @{thm def_induct}
krauss@26056
    46
  end;
krauss@26056
    47
krauss@26056
    48
structure Standard_Prod =
krauss@26056
    49
  struct
wenzelm@26189
    50
  val sigma     = @{const Sigma}
wenzelm@26189
    51
  val pair      = @{const Pair}
wenzelm@26189
    52
  val split_name = @{const_name split}
krauss@26056
    53
  val pair_iff  = @{thm Pair_iff}
krauss@26056
    54
  val split_eq  = @{thm split}
krauss@26056
    55
  val fsplitI   = @{thm splitI}
krauss@26056
    56
  val fsplitD   = @{thm splitD}
krauss@26056
    57
  val fsplitE   = @{thm splitE}
krauss@26056
    58
  end;
krauss@26056
    59
krauss@26056
    60
structure Standard_CP = CartProd_Fun (Standard_Prod);
krauss@26056
    61
krauss@26056
    62
structure Standard_Sum =
krauss@26056
    63
  struct
wenzelm@26189
    64
  val sum       = @{const sum}
wenzelm@26189
    65
  val inl       = @{const Inl}
wenzelm@26189
    66
  val inr       = @{const Inr}
wenzelm@26189
    67
  val elim      = @{const case}
krauss@26056
    68
  val case_inl  = @{thm case_Inl}
krauss@26056
    69
  val case_inr  = @{thm case_Inr}
krauss@26056
    70
  val inl_iff   = @{thm Inl_iff}
krauss@26056
    71
  val inr_iff   = @{thm Inr_iff}
krauss@26056
    72
  val distinct  = @{thm Inl_Inr_iff}
krauss@26056
    73
  val distinct' = @{thm Inr_Inl_iff}
krauss@26056
    74
  val free_SEs  = Ind_Syntax.mk_free_SEs
krauss@26056
    75
            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
krauss@26056
    76
  end;
krauss@26056
    77
krauss@26056
    78
krauss@26056
    79
structure Ind_Package =
krauss@26056
    80
    Add_inductive_def_Fun
krauss@26056
    81
      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
krauss@26056
    82
       and Su=Standard_Sum val coind = false);
krauss@26056
    83
krauss@26056
    84
krauss@26056
    85
structure Gfp =
krauss@26056
    86
  struct
wenzelm@26189
    87
  val oper      = @{const gfp}
wenzelm@26189
    88
  val bnd_mono  = @{const bnd_mono}
krauss@26056
    89
  val bnd_monoI = @{thm bnd_monoI}
krauss@26056
    90
  val subs      = @{thm def_gfp_subset}
krauss@26056
    91
  val Tarski    = @{thm def_gfp_unfold}
krauss@26056
    92
  val induct    = @{thm def_Collect_coinduct}
krauss@26056
    93
  end;
krauss@26056
    94
krauss@26056
    95
structure Quine_Prod =
krauss@26056
    96
  struct
wenzelm@26189
    97
  val sigma     = @{const QSigma}
wenzelm@26189
    98
  val pair      = @{const QPair}
wenzelm@26189
    99
  val split_name = @{const_name qsplit}
krauss@26056
   100
  val pair_iff  = @{thm QPair_iff}
krauss@26056
   101
  val split_eq  = @{thm qsplit}
krauss@26056
   102
  val fsplitI   = @{thm qsplitI}
krauss@26056
   103
  val fsplitD   = @{thm qsplitD}
krauss@26056
   104
  val fsplitE   = @{thm qsplitE}
krauss@26056
   105
  end;
krauss@26056
   106
krauss@26056
   107
structure Quine_CP = CartProd_Fun (Quine_Prod);
krauss@26056
   108
krauss@26056
   109
structure Quine_Sum =
krauss@26056
   110
  struct
wenzelm@26189
   111
  val sum       = @{const qsum}
wenzelm@26189
   112
  val inl       = @{const QInl}
wenzelm@26189
   113
  val inr       = @{const QInr}
wenzelm@26189
   114
  val elim      = @{const qcase}
krauss@26056
   115
  val case_inl  = @{thm qcase_QInl}
krauss@26056
   116
  val case_inr  = @{thm qcase_QInr}
krauss@26056
   117
  val inl_iff   = @{thm QInl_iff}
krauss@26056
   118
  val inr_iff   = @{thm QInr_iff}
krauss@26056
   119
  val distinct  = @{thm QInl_QInr_iff}
krauss@26056
   120
  val distinct' = @{thm QInr_QInl_iff}
krauss@26056
   121
  val free_SEs  = Ind_Syntax.mk_free_SEs
krauss@26056
   122
            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
krauss@26056
   123
  end;
krauss@26056
   124
krauss@26056
   125
krauss@26056
   126
structure CoInd_Package =
krauss@26056
   127
  Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
krauss@26056
   128
    and Su=Quine_Sum val coind = true);
krauss@26056
   129
wenzelm@60770
   130
\<close>
krauss@26056
   131
krauss@26056
   132
end