src/ZF/Datatype_ZF.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 48891 c0eafbd55de3
child 51717 9e7d1c139569
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41777
1f7cbe39d425 more precise headers;
wenzelm
parents: 38715
diff changeset
     1
(*  Title:      ZF/Datatype_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   1997  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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     6
header{*Datatype and CoDatatype Definitions*}
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
theory Datatype_ZF
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     9
imports Inductive_ZF Univ QUniv
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 41777
diff changeset
    10
keywords "datatype" "codatatype" :: thy_decl
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    11
begin
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    12
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    13
ML_file "Tools/datatype_package.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    14
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 26056
diff changeset
    15
ML {*
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    16
(*Typechecking rules for most datatypes involving univ*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    17
structure Data_Arg =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    18
  struct
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    19
  val intrs =
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    20
      [@{thm SigmaI}, @{thm InlI}, @{thm InrI},
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    21
       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    22
       @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    23
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    24
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    25
  val elims = [make_elim @{thm InlD}, make_elim @{thm InrD},   (*for mutual recursion*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    26
               @{thm SigmaE}, @{thm sumE}];                    (*allows * and + in spec*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    27
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    28
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    29
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    30
structure Data_Package =
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    31
  Add_datatype_def_Fun
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    32
   (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
    33
    and Su=Standard_Sum
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    34
    and Ind_Package = Ind_Package
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    35
    and Datatype_Arg = Data_Arg
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    36
    val coind = false);
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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    39
(*Typechecking rules for most codatatypes involving quniv*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    40
structure CoData_Arg =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    41
  struct
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    42
  val intrs =
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    43
      [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    44
       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    45
       @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    46
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    47
  val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD},   (*for mutual recursion*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    48
               @{thm QSigmaE}, @{thm qsumE}];                    (*allows * and + in spec*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    49
  end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    50
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    51
structure CoData_Package =
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    52
  Add_datatype_def_Fun
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    53
   (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
    54
    and Su=Quine_Sum
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    55
    and Ind_Package = CoInd_Package
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    56
    and Datatype_Arg = CoData_Arg
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    57
    val coind = true);
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    58
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    59
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    60
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    61
(*Simproc for freeness reasoning: compare datatype constructors for equality*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    62
structure DataFree =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    63
struct
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    64
  val trace = Unsynchronized.ref false;
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    65
38522
de7984a7172b deglobalization
haftmann
parents: 35409
diff changeset
    66
  fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    67
    | mk_new (largs,rargs) =
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 32740
diff changeset
    68
        Balanced_Tree.make FOLogic.mk_conj
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    69
                 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    70
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    71
 val datatype_ss = @{simpset};
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    72
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    73
 fun proc sg ss old =
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    74
   let val _ =
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    75
         if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term_global sg old)
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    76
         else ()
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    77
       val (lhs,rhs) = FOLogic.dest_eq old
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    78
       val (lhead, largs) = strip_comb lhs
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    79
       and (rhead, rargs) = strip_comb rhs
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    80
       val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    81
       val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    82
       val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    83
         handle Option => raise Match;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    84
       val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    85
         handle Option => raise Match;
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    86
       val new =
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    87
           if #big_rec_name lcon_info = #big_rec_name rcon_info
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    88
               andalso not (null (#free_iffs lcon_info)) then
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    89
               if lname = rname then mk_new (largs, rargs)
38522
de7984a7172b deglobalization
haftmann
parents: 35409
diff changeset
    90
               else Const(@{const_name False},FOLogic.oT)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    91
           else raise Match
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    92
       val _ =
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    93
         if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32010
diff changeset
    94
         else ();
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    95
       val goal = Logic.mk_equals (old, new)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    96
       val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
35409
5c5bb83f2bae more antiquotations;
wenzelm
parents: 32765
diff changeset
    97
         (fn _ => rtac @{thm iff_reflection} 1 THEN
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    98
           simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    99
         handle ERROR msg =>
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26928
diff changeset
   100
         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term_global sg goal);
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   101
          raise Match)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   102
   in SOME thm end
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   103
   handle Match => NONE;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   104
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   105
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 38522
diff changeset
   106
 val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc;
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   107
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   108
end;
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   109
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
Addsimprocs [DataFree.conv];
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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   114
end