summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Wed, 21 May 2008 14:04:41 +0200 | |

changeset 26964 | df1f238a05f7 |

parent 26963 | 290d23780204 |

child 26965 | 003b5781b845 |

Added entry explaining incompatibilities introduced by replacing sets by predicates.

--- a/NEWS Mon May 19 23:50:06 2008 +0200 +++ b/NEWS Wed May 21 14:04:41 2008 +0200 @@ -132,6 +132,72 @@ *** HOL *** +* Turned the type of sets "'a set" into an abbreviation for "'a => bool" + + INCOMPATIBILITIES: + + - Definitions of overloaded constants on sets have to be + replaced by definitions on => and bool. + + - Some definitions of overloaded operators on sets can now be proved + using the definitions of the operators on => and bool. + Therefore, the following theorems have been renamed: + + subset_def -> subset_eq + psubset_def -> psubset_eq + set_diff_def -> set_diff_eq + Compl_def -> Compl_eq + Sup_set_def -> Sup_set_eq + Inf_set_def -> Inf_set_eq + sup_set_def -> sup_set_eq + inf_set_def -> inf_set_eq + + - Due to the incompleteness of the HO unification algorithm, some + rules such as subst may require manual instantiation, if some of + the unknowns in the rule is a set. + + - Higher order unification and forward proofs: + The proof pattern + + have "P (S::'a set)" <...> + then have "EX S. P S" .. + + no longer works (due to the incompleteness of the HO unification algorithm) + and must be replaced by the pattern + + have "EX S. P S" + proof + show "P S" <...> + qed + + - Calculational reasoning with subst (or similar rules): + The proof pattern + + have "P (S::'a set)" <...> + also have "S = T" <...> + finally have "P T" . + + no longer works (for similar reasons as the previous example) and must be + replaced by something like + + have "P (S::'a set)" <...> + moreover have "S = T" <...> + ultimately have "P T" by simp + + - Tactics or packages written in ML code: + Code performing pattern matching on types via + + Type ("set", [T]) => ... + + must be rewritten. Moreover, functions like strip_type or binder_types no + longer return the right value when applied to a type of the form + + T1 => ... => Tn => U => bool + + rather than + + T1 => ... => Tn => U set + * Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations to "Wellfounded.thy".