src/ZF/Inductive_ZF.thy
author blanchet
Wed, 06 Nov 2013 22:50:12 +0100
changeset 54284 0b53378080d9
parent 48891 c0eafbd55de3
child 56146 8453d35e4684
permissions -rw-r--r--
simplified code
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
    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
     3
    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
     4
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     5
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
     6
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
     7
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     8
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
     9
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
    10
*)
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
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
    13
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    14
theory Inductive_ZF
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    15
imports Fixedpt QPair Nat_ZF
46947
b8c7eb0c2f89 declare minor keywords via theory header;
wenzelm
parents: 46821
diff changeset
    16
keywords
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
    17
  "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
    18
  "inductive_cases" :: thy_script and
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
    19
  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
46947
b8c7eb0c2f89 declare minor keywords via theory header;
wenzelm
parents: 46821
diff changeset
    20
  "elimination" "induction" "case_eqns" "recursor_eqns"
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    21
begin
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    22
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 38514
diff changeset
    23
lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    24
  by blast
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_trans: "f == g ==> g(a) = b ==> f(a) = b"
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    27
  by simp
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 refl_thin: "!!P. a = a ==> P ==> P" .
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    30
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    31
ML_file "ind_syntax.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    32
ML_file "Tools/ind_cases.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    33
ML_file "Tools/cartprod.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    34
ML_file "Tools/inductive_package.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    35
ML_file "Tools/induct_tacs.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    36
ML_file "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
    37
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    38
setup IndCases.setup
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    39
setup DatatypeTactics.setup
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    40
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 26190
diff changeset
    41
ML {*
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    42
structure Lfp =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    43
  struct
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    44
  val oper      = @{const lfp}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    45
  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
    46
  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
    47
  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
    48
  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
    49
  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
    50
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    51
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    52
structure Standard_Prod =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    53
  struct
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    54
  val sigma     = @{const Sigma}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    55
  val pair      = @{const Pair}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    56
  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
    57
  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
    58
  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
    59
  val fsplitI   = @{thm splitI}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    60
  val fsplitD   = @{thm splitD}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    61
  val fsplitE   = @{thm splitE}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    62
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    63
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    64
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
    65
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    66
structure Standard_Sum =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    67
  struct
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    68
  val sum       = @{const sum}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    69
  val inl       = @{const Inl}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    70
  val inr       = @{const Inr}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    71
  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
    72
  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
    73
  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
    74
  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
    75
  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
    76
  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
    77
  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
    78
  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
    79
            [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
    80
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    81
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    82
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    83
structure Ind_Package =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    84
    Add_inductive_def_Fun
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    85
      (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
    86
       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
    87
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    88
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    89
structure Gfp =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    90
  struct
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    91
  val oper      = @{const gfp}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    92
  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
    93
  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
    94
  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
    95
  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
    96
  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
    97
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    98
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    99
structure Quine_Prod =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   100
  struct
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   101
  val sigma     = @{const QSigma}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   102
  val pair      = @{const QPair}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   103
  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
   104
  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
   105
  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
   106
  val fsplitI   = @{thm qsplitI}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   107
  val fsplitD   = @{thm qsplitD}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   108
  val fsplitE   = @{thm qsplitE}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   109
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   110
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   111
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
   112
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   113
structure Quine_Sum =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   114
  struct
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   115
  val sum       = @{const qsum}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   116
  val inl       = @{const QInl}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   117
  val inr       = @{const QInr}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   118
  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
   119
  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
   120
  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
   121
  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
   122
  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
   123
  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
   124
  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
   125
  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
   126
            [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
   127
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   128
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   129
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   130
structure CoInd_Package =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   131
  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
   132
    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
   133
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   134
*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   135
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   136
end