moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
authorhaftmann
Fri May 23 16:05:04 2008 +0200 (2008-05-23)
changeset 26969cf3f998d0631
parent 26968 bb0a56a66180
child 26970 bc28e7bcb765
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri May 23 16:05:02 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri May 23 16:05:04 2008 +0200
     1.3 @@ -850,26 +850,22 @@
     1.4  
     1.5      (* prove distinctness theorems *)
     1.6  
     1.7 -    val distinctness_limit = Config.get_thy thy8 DatatypeProp.distinctness_limit;
     1.8 -    val thy8' = Config.put_thy DatatypeProp.distinctness_limit 1000 thy8;
     1.9 -    val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8';
    1.10 -    val thy8 = Config.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
    1.11 -
    1.12 +    val distinct_props = DatatypeProp.make_distincts descr' sorts';
    1.13      val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
    1.14        dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
    1.15          (constr_rep_thmss ~~ dist_lemmas);
    1.16  
    1.17 -    fun prove_distinct_thms (_, []) = []
    1.18 -      | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
    1.19 +    fun prove_distinct_thms _ (_, []) = []
    1.20 +      | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
    1.21            let
    1.22              val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
    1.23                simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
    1.24 -          in dist_thm::(standard (dist_thm RS not_sym))::
    1.25 -            (prove_distinct_thms (p, ts))
    1.26 +          in dist_thm :: (standard (dist_thm RS not_sym)) ::
    1.27 +            (prove_distinct_thms p (k, ts))
    1.28            end;
    1.29  
    1.30 -    val distinct_thms = map prove_distinct_thms
    1.31 -      (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props);
    1.32 +    val distinct_thms = map2 prove_distinct_thms
    1.33 +      (constr_rep_thmss ~~ dist_lemmas) distinct_props;
    1.34  
    1.35      (** prove equations for permutation functions **)
    1.36  
     2.1 --- a/src/HOL/Tools/datatype_prop.ML	Fri May 23 16:05:02 2008 +0200
     2.2 +++ b/src/HOL/Tools/datatype_prop.ML	Fri May 23 16:05:04 2008 +0200
     2.3 @@ -12,6 +12,8 @@
     2.4    val indexify_names: string list -> string list
     2.5    val make_tnames: typ list -> string list
     2.6    val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
     2.7 +  val make_distincts : DatatypeAux.descr list ->
     2.8 +    (string * sort) list -> (int * term list) list
     2.9    val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
    2.10    val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
    2.11    val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list ->
    2.12 @@ -20,8 +22,6 @@
    2.13      (string * sort) list -> theory -> term list
    2.14    val make_cases : string list -> DatatypeAux.descr list ->
    2.15      (string * sort) list -> theory -> term list list
    2.16 -  val make_distincts : string list -> DatatypeAux.descr list ->
    2.17 -    (string * sort) list -> theory -> term list list
    2.18    val make_splits : string list -> DatatypeAux.descr list ->
    2.19      (string * sort) list -> theory -> (term * term) list
    2.20    val make_weak_case_congs : string list -> DatatypeAux.descr list ->
    2.21 @@ -59,6 +59,43 @@
    2.22    in indexify_names (map type_name Ts) end;
    2.23  
    2.24  
    2.25 +(************************* distinctness of constructors ***********************)
    2.26 +
    2.27 +fun make_distincts descr sorts =
    2.28 +  let
    2.29 +    val descr' = List.concat descr;
    2.30 +    val recTs = get_rec_types descr' sorts;
    2.31 +    val newTs = Library.take (length (hd descr), recTs);
    2.32 +
    2.33 +    fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
    2.34 +
    2.35 +    fun make_distincts' _ [] = []
    2.36 +      | make_distincts' T ((cname, cargs)::constrs) =
    2.37 +          let
    2.38 +            val frees = map Free ((make_tnames cargs) ~~ cargs);
    2.39 +            val t = list_comb (Const (cname, cargs ---> T), frees);
    2.40 +
    2.41 +            fun make_distincts'' [] = []
    2.42 +              | make_distincts'' ((cname', cargs')::constrs') =
    2.43 +                  let
    2.44 +                    val frees' = map Free ((map ((op ^) o (rpair "'"))
    2.45 +                      (make_tnames cargs')) ~~ cargs');
    2.46 +                    val t' = list_comb (Const (cname', cargs' ---> T), frees')
    2.47 +                  in
    2.48 +                    HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')) ::
    2.49 +                    HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t', t)) ::
    2.50 +                      make_distincts'' constrs'
    2.51 +                  end
    2.52 +
    2.53 +          in make_distincts'' constrs @ make_distincts' T constrs end;
    2.54 +
    2.55 +    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
    2.56 +
    2.57 +  in
    2.58 +    map2 (fn ((_, (_, _, constrs))) => fn T =>
    2.59 +      (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs
    2.60 +  end;
    2.61 +
    2.62  (************************* injectivity of constructors ************************)
    2.63  
    2.64  fun make_injs descr sorts =
    2.65 @@ -268,45 +305,6 @@
    2.66        ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
    2.67    end;
    2.68  
    2.69 -(************************* distinctness of constructors ***********************)
    2.70 -
    2.71 -fun make_distincts new_type_names descr sorts thy =
    2.72 -  let
    2.73 -    val descr' = List.concat descr;
    2.74 -    val recTs = get_rec_types descr' sorts;
    2.75 -    val newTs = Library.take (length (hd descr), recTs);
    2.76 -
    2.77 -    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
    2.78 -
    2.79 -    fun make_distincts_1 _ [] = []
    2.80 -      | make_distincts_1 T ((cname, cargs)::constrs) =
    2.81 -          let
    2.82 -            val Ts = map (typ_of_dtyp descr' sorts) cargs;
    2.83 -            val frees = map Free ((make_tnames Ts) ~~ Ts);
    2.84 -            val t = list_comb (Const (cname, Ts ---> T), frees);
    2.85 -
    2.86 -            fun make_distincts' [] = []
    2.87 -              | make_distincts' ((cname', cargs')::constrs') =
    2.88 -                  let
    2.89 -                    val Ts' = map (typ_of_dtyp descr' sorts) cargs';
    2.90 -                    val frees' = map Free ((map ((op ^) o (rpair "'"))
    2.91 -                      (make_tnames Ts')) ~~ Ts');
    2.92 -                    val t' = list_comb (Const (cname', Ts' ---> T), frees')
    2.93 -                  in
    2.94 -                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
    2.95 -                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t', t)))::
    2.96 -                      (make_distincts' constrs')
    2.97 -                  end
    2.98 -
    2.99 -          in (make_distincts' constrs) @ (make_distincts_1 T constrs)
   2.100 -          end;
   2.101 -
   2.102 -  in map (fn (((_, (_, _, constrs)), T), tname) =>
   2.103 -      if length constrs < Config.get_thy thy distinctness_limit
   2.104 -      then make_distincts_1 T constrs else [])
   2.105 -        ((hd descr) ~~ newTs ~~ new_type_names)
   2.106 -  end;
   2.107 -
   2.108  
   2.109  (*************************** the "split" - equations **************************)
   2.110  
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri May 23 16:05:02 2008 +0200
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri May 23 16:05:04 2008 +0200
     3.3 @@ -519,17 +519,21 @@
     3.4        dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
     3.5          (constr_rep_thms ~~ dist_lemmas);
     3.6  
     3.7 -    fun prove_distinct_thms (_, []) = []
     3.8 -      | prove_distinct_thms (dist_rewrites', t::_::ts) =
     3.9 -          let
    3.10 -            val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    3.11 -              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    3.12 -          in dist_thm::(standard (dist_thm RS not_sym))::
    3.13 -            (prove_distinct_thms (dist_rewrites', ts))
    3.14 -          end;
    3.15 +    fun prove_distinct_thms _ _ (_, []) = []
    3.16 +      | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) =
    3.17 +          if k >= lim then [] else let
    3.18 +            fun prove [] = []
    3.19 +              | prove (t :: _ :: ts) =
    3.20 +                  let
    3.21 +                    val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    3.22 +                      EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    3.23 +                  in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
    3.24 +          in prove ts end;
    3.25  
    3.26 -    val distinct_thms = map prove_distinct_thms (dist_rewrites ~~
    3.27 -      DatatypeProp.make_distincts new_type_names descr sorts thy5);
    3.28 +    val distincts = DatatypeProp.make_distincts descr sorts;
    3.29 +    val distinct_thms = map2 (prove_distinct_thms
    3.30 +      (Config.get_thy thy5 DatatypeProp.distinctness_limit))
    3.31 +      dist_rewrites distincts;
    3.32  
    3.33      val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
    3.34        if length constrs < Config.get_thy thy5 DatatypeProp.distinctness_limit