clarified strip_shyps: proper type witnesses for present sorts;
authorwenzelm
Mon Jul 06 22:42:27 2009 +0200 (2009-07-06)
changeset 319477daee3bed3af
parent 31946 99ac0321cd47
child 31948 ea8c8bf47ce3
clarified strip_shyps: proper type witnesses for present sorts;
moved fold_terms to thm.ML;
src/Pure/more_thm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/more_thm.ML	Mon Jul 06 22:41:00 2009 +0200
     1.2 +++ b/src/Pure/more_thm.ML	Mon Jul 06 22:42:27 2009 +0200
     1.3 @@ -31,7 +31,6 @@
     1.4    val check_shyps: sort list -> thm -> thm
     1.5    val is_dummy: thm -> bool
     1.6    val plain_prop_of: thm -> term
     1.7 -  val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
     1.8    val add_thm: thm -> thm list -> thm list
     1.9    val del_thm: thm -> thm list -> thm list
    1.10    val merge_thms: thm list * thm list -> thm list
    1.11 @@ -211,10 +210,6 @@
    1.12      else prop
    1.13    end;
    1.14  
    1.15 -fun fold_terms f th =
    1.16 -  let val {tpairs, prop, hyps, ...} = Thm.rep_thm th
    1.17 -  in fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps end;
    1.18 -
    1.19  
    1.20  (* collections of theorems in canonical order *)
    1.21  
     2.1 --- a/src/Pure/thm.ML	Mon Jul 06 22:41:00 2009 +0200
     2.2 +++ b/src/Pure/thm.ML	Mon Jul 06 22:42:27 2009 +0200
     2.3 @@ -115,6 +115,7 @@
     2.4    val incr_indexes_cterm: int -> cterm -> cterm
     2.5    val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
     2.6    val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
     2.7 +  val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
     2.8    val terms_of_tpairs: (term * term) list -> term list
     2.9    val full_prop_of: thm -> term
    2.10    val maxidx_of: thm -> int
    2.11 @@ -367,6 +368,9 @@
    2.12      prop = cterm maxidx prop}
    2.13    end;
    2.14  
    2.15 +fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
    2.16 +  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
    2.17 +
    2.18  fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
    2.19  
    2.20  fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
    2.21 @@ -473,29 +477,28 @@
    2.22  
    2.23  (** sort contexts of theorems **)
    2.24  
    2.25 -fun present_sorts (Thm (_, {hyps, tpairs, prop, ...})) =
    2.26 -  fold (fn (t, u) => Sorts.insert_term t o Sorts.insert_term u) tpairs
    2.27 -    (Sorts.insert_terms hyps (Sorts.insert_term prop []));
    2.28 -
    2.29 -(*remove extra sorts that are non-empty by virtue of type signature information*)
    2.30 +(*remove extra sorts that are witnessed by type signature information*)
    2.31  fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
    2.32    | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
    2.33        let
    2.34          val thy = Theory.deref thy_ref;
    2.35 -        val present = present_sorts thm;
    2.36 -        val extra = Sorts.subtract present shyps;
    2.37 -        val extra' =
    2.38 -          Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
    2.39 +        val present =
    2.40 +          (fold_terms o fold_types o fold_atyps)
    2.41 +            (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
    2.42 +              | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
    2.43 +        val extra = fold (Sorts.remove_sort o #2) present shyps;
    2.44 +        val witnessed = Sign.witness_sorts thy present extra;
    2.45 +        val extra' = fold (Sorts.remove_sort o #2) witnessed extra
    2.46            |> Sorts.minimal_sorts (Sign.classes_of thy);
    2.47 -        val shyps' = Sorts.union present extra'
    2.48 -          |> Sorts.remove_sort [];
    2.49 +        val shyps' = fold (Sorts.insert_sort o #2) present extra';
    2.50        in
    2.51          Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
    2.52            shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
    2.53        end;
    2.54  
    2.55  (*dangling sort constraints of a thm*)
    2.56 -fun extra_shyps (th as Thm (_, {shyps, ...})) = Sorts.subtract (present_sorts th) shyps;
    2.57 +fun extra_shyps (th as Thm (_, {shyps, ...})) =
    2.58 +  Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
    2.59  
    2.60  
    2.61