turned distinct and sorted into inductive predicates: yields nice induction principles for free
authorhaftmann
Mon Oct 04 14:46:48 2010 +0200 (2010-10-04)
changeset 399168c83139a1433
parent 39915 ecf97cf3d248
child 39917 b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free
NEWS
src/HOL/Library/Permutation.thy
     1.1 --- a/NEWS	Mon Oct 04 12:22:58 2010 +0200
     1.2 +++ b/NEWS	Mon Oct 04 14:46:48 2010 +0200
     1.3 @@ -74,6 +74,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Predicates `distinct` and `sorted` now defined inductively, with nice
     1.8 +induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps
     1.9 +now named distinct_simps and sorted_simps.
    1.10 +
    1.11  * Constant `contents` renamed to `the_elem`, to free the generic name
    1.12  contents for other uses.  INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/HOL/Library/Permutation.thy	Mon Oct 04 12:22:58 2010 +0200
     2.2 +++ b/src/HOL/Library/Permutation.thy	Mon Oct 04 14:46:48 2010 +0200
     2.3 @@ -168,7 +168,7 @@
     2.4      apply simp
     2.5      apply (subgoal_tac "a#list <~~> a#ysa@zs")
     2.6       apply (metis Cons_eq_appendI perm_append_Cons trans)
     2.7 -    apply (metis Cons Cons_eq_appendI distinct.simps(2)
     2.8 +    apply (metis Cons Cons_eq_appendI distinct_simps(2)
     2.9        distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
    2.10     apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
    2.11      apply (fastsimp simp add: insert_ident)