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