src/ZF/Datatype_ZF.thy
changeset 26056 6a0801279f4c
child 26480 544cef16045b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Mon Feb 11 15:40:21 2008 +0100
     1.3 @@ -0,0 +1,114 @@
     1.4 +(*  Title:      ZF/Datatype.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +header{*Datatype and CoDatatype Definitions*}
    1.12 +
    1.13 +theory Datatype_ZF
    1.14 +imports Inductive_ZF Univ QUniv
    1.15 +uses "Tools/datatype_package.ML"
    1.16 +begin
    1.17 +
    1.18 +ML_setup {*
    1.19 +(*Typechecking rules for most datatypes involving univ*)
    1.20 +structure Data_Arg =
    1.21 +  struct
    1.22 +  val intrs = 
    1.23 +      [@{thm SigmaI}, @{thm InlI}, @{thm InrI},
    1.24 +       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ}, 
    1.25 +       @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];
    1.26 +
    1.27 +
    1.28 +  val elims = [make_elim @{thm InlD}, make_elim @{thm InrD},   (*for mutual recursion*)
    1.29 +               @{thm SigmaE}, @{thm sumE}];                    (*allows * and + in spec*)
    1.30 +  end;
    1.31 +
    1.32 +
    1.33 +structure Data_Package = 
    1.34 +  Add_datatype_def_Fun
    1.35 +   (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    1.36 +    and Su=Standard_Sum
    1.37 +    and Ind_Package = Ind_Package
    1.38 +    and Datatype_Arg = Data_Arg
    1.39 +    val coind = false);
    1.40 +
    1.41 +
    1.42 +(*Typechecking rules for most codatatypes involving quniv*)
    1.43 +structure CoData_Arg =
    1.44 +  struct
    1.45 +  val intrs = 
    1.46 +      [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
    1.47 +       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv}, 
    1.48 +       @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];
    1.49 +
    1.50 +  val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD},   (*for mutual recursion*)
    1.51 +               @{thm QSigmaE}, @{thm qsumE}];                    (*allows * and + in spec*)
    1.52 +  end;
    1.53 +
    1.54 +structure CoData_Package = 
    1.55 +  Add_datatype_def_Fun
    1.56 +   (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    1.57 +    and Su=Quine_Sum
    1.58 +    and Ind_Package = CoInd_Package
    1.59 +    and Datatype_Arg = CoData_Arg
    1.60 +    val coind = true);
    1.61 +
    1.62 +
    1.63 +
    1.64 +(*Simproc for freeness reasoning: compare datatype constructors for equality*)
    1.65 +structure DataFree =
    1.66 +struct
    1.67 +  val trace = ref false;
    1.68 +
    1.69 +  fun mk_new ([],[]) = Const("True",FOLogic.oT)
    1.70 +    | mk_new (largs,rargs) =
    1.71 +        BalancedTree.make FOLogic.mk_conj
    1.72 +                 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    1.73 +
    1.74 + val datatype_ss = @{simpset};
    1.75 +
    1.76 + fun proc sg ss old =
    1.77 +   let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    1.78 +                                       string_of_cterm (cterm_of sg old))
    1.79 +               else ()
    1.80 +       val (lhs,rhs) = FOLogic.dest_eq old
    1.81 +       val (lhead, largs) = strip_comb lhs
    1.82 +       and (rhead, rargs) = strip_comb rhs
    1.83 +       val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
    1.84 +       val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
    1.85 +       val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname)
    1.86 +         handle Option => raise Match;
    1.87 +       val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
    1.88 +         handle Option => raise Match;
    1.89 +       val new = 
    1.90 +           if #big_rec_name lcon_info = #big_rec_name rcon_info 
    1.91 +               andalso not (null (#free_iffs lcon_info)) then
    1.92 +               if lname = rname then mk_new (largs, rargs)
    1.93 +               else Const("False",FOLogic.oT)
    1.94 +           else raise Match
    1.95 +       val _ = if !trace then 
    1.96 +                 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
    1.97 +               else ();
    1.98 +       val goal = Logic.mk_equals (old, new)
    1.99 +       val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
   1.100 +         (fn _ => rtac iff_reflection 1 THEN
   1.101 +           simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
   1.102 +         handle ERROR msg =>
   1.103 +         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
   1.104 +          raise Match)
   1.105 +   in SOME thm end
   1.106 +   handle Match => NONE;
   1.107 +
   1.108 +
   1.109 + val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
   1.110 +
   1.111 +end;
   1.112 +
   1.113 +
   1.114 +Addsimprocs [DataFree.conv];
   1.115 +*}
   1.116 +
   1.117 +end