src/ZF/Datatype_ZF.thy
author wenzelm
Sat Nov 04 19:17:19 2017 +0100 (21 months ago)
changeset 67006 b1278ed3cd46
parent 62913 13252110a6fe
permissions -rw-r--r--
prefer main entry points of HOL;
wenzelm@41777
     1
(*  Title:      ZF/Datatype_ZF.thy
krauss@26056
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
krauss@26056
     3
    Copyright   1997  University of Cambridge
krauss@26056
     4
*)
krauss@26056
     5
wenzelm@60770
     6
section\<open>Datatype and CoDatatype Definitions\<close>
krauss@26056
     7
krauss@26056
     8
theory Datatype_ZF
krauss@26056
     9
imports Inductive_ZF Univ QUniv
wenzelm@46950
    10
keywords "datatype" "codatatype" :: thy_decl
krauss@26056
    11
begin
krauss@26056
    12
wenzelm@48891
    13
ML_file "Tools/datatype_package.ML"
wenzelm@48891
    14
wenzelm@60770
    15
ML \<open>
krauss@26056
    16
(*Typechecking rules for most datatypes involving univ*)
krauss@26056
    17
structure Data_Arg =
krauss@26056
    18
  struct
wenzelm@32432
    19
  val intrs =
krauss@26056
    20
      [@{thm SigmaI}, @{thm InlI}, @{thm InrI},
wenzelm@32432
    21
       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
krauss@26056
    22
       @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];
krauss@26056
    23
krauss@26056
    24
krauss@26056
    25
  val elims = [make_elim @{thm InlD}, make_elim @{thm InrD},   (*for mutual recursion*)
krauss@26056
    26
               @{thm SigmaE}, @{thm sumE}];                    (*allows * and + in spec*)
krauss@26056
    27
  end;
krauss@26056
    28
krauss@26056
    29
wenzelm@32432
    30
structure Data_Package =
krauss@26056
    31
  Add_datatype_def_Fun
krauss@26056
    32
   (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
krauss@26056
    33
    and Su=Standard_Sum
krauss@26056
    34
    and Ind_Package = Ind_Package
krauss@26056
    35
    and Datatype_Arg = Data_Arg
krauss@26056
    36
    val coind = false);
krauss@26056
    37
krauss@26056
    38
krauss@26056
    39
(*Typechecking rules for most codatatypes involving quniv*)
krauss@26056
    40
structure CoData_Arg =
krauss@26056
    41
  struct
wenzelm@32432
    42
  val intrs =
krauss@26056
    43
      [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
wenzelm@32432
    44
       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
krauss@26056
    45
       @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];
krauss@26056
    46
krauss@26056
    47
  val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD},   (*for mutual recursion*)
krauss@26056
    48
               @{thm QSigmaE}, @{thm qsumE}];                    (*allows * and + in spec*)
krauss@26056
    49
  end;
krauss@26056
    50
wenzelm@32432
    51
structure CoData_Package =
krauss@26056
    52
  Add_datatype_def_Fun
krauss@26056
    53
   (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
krauss@26056
    54
    and Su=Quine_Sum
krauss@26056
    55
    and Ind_Package = CoInd_Package
krauss@26056
    56
    and Datatype_Arg = CoData_Arg
krauss@26056
    57
    val coind = true);
krauss@26056
    58
krauss@26056
    59
krauss@26056
    60
krauss@26056
    61
(*Simproc for freeness reasoning: compare datatype constructors for equality*)
krauss@26056
    62
structure DataFree =
krauss@26056
    63
struct
wenzelm@32740
    64
  val trace = Unsynchronized.ref false;
krauss@26056
    65
haftmann@38522
    66
  fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
krauss@26056
    67
    | mk_new (largs,rargs) =
wenzelm@32765
    68
        Balanced_Tree.make FOLogic.mk_conj
krauss@26056
    69
                 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
krauss@26056
    70
wenzelm@51717
    71
 val datatype_ss = simpset_of @{context};
krauss@26056
    72
wenzelm@61144
    73
 fun proc ctxt ct =
wenzelm@61144
    74
   let val old = Thm.term_of ct
wenzelm@61144
    75
       val thy = Proof_Context.theory_of ctxt
wenzelm@51717
    76
       val _ =
wenzelm@51717
    77
         if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term ctxt old)
wenzelm@32432
    78
         else ()
krauss@26056
    79
       val (lhs,rhs) = FOLogic.dest_eq old
krauss@26056
    80
       val (lhead, largs) = strip_comb lhs
krauss@26056
    81
       and (rhead, rargs) = strip_comb rhs
krauss@26056
    82
       val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
krauss@26056
    83
       val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
wenzelm@51717
    84
       val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname)
wenzelm@51930
    85
         handle Option.Option => raise Match;
wenzelm@51717
    86
       val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname)
wenzelm@51930
    87
         handle Option.Option => raise Match;
wenzelm@32432
    88
       val new =
wenzelm@32432
    89
           if #big_rec_name lcon_info = #big_rec_name rcon_info
krauss@26056
    90
               andalso not (null (#free_iffs lcon_info)) then
krauss@26056
    91
               if lname = rname then mk_new (largs, rargs)
haftmann@38522
    92
               else Const(@{const_name False},FOLogic.oT)
krauss@26056
    93
           else raise Match
wenzelm@32432
    94
       val _ =
wenzelm@51717
    95
         if !trace then writeln ("NEW = " ^ Syntax.string_of_term ctxt new)
wenzelm@32432
    96
         else ();
krauss@26056
    97
       val goal = Logic.mk_equals (old, new)
wenzelm@51717
    98
       val thm = Goal.prove ctxt [] [] goal
wenzelm@59498
    99
         (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN
wenzelm@51717
   100
           simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1)
krauss@26056
   101
         handle ERROR msg =>
wenzelm@51717
   102
         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
krauss@26056
   103
          raise Match)
krauss@26056
   104
   in SOME thm end
krauss@26056
   105
   handle Match => NONE;
krauss@26056
   106
krauss@26056
   107
wenzelm@61144
   108
  val conv =
wenzelm@61144
   109
    Simplifier.make_simproc @{context} "data_free"
wenzelm@62913
   110
     {lhss = [@{term "(x::i) = y"}], proc = K proc};
krauss@26056
   111
krauss@26056
   112
end;
wenzelm@60770
   113
\<close>
krauss@26056
   114
wenzelm@60770
   115
setup \<open>
wenzelm@54388
   116
  Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv])
wenzelm@60770
   117
\<close>
krauss@26056
   118
krauss@26056
   119
end