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