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