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