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