src/ZF/Datatype.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 7693 c3e0c26e7d6f
child 12134 7049eead7a50
permissions -rw-r--r--
cleaned up;
     1 (*  Title:      ZF/Datatype.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 (Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
     7 *)
     8 
     9 
    10 (*Typechecking rules for most datatypes involving univ*)
    11 structure Data_Arg =
    12   struct
    13   val intrs = 
    14       [SigmaI, InlI, InrI,
    15        Pair_in_univ, Inl_in_univ, Inr_in_univ, 
    16        zero_in_univ, A_into_univ, nat_into_univ, UnCI];
    17 
    18 
    19   val elims = [make_elim InlD, make_elim InrD,   (*for mutual recursion*)
    20 	       SigmaE, sumE];			 (*allows * and + in spec*)
    21   end;
    22 
    23 
    24 structure Data_Package = 
    25     Add_datatype_def_Fun
    26       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    27        and Su=Standard_Sum
    28        and Ind_Package = Ind_Package
    29        and Datatype_Arg = Data_Arg);
    30 
    31 
    32 (*Typechecking rules for most codatatypes involving quniv*)
    33 structure CoData_Arg =
    34   struct
    35   val intrs = 
    36       [QSigmaI, QInlI, QInrI,
    37        QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    38        zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
    39 
    40   val elims = [make_elim QInlD, make_elim QInrD,   (*for mutual recursion*)
    41 	       QSigmaE, qsumE];			   (*allows * and + in spec*)
    42   end;
    43 
    44 structure CoData_Package = 
    45     Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    46                           and Su=Quine_Sum
    47 			  and Ind_Package = CoInd_Package
    48 			  and Datatype_Arg = CoData_Arg);
    49 
    50 
    51 
    52 (*Simproc for freeness reasoning: compare datatype constructors for equality*)
    53 structure DataFree =
    54 struct
    55   (*prove while suppressing timing information*)
    56   fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
    57 
    58   val trace = ref false;
    59 
    60   fun mk_new ([],[]) = Const("True",FOLogic.oT)
    61     | mk_new (largs,rargs) =
    62 	fold_bal FOLogic.mk_conj
    63 		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    64 
    65 
    66  fun proc sg _ old =
    67    let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    68 				       string_of_cterm (cterm_of sg old))
    69 	       else ()
    70        val (lhs,rhs) = FOLogic.dest_eq old
    71        val (lhead, largs) = strip_comb lhs
    72        and (rhead, rargs) = strip_comb rhs
    73        val lname = #1 (dest_Const lhead)
    74        and rname = #1 (dest_Const rhead)
    75        val lcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, lname))
    76        and rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
    77        val new = 
    78 	   if #big_rec_name lcon_info = #big_rec_name rcon_info 
    79 	       andalso not (null (#free_iffs lcon_info)) then
    80 	       if lname = rname then mk_new (largs, rargs)
    81 	       else Const("False",FOLogic.oT)
    82 	   else raise Match
    83        val _ = if !trace then 
    84 		 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
    85 	       else ()
    86        val ct = Thm.cterm_of sg (Logic.mk_equals (old, new))
    87        val thm = prove ct 
    88 		   (fn _ => [rtac iff_reflection 1,
    89 			     simp_tac (simpset_of Datatype.thy
    90   				          addsimps #free_iffs lcon_info) 1])
    91 	 handle ERROR =>
    92 	 error("data_free simproc:\nfailed to prove " ^
    93 	       string_of_cterm ct)
    94    in Some thm end
    95    handle _ => None;
    96 
    97 
    98  val conv = 
    99      Simplifier.mk_simproc "data_free"
   100        [Thm.read_cterm (sign_of ZF.thy) ("(x::i) = y", FOLogic.oT)]
   101        proc;
   102 end;
   103 
   104 
   105 Addsimprocs [DataFree.conv];