author wenzelm
Tue, 29 Sep 2009 22:48:24 +0200
changeset 32765 3032c0308019
parent 32740 9dd0a2f83429
child 35409 5c5bb83f2bae
permissions -rw-r--r--
modernized Balanced_Tree;

(*  Title:      ZF/Datatype.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

header{*Datatype and CoDatatype Definitions*}

theory Datatype_ZF
imports Inductive_ZF Univ QUniv
uses "Tools/datatype_package.ML"

ML {*
(*Typechecking rules for most datatypes involving univ*)
structure Data_Arg =
  val intrs =
      [@{thm SigmaI}, @{thm InlI}, @{thm InrI},
       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
       @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];

  val elims = [make_elim @{thm InlD}, make_elim @{thm InrD},   (*for mutual recursion*)
               @{thm SigmaE}, @{thm sumE}];                    (*allows * and + in spec*)

structure Data_Package =
   (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    and Su=Standard_Sum
    and Ind_Package = Ind_Package
    and Datatype_Arg = Data_Arg
    val coind = false);

(*Typechecking rules for most codatatypes involving quniv*)
structure CoData_Arg =
  val intrs =
      [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
       @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];

  val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD},   (*for mutual recursion*)
               @{thm QSigmaE}, @{thm qsumE}];                    (*allows * and + in spec*)

structure CoData_Package =
   (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    and Su=Quine_Sum
    and Ind_Package = CoInd_Package
    and Datatype_Arg = CoData_Arg
    val coind = true);

(*Simproc for freeness reasoning: compare datatype constructors for equality*)
structure DataFree =
  val trace = Unsynchronized.ref false;

  fun mk_new ([],[]) = Const("True",FOLogic.oT)
    | mk_new (largs,rargs) =
        Balanced_Tree.make FOLogic.mk_conj
                 (map FOLogic.mk_eq ( (largs,rargs)));

 val datatype_ss = @{simpset};

 fun proc sg ss old =
   let val _ =
         if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term_global sg old)
         else ()
       val (lhs,rhs) = FOLogic.dest_eq old
       val (lhead, largs) = strip_comb lhs
       and (rhead, rargs) = strip_comb rhs
       val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
       val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
       val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname)
         handle Option => raise Match;
       val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
         handle Option => raise Match;
       val new =
           if #big_rec_name lcon_info = #big_rec_name rcon_info
               andalso not (null (#free_iffs lcon_info)) then
               if lname = rname then mk_new (largs, rargs)
               else Const("False",FOLogic.oT)
           else raise Match
       val _ =
         if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
         else ();
       val goal = Logic.mk_equals (old, new)
       val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
         (fn _ => rtac iff_reflection 1 THEN
           simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
         handle ERROR msg =>
         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term_global sg goal);
          raise Match)
   in SOME thm end
   handle Match => NONE;

 val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;


Addsimprocs [DataFree.conv];