more precise spec rules for selectors
authorblanchet
Fri Feb 14 07:53:46 2014 +0100 (2014-02-14)
changeset 55471198498f861ee
parent 55470 46e6e1d91056
child 55472 990651bfc65b
more precise spec rules for selectors
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -225,9 +225,6 @@
     1.4  
     1.5  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
     1.6  
     1.7 -fun lhs_head_of_hd (thm :: _) =
     1.8 -  [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))];
     1.9 -
    1.10  fun flat_rec_arg_args xss =
    1.11    (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
    1.12       order. The second line is for compatibility with the old datatype package. *)
    1.13 @@ -1353,9 +1350,9 @@
    1.14              in
    1.15                (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
    1.16                 lthy
    1.17 -               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd map_thms)
    1.18 -               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd rel_eq_thms)
    1.19 -               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd set_thms)
    1.20 +               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) map_thms)
    1.21 +               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) rel_eq_thms)
    1.22 +               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) set_thms)
    1.23                 |> Local_Theory.notes (anonymous_notes @ notes)
    1.24                 |> snd)
    1.25              end;
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     2.3 @@ -941,8 +941,10 @@
     2.4          (ctr_sugar,
     2.5           lthy
     2.6           |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
     2.7 -         |> Spec_Rules.add Spec_Rules.Equational (flat selss, all_sel_thms)
     2.8 -         |> fold (Spec_Rules.add Spec_Rules.Equational) (map single discs ~~ nontriv_disc_eq_thmss)
     2.9 +         |> fold (Spec_Rules.add Spec_Rules.Equational)
    2.10 +           (AList.group (eq_list (op aconv)) (map (`lhs_heads_of) all_sel_thms))
    2.11 +         |> fold (Spec_Rules.add Spec_Rules.Equational)
    2.12 +           (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
    2.13           |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.14                (fn phi => Case_Translation.register
    2.15                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
     3.3 @@ -39,6 +39,8 @@
     3.4    val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
     3.5    val subst_nonatomic_types: (typ * typ) list -> term -> term
     3.6  
     3.7 +  val lhs_heads_of : thm -> term list
     3.8 +
     3.9    val mk_predT: typ list -> typ
    3.10    val mk_pred1T: typ -> typ
    3.11  
    3.12 @@ -168,6 +170,9 @@
    3.13  fun subst_nonatomic_types [] = I
    3.14    | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst);
    3.15  
    3.16 +fun lhs_heads_of thm =
    3.17 +  [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))];
    3.18 +
    3.19  fun mk_predT Ts = Ts ---> HOLogic.boolT;
    3.20  fun mk_pred1T T = mk_predT [T];
    3.21  
     4.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Feb 14 07:53:46 2014 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Feb 14 07:53:46 2014 +0100
     4.3 @@ -141,7 +141,7 @@
     4.4  
     4.5  fun the_pred_data ctxt name =
     4.6    (case lookup_pred_data ctxt name of
     4.7 -    NONE => error ("No such predicate " ^ quote name)  
     4.8 +    NONE => error ("No such predicate: " ^ quote name)  
     4.9    | SOME data => data)
    4.10  
    4.11  val is_registered = is_some oo lookup_pred_data