tuned signature;
authorwenzelm
Sat Dec 17 13:08:03 2011 +0100 (2011-12-17)
changeset 459096fe61da4c467
parent 45908 143d2514347f
child 45910 566c34b64f70
tuned signature;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Set.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/rep_datatype.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 17 12:51:30 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 17 13:08:03 2011 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  
     1.5  (*******************************)
     1.6  
     1.7 -val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
     1.8 +val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of Datatype.distinct_lemma);
     1.9  
    1.10  
    1.11  (** simplification procedure for sorting permutations **)
    1.12 @@ -769,7 +769,7 @@
    1.13            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
    1.14          val dist =
    1.15            Drule.export_without_context
    1.16 -            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    1.17 +            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] Datatype.distinct_lemma);
    1.18          val (thy', defs', eqns') = fold (make_constr_def tname T T')
    1.19            (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
    1.20        in
     2.1 --- a/src/HOL/Set.thy	Sat Dec 17 12:51:30 2011 +0100
     2.2 +++ b/src/HOL/Set.thy	Sat Dec 17 13:08:03 2011 +0100
     2.3 @@ -1560,9 +1560,6 @@
     2.4  lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
     2.5    by blast
     2.6  
     2.7 -lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
     2.8 -  by iprover
     2.9 -
    2.10  lemma ball_simps [simp, no_atp]:
    2.11    "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
    2.12    "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
    2.13 @@ -1796,7 +1793,6 @@
    2.14  val bex_triv = @{thm bex_triv}
    2.15  val bspec = @{thm bspec}
    2.16  val contra_subsetD = @{thm contra_subsetD}
    2.17 -val distinct_lemma = @{thm distinct_lemma}
    2.18  val equalityCE = @{thm equalityCE}
    2.19  val equalityD1 = @{thm equalityD1}
    2.20  val equalityD2 = @{thm equalityD2}
     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 17 12:51:30 2011 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 17 13:08:03 2011 +0100
     3.3 @@ -10,6 +10,7 @@
     3.4  signature DATATYPE =
     3.5  sig
     3.6    include DATATYPE_DATA
     3.7 +  val distinct_lemma: thm
     3.8    type spec =
     3.9      (binding * (string * sort) list * mixfix) *
    3.10      (binding * typ list * mixfix) list
    3.11 @@ -28,6 +29,7 @@
    3.12  
    3.13  (** auxiliary **)
    3.14  
    3.15 +val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover};
    3.16  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    3.17  
    3.18  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
     4.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 17 12:51:30 2011 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 17 13:08:03 2011 +0100
     4.3 @@ -20,16 +20,12 @@
     4.4  structure Rep_Datatype: REP_DATATYPE =
     4.5  struct
     4.6  
     4.7 -type config = Datatype_Aux.config;
     4.8 -type descr = Datatype_Aux.descr;
     4.9 -
    4.10 -
    4.11 -
    4.12  (** derived definitions and proofs **)
    4.13  
    4.14  (* case distinction theorems *)
    4.15  
    4.16 -fun prove_casedist_thms (config : config) new_type_names descr induct case_names_exhausts thy =
    4.17 +fun prove_casedist_thms (config : Datatype_Aux.config)
    4.18 +    new_type_names descr induct case_names_exhausts thy =
    4.19    let
    4.20      val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
    4.21  
    4.22 @@ -76,7 +72,7 @@
    4.23  
    4.24  (* primrec combinators *)
    4.25  
    4.26 -fun prove_primrec_thms (config : config) new_type_names descr
    4.27 +fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr
    4.28      injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
    4.29    let
    4.30      val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
    4.31 @@ -273,7 +269,8 @@
    4.32  
    4.33  (* case combinators *)
    4.34  
    4.35 -fun prove_case_thms (config : config) new_type_names descr reccomb_names primrec_thms thy =
    4.36 +fun prove_case_thms (config : Datatype_Aux.config)
    4.37 +    new_type_names descr reccomb_names primrec_thms thy =
    4.38    let
    4.39      val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
    4.40  
    4.41 @@ -348,7 +345,7 @@
    4.42  
    4.43  (* case splitting *)
    4.44  
    4.45 -fun prove_split_thms (config : config)
    4.46 +fun prove_split_thms (config : Datatype_Aux.config)
    4.47      new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
    4.48    let
    4.49      val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
    4.50 @@ -398,7 +395,7 @@
    4.51  
    4.52  (* additional theorems for TFL *)
    4.53  
    4.54 -fun prove_nchotomys (config : config) new_type_names descr casedist_thms thy =
    4.55 +fun prove_nchotomys (config : Datatype_Aux.config) new_type_names descr casedist_thms thy =
    4.56    let
    4.57      val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
    4.58