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