src/ZF/Datatype_ZF.thy
changeset 32432 64f30bdd3ba1
parent 32010 cb1a1c94b4cd
child 32740 9dd0a2f83429
     1.1 --- a/src/ZF/Datatype_ZF.thy	Fri Aug 28 18:23:24 2009 +0200
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Fri Aug 28 21:04:03 2009 +0200
     1.3 @@ -14,9 +14,9 @@
     1.4  (*Typechecking rules for most datatypes involving univ*)
     1.5  structure Data_Arg =
     1.6    struct
     1.7 -  val intrs = 
     1.8 +  val intrs =
     1.9        [@{thm SigmaI}, @{thm InlI}, @{thm InrI},
    1.10 -       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ}, 
    1.11 +       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
    1.12         @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];
    1.13  
    1.14  
    1.15 @@ -25,7 +25,7 @@
    1.16    end;
    1.17  
    1.18  
    1.19 -structure Data_Package = 
    1.20 +structure Data_Package =
    1.21    Add_datatype_def_Fun
    1.22     (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    1.23      and Su=Standard_Sum
    1.24 @@ -37,16 +37,16 @@
    1.25  (*Typechecking rules for most codatatypes involving quniv*)
    1.26  structure CoData_Arg =
    1.27    struct
    1.28 -  val intrs = 
    1.29 +  val intrs =
    1.30        [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
    1.31 -       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv}, 
    1.32 +       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
    1.33         @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];
    1.34  
    1.35    val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD},   (*for mutual recursion*)
    1.36                 @{thm QSigmaE}, @{thm qsumE}];                    (*allows * and + in spec*)
    1.37    end;
    1.38  
    1.39 -structure CoData_Package = 
    1.40 +structure CoData_Package =
    1.41    Add_datatype_def_Fun
    1.42     (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    1.43      and Su=Quine_Sum
    1.44 @@ -69,9 +69,9 @@
    1.45   val datatype_ss = @{simpset};
    1.46  
    1.47   fun proc sg ss old =
    1.48 -   let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    1.49 -                                       Display.string_of_cterm (cterm_of sg old))
    1.50 -               else ()
    1.51 +   let val _ =
    1.52 +         if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term_global sg old)
    1.53 +         else ()
    1.54         val (lhs,rhs) = FOLogic.dest_eq old
    1.55         val (lhead, largs) = strip_comb lhs
    1.56         and (rhead, rargs) = strip_comb rhs
    1.57 @@ -81,15 +81,15 @@
    1.58           handle Option => raise Match;
    1.59         val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
    1.60           handle Option => raise Match;
    1.61 -       val new = 
    1.62 -           if #big_rec_name lcon_info = #big_rec_name rcon_info 
    1.63 +       val new =
    1.64 +           if #big_rec_name lcon_info = #big_rec_name rcon_info
    1.65                 andalso not (null (#free_iffs lcon_info)) then
    1.66                 if lname = rname then mk_new (largs, rargs)
    1.67                 else Const("False",FOLogic.oT)
    1.68             else raise Match
    1.69 -       val _ = if !trace then 
    1.70 -                 writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new))
    1.71 -               else ();
    1.72 +       val _ =
    1.73 +         if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
    1.74 +         else ();
    1.75         val goal = Logic.mk_equals (old, new)
    1.76         val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
    1.77           (fn _ => rtac iff_reflection 1 THEN